1	import Base
2	
3	def capacity(d: Nat) -> Nat:
4	  match d:
5	    case 0n:
6	      1n
7	    case 1n+p:
8	      +n = capacity(p)
9	      Nat.add(n, n)
10	
11	def Path(d: Nat) -> Data:
12	  match d:
13	    case 0n:
14	      Unit
15	    case 1n+p:
16	      Step<p>
17	
18	type Step<-d: Nat> is Data:
19	  Step{bit: Bool, tail: Path(d)}
20	
21	def offset_step(b: Bool, half: Nat, tail: Nat) -> Nat:
22	  match b:
23	    case False{}:
24	      tail
25	    case True{}:
26	      Nat.add(half, tail)
27	
28	def offset(d: Nat, path: Path(d)) -> Nat:
29	  match d:
30	    case 0n:
31	      0n
32	    case 1n++p:
33	      Step{b, rest} = path
34	      offset_step(b, capacity(p), offset(p, rest))
35	
36	def same(d: Nat, a: Path(d), b: Path(d)) -> Bool:
37	  match d:
38	    case 0n:
39	      True{}
40	    case 1n+p:
41	      Step{ab, ar} = a
42	      Step{bb, br} = b
43	      Bool.and(Bool.not(Bool.xor(ab, bb)), same(p, ar, br))
44	
45	def Balanced(-T: Type, d: Nat, array: Array<T>) -> Type:
46	  match d array:
47	    case 0n ALeaf{x}:
48	      Unit
49	    case 0n ANode{xs, ys}:
50	      Empty
51	    case 1n+p ALeaf{x}:
52	      Empty
53	    case 1n++p ANode{xs, ys}:
54	      Balanced(T, p, xs) & Balanced(T, p, ys)
55	
56	def observe(-T: Data, d: Nat, array: Array<T>, path: Path(d)) -> Maybe<&2, T>:
57	  match d array:
58	    case 0n ALeaf{x}:
59	      Some{x}
60	    case 0n ANode{xs, ys}:
61	      None{}
62	    case 1n+p ALeaf{x}:
63	      None{}
64	    case 1n+p ANode{xs, ys}:
65	      Step{bit, rest} = path
66	      match bit:
67	        case False{}:
68	          observe(T, p, xs, rest)
69	        case True{}:
70	          observe(T, p, ys, rest)
71	
72	def select(-T: Data, b: Bool, value: T, old: Maybe<&2, T>) -> Maybe<&2, T>:
73	  match b:
74	    case False{}:
75	      old
76	    case True{}:
77	      Some{value}