From 7f2fb20a394cc5d85fff10ed3eb7e11aac1f64df Mon Sep 17 00:00:00 2001
From: ComFreek <comfreek@outlook.com>
Date: Thu, 27 Jul 2023 16:53:38 +0200
Subject: [PATCH] fix stepUntil
---
scala/info/kwarc/mmt/frameit/rules/StepUntil.scala | 14 ++++++++------
source/.idea/.gitignore | 3 ---
source/.idea/codeStyles/Project.xml | 14 --------------
source/.idea/codeStyles/codeStyleConfig.xml | 5 -----
source/.idea/misc.xml | 6 ------
source/.idea/modules.xml | 8 --------
source/.idea/vcs.xml | 6 ------
source/IntegrationTests/StepUntilDebug.mmt | 11 +++++++++++
source/dynamics.mmt | 11 +++++++----
9 files changed, 26 insertions(+), 52 deletions(-)
delete mode 100644 source/.idea/.gitignore
delete mode 100644 source/.idea/codeStyles/Project.xml
delete mode 100644 source/.idea/codeStyles/codeStyleConfig.xml
delete mode 100644 source/.idea/misc.xml
delete mode 100644 source/.idea/modules.xml
delete mode 100644 source/.idea/vcs.xml
create mode 100644 source/IntegrationTests/StepUntilDebug.mmt
diff --git a/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala b/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
index 10f3d1b..f53dc66 100644
--- a/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
+++ b/scala/info/kwarc/mmt/frameit/rules/StepUntil.scala
@@ -10,9 +10,11 @@ import info.kwarc.mmt.lf.{Apply, Arrow, OfType, Pi}
import info.kwarc.mmt.LFX.datatypes.{Listtype, Ls}
import info.kwarc.mmt.api.utils.URI
+import scala.collection.mutable
+
object StepUntil {
val ns: DPath = DPath(URI.http colon "mathhub.info") / "FrameIT" / "frameworld"
- val path: GlobalName = ns ? "StepUntilWrap" ? "stepUntil"
+ 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 {
@@ -35,21 +37,21 @@ 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) =>
- var values = Seq[Term]()
+ val values = mutable.ListBuffer[Term]()
var iter = 0
var cur = iv
while (iter < DEBUG_MAX_ITER_COUNT) {
iter += 1
check.tryToCheckWithoutDelay(Equality(stack, Apply(tC, cur), truetm, None)) match {
case Some(true) =>
- return Simplify(Ls(values : _*))
+ return Simplify(Ls(values.toSeq : _*))
case Some(false) | None =>
- values = values :+ cur
- cur = Apply(f, cur)
+ values += cur
+ cur = check.simplify(Apply(f, cur))
}
}
// todo: try to log something via stack, history, check, or this
- Simplify(Ls(values : _*))
+ Simplify(Ls(values.toSeq : _*))
case _ => Simplifiability.NoRecurse
}
}
diff --git a/source/.idea/.gitignore b/source/.idea/.gitignore
deleted file mode 100644
index 26d3352..0000000
--- a/source/.idea/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-# Default ignored files
-/shelf/
-/workspace.xml
diff --git a/source/.idea/codeStyles/Project.xml b/source/.idea/codeStyles/Project.xml
deleted file mode 100644
index 508ba9c..0000000
--- a/source/.idea/codeStyles/Project.xml
+++ /dev/null
@@ -1,14 +0,0 @@
-<component name="ProjectCodeStyleConfiguration">
- <code_scheme name="Project" version="173">
- <option name="OTHER_INDENT_OPTIONS">
- <value>
- <option name="TAB_SIZE" value="2" />
- </value>
- </option>
- <option name="LINE_SEPARATOR" value=" " />
- <option name="FORMATTER_TAGS_ENABLED" value="true" />
- <ScalaCodeStyleSettings>
- <option name="MULTILINE_STRING_CLOSING_QUOTES_ON_NEW_LINE" value="true" />
- </ScalaCodeStyleSettings>
- </code_scheme>
-</component>
\ No newline at end of file
diff --git a/source/.idea/codeStyles/codeStyleConfig.xml b/source/.idea/codeStyles/codeStyleConfig.xml
deleted file mode 100644
index a55e7a1..0000000
--- a/source/.idea/codeStyles/codeStyleConfig.xml
+++ /dev/null
@@ -1,5 +0,0 @@
-<component name="ProjectCodeStyleConfiguration">
- <state>
- <option name="PREFERRED_PROJECT_CODE_STYLE" value="Default" />
- </state>
-</component>
\ No newline at end of file
diff --git a/source/.idea/misc.xml b/source/.idea/misc.xml
deleted file mode 100644
index 639900d..0000000
--- a/source/.idea/misc.xml
+++ /dev/null
@@ -1,6 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
- <component name="ProjectRootManager">
- <output url="file://$PROJECT_DIR$/out" />
- </component>
-</project>
\ No newline at end of file
diff --git a/source/.idea/modules.xml b/source/.idea/modules.xml
deleted file mode 100644
index 66f3350..0000000
--- a/source/.idea/modules.xml
+++ /dev/null
@@ -1,8 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
- <component name="ProjectModuleManager">
- <modules>
- <module fileurl="file://$PROJECT_DIR$/.idea/source.iml" filepath="$PROJECT_DIR$/.idea/source.iml" />
- </modules>
- </component>
-</project>
\ No newline at end of file
diff --git a/source/.idea/vcs.xml b/source/.idea/vcs.xml
deleted file mode 100644
index 6c0b863..0000000
--- a/source/.idea/vcs.xml
+++ /dev/null
@@ -1,6 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
- <component name="VcsDirectoryMappings">
- <mapping directory="$PROJECT_DIR$/.." vcs="Git" />
- </component>
-</project>
\ No newline at end of file
diff --git a/source/IntegrationTests/StepUntilDebug.mmt b/source/IntegrationTests/StepUntilDebug.mmt
new file mode 100644
index 0000000..7c8dec7
--- /dev/null
+++ b/source/IntegrationTests/StepUntilDebug.mmt
@@ -0,0 +1,11 @@
+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) â™
+âš
diff --git a/source/dynamics.mmt b/source/dynamics.mmt
index 6e77c20..cf72a7e 100644
--- a/source/dynamics.mmt
+++ b/source/dynamics.mmt
@@ -3,10 +3,13 @@ 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 âš
-fixmeta ?FrameworldMeta âš
-theory StepUntilWrap =
- stepUntil: ℠⟶ (℠⟶ â„) ⟶ (℠⟶ bool) ⟶ List[â„] ☠# stepUntil 1 2 3 â™
- rule rules?StepUntilRule (true) â™
+theory StepUntilRaw =
+ // {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] â™
+ stepUntil # stepUntil 1 2 3 â™
âš
+theory StepUntil : ?FrameworldMeta =
+ include ?StepUntilRaw â™
+ rule rules?StepUntilRule (true) â™
+âš
--
GitLab