src/storage/size.bend
bendtorch-core@0.1.0.0 · 57 lines · 6 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3
4def capacity(d: Nat) -> U32:
5 match d:
6 case 0n:
7 1
8 case 1n+p:
9 U32.shl(capacity(p))
10
11type Sized<-T: Data, -d: Nat, -original: Array<T>> is Type:
12 Sized{array: Array<T>, size: U32,
13 retained: {array == original : Array<T>},
14 measured: {(array, size) == Array.size(T, original) : Array<T> & U32},
15 extent: {size == capacity(d) : U32},
16 balanced: Model.Balanced(T, d, array)}
17
18def join(-T: Data, -d: Nat, -original: Array<T>, ys: Array<T>,
19 child: Sized<T, d, original>, valid: Model.Balanced(T, d, ys)) ->
20 Sized<T, 1n+d, ANode{original, ys}>:
21 match child:
22 case Sized{xs, n, retained, measured, extent, balanced}:
23 Sized{ANode{xs, ys}, U32.shl(n),
24 Equal.cong(Array<T>, Array<T>, x => ANode{x, ys}, xs, original, retained),
25 Equal.cong(Array<T> & U32, Array<T> & U32, r => Array.size.node(T, ys, r),
26 (xs, n), Array.size(T, original), measured),
27 Equal.cong(U32, U32, x => U32.shl(x), n, capacity(d), extent), (balanced, valid)}
28
29def certify(-T: Data, +d: Nat, array: Array<T>, valid: Model.Balanced(T, d, array)) -> Sized<T, d, array>:
30 match d array:
31 case 0n ALeaf{x}:
32 Sized{ALeaf{x}, 1, {==}, {==}, {==}, valid}
33 case 0n ANode{xs, ys}:
34 match valid:
35 case 1n+p ALeaf{x}:
36 match valid:
37 case 1n++p ANode{xs, ys}:
38 (ex, ey) = valid
39 join(T, p, xs, ys, certify(T, p, xs, ex), ey)
40
41def retains(-T: Data, -d: Nat, -original: Array<T>, sized: Sized<T, d, original>) ->
42 {Pair.fst(Array<T>, U32, Array.size(T, original)) == original : Array<T>}:
43 match sized:
44 case Sized{array, n, retained, measured, extent, balanced}:
45 Equal.trans(Array<T>, Pair.fst(Array<T>, U32, Array.size(T, original)), array, original,
46 Equal.cong(Array<T> & U32, Array<T>, r => Pair.fst(Array<T>, U32, r),
47 Array.size(T, original), (array, n),
48 Equal.sym(Array<T> & U32, (array, n), Array.size(T, original), measured)), retained)
49
50def extent(-T: Data, -d: Nat, -original: Array<T>, sized: Sized<T, d, original>) ->
51 {Pair.snd(Array<T>, U32, Array.size(T, original)) == capacity(d) : U32}:
52 match sized:
53 case Sized{array, n, retained, measured, extent, balanced}:
54 Equal.trans(U32, Pair.snd(Array<T>, U32, Array.size(T, original)), n, capacity(d),
55 Equal.cong(Array<T> & U32, U32, r => Pair.snd(Array<T>, U32, r),
56 Array.size(T, original), (array, n),
57 Equal.sym(Array<T> & U32, (array, n), Array.size(T, original), measured)), extent)