1	import Base
2	import ./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	
9	def 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)
17	def 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)
24	def 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	
33	def reads(n: Nat, a: Array<U32>) -> String:
34	  reads.go(n, 0, Array.get(U32, a, 0))
35	
36	def 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