Change the Debug File

source/IntegrationTests/DynamicsDebug.mmt

@@ -18,6 +18,12 @@ theory StepUntilDebug =
     //my_list: ℝ ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
 ❚
 
+theory GetListAtIndDebug =
+    include ☞http://mathhub.info/FrameIT/frameworld?GetListAtInd ❙
+    //my_list: List[ℝ] ❘ = (cons 0.0 (cons 2.0 nil)) map ([x: ℝ] plus_real_lit x 1.0) ❙
+    my_ele: ℝ ❘ = ℝ getlistatind (cons 0.0 (cons 2.0 nil)) 1 ❙
+❚
+
 theory StepUntilXDebug =
     include ☞http://mathhub.info/FrameIT/frameworld?StepUntilX ❙
     //my_list: List[ℝ] ❘ = (cons 0.0 (cons 2.0 nil)) map ([x: ℝ] plus_real_lit x 1.0) ❙
@@ -25,19 +31,49 @@ theory StepUntilXDebug =
     //my_list: ℝ ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
 ❚
 
-theory W3Debug =
-    map_func : ℝ ⟶ (ℝ × ℝ) ❘ =
-        [ca] ⟨ca, ca⟩ ❙
-    add_map_func : ℝ ⟶ ℝ ❘ =
-        [wi] plus_real_lit 1.0 wi ❙
-    add_fold_func : (ℝ × ℝ) ⟶ (ℝ × ℝ) ⟶ (ℝ × ℝ) ❘ = 
-        [cur][acc] ⟨plus_real_lit (πl acc) (πl cur), plus_real_lit (πr acc) (πr cur)⟩ ❙
-    add_one : List[ℝ] ⟶ List[ℝ] ❘ =
-        [w] w map add_map_func ❙
-    duplicate : List[ℝ] ⟶ (ℝ × ℝ) ❘ =
-        [a] (a map map_func) fold ⟨1.0, 1.0⟩ add_fold_func ❙
-    test_fold4 : List[ℝ] ⟶ (ℝ × ℝ) ❘ =
-        [rl] duplicate (add_one rl) ❙
+theory Simpl1Debug =
+    rule rules?FilterRule (true) ❙
+    test_l : List[ℝ] ❘ = (cons (-1.0) (cons 2.0 nil)) ❙
+    test_fun : {X: type} (X ⟶ List[X]) ⟶ List[X] ❘ # testf 1 2 ❙
+    check : ℝ ⟶ bool ❘ =
+        [r] leq_real_lit 0.0 r ❙
+    add_list : List[ℝ] ⟶ ℝ ⟶ List[ℝ] ❘ =
+        [ls, a] (ls map ([lsi] plus_real_lit lsi a)) filter ([wib] check wib) ❙
+    add_list2 : List[ℝ] ⟶ ℝ ⟶ List[ℝ] ❘ =
+        [ls, a] ls map ([lsi] plus_real_lit lsi a) ❙
+    new_vals : List[ℝ] ⟶ (ℝ ⟶ List[ℝ]) ❘ =
+        [lsr] ([v] add_list lsr v) ❙
+    new_vals2 : List[ℝ] ⟶ (ℝ ⟶ List[ℝ]) ❘ =
+        [lsr] ([v] add_list2 lsr v) ❙
+    my_list: List[ℝ] ❘ = testf ℝ (new_vals test_l) ❙
+    my_list2: List[ℝ] ❘ = testf ℝ (new_vals2 test_l) ❙
+❚
+
+theory Simpl2Debug =
+    //include ☞http://mathhub.info/FrameIT/frameworld?StepUntil ❙
+    include ☞http://mathhub.info/FrameIT/frameworld?IfThenElseX ❙
+    rule rules?FilterRule (true) ❙
+    stepUntil : {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❘ # stepUntil 1 2 3 4 ❙
+    test_l : List[ℝ] ❘ = (cons 1.0 (cons 2.0 nil)) ❙
+    fold_max : ℝ ⟶ ℝ ⟶ ℝ ❘ =
+        [cur][acc] ℝ ifx (leq_real_lit cur acc) thenx acc elsex cur ❙
+    check : ℝ ⟶ bool ❘ =
+        [r] leq_real_lit 1.0 r ❙
+    
+    add_list : List[ℝ] ⟶ ℝ ⟶ List[ℝ] ❘ =
+        [ls, a] (ls map ([lsi] plus_real_lit lsi a)) filter ([wib] check wib) ❙
+    add_list2 : List[ℝ] ⟶ ℝ ⟶ List[ℝ] ❘ =
+        [ls, a] ls map ([lsi] plus_real_lit lsi a) ❙
+    
+    get_next_vals : List[ℝ] ⟶ (ℝ ⟶ ℝ) ❘ = 
+		[wsi] ([v : ℝ] (add_list wsi v) fold 0.0 fold_max) ❙
+    get_next_vals2 : List[ℝ] ⟶ (ℝ ⟶ ℝ) ❘ = 
+		[wsi] ([v : ℝ] (add_list2 wsi v) fold 0.0 fold_max) ❙
+    
+	end_cond : ℝ ⟶ bool ❘ =
+        [vals] leq_real_lit 50.0 vals ❙
+    my_list: List[ℝ] ❘ = stepUntil ℝ 1.0 (get_next_vals test_l) end_cond ❙
+    my_list2: List[ℝ] ❘ = stepUntil ℝ 1.0 (get_next_vals2 test_l) end_cond ❙
 ❚
 //theory StepUntilX2Debug =
     include ☞http://mathhub.info/FrameIT/frameworld?StepUntilX ❙