fix stepUntil

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
     }
   }

source/.idea/.gitignore

-# Default ignored files
-/shelf/
-/workspace.xml

source/.idea/codeStyles/Project.xml

-<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="&#10;" />
-    <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

source/.idea/codeStyles/codeStyleConfig.xml

-<component name="ProjectCodeStyleConfiguration">
-  <state>
-    <option name="PREFERRED_PROJECT_CODE_STYLE" value="Default" />
-  </state>
-</component>
\ No newline at end of file

source/.idea/misc.xml

-<?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

source/.idea/modules.xml

-<?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

source/.idea/vcs.xml

-<?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

source/IntegrationTests/StepUntilDebug.mmt

+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) ❙
+❚

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) ❙
+❚