1	import Base
2	import ./model.bend as Model
3	
4	def capacity(d: Nat) -> U32:
5	  match d:
6	    case 0n:
7	      1
8	    case 1n+p:
9	      U32.shl(capacity(p))
10	
11	type 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	
18	def 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	
29	def 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	
41	def 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	
50	def 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)