check.bend

bend-osdev-array@0.1.0.0 · 44 lines · 0 definitions

1import Base
2import bend-osdev-array@0.1.0.0/array.bend as A
3
4# Arrays.is_perfect and Arrays.leaves are specifications: they match on
5# ALeaf / ANode for any element type, which the compiled runtime (holding an
6# array natively) does not run, so they appear in laws only (LAWS.bend has
7# their vectors). Base's Array.to_list lists the same slots at run time.
8
9def show_list(xs: List<U32>) -> String:
10  match xs:
11    case Nil{}:
12      ""
13    case Con{h, t}:
14      U32.show(h) ++ " " ++ show_list(t)
15
16# a depth-3 array (8 slots) with slots 1, 5 and 6 written (14 wraps to 6)
17def sample() -> Array<U32>:
18  a = Array.new(U32, 3n, 0)
19  a = Array.set(U32, a, 1, 10)
20  a = Array.set(U32, a, 5, 50)
21  Array.set(U32, a, 14, 60)
22
23# the reads of indices from i on, n of them (r: the read of index i)
24def reads.go(n: Nat, +i: U32, r: Array<U32> & U32) -> String:
25  match n:
26    case 0n:
27      (a, x) = r
28      U32.show(x)
29    case 1n+p:
30      (a, x) = r
31      U32.show(x) ++ " " ++ reads.go(p, U32.add(i, 1), Array.get(U32, a, U32.add(i, 1)))
32
33def reads(n: Nat, a: Array<U32>) -> String:
34  reads.go(n, 0, Array.get(U32, a, 0))
35
36def main() -> IO(Unit):
37  do IO<Unit>:
38    IO.print(reads(9n, sample()))
39    IO.print(show_list(Array.to_list(~U32, sample())))
40    IO.print(Nat.show(A.Arrays.index(3n, 14)) ++ " " ++ Nat.show(A.Arrays.slots(3n)))
41
42#|0 10 0 0 0 50 60 0 0 10
43#|0 10 0 0 0 50 60 0 
44#|6 8