src/storage/array.bend
bendtorch-core@0.1.0.0 · 106 lines · 11 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3
4def left(-T: Type, -d: Nat, -xs: Array<T>, -ys: Array<T>,
5 e: Model.Balanced(T, d, xs) & Model.Balanced(T, d, ys)) -> Model.Balanced(T, d, xs):
6 (ex, ey) = e
7 ex
8
9def right(-T: Type, -d: Nat, -xs: Array<T>, -ys: Array<T>,
10 e: Model.Balanced(T, d, xs) & Model.Balanced(T, d, ys)) -> Model.Balanced(T, d, ys):
11 (ex, ey) = e
12 ey
13
14def new_balanced(-T: Data, +d: Nat, +value: T) -> Model.Balanced(T, d, Array.new(T, d, value)):
15 match d:
16 case 0n:
17 Unit{}
18 case 1n++p:
19 (new_balanced(T, p, value), new_balanced(T, p, value))
20
21type Read<-T: Data, -d: Nat, -original: Array<T>, -path: Model.Path(d)> is Type:
22 Read{array: Array<T>, value: Maybe<&2, T>, -balanced: Model.Balanced(T, d, array),
23 retained: {array == original : Array<T>},
24 observed: {value == Model.observe(T, d, original, path) : Maybe<&2, T>}}
25
26def low(-T: Data, -d: Nat, -original: Array<T>, -path: Model.Path(d), ys: Array<T>,
27 read: Read<T, d, original, path>, -ey: Model.Balanced(T, d, ys)) ->
28 Read<T, 1n+d, ANode{original, ys}, Model.Step{False{}, path}>:
29 match read:
30 case Read{xs, value, ex, kept, observed}:
31 Read{ANode{xs, ys}, value, (ex, ey),
32 Equal.cong(Array<T>, Array<T>, x => ANode{x, ys}, xs, original, kept), observed}
33
34def high(-T: Data, -d: Nat, -original: Array<T>, -path: Model.Path(d), xs: Array<T>,
35 read: Read<T, d, original, path>, -ex: Model.Balanced(T, d, xs)) ->
36 Read<T, 1n+d, ANode{xs, original}, Model.Step{True{}, path}>:
37 match read:
38 case Read{ys, value, ey, kept, observed}:
39 Read{ANode{xs, ys}, value, (ex, ey),
40 Equal.cong(Array<T>, Array<T>, y => ANode{xs, y}, ys, original, kept), observed}
41
42def read_path(-T: Data, +d: Nat, array: Array<T>, path: Model.Path(d),
43 -valid: Model.Balanced(T, d, array)) -> Read<T, d, array, path>:
44 match d array:
45 case 0n ALeaf{+value}:
46 Read{ALeaf{value}, Some{value}, valid, {==}, {==}}
47 case 0n ANode{xs, ys}:
48 Read{ANode{xs, ys}, None{}, valid, {==}, {==}}
49 case 1n+p ALeaf{value}:
50 Read{ALeaf{value}, None{}, valid, {==}, {==}}
51 case 1n++p ANode{xs, ys}:
52 Model.Step{bit, rest} = path
53 match bit:
54 case False{}:
55 low(T, p, xs, rest, ys, read_path(T, p, xs, rest, left(T, p, xs, ys, valid)),
56 right(T, p, xs, ys, valid))
57 case True{}:
58 high(T, p, ys, rest, xs, read_path(T, p, ys, rest, right(T, p, xs, ys, valid)),
59 left(T, p, xs, ys, valid))
60
61def write_path(-T: Data, d: Nat, array: Array<T>, path: Model.Path(d), value: T) -> Array<T>:
62 match d array:
63 case 0n ALeaf{old}:
64 ALeaf{value}
65 case 0n ANode{xs, ys}:
66 ANode{xs, ys}
67 case 1n+p ALeaf{old}:
68 ALeaf{old}
69 case 1n+p ANode{xs, ys}:
70 Model.Step{bit, rest} = path
71 match bit:
72 case False{}:
73 ANode{write_path(T, p, xs, rest, value), ys}
74 case True{}:
75 ANode{xs, write_path(T, p, ys, rest, value)}
76
77def write_balanced(-T: Data, d: Nat, array: Array<T>, path: Model.Path(d), value: T,
78 valid: Model.Balanced(T, d, array)) -> Model.Balanced(T, d, write_path(T, d, array, path, value)):
79 match d array:
80 case 0n ALeaf{old}:
81 valid
82 case 0n ANode{xs, ys}:
83 valid
84 case 1n+p ALeaf{old}:
85 valid
86 case 1n+p ANode{xs, ys}:
87 Model.Step{bit, rest} = path
88 match bit:
89 case False{}:
90 (ex, ey) = valid
91 (write_balanced(T, p, xs, rest, value, ex), ey)
92 case True{}:
93 (ex, ey) = valid
94 (ex, write_balanced(T, p, ys, rest, value, ey))
95
96def observation(-T: Data, -d: Nat, -original: Array<T>, -path: Model.Path(d),
97 read: Read<T, d, original, path>) -> Maybe<&2, T>:
98 match read:
99 case Read{array, value, valid, kept, observed}:
100 value
101
102def retained(-T: Data, -d: Nat, -original: Array<T>, -path: Model.Path(d),
103 read: Read<T, d, original, path>) -> Array<T>:
104 match read:
105 case Read{array, value, valid, kept, observed}:
106 array