src/sim.bend

bend-lawful-stdlib@0.1.0.0 · 95 lines · 8 definitions

1import Base
2import bend-lawful-stdlib@0.1.0.0/src/class.bend as C
3
4# sim.bend: integer leapfrog steps that can be undone exactly.
5#
6#   import ./sim.bend as Sim
7#   Sim.run(~V2, ~V2.group(), ~force, n, s)
8#
9# A state is a position x and a velocity v in a type P whose + and - undo
10# each other (a C.Group: U32, or a record of U32s for 2D or 3D). step adds
11# the force F(x) to the velocity, then the new velocity to the position;
12# back undoes both. The laws hold for every state and every force ~F that
13# reads only the position. Wrapping integer + and - are exact inverses,
14# so no rounding is involved.
15#
16# A negative velocity is its two's complement: U32.sub(0, 3) moves 3 back.
17
18type State<-P: Data> is Data:
19  State{x: P, v: P}
20
21def step(~P: Data, ~g: C.Group<P>, ~F: P -> P, s: State<P>) -> State<P>:
22  match s:
23    case State{+x, v}:
24      +w = C.Group.add(P, g, v, F(x))
25      State{C.Group.add(P, g, x, w), w}
26
27def back(~P: Data, ~g: C.Group<P>, ~F: P -> P, s: State<P>) -> State<P>:
28  match s:
29    case State{x, +w}:
30      +x0 = C.Group.sub(P, g, x, w)
31      State{x0, C.Group.sub(P, g, w, F(x0))}
32
33# back undoes step
34law back_step:
35  for ~P: Data
36  for ~g: C.Group<P>
37  for ~F: P -> P
38  for s: State<P>
39  {s == back(~P, ~g, ~F, step(~P, ~g, ~F, s)) : State<P>}
40
41def back_step(P, g, F, s):
42  match s:
43    case State{+x, +v}:
44      +w = C.Group.add(P, g, v, F(x))
45      %C.Group.sub_add(P, g, x, w) : {State{x, v} == State{_, C.Group.sub(P, g, w, F(_))} : State<P>}
46      %C.Group.sub_add(P, g, v, F(x)) : {State{x, v} == State{x, _} : State<P>}
47      {==}
48
49def run(~P: Data, ~g: C.Group<P>, ~F: P -> P, n: Nat, s: State<P>) -> State<P>:
50  match n:
51    case 0n:
52      s
53    case 1n+k:
54      run(~P, ~g, ~F, k, step(~P, ~g, ~F, s))
55
56def rewind(~P: Data, ~g: C.Group<P>, ~F: P -> P, n: Nat, s: State<P>) -> State<P>:
57  match n:
58    case 0n:
59      s
60    case 1n+k:
61      rewind(~P, ~g, ~F, k, back(~P, ~g, ~F, s))
62
63# run's last step is its outermost one
64law run_step:
65  for ~P: Data
66  for ~g: C.Group<P>
67  for ~F: P -> P
68  for k: Nat
69  for s: State<P>
70  {step(~P, ~g, ~F, run(~P, ~g, ~F, k, s)) == run(~P, ~g, ~F, k, step(~P, ~g, ~F, s)) : State<P>}
71
72def run_step(P, g, F, k, s):
73  match k:
74    case 0n:
75      {==}
76    case 1n+j:
77      run_step(~P, ~g, ~F, j, step(~P, ~g, ~F, s))
78
79# rewinding n steps undoes running n steps
80law rewind_run:
81  for ~P: Data
82  for ~g: C.Group<P>
83  for ~F: P -> P
84  for +n: Nat
85  for +s: State<P>
86  {s == rewind(~P, ~g, ~F, n, run(~P, ~g, ~F, n, s)) : State<P>}
87
88def rewind_run(P, g, F, n, s):
89  match n:
90    case 0n:
91      {==}
92    case 1n+k:
93      %run_step(~P, ~g, ~F, k, s) : {s == rewind(~P, ~g, ~F, k, back(~P, ~g, ~F, _)) : State<P>}
94      %back_step(~P, ~g, ~F, run(~P, ~g, ~F, k, s)) : {s == rewind(~P, ~g, ~F, k, _) : State<P>}
95      rewind_run(~P, ~g, ~F, k, s)