1	import Base
2	
3	# lawful-arrays definitions. The laws are in LAWS.bend.
4	#
5	# Base's Array<T> is a binary tree (ALeaf, ANode) that the runtime stores as one
6	# flat block; Array.get and Array.set are one load or store there. The laws
7	# describe an array by the list of its leaves, left to right.
8	
9	# a is a perfect tree of depth d: 2^d leaves, every one at depth d. Arrays
10	# made by Array.new are; Array.set and Array.get keep it so.
11	def full(-T: Type, a: Array<T>, +d: Nat) -> Bool:
12	  match a d:
13	    case ALeaf{x} 0n:
14	      True{}
15	    case ALeaf{x} 1n+p:
16	      False{}
17	    case ANode{xs, ys} 0n:
18	      False{}
19	    case ANode{xs, ys} 1n+p:
20	      full(T, xs, p) && full(T, ys, p)
21	
22	# The leaves of a, left to right (the same list as Base's Array.to_list, which
23	# is a template and cannot appear in a law). Elements must be Data.
24	def view(-T: Data, a: Array<T>) -> List<&2, T>:
25	  match a:
26	    case ALeaf{x}:
27	      [x]
28	    case ANode{xs, ys}:
29	      List.append(&2, T, view(T, xs), view(T, ys))
30	
31	# The leaf an access at index i reaches in a perfect tree of depth d < 32:
32	# i modulo 2^d. (From depth 32 up, Base's Array.size wraps to 0 and every
33	# access reaches the last leaf; the laws exclude that.)
34	def slot(i: U32, d: Nat) -> Nat:
35	  Nat.mod(U32.to_nat(i), Nat.pow(2n, d))