1	import Base
2	import ./model.bend as Model
3	
4	def 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	
9	def 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	
14	def 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	
21	type 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	
26	def 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	
34	def 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	
42	def 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	
61	def 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	
77	def 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	
96	def 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	
102	def 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