DynamicsDebug.mmt

namespace http://mathhub.info/FrameIT/frameworld/integrationtests/dynamicsdebug ❚

rule scala://parser.api.mmt.kwarc.info?MMTURILexer ❚

import rules scala://datatypes.LFX.mmt.kwarc.info ❚
import frameworld http://mathhub.info/FrameIT/frameworld ❚
fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚

theory IfElseDebug =
    include ☞http://mathhub.info/FrameIT/frameworld?IfThenElseX ❙
    c: ℝ ❘ = ℝ ifx (leq_real_lit 20.0 30.0) thenx 1.0 elsex 0.0 ❙
❚

theory StepUntilDebug =
    include ☞http://mathhub.info/FrameIT/frameworld?StepUntil ❙
    //my_list: List[ℝ] ❘ = (cons 0.0 (cons 2.0 nil)) map ([x: ℝ] plus_real_lit x 1.0) ❙
    my_list: List[ℝ] ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
    //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) ❙
    my_list: List[ℝ] ❘ = stepUntilX ℝ List[ℝ] (ℝ × ℝ) (cons 1.0 nil) ⟨2.0, 1.0⟩ 0.0 ([x: List[ℝ], y: ℝ × ℝ, z: ℝ] times_real_lit (plus_real_lit (x fold 0.0 ([curr: ℝ][acc: ℝ] plus_real_lit curr acc)) z) (πl y)) ([x: ℝ] leq_real_lit 50.0 x) ❙
    //my_list: ℝ ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
❚

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 ❙
    include ☞http://mathhub.info/FrameIT/frameworld?IfThenElseX ❙
    rule rules?FilterRule (true) ❙
    calc_new_vals : (ℝ × ℝ) ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ)) ❘ =
		[bv, v] ⟨⟨plus_real_lit (πl (πl v)) (times_real_lit (πl (πl (πr v))) (πl (πr (πr v)))), plus_real_lit (plus_real_lit (πr (πl v)) (times_real_lit (πr (πl (πr v))) (πl (πr (πr v))))) (times_real_lit (times_real_lit 0.5 (πl bv)) (times_real_lit (πl (πr (πr v))) (πl (πr (πr v)))))⟩, ⟨ times_real_lit (πr bv) (plus_real_lit (πl (πl (πr v))) (times_real_lit (times_real_lit (times_real_lit 2.0 (πr (πr (πr v)))) (plus_real_lit (πr (πl (πr v))) (minus_real_lit (times_real_lit (πr (πr (πr v))) (πl (πl (πr v))))))) (inv_real_lit (plus_real_lit 1.0 (times_real_lit (πr (πr (πr v))) (πr (πr (πr v)))))))), times_real_lit (πr bv) (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (times_real_lit 2.0 (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (πr (πr (πr v))) (πl (πl (πr v))))))) (inv_real_lit (plus_real_lit 1.0 (times_real_lit (πr (πr (πr v))) (πr (πr (πr v)))))))))⟩⟩ ❙
    fold_func : (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ⟶ (ℝ × ℝ) ⟶ (ℝ × ℝ) ❘ =
        [cur][acc] (ℝ × ℝ) ifx (leq_real_lit (πl acc) (πr (πl (πl cur)))) thenx acc elsex ⟨πr (πl (πl cur)), πr cur⟩ ❙
    check_hit : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
        [p] leq_real_lit 0.000001 (πr (πl p)) ❙
    check_hit2 : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
        [p] leq_real_lit (πl (πr p)) (πl (πl p)) ❙
    check_hit3 : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
        [p] leq_real_lit (πl (πl p)) (πr (πr p)) ❙
    get_hit_time_pos : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = 
        [wi, x, y, xv, yv, g] times_real_lit (inv_real_lit g) (plus_real_lit (plus_real_lit (times_real_lit (πl (πl wi)) xv) (minus_real_lit yv)) (sqrt ( plus_real_lit (times_real_lit (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv))) (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv)))) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) (plus_real_lit (plus_real_lit y (minus_real_lit (times_real_lit (πl (πl wi)) x))) (minus_real_lit (πr (πl wi))))))))) ❙
    get_hit_time_neg : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = 
        [wi, x, y, xv, yv, g] times_real_lit (inv_real_lit g) (plus_real_lit (plus_real_lit (times_real_lit (πl (πl wi)) xv) (minus_real_lit yv)) (minus_real_lit (sqrt ( plus_real_lit (times_real_lit (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv))) (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv)))) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) (plus_real_lit (plus_real_lit y (minus_real_lit (times_real_lit (πl (πl wi)) x))) (minus_real_lit (πr (πl wi)))))))))) ❙
    get_x_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = [x, xv, ht] plus_real_lit x (times_real_lit xv ht) ❙

    combine_ht_info_pos : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ❘ = 
        [wi, x, y, xv, yv, g] ⟨⟨⟨get_x_ht x xv (get_hit_time_pos wi x y xv yv g), get_hit_time_pos wi x y xv yv g⟩, ⟨(πl (πr wi)), (πr (πr wi))⟩⟩, (πl (πl wi))⟩ ❙
    combine_ht_info_neg : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ❘ = 
        [wi, x, y, xv, yv, g] ⟨⟨⟨get_x_ht x xv (get_hit_time_neg wi x y xv yv g), get_hit_time_neg wi x y xv yv g⟩, ⟨(πl (πr wi)), (πr (πr wi))⟩⟩, (πl (πl wi))⟩ ❙

    get_m : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ❘ = [w] times_real_lit (plus_real_lit (πr (πr w)) (minus_real_lit (πr (πl w)))) (inv_real_lit (plus_real_lit (πl (πr w)) (minus_real_lit (πl (πl w))))) ❙
    get_c : (ℝ × ℝ) ⟶ ℝ ⟶ ℝ ❘ = [w][m] plus_real_lit (πr w) (minus_real_lit (times_real_lit (πl w) m)) ❙
    get_mc : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ)) ❘ = [w] ⟨⟨get_m w, get_c (πl w) (get_m w)⟩, ⟨πl (πl w), πl (πr w)⟩⟩ ❙

    reduce_list_ht_pos : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ =
        [wsi, x, y, xv, yv, g] (((wsi map ([wi] combine_ht_info_pos wi x y xv yv g)) filter ([wib] check_hit (πl wib))) filter ([wib] check_hit2 (πl wib))) filter ([wib] check_hit3 (πl wib)) ❙
    reduce_list_ht_neg : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ =
        [wsi, x, y, xv, yv, g] (((wsi map ([wi] combine_ht_info_neg wi x y xv yv g)) filter ([wib] check_hit (πl wib))) filter ([wib] check_hit2 (πl wib))) filter ([wib] check_hit3 (πl wib)) ❙
    prep : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ =
		[wsi, x, y, xv, yv, g]  ⟨⟨x, y⟩, ⟨xv, yv⟩, (reduce_list_ht_pos wsi x y xv yv g) fold ((reduce_list_ht_neg wsi x y xv yv g) fold ⟨99999.9, -1.0⟩ fold_func) fold_func ⟩ ❙
    get_next_vals : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ (ℝ × ℝ) ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ = 
		[wsi, bv, v] ([x : ((ℝ × ℝ) × (ℝ × ℝ))] ⟨⟨πl (πl x), πr (πl x)⟩, ⟨πl (πr x), πr (πr x)⟩, (reduce_list_ht_pos wsi (πl (πl x)) (πr (πl x)) (πl (πr x)) (πr (πr x)) (πl bv)) fold ((reduce_list_ht_neg wsi (πl (πl x)) (πr (πl x)) (πl (πr x)) (πr (πr x)) (πl bv)) fold ⟨99999.9, -1.0⟩ fold_func) fold_func ⟩) (calc_new_vals bv v) ❙
    end_cond : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
        [vals] leq_real_lit (πl (πr (πr vals))) 0.1 ❙
    red_ht : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ❘ =
        [cele] πl (πr (πr cele)) ❙
    get_pos_fun: ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (ℝ ⟶ (ℝ × ℝ)) ❘ =
        [x,y,xv,yv,g] ([t] ⟨plus_real_lit x (times_real_lit xv t), plus_real_lit (times_real_lit (times_real_lit 0.5 g) (times_real_lit t t)) (plus_real_lit y (times_real_lit yv t))⟩ ) ❙
    my_list: List[(ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)] ❘ = stepUntilX ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) List[(ℝ × ℝ) × (ℝ × ℝ)] (ℝ × ℝ) ((cons ⟨⟨-10000.0, 0.0⟩, ⟨10000.0, 0.0⟩⟩ (cons ⟨⟨0.0, -1000.0⟩, ⟨0.1, 1000.0⟩⟩ (cons ⟨⟨50.0, -150.0⟩, ⟨50.1, 150.0⟩⟩ nil))) map get_mc) ⟨-200.0, 0.5⟩ (prep ((cons ⟨⟨-10000.0, 0.0⟩, ⟨10000.0, 0.0⟩⟩ (cons ⟨⟨0.0, -1000.0⟩, ⟨0.1, 1000.0⟩⟩ (cons ⟨⟨50.0, -150.0⟩, ⟨50.1, 150.0⟩⟩ nil))) map get_mc) 200.0 300.0 (-100.0) 100.0 (-200.0)) get_next_vals end_cond ❙
    //my_list: ℝ ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
    // full_list	
			: List[ ℝ×ℝ×(ℝ×ℝ)×(ℝ×ℝ)]
			= stepUntilX (ℝ×ℝ×(ℝ×ℝ)×(ℝ×ℝ)) List[ ℝ×ℝ×(ℝ×ℝ)] (ℝ×ℝ) cons ⟨⟨0.0,0.0⟩,⟨-10000.0,10000.0⟩⟩ nil  ⟨-200.0,0.5⟩ ⟨⟨200.0,300.0⟩,⟨-100.0,100.0⟩,⟨2.302775638,0.0⟩⟩ [wsi,bv,v]([xt:ℝ×ℝ×(ℝ×ℝ)]⟨⟨πl πl xt,πr πl xt⟩,⟨πl πr xt,πr πr xt⟩,(([wsit,x,y,xv,yv,g]wsit map [wi]([wi,x,y,xv,yv,g]⟨⟨⟨([x,xv,ht]x+(xv×ht)) x xv (([wi,x,y,xv,yv,g]g⁻¹×((πl πl wi)×xv)+-yv+-(sqrt (yv+-((πl πl wi)×xv)×yv+-((πl πl wi)×xv))+-(2.0×g×y+-((πl πl wi)×x)+-πr πl wi))) wi x y xv yv g),([wi,x,y,xv,yv,g]g⁻¹×((πl πl wi)×xv)+-yv+-(sqrt (yv+-((πl πl wi)×xv)×yv+-((πl πl wi)×xv))+-(2.0×g×y+-((πl πl wi)×x)+-πr πl wi))) wi x y xv yv g⟩,⟨πl πr wi,πr πr wi⟩⟩,πl πl wi⟩) wi x y xv yv g) wsi (πl πl xt) (πr πl xt) (πl πr xt) (πr πr xt) πl bv) fold ⟨99999.9,-1.0⟩ [cur][acc](ℝ×ℝ) ifx (leq_real_lit (πl acc) πr πl πl cur) thenx acc elsex ⟨πr πl πl cur,πr cur⟩⟩) (([bv,v]⟨⟨(πl πl v)+((πl πl πr v)×πl πr πr v),(πr πl v)+((πr πl πr v)×πl πr πr v)+(0.5×πl bv×((πl πr πr v)×πl πr πr v))⟩,⟨(πr bv)×(πl πl πr v)+(2.0×πr πr πr v×(πr πl πr v)+-((πr πr πr v)×πl πl πr v)×(1.0+((πr πr πr v)×πr πr πr v))⁻¹),(πr bv)×(πr πl πr v)+((πl bv)×πl πr πr v)+-(2.0×(πr πl πr v)+((πl bv)×πl πr πr v)+-((πr πr πr v)×πl πl πr v)×(1.0+((πr πr πr v)×πr πr πr v))⁻¹)⟩⟩) bv v) [vals]leq_real_lit (πl πr πr vals) 0.1 ❙

    //iterated_fun: List[ ℝ×ℝ×(ℝ×ℝ)] ⟶ (ℝ×ℝ) ⟶ (ℝ×ℝ×(ℝ×ℝ)×(ℝ×ℝ)) ⟶ (ℝ×ℝ×(ℝ×ℝ)) ⟶ (ℝ×ℝ×(ℝ×ℝ)×(ℝ×ℝ)) ❘
    = [wsi,bv,v,xt] ⟨⟨πl πl xt,πr πl xt⟩,⟨πl πr xt,πr πr xt⟩,(([wsit: List[(ℝ × ℝ) × (ℝ × ℝ)],x: ℝ,y: ℝ,xv: ℝ,yv: ℝ,g: ℝ]wsit map [wi: (ℝ × ℝ) × (ℝ × ℝ)]([wi: (ℝ × ℝ) × (ℝ × ℝ), x: ℝ,y: ℝ, xv: ℝ, yv: ℝ, g: ℝ]⟨⟨⟨([x: ℝ,xv: ℝ,ht: ℝ]x+(xv×ht)) x xv (([wi: (ℝ × ℝ) × (ℝ × ℝ), x: ℝ,y: ℝ, xv: ℝ, yv: ℝ, g: ℝ]g⁻¹×((πl πl wi)×xv)+-yv+-(sqrt (yv+-((πl πl wi)×xv)×yv+-((πl πl wi)×xv))+-(2.0×g×y+-((πl πl wi)×x)+-πr πl wi))) wi x y xv yv g),([wi: (ℝ × ℝ) × (ℝ × ℝ), x: ℝ,y: ℝ, xv: ℝ, yv: ℝ, g: ℝ]g⁻¹×((πl πl wi)×xv)+-yv+-(sqrt (yv+-((πl πl wi)×xv)×yv+-((πl πl wi)×xv))+-(2.0×g×y+-((πl πl wi)×x)+-πr πl wi))) wi x y xv yv g⟩,⟨πl πr wi,πr πr wi⟩⟩,πl πl wi⟩) wi x y xv yv g) wsi (πl πl xt) (πr πl xt) (πl πr xt) (πr πr xt) πl bv) fold ⟨99999.9,-1.0⟩ [cur: ((ℝ × ℝ) × (ℝ × ℝ)) × ℝ][acc: ℝ × ℝ](ℝ×ℝ) ifx (leq_real_lit (πl acc) πr πl πl cur) thenx acc elsex ⟨πr πl πl cur,πr cur⟩⟩ ❙ 
    
    
    // (([bv,v]⟨⟨(πl πl v)+((πl πl πr v)×πl πr πr v),(πr πl v)+((πr πl πr v)×πl πr πr v)+(0.5×πl bv×((πl πr πr v)×πl πr πr v))⟩,⟨(πr bv)×(πl πl πr v)+(2.0×πr πr πr v×(πr πl πr v)+-((πr πr πr v)×πl πl πr v)×(1.0+((πr πr πr v)×πr πr πr v))⁻¹),(πr bv)×(πr πl πr v)+((πl bv)×πl πr πr v)+-(2.0×(πr πl πr v)+((πl bv)×πl πr πr v)+-((πr πr πr v)×πl πl πr v)×(1.0+((πr πr πr v)×πr πr πr v))⁻¹)⟩⟩) bv v) ❙
❚