Skip to content
Snippets Groups Projects
IfThenElse.scala 2.21 KiB
Newer Older
  • Learn to ignore specific revisions
  • ComFreek's avatar
    ComFreek committed
    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
        }
      }
    }