Added way to deal with acceleration vectors for bouncing

connect_to_mmt_W3Bounce.py

@@ -148,10 +148,10 @@ def create_point_fact(val, ref):
 			                     {"kind": "OMF", "float": val[1]},
 			                     {"kind": "OMF", "float": val[2]}]}}
 
-g = -200.0
+g = [0.0, 0.0, -200.0]
 pos_fact = create_point_fact([380.0, 0.0, 300.0], pos_ref)
 vel_fact = create_point_fact([-490.0, 100.0, 150.0], vel_ref)
-G_fact = create_point_fact([0.0, g, 0.0], G_ref)
+G_fact = create_point_fact(g, G_ref)
 B_fact = create_R_fact(0.8, B_ref)
 #wallsr_list = [[[-400.0, -400.0, 0.0], [400.0, -400.0, 0.0], [400.0, 400.0, 0.0], [-400.0, 400.0, 0.0]]]
 wallsr_list = [[[0.0, 0.0, 0.0], [400.0, 0.0, 0.0], [400.0, 0.0, 400.0], [0.0, 0.0, 400.0]],
@@ -224,9 +224,9 @@ import numpy as np
 
 def get_xyz_wrap(xs, ys, zs, xv, yv, zv):
     def get_xyz(ct):
-        rx = xs + ct * xv
-        ry = ys + ct * yv
-        rz = zs + ct * zv + 0.5 * g * ct**2
+        rx = xs + ct * xv + 0.5 * g[0] * ct**2
+        ry = ys + ct * yv + 0.5 * g[1] * ct**2
+        rz = zs + ct * zv + 0.5 * g[2] * ct**2
         return np.array([rx, ry, rz])
     return get_xyz
 

source/Scrolls/W3DBouncingScroll.mmt

@@ -21,11 +21,11 @@ theory W3DBouncingScroll =
                                        thenx true
                                        elsex false)
                          elsex false ❙
-        get_abcs : List[wall] ⟶ point ⟶ point ⟶ ℝ  ⟶ List[point × wall] ❘ =
-            [w, p, v, g] w map ([wi : wall] ⟨⟨(times_real_lit (wi.c) g),
-                                      (plus_real_lit (plus_real_lit (times_real_lit (wi.a) (v _x)) (times_real_lit (wi.b) (v _y))) (times_real_lit (wi.c) (v _z))),
-                                      (plus_real_lit (plus_real_lit (plus_real_lit (times_real_lit (wi.a) (p _x)) (times_real_lit (wi.b) (p _y))) (times_real_lit (wi.c) (p _z))) (minus_real_lit (wi.d)))⟩,
-                                    wi⟩) ❙
+        get_abcs : List[wall] ⟶ point ⟶ point ⟶ point  ⟶ List[point × wall] ❘ =
+            [w, p, v, g] w map ([wi : wall] ⟨⟨(plus_real_lit (times_real_lit (wi.a) (g _x)) (plus_real_lit (times_real_lit (wi.b) (g _y)) (times_real_lit (wi.c) (g _z)))),
+                                             (plus_real_lit (plus_real_lit (times_real_lit (wi.a) (v _x)) (times_real_lit (wi.b) (v _y))) (times_real_lit (wi.c) (v _z))),
+                                             (plus_real_lit (plus_real_lit (plus_real_lit (times_real_lit (wi.a) (p _x)) (times_real_lit (wi.b) (p _y))) (times_real_lit (wi.c) (p _z))) (minus_real_lit (wi.d)))⟩,
+                                            wi⟩) ❙
         mget_hts : (point × wall) ⟶ (ℝ × ℝ × wall) ❘ =
             [cabc] (ℝ × ℝ × wall) ifx (eq_zero ((πl cabc) _x))
                                   thenx ((ℝ × ℝ × wall) ifx (eq_zero ((πl cabc) _y))
@@ -36,11 +36,11 @@ theory W3DBouncingScroll =
                                                         thenx (⟨times_real_lit (plus_real_lit (minus_real_lit ((πl cabc) _y)) (sqrt (plus_real_lit (times_real_lit ((πl cabc) _y) ((πl cabc) _y)) (minus_real_lit (times_real_lit 2.0 (times_real_lit ((πl cabc) _x) ((πl cabc) _z))))))) (inv_real_lit ((πl cabc) _x)),
                                                                 times_real_lit (plus_real_lit (minus_real_lit ((πl cabc) _y)) (minus_real_lit (sqrt (plus_real_lit (times_real_lit ((πl cabc) _y) ((πl cabc) _y)) (minus_real_lit (times_real_lit 2.0 (times_real_lit ((πl cabc) _x) ((πl cabc) _z)))))))) (inv_real_lit ((πl cabc) _x)), (πr cabc)⟩)
                                                         elsex (⟨-1.0, -1.0, (πr cabc)⟩)) ❙
-	    get_pt : ℝ ⟶ point ⟶ point ⟶ ℝ  ⟶ point ❘ = 
-            [rht, rp, rv, rg] ⟨plus_real_lit (rp _x) (times_real_lit (rv _x) rht),
-                               plus_real_lit (rp _y) (times_real_lit (rv _y) rht),
-                               plus_real_lit (plus_real_lit (rp _z) (times_real_lit (rv _z) rht)) (times_real_lit (times_real_lit 0.5 rg) (times_real_lit rht rht))⟩ ❙
-        check_hit : (ℝ × wall) ⟶ point ⟶ point ⟶ ℝ  ⟶ bool ❘ = 
+	    get_pt : ℝ ⟶ point ⟶ point ⟶ point  ⟶ point ❘ = 
+            [rht, rp, rv, rg] ⟨plus_real_lit (plus_real_lit (rp _x) (times_real_lit (rv _x) rht)) (times_real_lit (times_real_lit 0.5 (rg _x)) (times_real_lit rht rht)),
+                               plus_real_lit (plus_real_lit (rp _y) (times_real_lit (rv _y) rht)) (times_real_lit (times_real_lit 0.5 (rg _y)) (times_real_lit rht rht)),
+                               plus_real_lit (plus_real_lit (rp _z) (times_real_lit (rv _z) rht)) (times_real_lit (times_real_lit 0.5 (rg _z)) (times_real_lit rht rht))⟩ ❙
+        check_hit : (ℝ × wall) ⟶ point ⟶ point ⟶ point  ⟶ bool ❘ = 
             [rw, rp, rv, rg] ([np : point] (bool) ifx (leq_real_lit (scalar_productI ((πr rw).point1) ((πr rw).u)) (scalar_productI np ((πr rw).u)))
                                                   thenx ((bool) ifx (leq_real_lit (scalar_productI np ((πr rw).u)) (scalar_productI ((πr rw).point2) ((πr rw).u)))
                                                                 thenx ((bool) ifx (leq_real_lit (scalar_productI ((πr rw).point1) (point_subtractI ((πr rw).point4) ((πr rw).point1))) (scalar_productI np (point_subtractI ((πr rw).point4) ((πr rw).point1))))
@@ -50,8 +50,8 @@ 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) ❘ =
-            [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)))))) (⟨(πl (πr v)) _x, (πl (πr v)) _y, plus_real_lit ((πl (πr v)) _z) (times_real_lit (πr (πr (πr v))) (πl bv))⟩)⟩ ❙
+        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 ❙
         map_reduce_hts : (ℝ × ℝ × wall) ⟶ (ℝ × wall) ❘ =
@@ -64,12 +64,12 @@ 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 × ℝ))) ❘ =
+        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 × ℝ)) ❘ =
+        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_pos_fun: point ⟶ point ⟶ ℝ ⟶ (ℝ ⟶ point) ❘ =
-            [p, v, g] ([t] ⟨plus_real_lit (p _x) (times_real_lit (v _x) t), plus_real_lit (p _y) (times_real_lit (v _y) t), plus_real_lit (times_real_lit (times_real_lit 0.5 g) (times_real_lit t t)) (plus_real_lit (p _z) (times_real_lit (v _z) t))⟩) ❙
+        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)) ❙
     ❚
@@ -89,9 +89,9 @@ 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 _y)) (get_next_vals (wallsr map ([cw] create_wall (πl cw) (πl (πr cw)) (πl (πr (πr cw))) (πr (πr (πr cw))))) ⟨(g_base _y), bounce⟩) end_cond ❙
+        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 _y)) ❙
+		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 " ❙
     ❚