defs.bend
1import 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.
11def 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.
24def 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.)
34def slot(i: U32, d: Nat) -> Nat:
35 Nat.mod(U32.to_nat(i), Nat.pow(2n, d))