package leon
package synthesis

class Task(synth: Synthesizer,
           val parent: Task,
           val problem: Problem,
           val rule: Rule) extends Ordered[Task] {

  def compare(that: Task) = {
    val cproblem = -(this.problem.complexity compare that.problem.complexity) // problem DESC

    if (cproblem == 0) {
      // On equal complexity, order tasks by rule priority
      this.rule.priority-that.rule.priority
    } else {
      cproblem
    }
  }

  def isBetterSolutionThan(sol: Solution, osol: Option[Solution]): Boolean = {
    osol match {
      case Some(s) => s.complexity > sol.complexity
      case None => true
    }
  }

  var solution: Option[Solution] = None
  var solver: Option[RuleApplication] = None

  var alternatives = Set[RuleApplication]()

  var minComplexity: AbsSolComplexity = new FixedSolComplexity(0)

  class TaskStep(val subProblems: List[Problem]) {
    var subSolutions = Map[Problem, Solution]()
    var subSolvers   = Map[Problem, Task]()
    var failures     = Set[Rule]()
  }

  class RuleApplication(
    val initProblems: List[Problem],
    val allNextSteps: List[List[Solution] => List[Problem]], 
    val onSuccess: List[Solution] => (Solution, Boolean)) {

    var allSteps    = List(new TaskStep(initProblems))
    var nextSteps   = allNextSteps
    def currentStep = allSteps.head

    def isSolvedFor(p: Problem) = allSteps.exists(_.subSolutions contains p) 

    def partlySolvedBy(t: Task, s: Solution) {
      if (currentStep.subProblems.contains(t.problem)) {
        if (isBetterSolutionThan(s, currentStep.subSolutions.get(t.problem))) {
          currentStep.subSolutions += t.problem -> s
          currentStep.subSolvers   += t.problem -> t

          if (currentStep.subSolutions.size == currentStep.subProblems.size) {
            val solutions = currentStep.subProblems map currentStep.subSolutions

            if (!nextSteps.isEmpty) {
              // Advance to the next step
              val newProblems = nextSteps.head.apply(solutions)
              nextSteps = nextSteps.tail

              synth.addProblems(Task.this, newProblems)

              allSteps = new TaskStep(newProblems) :: allSteps
            } else {
              onSuccess(solutions) match {
                case (s, true) =>
                  if (isBetterSolutionThan(s, solution)) {
                    solution = Some(s)
                    solver   = Some(this)

                    parent.partlySolvedBy(Task.this, s)
                  }
                case _ =>
                  // solution is there, but it is incomplete (precondition not strongest)
                  //parent.partlySolvedBy(this, Solution.choose(problem))
              }
            }
          }
        }
      }
    }

    val minComplexity: AbsSolComplexity = {
      val simplestSubSolutions = allNextSteps.foldLeft(initProblems.map(Solution.basic(_))){
        (sols, step) => step(sols).map(Solution.basic(_)) 
      }
      val simplestSolution = onSuccess(simplestSubSolutions)._1
      new FixedSolComplexity(parent.minComplexity.value + simplestSolution.complexity.value)
    }
  }

  // Is this subproblem already fixed?
  def isSolvedFor(problem: Problem): Boolean = parent.isSolvedFor(this.problem) || (alternatives.exists(_.isSolvedFor(problem)))

  def partlySolvedBy(t: Task, s: Solution) {
    alternatives.foreach(_.partlySolvedBy(t, s))
  }

  def run(): List[Problem] = {
    rule.applyOn(this) match {
      case RuleSuccess(solution) =>
        // Solved
        this.solution = Some(solution)
        parent.partlySolvedBy(this, solution)

        Nil

      case RuleAlternatives(steps) =>
        this.alternatives = steps.map( step => new RuleApplication(step.subProblems, step.interSteps, step.onSuccess) )

        this.alternatives.flatMap(_.initProblems).toList
      case RuleInapplicable =>
        Nil
    }
  }

  override def toString = "Applying "+rule+" on "+problem
}

class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, problem, null) {
  var solverTask: Option[Task] = None

  override def run() = {
    List(problem)
  }

  override def isSolvedFor(problem: Problem) = solverTask.isDefined

  override def partlySolvedBy(t: Task, s: Solution) {
    if (isBetterSolutionThan(s, solution)) {
      solution   = Some(s)
      solverTask = Some(t)
    }
  }
}