diff --git a/connect_to_mmt_W3Bounce.py b/connect_to_mmt_W3Bounce.py index c4d99d1f1d51a3541cd715398f053dc13cb490c5..981b66d7dd22fa89c3263e2ab3c3517cfda9cce5 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 efcc271b8da7ead40f80c5d5f555f0b12ddffd5b..f80d4ee9798dd5100d5609c70e95d601e8bbc483 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 " â™ âš