1	import Base
2	
3	# Persistent fixed-size vector: a perfect binary tree of depth d holding
4	# 2^d slots, slot j addressed by comparing j with 2^(d-1) at each level.
5	# get/set cost O(d) = O(log size); the tree is immutable Data, so updates
6	# share all untouched subtrees. Shared by structures that need indexed
7	# storage. Do not instantiate with U32 payloads through this
8	# erased-generic code (see docs/VALIDATION.md, runtime defects).
9	
10	type Vec<-T: Data> is Data:
11	  VLeaf{value: T}
12	  VNode{lo: Vec<T>, hi: Vec<T>}
13	
14	def pow2(k: Nat) -> Nat:
15	  match k:
16	    case 0n:
17	      1n
18	    case 1n+p:
19	      Nat.double(pow2(p))
20	
21	# Branch decision at a node of depth d for slot j: True = lower half.
22	def dec(d: Nat, +j: Nat) -> Bool:
23	  match d:
24	    case 0n:
25	      False{}
26	    case 1n+q:
27	      Nat.is_lt(j, pow2(q))
28	
29	def get_go(-T: Data, d: Nat, t: Vec<T>, +j: Nat, left: Bool) -> Maybe<&2, T>:
30	  match d t left:
31	    case 0n VLeaf{x} _:
32	      Some{x}
33	    case 0n VNode{l, r} _:
34	      None{}
35	    case 1n+p VLeaf{x} _:
36	      None{}
37	    case 1n+ +p VNode{l, r} True{}:
38	      get_go(T, p, l, j, dec(p, j))
39	    case 1n+ +p VNode{l, r} False{}:
40	      get_go(T, p, r, Nat.sub(j, pow2(p)), dec(p, Nat.sub(j, pow2(p))))
41	
42	# Slot j of a depth-d vector (None only for a malformed tree).
43	def get(-T: Data, +d: Nat, t: Vec<T>, +j: Nat) -> Maybe<&2, T>:
44	  get_go(T, d, t, j, dec(d, j))
45	
46	def set_go(-T: Data, d: Nat, t: Vec<T>, +j: Nat, +v: T, left: Bool) -> Vec<T>:
47	  match d t left:
48	    case 0n VLeaf{x} _:
49	      VLeaf{v}
50	    case 0n VNode{l, r} _:
51	      VNode{l, r}
52	    case 1n+p VLeaf{x} _:
53	      VLeaf{x}
54	    case 1n+ +p VNode{l, r} True{}:
55	      VNode{set_go(T, p, l, j, v, dec(p, j)), r}
56	    case 1n+ +p VNode{l, r} False{}:
57	      VNode{l, set_go(T, p, r, Nat.sub(j, pow2(p)), v, dec(p, Nat.sub(j, pow2(p))))}
58	
59	# Replace slot j (j < 2^d).
60	def set(-T: Data, +d: Nat, t: Vec<T>, +j: Nat, +v: T) -> Vec<T>:
61	  set_go(T, d, t, j, v, dec(d, j))
62	
63	# Smallest depth whose capacity covers n more slots: `room` counts the free
64	# slots left at the current depth (capacity 2^d).
65	def depth_go(n: Nat, +d: Nat, room: Nat) -> Nat:
66	  match n room:
67	    case 0n _:
68	      d
69	    case 1n+p 0n:
70	      depth_go(p, 1n+d, Nat.sub(pow2(d), 1n))
71	    case 1n+p 1n+r:
72	      depth_go(p, d, r)
73	
74	def depth_for(n: Nat) -> Nat:
75	  depth_go(n, 0n, 1n)