shared/tables.bend

bend-lint-api@0.2.0.0 · 71 lines · 5 definitions

1import 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.
5type 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.
13def 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
22def 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.
27def 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
70def 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))