src/storage/clone.bend
bendtorch-core@0.1.0.0 · 79 lines · 8 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3
4type Cloned<-T: Data, -d: Nat, -original: Array<T>> is Type:
5 Cloned{first: Array<T>, second: Array<T>,
6 exact: {(first, second) == Array.clone(T, original) : Array<T> & Array<T>},
7 first_equal: {first == original : Array<T>},
8 second_equal: {second == original : Array<T>},
9 first_balanced: Model.Balanced(T, d, first),
10 second_balanced: Model.Balanced(T, d, second)}
11
12def node_equal(-T: Data, -a: Array<T>, -b: Array<T>, -x: Array<T>, -y: Array<T>,
13 left: {a == x : Array<T>}, right: {b == y : Array<T>}) ->
14 {ANode{a, b} == ANode{x, y} : Array<T>}:
15 Equal.trans(Array<T>, ANode{a, b}, ANode{x, b}, ANode{x, y},
16 Equal.cong(Array<T>, Array<T>, v => ANode{v, b}, a, x, left),
17 Equal.cong(Array<T>, Array<T>, v => ANode{x, v}, b, y, right))
18
19def join(-T: Data, -d: Nat, -xs: Array<T>, -ys: Array<T>,
20 left: Cloned<T, d, xs>, right: Cloned<T, d, ys>) -> Cloned<T, 1n+d, ANode{xs, ys}>:
21 match left:
22 case Cloned{xa, xb, exact_x, same_xa, same_xb, valid_xa, valid_xb}:
23 match right:
24 case Cloned{ya, yb, exact_y, same_ya, same_yb, valid_ya, valid_yb}:
25 Cloned{ANode{xa, ya}, ANode{xb, yb},
26 Equal.trans(Array<T> & Array<T>, (ANode{xa, ya}, ANode{xb, yb}),
27 Array.clone.node(T, Array.clone(T, xs), (ya, yb)),
28 Array.clone.node(T, Array.clone(T, xs), Array.clone(T, ys)),
29 Equal.cong(Array<T> & Array<T>, Array<T> & Array<T>,
30 r => Array.clone.node(T, r, (ya, yb)), (xa, xb), Array.clone(T, xs), exact_x),
31 Equal.cong(Array<T> & Array<T>, Array<T> & Array<T>,
32 r => Array.clone.node(T, Array.clone(T, xs), r), (ya, yb), Array.clone(T, ys), exact_y)),
33 node_equal(T, xa, ya, xs, ys, same_xa, same_ya),
34 node_equal(T, xb, yb, xs, ys, same_xb, same_yb),
35 (valid_xa, valid_ya), (valid_xb, valid_yb)}
36
37def certify(-T: Data, +d: Nat, array: Array<T>, valid: Model.Balanced(T, d, array)) -> Cloned<T, d, array>:
38 match d array:
39 case 0n ALeaf{+value}:
40 Cloned{ALeaf{value}, ALeaf{value}, {==}, {==}, {==}, Unit{}, Unit{}}
41 case 0n ANode{xs, ys}:
42 match valid:
43 case 1n+p ALeaf{value}:
44 match valid:
45 case 1n++p ANode{xs, ys}:
46 (ex, ey) = valid
47 join(T, p, xs, ys, certify(T, p, xs, ex), certify(T, p, ys, ey))
48
49def first_equal(-T: Data, -d: Nat, -original: Array<T>, cloned: Cloned<T, d, original>) ->
50 {Pair.fst(Array<T>, Array<T>, Array.clone(T, original)) == original : Array<T>}:
51 match cloned:
52 case Cloned{first, second, exact, same_first, same_second, valid_first, valid_second}:
53 Equal.trans(Array<T>, Pair.fst(Array<T>, Array<T>, Array.clone(T, original)), first, original,
54 Equal.cong(Array<T> & Array<T>, Array<T>, r => Pair.fst(Array<T>, Array<T>, r),
55 Array.clone(T, original), (first, second),
56 Equal.sym(Array<T> & Array<T>, (first, second), Array.clone(T, original), exact)), same_first)
57
58def second_equal(-T: Data, -d: Nat, -original: Array<T>, cloned: Cloned<T, d, original>) ->
59 {Pair.snd(Array<T>, Array<T>, Array.clone(T, original)) == original : Array<T>}:
60 match cloned:
61 case Cloned{first, second, exact, same_first, same_second, valid_first, valid_second}:
62 Equal.trans(Array<T>, Pair.snd(Array<T>, Array<T>, Array.clone(T, original)), second, original,
63 Equal.cong(Array<T> & Array<T>, Array<T>, r => Pair.snd(Array<T>, Array<T>, r),
64 Array.clone(T, original), (first, second),
65 Equal.sym(Array<T> & Array<T>, (first, second), Array.clone(T, original), exact)), same_second)
66
67def first_balanced(-T: Data, -d: Nat, -original: Array<T>, cloned: Cloned<T, d, original>) ->
68 Model.Balanced(T, d, Pair.fst(Array<T>, Array<T>, Array.clone(T, original))):
69 match cloned:
70 case Cloned{first, second, exact, same_first, same_second, valid_first, valid_second}:
71 %exact : Model.Balanced(T, d, Pair.fst(Array<T>, Array<T>, _))
72 valid_first
73
74def second_balanced(-T: Data, -d: Nat, -original: Array<T>, cloned: Cloned<T, d, original>) ->
75 Model.Balanced(T, d, Pair.snd(Array<T>, Array<T>, Array.clone(T, original))):
76 match cloned:
77 case Cloned{first, second, exact, same_first, same_second, valid_first, valid_second}:
78 %exact : Model.Balanced(T, d, Pair.snd(Array<T>, Array<T>, _))
79 valid_second