src/containers/internal/vec.bend
bend-collections-laws-containers@1.0.0.0 · 75 lines · 0 definitions
1import 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
10type Vec<-T: Data> is Data:
11 VLeaf{value: T}
12 VNode{lo: Vec<T>, hi: Vec<T>}
13
14def 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.
22def 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
29def 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).
43def get(-T: Data, +d: Nat, t: Vec<T>, +j: Nat) -> Maybe<&2, T>:
44 get_go(T, d, t, j, dec(d, j))
45
46def 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).
60def 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).
65def 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
74def depth_for(n: Nat) -> Nat:
75 depth_go(n, 0n, 1n)