src/storage/model.bend

bendtorch-core@0.1.0.0 · 77 lines · 9 definitions

1import Base
2
3def capacity(d: Nat) -> Nat:
4  match d:
5    case 0n:
6      1n
7    case 1n+p:
8      +n = capacity(p)
9      Nat.add(n, n)
10
11def Path(d: Nat) -> Data:
12  match d:
13    case 0n:
14      Unit
15    case 1n+p:
16      Step<p>
17
18type Step<-d: Nat> is Data:
19  Step{bit: Bool, tail: Path(d)}
20
21def offset_step(b: Bool, half: Nat, tail: Nat) -> Nat:
22  match b:
23    case False{}:
24      tail
25    case True{}:
26      Nat.add(half, tail)
27
28def offset(d: Nat, path: Path(d)) -> Nat:
29  match d:
30    case 0n:
31      0n
32    case 1n++p:
33      Step{b, rest} = path
34      offset_step(b, capacity(p), offset(p, rest))
35
36def same(d: Nat, a: Path(d), b: Path(d)) -> Bool:
37  match d:
38    case 0n:
39      True{}
40    case 1n+p:
41      Step{ab, ar} = a
42      Step{bb, br} = b
43      Bool.and(Bool.not(Bool.xor(ab, bb)), same(p, ar, br))
44
45def Balanced(-T: Type, d: Nat, array: Array<T>) -> Type:
46  match d array:
47    case 0n ALeaf{x}:
48      Unit
49    case 0n ANode{xs, ys}:
50      Empty
51    case 1n+p ALeaf{x}:
52      Empty
53    case 1n++p ANode{xs, ys}:
54      Balanced(T, p, xs) & Balanced(T, p, ys)
55
56def observe(-T: Data, d: Nat, array: Array<T>, path: Path(d)) -> Maybe<&2, T>:
57  match d array:
58    case 0n ALeaf{x}:
59      Some{x}
60    case 0n ANode{xs, ys}:
61      None{}
62    case 1n+p ALeaf{x}:
63      None{}
64    case 1n+p ANode{xs, ys}:
65      Step{bit, rest} = path
66      match bit:
67        case False{}:
68          observe(T, p, xs, rest)
69        case True{}:
70          observe(T, p, ys, rest)
71
72def select(-T: Data, b: Bool, value: T, old: Maybe<&2, T>) -> Maybe<&2, T>:
73  match b:
74    case False{}:
75      old
76    case True{}:
77      Some{value}