StepUntil + IfThenElse

scala/info/kwarc/mmt/frameit/rules/IfThenElse.scala

+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
+    }
+  }
+}
\ No newline at end of file

scala/info/kwarc/mmt/frameit/rules/StepUntil.scala

@@ -16,9 +16,10 @@ object StepUntil {
   val ns: DPath = DPath(URI.http colon "mathhub.info") / "FrameIT" / "frameworld"
   val path: GlobalName = ns ? "StepUntilRaw" ? "stepUntil"
   val term: OMID = OMS(path)
-  def apply(iv: Term, f: Term, tC: Term): Term = OMA(this.term, List(iv, f, tC))
-  def unapply(tm : Term) : Option[(Term,Term,Term)] = tm match {
-    case OMA(this.term, List(iv, f, tC)) => Some((iv, f, tC))
+  def apply(tp: Term, iv: Term, f: Term, tC: Term): Term =
+    OMA(this.term, List(tp, iv, f, tC))
+  def unapply(tm : Term) : Option[(Term, Term, Term, Term)] = tm match {
+    case OMA(this.term, List(tp, iv, f, tC)) => Some((tp, iv, f, tC))
     case _ => None
   }
 }
@@ -36,7 +37,7 @@ object StepUntilRule extends ParametricRule {
 
   case class StepUntilComp(truetm: Term) extends ComputationRule(StepUntil.path) {
     override def apply(check: CheckingCallback)(tm: Term, covered: Boolean)(implicit stack: Stack, history: History): Simplifiability = tm match {
-      case StepUntil(iv, f, tC) =>
+      case StepUntil(_, iv, f, tC) =>
         val values = mutable.ListBuffer[Term]()
         var iter = 0
         var cur = iv
@@ -59,7 +60,7 @@ object StepUntilRule extends ParametricRule {
   case class StepUntilInfTypingRule(truetm: Term) extends InferenceAndTypingRule(StepUntil.path, OfType.path) {
     override def apply(solver: Solver, tm: Term, tp: Option[Term], covered: Boolean)(implicit stack: Stack, history: History)
     : (Option[Term], Option[Boolean]) = tm match {
-        case StepUntil(iv, _, _)  =>
+        case StepUntil(tp, iv, _, _)  =>
           solver.inferType(iv) match {
             case Some(tpA) =>
               (Some(Listtype(tpA)),Some(true))

source/IntegrationTests/StepUntilDebug.mmt → source/IntegrationTests/DynamicsDebug.mmt

-namespace http://mathhub.info/FrameIT/frameworld/integrationtests/stepuntildebug ❚
+namespace http://mathhub.info/FrameIT/frameworld/integrationtests/dynamicsdebug ❚
 
 rule scala://parser.api.mmt.kwarc.info?MMTURILexer ❚
 
 import frameworld http://mathhub.info/FrameIT/frameworld ❚
 fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚
 
-theory StepUntilDebug =
+theory IfElseDebug =
+    if_then_elsex: {A: 𝒰 100} bool ⟶ A ⟶ A ⟶ A ❘ # ifx 2 thenx 3 elsex 4 ❙
+    simplify_ifelse1: {A: 𝒰 100, a: A, b: A} ⊦ (ifx true  thenx a elsex b) ≐ a ❘ role Simplify ❙
+    simplify_ifelse2: {A: 𝒰 100, a: A, b: A} ⊦ (ifx false thenx a elsex b) ≐ b ❘ role Simplify ❙
+
+    c = ifx true thenx 1.0 elsex 0.0 ❙
+❚
+
+// theory StepUntilDebug =
     include ☞http://mathhub.info/FrameIT/frameworld?StepUntil ❙
     my_list: List[ℝ] ❘ = stepUntil 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
 ❚