Added IfThenElse and changed StepUntil to include typechecking

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

@@ -13,50 +13,43 @@ import info.kwarc.mmt.api.utils.URI
 import scala.collection.mutable
 
 // TODO: ADJUST ALL PATHS
-object IfThenElse {
+object IfThenElseX {
   val ns: DPath = DPath(URI.http colon "mathhub.info") / "FrameIT" / "frameworld"
-  val path: GlobalName = ns ? "StepUntilRaw" ? "stepUntil"
+  val path: GlobalName = ns ? "IfThenElseX" ? "ifthenelsex"
   val rawhead: OMID = OMS(path)
 
-  def apply(tp: Term, iv: Term, f: Term, tC: Term): Term =
-    ApplySpine(this.rawhead, tp, iv, f, tC)
+  def apply(tp: Term, cond: Term, tt: Term, ft: Term): Term =
+    ApplySpine(this.rawhead, tp, cond, tt, ft)
   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 ApplySpine(this.rawhead, List(tp, cond, tt, ft)) => Some((tp, cond, tt, ft))
     case _ => None
   }
 }
 
-object IfThenElseRule extends ParametricRule {
+object IfThenElseRuleX extends ParametricRule {
   override def apply(controller: Controller, home: Term, args: List[Term]): Rule = args match {
-    case List(truetm) =>
-      RuleSet(IfThenElseComp(truetm))
+    case List(truetm, falsetm) =>
+      RuleSet(IfThenElseCompX(truetm, falsetm))
     case _ =>
       ???
   }
 
-  case class IfThenElseComp(truetm: Term) extends ComputationRule(StepUntil.path) {
+  case class IfThenElseCompX(truetm: Term, falsetm: Term) extends ComputationRule(IfThenElseX.path) {
     override def applicable(t: Term): Boolean = t match {
-      case IfThenElse(_, _, _, _) => true
+      case IfThenElseX(_, _, _, _) => 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))
-          }
+      case IfThenElseX(_, cond, tt, ft) =>
+        check.tryToCheckWithoutDelay(Equality(stack, check.simplify(cond), truetm, None)) match {
+          case Some(true) => Simplify(tt)
+          case Some(false) | None =>
+            check.tryToCheckWithoutDelay(Equality(stack, check.simplify(cond), falsetm, None)) match {
+              case Some(true) => Simplify(ft)
+              case Some(false) | None => Simplifiability.NoRecurse
+            }
         }
-        // todo: try to log something via stack, history, check, or this
-        Simplify(Ls(values.toSeq : _*))
       case _ => Simplifiability.NoRecurse
     }
   }

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

@@ -6,7 +6,7 @@ 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, Arrow, OfType, Pi}
+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
 
@@ -14,12 +14,12 @@ import scala.collection.mutable
 
 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(tp: Term, iv: Term, f: Term, tC: Term): Term =
-    OMA(this.term, List(tp, iv, f, tC))
+  val path: GlobalName = ns ? "StepUntil" ? "stepUntil"
+  val rawhead: OMID = OMS(path)
+  def apply(tp1: Term, iv: Term, f: Term, tC: Term): Term =
+    ApplySpine(this.rawhead, tp1, 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 ApplySpine(this.rawhead, List(tp1, iv, f, tC)) => Some((tp1, iv, f, tC))
     case _ => None
   }
 }
@@ -30,12 +30,16 @@ object StepUntilRule extends ParametricRule {
 
   override def apply(controller: Controller, home: Term, args: List[Term]): Rule = args match {
     case List(truetm) =>
-      RuleSet(StepUntilComp(truetm), StepUntilInfTypingRule(truetm))
+      RuleSet(StepUntilComp(truetm))
     case _ =>
       ???
   }
 
   case class StepUntilComp(truetm: Term) extends ComputationRule(StepUntil.path) {
+    override def applicable(t: Term): Boolean = t match {
+      case StepUntil(_, _, _, _) => true
+      case _ => false
+    }
     override def apply(check: CheckingCallback)(tm: Term, covered: Boolean)(implicit stack: Stack, history: History): Simplifiability = tm match {
       case StepUntil(_, iv, f, tC) =>
         val values = mutable.ListBuffer[Term]()
@@ -56,53 +60,4 @@ object StepUntilRule extends ParametricRule {
       case _ => Simplifiability.NoRecurse
     }
   }
-
-  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(tp, iv, _, _)  =>
-          solver.inferType(iv) match {
-            case Some(tpA) =>
-              (Some(Listtype(tpA)),Some(true))
-            case _ =>
-              (None, None)
-          }
-        case _ =>
-          (None, None)
-      }
-      /**val (p, tpA) = (tm, tp) match {
-        case (StepUntil(iv, f, tC), Some(Listtype(tp1))) =>
-          solver.check(Typing(stack, iv, tp1, None))
-          solver.inferType(f).map(solver.safeSimplifyUntil(_)(Arrow.unapply)._1) match {
-            case Some(Pi(x,tpA1,tpB1)) if !tpB1.freeVars.contains(x) =>
-              if (!covered) {
-                solver.check(Subtyping(stack, iv, tpA1))
-                solver.check(Typing(stack, iv, tpB1))
-              }
-              (tC, tp1)
-            case _ =>
-              return (None,None)
-          }
-        case (StepUntil(iv, f, tC), _) =>
-          solver.inferType(f).map(solver.safeSimplifyUntil(_)(Arrow.unapply)._1) match {
-            case Some(Pi(x,tpA1,tpB1)) if !tpB1.freeVars.contains(x) =>
-              solver.check(Subtyping(stack, iv, tpA1))
-              solver.check(Typing(stack, iv, tpB1))
-              (tC, iv)
-            case _ =>
-              return (None,None)
-          }
-        case _ =>
-          return (None, None)
-      }
-      if (!covered) {
-        val proptp = solver.inferType(truetm) match {
-          case Some(t) => t
-          case _ => return (None, None)
-        }
-        val (name, _) = Context.pickFresh((stack ++ solver.constantContext ++ solver.outerContext).context, LocalName("ls"))
-        solver.check(Typing(stack++name%tpA,Apply(p,OMV(name)),proptp))
-      }
-      (Some(Listtype(tpA)),Some(true))*/
-  }
 }
\ No newline at end of file

source/IntegrationTests/DynamicsDebug.mmt

@@ -6,14 +6,13 @@ import frameworld http://mathhub.info/FrameIT/frameworld ❚
 fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚
 
 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 ❙
+    include ☞http://mathhub.info/FrameIT/frameworld?IfThenElseX ❙
+    c: ℝ ❘ = ifx (leq_real_lit 20.0 10.0) thenx 1.0 elsex 0.0 ❙
 ❚
 
-// theory StepUntilDebug =
+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) ❙
+    //my_list: List[ℝ] ❘ = (cons 0.0 (cons 2.0 nil)) map ([x: ℝ] plus_real_lit x 1.0) ❙
+    my_list: List[ℝ] ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
+    //my_list: ℝ ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
 ❚

source/Scrolls/BouncingScroll.mmt

@@ -8,7 +8,7 @@ fixmeta ?FrameworldMeta ❚
 theory BouncingScroll =
     meta ?MetaAnnotations?problemTheory ?BouncingScroll/Problem ❙
     meta ?MetaAnnotations?solutionTheory ?BouncingScroll/Solution ❙
-    include ?StepUntilWrap ❙
+    include ?StepUntil ❙
     theory funcs =
         //get_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
             [z,zv,g] times_real_lit (minus_real_lit (plus_real_lit zv (sqrt (plus_real_lit (times_real_lit zv zv) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) z)))))) (inv_real_lit g) ❙
@@ -72,7 +72,7 @@ theory BouncingScroll =
             [x] plus_real_lit x 1.0 ❙
         test_bool : ℝ ⟶ bool ❘ =
             [x] leq_real_lit 10.0 x ❙
-        out_list: List[ℝ] ❘ = stepUntil 0.0 test_func test_bool ❙
+        out_list: List[ℝ] ❘ = stepUntil ℝ 0.0 test_func test_bool ❙
         meta ?MetaAnnotations?label "BouncingScroll" ❙
         meta ?MetaAnnotations?description s"Bouncing " ❙
     ❚

source/dynamics.mmt

@@ -3,13 +3,15 @@ namespace http://mathhub.info/FrameIT/frameworld ❚
 import base http://mathhub.info/MitM/Foundation ❚
 import arith http://mathhub.info/MitM/core/arithmetics ❚
 import rules scala://rules.frameit.mmt.kwarc.info ❚
-
-theory StepUntilRaw =
+fixmeta ?FrameworldMeta ❚
+theory StepUntil =
     // {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❙
-    stepUntil # stepUntil 1 2 3 ❙
-❚
-
-theory StepUntil : ?FrameworldMeta =
-    include ?StepUntilRaw ❙
+    stepUntil : {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❘ # stepUntil 1 2 3 4 ❙
+    //stepUntil : {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ X ❘ # stepUntil 1 2 3 4 ❙
     rule rules?StepUntilRule (true) ❙
 ❚
+theory IfThenElseX =
+    // {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❙
+    ifthenelsex : {X: type} bool ⟶ X ⟶ X ⟶ X ❘ # ifx 2 thenx 3 elsex 4 ❙
+    rule rules?IfThenElseRuleX (true) (false) ❙
+❚