1	import Base
2	import ./defs.bend as D
3	
4	# lawful-arrays: what Base's Array operations do, stated on the list of an
5	# array's leaves (D.view). The laws are about perfect trees (D.full: depth d,
6	# 2^d leaves), which is what Array.new makes and every operation keeps. For
7	# d < 32, an index i reaches leaf i modulo 2^d (D.slot); from 32 up Base's
8	# Array.size wraps to 0, so the indexing laws require d < 32. Elements are Data
9	# (Array.get requires it, and so does D.view); only swap_full also covers
10	# other element types.
11	
12	# ==========================================================================
13	# Creating
14	# ==========================================================================
15	
16	law new_full:
17	  for -T: Data
18	  for d: Nat
19	  for v: T
20	  {D.full(T, Array.new(T, d, v), d) == True{} : Bool}
21	
22	law new_view:
23	  for -T: Data
24	  for d: Nat
25	  for v: T
26	  {D.view(T, Array.new(T, d, v)) == List.replicate(T, Nat.pow(2n, d), v) : List<&2, T>}
27	
28	# ==========================================================================
29	# Size
30	# ==========================================================================
31	
32	law view_length:
33	  for -T: Data
34	  for a: Array<T>
35	  for d: Nat
36	  for hf: {D.full(T, a, d) == True{} : Bool}
37	  {List.length(&2, T, D.view(T, a)) == Nat.pow(2n, d) : Nat}
38	
39	# Array.size doubles 1 once per level of the left spine: for a perfect tree of
40	# depth d below 32 that is the number of leaves, 2^d.
41	law size_count:
42	  for -T: Data
43	  for a: Array<T>
44	  for d: Nat
45	  for hf: {D.full(T, a, d) == True{} : Bool}
46	  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
47	  {U32.to_nat(Pair.snd(Array<T>, U32, Array.size(T, a))) == Nat.pow(2n, d) : Nat}
48	
49	law size_kept:
50	  for -T: Data
51	  for a: Array<T>
52	  {Pair.fst(Array<T>, U32, Array.size(T, a)) == a : Array<T>}
53	
54	# ==========================================================================
55	# Reading
56	# ==========================================================================
57	
58	# Array.get reads leaf i (modulo the size).
59	law get_view:
60	  for -T: Data
61	  for a: Array<T>
62	  for d: Nat
63	  for i: U32
64	  for hf: {D.full(T, a, d) == True{} : Bool}
65	  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
66	  {Some{Pair.snd(Array<T>, T, Array.get(T, a, i))} == List.get(&2, T, D.view(T, a), D.slot(i, d)) : Maybe<&2, T>}
67	
68	# Array.get hands back the same array.
69	law get_kept:
70	  for -T: Data
71	  for a: Array<T>
72	  for i: U32
73	  {Pair.fst(Array<T>, T, Array.get(T, a, i)) == a : Array<T>}
74	
75	# ==========================================================================
76	# Writing
77	# ==========================================================================
78	
79	# Array.set replaces leaf i (modulo the size) and nothing else.
80	law set_view:
81	  for -T: Data
82	  for a: Array<T>
83	  for d: Nat
84	  for i: U32
85	  for v: T
86	  for hf: {D.full(T, a, d) == True{} : Bool}
87	  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
88	  {D.view(T, Array.set(T, a, i, v)) == List.set(&2, T, D.view(T, a), D.slot(i, d), v) : List<&2, T>}
89	
90	law set_full:
91	  for -T: Data
92	  for a: Array<T>
93	  for d: Nat
94	  for i: U32
95	  for v: T
96	  for hf: {D.full(T, a, d) == True{} : Bool}
97	  {D.full(T, Array.set(T, a, i, v), d) == True{} : Bool}
98	
99	# Reading what was just written gives it back.
100	# (This holds for every tree: set and get take the same path.)
101	law get_set_same:
102	  for -T: Data
103	  for a: Array<T>
104	  for i: U32
105	  for v: T
106	  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}
107	
108	# Writing leaf i does not change leaf j (j a different leaf modulo the size).
109	law get_set_other:
110	  for -T: Data
111	  for a: Array<T>
112	  for d: Nat
113	  for i: U32
114	  for j: U32
115	  for v: T
116	  for hf: {D.full(T, a, d) == True{} : Bool}
117	  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
118	  for hij: {Nat.is_eq(D.slot(i, d), D.slot(j, d)) == False{} : Bool}
119	  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array<T>, T, Array.get(T, a, j)) : T}
120	
121	# ==========================================================================
122	# Swapping (Array.set is a swap that drops the old value; for elements that
123	# are not Data only swap_full applies)
124	# ==========================================================================
125	
126	law swap_view:
127	  for -T: Data
128	  for a: Array<T>
129	  for d: Nat
130	  for i: U32
131	  for v: T
132	  for hf: {D.full(T, a, d) == True{} : Bool}
133	  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
134	  {D.view(T, Pair.fst(Array<T>, T, Array.swap(T, a, i, v))) == List.set(&2, T, D.view(T, a), D.slot(i, d), v) : List<&2, T>}
135	
136	law swap_old:
137	  for -T: Data
138	  for a: Array<T>
139	  for d: Nat
140	  for i: U32
141	  for v: T
142	  for hf: {D.full(T, a, d) == True{} : Bool}
143	  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
144	  {Some{Pair.snd(Array<T>, T, Array.swap(T, a, i, v))} == List.get(&2, T, D.view(T, a), D.slot(i, d)) : Maybe<&2, T>}
145	
146	law swap_full:
147	  for -T: Type
148	  for a: Array<T>
149	  for d: Nat
150	  for i: U32
151	  for v: T
152	  for hf: {D.full(T, a, d) == True{} : Bool}
153	  {D.full(T, Pair.fst(Array<T>, T, Array.swap(T, a, i, v)), d) == True{} : Bool}
154	
155	# ==========================================================================
156	# Shapes, equality and indexes
157	# ==========================================================================
158	
159	# Two perfect trees of the same depth with the same leaves are the same array.
160	law view_inj:
161	  for -T: Data
162	  for a: Array<T>
163	  for b: Array<T>
164	  for d: Nat
165	  for ha: {D.full(T, a, d) == True{} : Bool}
166	  for hb: {D.full(T, b, d) == True{} : Bool}
167	  for h: {D.view(T, a) == D.view(T, b) : List<&2, T>}
168	  {a == b : Array<T>}
169	
170	# Array.get as a literal pair (so code that destructures it can be rewritten).
171	law get_pair:
172	  for -T: Data
173	  for a: Array<T>
174	  for i: U32
175	  {Array.get(T, a, i) == (a, Pair.snd(Array<T>, T, Array.get(T, a, i))) : Array<T> & T}
176	
177	law size_pair:
178	  for -T: Data
179	  for a: Array<T>
180	  for d: Nat
181	  for hf: {D.full(T, a, d) == True{} : Bool}
182	  {Array.size(T, a) == (a, U32.shln(1, d)) : Array<T> & U32}
183	
184	# A new array reads as its initial value everywhere (every depth, every index).
185	law get_new:
186	  for -T: Data
187	  for d: Nat
188	  for v: T
189	  for i: U32
190	  {Pair.snd(Array<T>, T, Array.get(T, Array.new(T, d, v), i)) == v : T}
191	
192	law slot_lt:
193	  for i: U32
194	  for d: Nat
195	  {Nat.is_lt(D.slot(i, d), Nat.pow(2n, d)) == True{} : Bool}
196	
197	law slot_small:
198	  for i: U32
199	  for d: Nat
200	  for h: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, d)) == True{} : Bool}
201	  {D.slot(i, d) == U32.to_nat(i) : Nat}
202	
203	# ==========================================================================
204	# Cloning
205	# ==========================================================================
206	
207	# Array.clone gives two arrays equal to the original.
208	law clone_pair:
209	  for -T: Data
210	  for a: Array<T>
211	  {Array.clone(T, a) == (a, a) : Array<T> & Array<T>}