package dotty.tools
package dotc
package core

import Types._, Contexts._, Symbols._
import Decorators._
import config.Config
import config.Printers._

/** Methods for adding constraints and solving them.
 *
 * Constraints are required to be in normalized form. This means
 * (1) if P <: Q in C then also Q >: P in C
 * (2) if P r Q in C and Q r R in C then also P r R in C, where r is <: or :>
 *
 * "P <: Q in C" means here: There is a constraint P <: H[Q],
 *     where H is the multi-hole context given by:
 *
 *      H = []
 *          H & T
 *          T & H
 *          H | H
 *
 *  (the idea is that a parameter Q in a H context is guaranteed to be a supertype of P).
 *
 * "P >: Q in C" means: There is a constraint P >: L[Q],
 *     where L is the multi-hole context given by:
 *
 *      L = []
 *          L | T
 *          T | L
 *          L & L
 */
trait ConstraintHandling {
  
  implicit val ctx: Context
  
  def isSubType(tp1: Type, tp2: Type): Boolean
  def deSkolemize(tp: Type, toSuper: Boolean): Type
  
  val state: TyperState
  import state.constraint

  /** If the constraint is frozen we cannot add new bounds to the constraint. */
  protected var frozenConstraint = false

  /** If the constraint is ignored, subtype checks only take into account
   *  declared bounds of PolyParams. Used when forming unions and intersectons
   *  of constraint bounds
   */
  private var ignoreConstraint = false

  private def ignoringConstraint[T](op: => T): T = {
    val savedIgnore = ignoreConstraint
    val savedFrozen = frozenConstraint
    ignoreConstraint = true
    frozenConstraint = true
    try op
    finally {
      ignoreConstraint = savedIgnore
      frozenConstraint = savedFrozen
    }
  }

  protected def isSubTypeWhenFrozen(tp1: Type, tp2: Type): Boolean = {
    val saved = frozenConstraint
    frozenConstraint = true
    try isSubType(tp1, tp2)
    finally frozenConstraint = saved
  }
  
  protected def constraintImpliesSub(param: PolyParam, tp: Type): Boolean = 
    isSubTypeWhenFrozen(bounds(param).hi, tp)

  protected def constraintImpliesSuper(param: PolyParam, tp: Type): Boolean = 
    isSubTypeWhenFrozen(tp, bounds(param).lo)

    /** The current bounds of type parameter `param` */
  final def bounds(param: PolyParam): TypeBounds = constraint at param match {
    case bounds: TypeBounds if !ignoreConstraint => bounds
    case _ => param.binder.paramBounds(param.paramNum)
  }

  /** Compare a solution of the constraint instead of the constrained parameters.
   *  The solution maps every parameter to its lower bound.
   */
  protected var solvedConstraint = false

  /** The parameters currently being constrained by addConstraint */
  private var pendingParams: Set[PolyParam] = Set()

  /** Make p2 = p1, transfer all bounds of p2 to p1 */
  private def unify(p1: PolyParam, p2: PolyParam): Boolean = {
    constr.println(s"unifying $p1 $p2")
    val constraint1 = constraint.unify(p1, p2)
    val bounds = constraint1.bounds(p1)
    isSubType(bounds.lo, bounds.hi) && { constraint = constraint1; true }
  }

  /** If current constraint set is not frozen, add the constraint
   *
   *      param >: bound   if fromBelow is true
   *      param <: bound   otherwise
   *
   *  to the bounds of `param`. If `bound` is itself a constrained parameter, also
   *  add the dual constraint to `bound`.
   *  @pre `param` is in the constraint's domain
   *  @return Whether the augmented constraint is still satisfiable.
   */
  def addConstraint(param: PolyParam, bound0: Type, fromBelow: Boolean): Boolean = {

    /** Add bidirectional constraint. If new constraint implies 'A <: B' we also
     *  make sure 'B >: A' gets added and vice versa. Furthermore, if the constraint
     *  implies 'A <: B <: A', A and B get unified.
     */
    def addc(param: PolyParam, bound: Type, fromBelow: Boolean): Boolean = {
      val pbounds0 = constraint.bounds(param)
      bound match {
        case bound: PolyParam if constraint contains bound =>
          val bbounds0 @ TypeBounds(lo, hi) = constraint.bounds(bound)
          if (lo eq hi)
            addc(param, lo, fromBelow)
          else if (param == bound)
            true
          else if (fromBelow && param.occursIn(lo, fromBelow = true))
            unify(param, bound)
          else if (!fromBelow && param.occursIn(hi, fromBelow = false))
            unify(bound, param)
          else {
            val pbounds = prepare(param, bound, fromBelow)
            val bbounds = prepare(bound, param, !fromBelow)
            pbounds.exists && bbounds.exists && {
              install(param, pbounds.bounds, pbounds0)
              install(bound, bbounds.bounds, bbounds0)
              true
            }
          }
        case bound: AndOrType if fromBelow != bound.isAnd =>
          addc(param, bound.tp1, fromBelow) &&
            addc(param, bound.tp2, fromBelow)
        case bound: WildcardType =>
          true
        case bound => // !!! remove to keep the originals
          val pbounds = prepare(param, bound, fromBelow)
          pbounds.exists && {
            install(param, pbounds.bounds, pbounds0)
            true
          }
      }
    }

    /** Install bounds for param */
    def install(param: PolyParam, newBounds: TypeBounds, oldBounds: TypeBounds): Unit = {
      val curBounds = constraint.bounds(param)
      try {
        constraint = constraint.updated(param, newBounds)
      } catch {
        case ex: AssertionError =>
          println(i"error while updating $param $newBounds\n$constraint")
          throw ex
      }
      if (curBounds ne oldBounds) {
        // In this case the bounds were updated previously by a recursive isSubType in
        // the satisfiability check of prepare. Reapply the previously added bounds, but
        // go through a full addConstraint in order to eliminate any cyclic dependencies
        // via unification.
        if (!ignoringConstraint(isSubType(curBounds.lo, newBounds.lo)))
          addConstraint(param, curBounds.lo, fromBelow)
        if (!ignoringConstraint(isSubType(newBounds.hi, curBounds.hi)))
          addConstraint(param, curBounds.hi, !fromBelow)
      }
    }

    /** Compute new bounds for `param` and check whether they are
     *  satisfiable. The check might in turn trigger other additions to the constraint.
     *  @return  The new bounds for `param` (which are not installed yet), or
     *           NoType, if the new constraint would not be satisfiable.
     */
    def prepare(param: PolyParam, bound: Type, fromBelow: Boolean): Type = {
      constr.println(s"prepare ${param.show} ${if (fromBelow) ">:>" else "<:<"} ${bound.show}")
      val oldBounds = constraint.bounds(param)
      val newBounds = ignoringConstraint {
        if (fromBelow) oldBounds.derivedTypeBounds(oldBounds.lo | bound, oldBounds.hi)
        else oldBounds.derivedTypeBounds(oldBounds.lo, oldBounds.hi & bound)
      }
      val ok =
        (param == bound) ||
          (oldBounds eq newBounds) ||
          {
            if (pendingParams contains param) {
              // Why the pendingParams test? It is possible that recursive subtype invocations
              // come back with another constraint for `param`. An example came up when compiling
              // ElimRepeated where we got the constraint
              //
              //      Coll <: IterableLike[Tree, Coll]
              //
              // and added
              //
              //      List[Tree] <: Coll
              //
              // The recursive bounds test is then
              //
              //      List[Tree] <: IterableLike[Tree, Coll]
              //
              // and because of the F-bounded polymorphism in the supertype of List,
              // i.e. List[T] <: IterableLike[T, List[T]], this leads again to
              //
              //      List[Tree] <: Coll
              //
              // If a parameter is already pending, we avoid revisiting it here.
              // Instead we combine the bounds computed here with the originally
              // computed bounds when installing the original type.
              constr.println(i"deferred bounds: $param $newBounds")
              true
            } else {
              pendingParams += param
              try isSubType(newBounds.lo, newBounds.hi)
              finally pendingParams -= param
            }
          }
      if (ok) newBounds else NoType
    }
    val bound = deSkolemize(bound0, toSuper = fromBelow).dealias.stripTypeVar
    def description = s"${param.show} ${if (fromBelow) ">:>" else "<:<"} ${bound.show} to ${constraint.show}"
    constr.println(s"adding $description")
    val res = addc(param, bound, fromBelow)
    constr.println(s"added $description")
    if (Config.checkConstraintsNonCyclicTrans) constraint.checkNonCyclicTrans()
    res
  }

  final def canConstrain(param: PolyParam): Boolean =
    !frozenConstraint && !solvedConstraint && (constraint contains param)

  /** Test whether the lower bounds of all parameters in this
   *  constraint are a solution to the constraint.
   */
  final def isSatisfiable: Boolean = {
    val saved = solvedConstraint
    solvedConstraint = true
    try
      constraint.forallParams { param =>
        val TypeBounds(lo, hi) = constraint.at(param)
        isSubType(lo, hi) || {
          ctx.log(i"sub fail $lo <:< $hi")
          ctx.log(i"approximated = ${approxParams(lo)} <:< ${approxParams(hi)}")
          false
        }
      }
    finally solvedConstraint = saved
  }

  /** Solve constraint set for given type parameter `param`.
   *  If `fromBelow` is true the parameter is approximated by its lower bound,
   *  otherwise it is approximated by its upper bound. However, any occurrences
   *  of the parameter in a refinement somewhere in the bound are removed.
   *  (Such occurrences can arise for F-bounded types).
   *  The constraint is left unchanged.
   *  @return the instantiating type
   *  @pre `param` is in the constraint's domain.
   */
  final def approximation(param: PolyParam, fromBelow: Boolean): Type = {
    val avoidParam = new TypeMap {
      override def stopAtStatic = true
      def apply(tp: Type) = mapOver {
        tp match {
          case tp: RefinedType if param occursIn tp.refinedInfo => tp.parent
          case _ => tp
        }
      }
    }
    val bounds = constraint.bounds(param)
    val bound = if (fromBelow) bounds.lo else bounds.hi
    val inst = avoidParam(bound)
    typr.println(s"approx ${param.show}, from below = $fromBelow, bound = ${bound.show}, inst = ${inst.show}")
    inst
  }

  /** Map that approximates each param in constraint by its lower bound.
   *  Currently only used for diagnostics.
   */
  final def approxParams = new TypeMap { // !!! Dotty problem: Turn this def into a val => -Ycheck:mix fails
    def apply(tp: Type): Type = tp.stripTypeVar match {
      case tp: PolyParam if constraint contains tp =>
        this(constraint.bounds(tp).lo)
      case tp =>
        mapOver(tp)
    }
  }
}