1	import Base
2	
3	# Values by number, from 0: a balanced tree. Each node parts its values by a bit of their number, the lowest first, so
4	# a lookup reads the bits of a number, and no text.
5	type Table<-A: Data> is Data:
6	  TLeaf{value: Maybe<&2, A>}
7	  TNode{even: Table<A>, odd: Table<A>}
8	
9	# A table grows one value at a time: a leaf holds the value whose number has no bits left (the number read from its
10	# lowest bit, a bit a level), so a value numbered `i` is about log2(i) levels down.
11	
12	# The value numbered `i` in `t`: `odd` is whether `i` is.
13	def Table.get.go(-A: Data, t: Table<A>, +i: U32, odd: Bool) -> Maybe<&2, A>:
14	  match t odd:
15	    case TLeaf{v} _:
16	      Bool.pick(Maybe<&2, A>, U32.is_zero(i), v, None{})
17	    case TNode{e, o} False{}:
18	      Table.get.go(A, e, U32.shr(i), U32.is_eq(U32.and(U32.shr(i), 1), 1))
19	    case TNode{e, o} True{}:
20	      Table.get.go(A, o, U32.shr(i), U32.is_eq(U32.and(U32.shr(i), 1), 1))
21	
22	def Table.get(-A: Data, t: Table<A>, +i: U32) -> Maybe<&2, A>:
23	  Table.get.go(A, t, i, U32.is_eq(U32.and(i, 1), 1))
24	
25	# `t` with `x` numbered `i`: `odd` is whether `i` is, and `zero` whether it is 0. A leaf of another number parts
26	# first. `fuel` bounds the levels: two a bit.
27	def Table.set.go(
28	  -A: Data,
29	  fuel: Nat,
30	  t: Table<A>,
31	  +i: U32,
32	  x: A,
33	  odd: Bool,
34	  zero: Bool
35	) -> Table<A>:
36	  match fuel t odd zero:
37	    case 0n _ _ _:
38	      t
39	    case 1n+f TLeaf{v} _ True{}:
40	      TLeaf{Some{x}}
41	    case 1n+f TLeaf{v} _ False{}:
42	      Table.set.go(A, f, TNode{TLeaf{v}, TLeaf{None{}}}, i, x, odd, zero)
43	    case 1n+f TNode{e, o} False{} _:
44	      TNode{
45	        Table.set.go(
46	          A,
47	          f,
48	          e,
49	          U32.shr(i),
50	          x,
51	          U32.is_eq(U32.and(U32.shr(i), 1), 1),
52	          U32.is_zero(U32.shr(i))
53	        ),
54	        o
55	      }
56	    case 1n+f TNode{e, o} True{} _:
57	      TNode{
58	        e,
59	        Table.set.go(
60	          A,
61	          f,
62	          o,
63	          U32.shr(i),
64	          x,
65	          U32.is_eq(U32.and(U32.shr(i), 1), 1),
66	          U32.is_zero(U32.shr(i))
67	        )
68	      }
69	
70	def Table.set(-A: Data, t: Table<A>, +i: U32, x: A) -> Table<A>:
71	  Table.set.go(A, 66n, t, i, x, U32.is_eq(U32.and(i, 1), 1), U32.is_zero(i))