src/storage/frame.bend
bendtorch-core@0.1.0.0 · 122 lines · 10 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore
4import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
5import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
6
7def write_read(-T: Data, +d: Nat, array: Array<T>, +path: Model.Path(d), value: T, valid: Model.Balanced(T, d, array)) ->
8 {Model.observe(T, d, ArrayCore.write_path(T, d, array, path, value), path) == Some{value} : Maybe<&2, T>}:
9 match d array:
10 case 0n ALeaf{old}:
11 {==}
12 case 0n ANode{xs, ys}:
13 match valid:
14 case 1n+p ALeaf{old}:
15 match valid:
16 case 1n++p ANode{xs, ys}:
17 Model.Step{bit, rest} = path
18 match bit:
19 case False{}:
20 (ex, ey) = valid
21 write_read(T, p, xs, rest, value, ex)
22 case True{}:
23 (ex, ey) = valid
24 write_read(T, p, ys, rest, value, ey)
25
26def update_frame(-T: Data, +d: Nat, array: Array<T>, +i: Model.Path(d), +j: Model.Path(d), +value: T, valid: Model.Balanced(T, d, array)) ->
27 {Model.observe(T, d, ArrayCore.write_path(T, d, array, i, value), j) == Model.select(T, Model.same(d, i, j), value, Model.observe(T, d, array, j)) : Maybe<&2, T>}:
28 match d array:
29 case 0n ALeaf{old}:
30 {==}
31 case 0n ANode{xs, ys}:
32 match valid:
33 case 1n+p ALeaf{old}:
34 match valid:
35 case 1n++p ANode{xs, ys}:
36 Model.Step{ib, ir} = i
37 match ib:
38 case False{}:
39 Model.Step{jb, jr} = j
40 match jb:
41 case False{}:
42 (ex, ey) = valid
43 update_frame(T, p, xs, ir, jr, value, ex)
44 case True{}:
45 {==}
46 case True{}:
47 Model.Step{jb, jr} = j
48 match jb:
49 case False{}:
50 {==}
51 case True{}:
52 (ex, ey) = valid
53 update_frame(T, p, ys, ir, jr, value, ey)
54
55def observed_correct(-T: Data, -d: Nat, -array: Array<T>, -path: Model.Path(d),
56 read: ArrayCore.Read<T, d, array, path>) ->
57 {ArrayCore.observation(T, d, array, path, read) == Model.observe(T, d, array, path) : Maybe<&2, T>}:
58 match read:
59 case ArrayCore.Read{retained, value, balanced, kept, observed}:
60 observed
61
62def retained_correct(-T: Data, -d: Nat, -array: Array<T>, -path: Model.Path(d),
63 read: ArrayCore.Read<T, d, array, path>) ->
64 {ArrayCore.retained(T, d, array, path, read) == array : Array<T>}:
65 match read:
66 case ArrayCore.Read{retained, value, balanced, kept, observed}:
67 kept
68
69def read_refines(-T: Data, +d: Nat, array: Array<T>, +path: Model.Path(d), valid: Model.Balanced(T, d, array)) ->
70 {ArrayCore.observation(T, d, array, path, ArrayCore.read_path(T, d, array, path, valid)) == Model.observe(T, d, array, path) : Maybe<&2, T>}:
71 observed_correct(T, d, array, path, ArrayCore.read_path(T, d, array, path, valid))
72
73def read_retains(-T: Data, +d: Nat, array: Array<T>, +path: Model.Path(d), valid: Model.Balanced(T, d, array)) ->
74 {ArrayCore.retained(T, d, array, path, ArrayCore.read_path(T, d, array, path, valid)) == array : Array<T>}:
75 retained_correct(T, d, array, path, ArrayCore.read_path(T, d, array, path, valid))
76
77def primitive_frame_cloned(-T: Data, +d: Nat, -original: Array<T>, +i: U32,
78 +other: Model.Path(d), +value: T, cloned: Clone.Cloned<T, d, original>) ->
79 {Model.observe(T, d, Array.set(T, original, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, original, other)) : Maybe<&2, T>}:
80 match cloned:
81 case Clone.Cloned{first, second, exact, +same_first, +same_second, valid_first, valid_second}:
82 %same_second :
83 {Model.observe(T, d, Array.set(T, original, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, _, other)) : Maybe<&2, T>}
84 %same_first :
85 {Model.observe(T, d, Array.set(T, _, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, second, other)) : Maybe<&2, T>}
86 %Equal.sym(Array<T>, Array.set(T, first, i, value), ArrayCore.write_path(T, d, first, Refinement.route(d, i), value),
87 Refinement.law_set_refines(T, d, first, i, value, valid_first)) :
88 {Model.observe(T, d, _, other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, second, other)) : Maybe<&2, T>}
89 %Equal.trans(Array<T>, second, original, first, same_second,
90 Equal.sym(Array<T>, first, original, same_first)) :
91 {Model.observe(T, d, ArrayCore.write_path(T, d, _, Refinement.route(d, i), value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, second, other)) : Maybe<&2, T>}
92 update_frame(T, d, second, Refinement.route(d, i), other, value, valid_second)
93
94def primitive_update_frame(-T: Data, +d: Nat, array: Array<T>, +i: U32, +other: Model.Path(d), +value: T, valid: Model.Balanced(T, d, array)) ->
95 {Model.observe(T, d, Array.set(T, array, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, array, other)) : Maybe<&2, T>}:
96 primitive_frame_cloned(T, d, array, i, other, value, Clone.certify(T, d, array, valid))
97
98def path_self_same(+d: Nat, +path: Model.Path(d)) ->
99 {Model.same(d, path, path) == True{} : Bool}:
100 match d:
101 case 0n:
102 {==}
103 case 1n+p:
104 Model.Step{bit, rest} = path
105 match bit:
106 case False{}:
107 path_self_same(p, rest)
108 case True{}:
109 path_self_same(p, rest)
110
111def primitive_write_read(-T: Data, +d: Nat, array: Array<T>, +i: U32, +value: T, valid: Model.Balanced(T, d, array)) ->
112 {Model.observe(T, d, Array.set(T, array, i, value), Refinement.route(d, i)) == Some{value} : Maybe<&2, T>}:
113 %Equal.sym(Maybe<&2, T>,
114 Model.observe(T, d, Array.set(T, array, i, value), Refinement.route(d, i)),
115 Model.select(T, Model.same(d, Refinement.route(d, i), Refinement.route(d, i)), value,
116 Model.observe(T, d, array, Refinement.route(d, i))),
117 primitive_update_frame(T, d, array, i, Refinement.route(d, i), value, valid)) :
118 {_ == Some{value} : Maybe<&2, T>}
119 %Equal.sym(Bool, Model.same(d, Refinement.route(d, i), Refinement.route(d, i)), True{},
120 path_self_same(d, Refinement.route(d, i))) :
121 {Model.select(T, _, value, Model.observe(T, d, array, Refinement.route(d, i))) == Some{value} : Maybe<&2, T>}
122 {==}