package info.kwarc.mmt.frameit.rules

import info.kwarc.mmt.api.checking._
import info.kwarc.mmt.api.{DPath, GlobalName, LocalName, ParametricRule, Rule, RuleSet}
import info.kwarc.mmt.api.frontend.Controller
import info.kwarc.mmt.api.objects._
import Conversions._
import info.kwarc.mmt.api.uom.{Simplifiability, Simplify}
import info.kwarc.mmt.lf.{Apply, ApplySpine, Arrow, OfType, Pi}
import info.kwarc.mmt.LFX.datatypes.{Listtype, Ls}
import info.kwarc.mmt.api.utils.URI

import scala.collection.mutable

// TODO: ADJUST ALL PATHS
object IfThenElse {
  val ns: DPath = DPath(URI.http colon "mathhub.info") / "FrameIT" / "frameworld"
  val path: GlobalName = ns ? "StepUntilRaw" ? "stepUntil"
  val rawhead: OMID = OMS(path)

  def apply(tp: Term, iv: Term, f: Term, tC: Term): Term =
    ApplySpine(this.rawhead, tp, iv, f, tC)
  def unapply(tm : Term) : Option[(Term, Term, Term, Term)] = tm match {
    case ApplySpine(this.rawhead, List(tp, iv, f, tC)) => Some((tp, iv, f, tC))
    case _ => None
  }
}

object IfThenElseRule extends ParametricRule {
  override def apply(controller: Controller, home: Term, args: List[Term]): Rule = args match {
    case List(truetm) =>
      RuleSet(IfThenElseComp(truetm))
    case _ =>
      ???
  }

  case class IfThenElseComp(truetm: Term) extends ComputationRule(StepUntil.path) {
    override def applicable(t: Term): Boolean = t match {
      case IfThenElse(_, _, _, _) => true
      case _ => false
    }

    override def apply(check: CheckingCallback)(tm: Term, covered: Boolean)(implicit stack: Stack, history: History): Simplifiability = tm match {
      case IfThenElse(_, iv, f, tC) =>
        val values = mutable.ListBuffer[Term]()
        var iter = 0
        var cur = iv
        while (iter < 123) {
          iter += 1
          check.tryToCheckWithoutDelay(Equality(stack, Apply(tC, cur), truetm, None)) match {
            case Some(true) =>
              return Simplify(Ls(values.toSeq : _*))
            case Some(false) | None =>
              values += cur
              cur = check.simplify(Apply(f, cur))
          }
        }
        // todo: try to log something via stack, history, check, or this
        Simplify(Ls(values.toSeq : _*))
      case _ => Simplifiability.NoRecurse
    }
  }
}