Skip to content
Snippets Groups Projects
Commit 57234dea authored by Lucas-He's avatar Lucas-He
Browse files

Fixed a bug in the Hit calculation

parent d598dee9
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
source/Scrolls/T3DBouncingScroll.mmt
+ 22
− 8
View file @ 57234dea
......@@ -42,12 +42,26 @@ theory T3DBouncingScroll =
[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 0.0 (scalar_productI (vec_cross (point_subtractI ((πr rw).point3) ((πr rw).point2)) (point_subtractI np ((πr rw).point2))) (vec_cross (point_subtractI ((πr rw).point3) ((πr rw).point2)) (point_subtractI ((πr rw).point1) ((πr rw).point2)))))
thenx ((bool) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr rw).point3) ((πr rw).point1)) (point_subtractI np ((πr rw).point1))) (vec_cross (point_subtractI ((πr rw).point3) ((πr rw).point1)) (point_subtractI ((πr rw).point2) ((πr rw).point1)))))
thenx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr rw).point2) ((πr rw).point1)) (point_subtractI np ((πr rw).point1))) (vec_cross (point_subtractI ((πr rw).point2) ((πr rw).point1)) (point_subtractI ((πr rw).point3) ((πr rw).point1)))))
elsex false)
elsex false) (get_pt (πl rw) rp rv rg) ❙
check_hit1 : point ⟶ point ⟶ point ⟶ ((ℝ × ℝ × wall) ⟶ (ℝ × ℝ × wall)) ❘ =
[rp, rv, rg] ([rw: ℝ × ℝ × wall] ([np : point] (ℝ × ℝ × wall) ifx (leq_real_lit (πl rw) 0.000001)
thenx (⟨-1.0, πl (πr rw), πr (πr rw)⟩)
elsex ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point2)) (point_subtractI np ((πr (πr rw)).point2))) (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point2)) (point_subtractI ((πr (πr rw)).point1) ((πr (πr rw)).point2)))))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)) (point_subtractI np ((πr (πr rw)).point1))) (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)) (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)))))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)) (point_subtractI np ((πr (πr rw)).point1))) (vec_cross (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)) (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)))))
thenx (rw)
elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))
elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))
elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))) (get_pt (πl rw) rp rv rg)) ❙
check_hit2 : point ⟶ point ⟶ point ⟶ ((ℝ × ℝ × wall) ⟶ (ℝ × ℝ × wall)) ❘ =
[rp, rv, rg] ([rw: ℝ × ℝ × wall] ([np : point] (ℝ × ℝ × wall) ifx (leq_real_lit (πl (πr rw)) 0.000001)
thenx (⟨πl rw, -1.0, πr (πr rw)⟩)
elsex ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point2)) (point_subtractI np ((πr (πr rw)).point2))) (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point2)) (point_subtractI ((πr (πr rw)).point1) ((πr (πr rw)).point2)))))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)) (point_subtractI np ((πr (πr rw)).point1))) (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)) (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)))))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)) (point_subtractI np ((πr (πr rw)).point1))) (vec_cross (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)) (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)))))
thenx (rw)
elsex (⟨πl rw, -1.0, πr (πr rw)⟩))
elsex (⟨πl rw, -1.0, πr (πr rw)⟩))
elsex (⟨πl rw, -1.0, πr (πr rw)⟩))) (get_pt (πl (πr 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 × ℝ) ❘ =
......@@ -71,9 +85,9 @@ theory T3DBouncingScroll =
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, π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)) ❙
[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 (check_hit1 (πl x) (πl (πr x)) (πl abv))) map (check_hit2 (πl x) (πl (πr x)) (πl abv))) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) 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⟩ ❙
[awi, p, v, g] ⟨p, v, (((((((get_abcs awi p v g) map mget_hts) map (check_hit1 p v g)) map (check_hit2 p v g)) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) 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 × ℝ)) ⟶ ℝ ❘ =
......
source/Scrolls/W3DBouncingScroll.mmt
+ 26
− 10
View file @ 57234dea
......@@ -42,14 +42,30 @@ theory W3DBouncingScroll =
[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))))
thenx (leq_real_lit (scalar_productI np (point_subtractI ((πr rw).point4) ((πr rw).point1))) (scalar_productI ((πr rw).point4) (point_subtractI ((πr rw).point4) ((πr rw).point1))))
elsex false)
elsex false)
elsex false) (get_pt (πl rw) rp rv rg) ❙
check_hit1 : point ⟶ point ⟶ point ⟶ ((ℝ × ℝ × wall) ⟶ (ℝ × ℝ × wall)) ❘ =
[rp, rv, rg] ([rw: ℝ × ℝ × wall] ([np : point] (ℝ × ℝ × wall) ifx (leq_real_lit (πl rw) 0.000001)
thenx (⟨-1.0, πl (πr rw), πr (πr rw)⟩)
elsex ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI ((πr (πr rw)).point1) ((πr (πr rw)).u)) (scalar_productI np ((πr (πr rw)).u)))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI np ((πr (πr rw)).u)) (scalar_productI ((πr (πr rw)).point2) ((πr (πr rw)).u)))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI ((πr (πr rw)).point1) (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))) (scalar_productI np (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI np (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))) (scalar_productI ((πr (πr rw)).point4) (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))))
thenx (rw)
elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))
elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))
elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))
elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))) (get_pt (πl rw) rp rv rg)) ❙
check_hit2 : point ⟶ point ⟶ point ⟶ ((ℝ × ℝ × wall) ⟶ (ℝ × ℝ × wall)) ❘ =
[rp, rv, rg] ([rw: ℝ × ℝ × wall] ([np : point] (ℝ × ℝ × wall) ifx (leq_real_lit (πl (πr rw)) 0.000001)
thenx (⟨πl rw, -1.0, πr (πr rw)⟩)
elsex ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI ((πr (πr rw)).point1) ((πr (πr rw)).u)) (scalar_productI np ((πr (πr rw)).u)))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI np ((πr (πr rw)).u)) (scalar_productI ((πr (πr rw)).point2) ((πr (πr rw)).u)))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI ((πr (πr rw)).point1) (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))) (scalar_productI np (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI np (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))) (scalar_productI ((πr (πr rw)).point4) (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))))
thenx (rw)
elsex (⟨πl rw, -1.0, πr (πr rw)⟩))
elsex (⟨πl rw, -1.0, πr (πr rw)⟩))
elsex (⟨πl rw, -1.0, πr (πr rw)⟩))
elsex (⟨πl rw, -1.0, πr (πr rw)⟩))) (get_pt (πl (πr 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 × ℝ) ❘ =
......@@ -73,9 +89,9 @@ theory W3DBouncingScroll =
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, π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)) ❙
[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 (check_hit1 (πl x) (πl (πr x)) (πl abv))) map (check_hit2 (πl x) (πl (πr x)) (πl abv))) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) 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⟩ ❙
[awi, p, v, g] ⟨p, v, (((((((get_abcs awi p v g) map mget_hts) map (check_hit1 p v g)) map (check_hit2 p v g)) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) 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 × ℝ)) ⟶ ℝ ❘ =
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment