diff --git a/scala/info/kwarc/mmt/frameit/rules/IfThenElse.scala b/scala/info/kwarc/mmt/frameit/rules/IfThenElse.scala
index 2cd9ae74a9331651c4c23e787425d0657bde216d..a0614b6ba9704dfbd30306d3e5b825cbb2c288da 100644
--- a/scala/info/kwarc/mmt/frameit/rules/IfThenElse.scala
+++ b/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
}
}
diff --git a/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala b/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
index f5d31d995a30752d78eaf8ea787752e85c1d2663..826333dcdd96b966ac91418f8f9242b439743357 100644
--- a/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
+++ b/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
diff --git a/source/IntegrationTests/DynamicsDebug.mmt b/source/IntegrationTests/DynamicsDebug.mmt
index 52b5a71073d6b93263b80c8f3ef1cc90063c5925..50266db211dd33cd84053a23a610732de1a31dcc 100644
--- a/source/IntegrationTests/DynamicsDebug.mmt
+++ b/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) â™
âš
diff --git a/source/Scrolls/BouncingScroll.mmt b/source/Scrolls/BouncingScroll.mmt
index 99075e63b5c336ec58f33f8122e112f104acd676..331f8a052ac5f65cf385a9723d02a33afc819ea2 100644
--- a/source/Scrolls/BouncingScroll.mmt
+++ b/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 " â™
âš
diff --git a/source/dynamics.mmt b/source/dynamics.mmt
index cf72a7e10fa2c6fdf115cb5a4e8e970295b5a34a..31bf8cf17311452c423bc5c057e3d80cfd9a492c 100644
--- a/source/dynamics.mmt
+++ b/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) â™
+âš