From cb6d71ba8e870ff89d0e1effe1f146458b4c4b0f Mon Sep 17 00:00:00 2001
From: Lucas <lucas.heublein@t-online.de>
Date: Tue, 12 Sep 2023 19:36:19 +0200
Subject: [PATCH] Changed W3DBouncingScroll output to also include hit
 intervals

---
 connect_to_mmt_W3Bounce.py           |  4 +++-
 source/Scrolls/W3DBouncingScroll.mmt | 25 ++++++++++++++-----------
 2 files changed, 17 insertions(+), 12 deletions(-)

diff --git a/connect_to_mmt_W3Bounce.py b/connect_to_mmt_W3Bounce.py
index c4d99d1..981b66d 100644
--- a/connect_to_mmt_W3Bounce.py
+++ b/connect_to_mmt_W3Bounce.py
@@ -208,9 +208,11 @@ for rf in rel_fact:
     rfa = rf["arguments"]
     cvals = []
     for ri2, rrf in enumerate(rfa):
-        if ri2 == len(rfa) - 1:
+        if ri2 == len(rfa) - 2:
             cvals.extend([x["float"] for x in rrf["arguments"][0]["arguments"]])
             cvals.append(rrf["arguments"][1]["float"])
+        elif ri2 == len(rfa) - 1:
+            cvals.append(rrf["float"])
         else:
             cvals.extend([x["float"] for x in rrf["arguments"]])
     values.append(cvals)
diff --git a/source/Scrolls/W3DBouncingScroll.mmt b/source/Scrolls/W3DBouncingScroll.mmt
index efcc271..f80d4ee 100644
--- a/source/Scrolls/W3DBouncingScroll.mmt
+++ b/source/Scrolls/W3DBouncingScroll.mmt
@@ -50,10 +50,10 @@ theory W3DBouncingScroll =
                                                   elsex false) (get_pt (πl rw) rp rv rg) ❙
         fold_func : (ℝ × wall) ⟶ (point × ℝ) ⟶ (point × ℝ) ❘ = 
             [cur][acc] (point × ℝ) ifx (leq_real_lit (πl cur) (πr acc)) thenx (⟨(πr cur).norm_vec, (πl cur)⟩) elsex acc ❙
-        calc_new_vals : (point × point × (point × ℝ)) ⟶ (point × ℝ) ⟶ (point × point) ❘ =
-            [v, bv] ⟨get_pt (πr (πr (πr v))) (πl v) (πl (πr v)) (πl bv), ([d : point] vec_multI (πr bv) (point_subtractI d (vec_multI (times_real_lit 2.0 (scalar_productI d (πl (πr (πr v))))) (πl (πr (πr v)))))) (⟨plus_real_lit ((πl (πr v)) _x) (times_real_lit (πr (πr (πr v))) ((πl bv) _x)), plus_real_lit ((πl (πr v)) _y) (times_real_lit (πr (πr (πr v))) ((πl bv) _y)), plus_real_lit ((πl (πr v)) _z) (times_real_lit (πr (πr (πr v))) ((πl bv) _z))⟩)⟩ ❙
-        end_cond : (point × point × (point × ℝ)) ⟶ bool ❘ =
-            [vals] leq_real_lit (πr (πr (πr vals))) 0.1 ❙
+        calc_new_vals : (point × point × (point × ℝ) × ℝ) ⟶ (point × ℝ) ⟶ (point × point × ℝ) ❘ =
+            [v, bv] ⟨get_pt (πr (πl (πr (πr v)))) (πl v) (πl (πr v)) (πl bv), ([d : point] vec_multI (πr bv) (point_subtractI d (vec_multI (times_real_lit 2.0 (scalar_productI d (πl (πl (πr (πr v)))))) (πl (πl (πr (πr v))))))) (⟨plus_real_lit ((πl (πr v)) _x) (times_real_lit (πr (πl (πr (πr v)))) ((πl bv) _x)), plus_real_lit ((πl (πr v)) _y) (times_real_lit (πr (πl (πr (πr v)))) ((πl bv) _y)), plus_real_lit ((πl (πr v)) _z) (times_real_lit (πr (πl (πr (πr v)))) ((πl bv) _z))⟩), plus_real_lit (πr (πr (πr v))) (πr (πl (πr (πr v))))⟩ ❙
+        end_cond : (point × point × (point × ℝ) × ℝ) ⟶ bool ❘ =
+            [vals] leq_real_lit (πr (πl (πr (πr vals)))) 0.1 ❙
         map_reduce_hts : (ℝ × ℝ × wall) ⟶ (ℝ × wall) ❘ =
             [wsi] (ℝ × wall) ifx (leq_real_lit (πl wsi) 0.000001)
                              thenx ((ℝ × wall) ifx (leq_real_lit (πl (πr wsi)) 0.000001)
@@ -64,14 +64,16 @@ theory W3DBouncingScroll =
                                                elsex ((ℝ × wall) ifx (leq_real_lit (πl wsi) (πl (πr wsi)))
                                                                  thenx (⟨πl wsi, πr (πr wsi)⟩)
                                                                  elsex (⟨πl (πr wsi), πr (πr wsi)⟩))) ❙
-        get_next_vals : List[wall] ⟶ (point × ℝ) ⟶ ((point × point × (point × ℝ)) ⟶ (point × point × (point × ℝ))) ❘ =
-            [aw, abv] ([v : point × point × (point × ℝ)] ([x : point × point] ⟨πl x, πr x, ((((((get_abcs aw (πl x) (πr x) (πl abv)) map mget_hts) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) filter ([wsk : ℝ × wall] check_hit wsk (πl x) (πr x) (πl abv))) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func)⟩) (calc_new_vals v abv)) ❙
-        prep : List[wall] ⟶ point ⟶ point ⟶ point ⟶ (point × point × (point × ℝ)) ❘ =
-		    [awi, p, v, g]  ⟨p, v, ((((((get_abcs awi p v g) map mget_hts) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) filter ([wsk : ℝ × wall] check_hit wsk p v g)) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func)⟩ ❙
+        get_next_vals : List[wall] ⟶ (point × ℝ) ⟶ ((point × point × (point × ℝ) × ℝ) ⟶ (point × point × (point × ℝ) × ℝ)) ❘ =
+            [aw, abv] ([v : point × point × (point × ℝ) × ℝ] ([x : point × point × ℝ] ⟨πl x, πl (πr x), ((((((get_abcs aw (πl x) (πl (πr x)) (πl abv)) map mget_hts) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) filter ([wsk : ℝ × wall] check_hit wsk (πl x) (πl (πr x)) (πl abv))) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func), πr (πr x)⟩) (calc_new_vals v abv)) ❙
+        prep : List[wall] ⟶ point ⟶ point ⟶ point ⟶ (point × point × (point × ℝ) × ℝ) ❘ =
+		    [awi, p, v, g]  ⟨p, v, ((((((get_abcs awi p v g) map mget_hts) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) filter ([wsk : ℝ × wall] check_hit wsk p v g)) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func), 0.0⟩ ❙
         get_pos_fun: point ⟶ point ⟶ point ⟶ (ℝ ⟶ point) ❘ =
             [p, v, g] ([t] ⟨plus_real_lit (times_real_lit (times_real_lit 0.5 (g _x)) (times_real_lit t t)) (plus_real_lit (p _x) (times_real_lit (v _x) t)), plus_real_lit (times_real_lit (times_real_lit 0.5 (g _y)) (times_real_lit t t)) (plus_real_lit (p _y) (times_real_lit (v _y) t)), plus_real_lit (times_real_lit (times_real_lit 0.5 (g _z)) (times_real_lit t t)) (plus_real_lit (p _z) (times_real_lit (v _z) t))⟩) ❙
         red_ht : (point × point × (point × ℝ)) ⟶ ℝ ❘ =
             [cele] πr (πr (πr cele)) ❙
+        map_fun_list : (point × point × (point × ℝ) × ℝ) ⟶ point ⟶ ((ℝ × ℝ) × (ℝ ⟶ ℝ) × (ℝ ⟶ point)) ❘ =
+            [vals, g] ⟨⟨πr (πr (πr vals)), plus_real_lit (πr (πr (πr vals))) (πr (πl (πr (πr vals))))⟩, ([ts : ℝ] plus_real_lit ts (minus_real_lit (πr (πr (πr vals))))), get_pos_fun (πl vals) (πl (πr vals)) g⟩ ❙
     ❚
     // start position and velocity ❙
     theory Problem =
@@ -89,9 +91,10 @@ theory W3DBouncingScroll =
         include ?W3DBouncingScroll/Problem ❙
         //testw : List[point × point × point × point] ❘ = cons (⟨⟨0.0, 0.0, 0.0⟩, ⟨1.0, 0.0, 0.0⟩, ⟨2.0, 0.0, 0.0⟩, ⟨3.0, 0.0, 0.0⟩⟩) (cons (⟨⟨0.0, 1.0, 0.0⟩, ⟨1.0, 1.0, 0.0⟩, ⟨2.0, 1.0, 0.0⟩, ⟨3.0, 1.0, 0.0⟩⟩) nil) ❙
         //wallse : List[wall] ❘ = wallsr map ([cw] create_wall (πl cw) (πl (πr cw)) (πl (πr (πr cw))) (πr (πr (πr cw)))) ❙
-        full_list: List[point × point × (point × ℝ)] ❘ = stepUntil (point × point × (point × ℝ)) (prep (wallsr map ([cw] create_wall (πl cw) (πl (πr cw)) (πl (πr (πr cw))) (πr (πr (πr cw))))) position velocity g_base) (get_next_vals (wallsr map ([cw] create_wall (πl cw) (πl (πr cw)) (πl (πr (πr cw))) (πr (πr (πr cw))))) ⟨g_base, bounce⟩) end_cond ❙
-        ht_list: List[ℝ] ❘ = full_list map red_ht ❙
-		fun_list : List[ℝ ⟶ point] ❘ = full_list map ([vals] get_pos_fun (πl vals) (πl (πr vals)) g_base) ❙
+        full_list: List[point × point × (point × ℝ) × ℝ] ❘ = stepUntil (point × point × (point × ℝ) × ℝ) (prep (wallsr map ([cw] create_wall (πl cw) (πl (πr cw)) (πl (πr (πr cw))) (πr (πr (πr cw))))) position velocity g_base) (get_next_vals (wallsr map ([cw] create_wall (πl cw) (πl (πr cw)) (πl (πr (πr cw))) (πr (πr (πr cw))))) ⟨g_base, bounce⟩) end_cond ❙
+        fun_list : List[(ℝ × ℝ) × (ℝ ⟶ ℝ) × (ℝ ⟶ point)] ❘ = full_list map ([vals : point × point × (point × ℝ) × ℝ] map_fun_list vals g_base) ❙
+        //ht_list: List[ℝ] ❘ = full_list map red_ht ❙
+		//fun_list : List[ℝ ⟶ point] ❘ = full_list map ([vals] get_pos_fun (πl vals) (πl (πr vals)) g_base) ❙
         meta ?MetaAnnotations?label "W3DBouncingScroll" ❙
         meta ?MetaAnnotations?description s"Bouncing " ❙
     ❚
-- 
GitLab