def Table.set.go

bend-lint-api@0.2.0.0 · shared/tables.bend:25

import bend-lint-api@0.2.0.0/shared/tables.bend as Tables
import Base

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      }

Uses (9)

Used by (1)