From 544f0b9cd3a20bb61b307f655c2156033a7984ce Mon Sep 17 00:00:00 2001
From: ComFreek <comfreek@outlook.com>
Date: Thu, 27 Jul 2023 18:00:53 +0200
Subject: [PATCH] StepUntil + IfThenElse
---
.../kwarc/mmt/frameit/rules/IfThenElse.scala | 63 +++++++++++++++++++
.../kwarc/mmt/frameit/rules/StepUntil.scala | 11 ++--
source/IntegrationTests/DynamicsDebug.mmt | 19 ++++++
source/IntegrationTests/StepUntilDebug.mmt | 11 ----
4 files changed, 88 insertions(+), 16 deletions(-)
create mode 100644 scala/info/kwarc/mmt/frameit/rules/IfThenElse.scala
create mode 100644 source/IntegrationTests/DynamicsDebug.mmt
delete mode 100644 source/IntegrationTests/StepUntilDebug.mmt
diff --git a/scala/info/kwarc/mmt/frameit/rules/IfThenElse.scala b/scala/info/kwarc/mmt/frameit/rules/IfThenElse.scala
new file mode 100644
index 0000000..2cd9ae7
--- /dev/null
+++ b/scala/info/kwarc/mmt/frameit/rules/IfThenElse.scala
@@ -0,0 +1,63 @@
+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
diff --git a/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala b/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
index f53dc66..f5d31d9 100644
--- a/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
+++ b/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))
diff --git a/source/IntegrationTests/DynamicsDebug.mmt b/source/IntegrationTests/DynamicsDebug.mmt
new file mode 100644
index 0000000..52b5a71
--- /dev/null
+++ b/source/IntegrationTests/DynamicsDebug.mmt
@@ -0,0 +1,19 @@
+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 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) â™
+âš
diff --git a/source/IntegrationTests/StepUntilDebug.mmt b/source/IntegrationTests/StepUntilDebug.mmt
deleted file mode 100644
index 7c8dec7..0000000
--- a/source/IntegrationTests/StepUntilDebug.mmt
+++ /dev/null
@@ -1,11 +0,0 @@
-namespace http://mathhub.info/FrameIT/frameworld/integrationtests/stepuntildebug âš
-
-rule scala://parser.api.mmt.kwarc.info?MMTURILexer âš
-
-import frameworld http://mathhub.info/FrameIT/frameworld âš
-fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta âš
-
-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) â™
-âš
--
GitLab