1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/list.bend as LL
5	import ../../../spec/lib/common.bend as SC
6	
7	# Slot layout of a dynamic array: the first n slots are Some, the rest None.
8	
9	def somes(-T: Data, xs: List<&2, Maybe<&2, T>>) -> List<&2, T>:
10	  match xs:
11	    case Nil{}:
12	      Nil{}
13	    case Con{None{}, r}:
14	      somes(T, r)
15	    case Con{Some{x}, r}:
16	      Con{x, somes(T, r)}
17	
18	def nones(-T: Data, xs: List<&2, Maybe<&2, T>>) -> Bool:
19	  match xs:
20	    case Nil{}:
21	      True{}
22	    case Con{None{}, r}:
23	      nones(T, r)
24	    case Con{Some{x}, r}:
25	      False{}
26	
27	def lay(-T: Data, xs: List<&2, Maybe<&2, T>>, n: Nat) -> Bool:
28	  match xs n:
29	    case Nil{} 0n:
30	      True{}
31	    case Nil{} 1n+m:
32	      False{}
33	    case Con{None{}, r} 0n:
34	      nones(T, r)
35	    case Con{None{}, r} 1n+m:
36	      False{}
37	    case Con{Some{x}, r} 0n:
38	      False{}
39	    case Con{Some{x}, r} 1n+m:
40	      lay(T, r, m)
41	
42	def nones_somes(-T: Data, +xs: List<&2, Maybe<&2, T>>, +h: {nones(T, xs) == True{} : Bool}) -> {somes(T, xs) == Nil{} : List<&2, T>}:
43	  match xs:
44	    case Nil{}:
45	      {==}
46	    case Con{None{}, +r}:
47	      nones_somes(T, r, h)
48	    case Con{Some{x}, r}:
49	      Empty.absurd({Con{x, somes(T, r)} == Nil{} : List<&2, T>}, L.false_true(h))
50	
51	def lay_len(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +h: {lay(T, xs, n) == True{} : Bool}) -> {SC.length(T, somes(T, xs)) == n : Nat}:
52	  match xs n:
53	    case Nil{} 0n:
54	      {==}
55	    case Nil{} 1n+m:
56	      Empty.absurd({0n == 1n+m : Nat}, L.false_true(h))
57	    case Con{None{}, +r} 0n:
58	      %Equal.sym(List<&2, T>, somes(T, r), Nil{}, nones_somes(T, r, h)) : {SC.length(T, _) == 0n : Nat}
59	      {==}
60	    case Con{None{}, r} 1n+m:
61	      Empty.absurd({SC.length(T, somes(T, r)) == 1n+m : Nat}, L.false_true(h))
62	    case Con{Some{x}, r} 0n:
63	      Empty.absurd({1n+SC.length(T, somes(T, r)) == 0n : Nat}, L.false_true(h))
64	    case Con{Some{x}, +r} 1n+m:
65	      N.succ_cong(SC.length(T, somes(T, r)), m, lay_len(T, r, m, h))
66	
67	def lay_le(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +h: {lay(T, xs, n) == True{} : Bool}) -> {Nat.is_le(n, SC.length(Maybe<&2, T>, xs)) == True{} : Bool}:
68	  match xs n:
69	    case Nil{} 0n:
70	      {==}
71	    case Nil{} 1n+m:
72	      Empty.absurd({Nat.is_le(1n+m, 0n) == True{} : Bool}, L.false_true(h))
73	    case Con{None{}, r} 0n:
74	      {==}
75	    case Con{None{}, r} 1n+m:
76	      Empty.absurd({Nat.is_le(1n+m, 1n+SC.length(Maybe<&2, T>, r)) == True{} : Bool}, L.false_true(h))
77	    case Con{Some{x}, r} 0n:
78	      {==}
79	    case Con{Some{x}, +r} 1n+m:
80	      lay_le(T, r, m, h)
81	
82	def lay_nil_pos(-T: Data, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {lay(T, Nil{}, n) == False{} : Bool}:
83	  match n:
84	    case 0n:
85	      Empty.absurd({True{} == False{} : Bool}, N.lt_zero_absurd(i, hi))
86	    case 1n+m:
87	      {==}
88	
89	# Slot i (< n) holds exactly the i-th item.
90	def lay_nth(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +i: Nat, +h: {lay(T, xs, n) == True{} : Bool}, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {SC.nth(Maybe<&2, T>, xs, i) == Some{SC.nth(T, somes(T, xs), i)} : Maybe<&2, Maybe<&2, T>>}:
91	  match xs n i:
92	    case Nil{} _ _:
93	      Empty.absurd({None{} == Some{None{}} : Maybe<&2, Maybe<&2, T>>}, L.true_not_false(lay(T, Nil{}, n), h, lay_nil_pos(T, n, i, hi)))
94	    case Con{None{}, r} 0n _:
95	      Empty.absurd({SC.nth(Maybe<&2, T>, Con{None{}, r}, i) == Some{SC.nth(T, somes(T, r), i)} : Maybe<&2, Maybe<&2, T>>}, N.lt_zero_absurd(i, hi))
96	    case Con{None{}, r} 1n+m _:
97	      Empty.absurd({SC.nth(Maybe<&2, T>, Con{None{}, r}, i) == Some{SC.nth(T, somes(T, r), i)} : Maybe<&2, Maybe<&2, T>>}, L.false_true(h))
98	    case Con{Some{x}, r} 0n _:
99	      Empty.absurd({SC.nth(Maybe<&2, T>, Con{Some{x}, r}, i) == Some{SC.nth(T, Con{x, somes(T, r)}, i)} : Maybe<&2, Maybe<&2, T>>}, L.false_true(h))
100	    case Con{Some{x}, r} 1n+m 0n:
101	      {==}
102	    case Con{Some{x}, +r} 1n+m 1n+j:
103	      lay_nth(T, r, m, j, h, hi)
104	
105	def nones_nth(-T: Data, +xs: List<&2, Maybe<&2, T>>, +i: Nat, +h: {nones(T, xs) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.length(Maybe<&2, T>, xs)) == True{} : Bool}) -> {SC.nth(Maybe<&2, T>, xs, i) == Some{None{}} : Maybe<&2, Maybe<&2, T>>}:
106	  match xs i:
107	    case Nil{} _:
108	      Empty.absurd({None{} == Some{None{}} : Maybe<&2, Maybe<&2, T>>}, N.lt_zero_absurd(i, hi))
109	    case Con{None{}, r} 0n:
110	      {==}
111	    case Con{None{}, +r} 1n+j:
112	      nones_nth(T, r, j, h, hi)
113	    case Con{Some{x}, r} _:
114	      Empty.absurd({SC.nth(Maybe<&2, T>, Con{Some{x}, r}, i) == Some{None{}} : Maybe<&2, Maybe<&2, T>>}, L.false_true(h))
115	
116	def nones_rep(-T: Data, +k: Nat) -> {nones(T, SC.replicate(Maybe<&2, T>, k, None{})) == True{} : Bool}:
117	  match k:
118	    case 0n:
119	      {==}
120	    case 1n+j:
121	      nones_rep(T, j)
122	
123	def somes_rep(-T: Data, +k: Nat) -> {somes(T, SC.replicate(Maybe<&2, T>, k, None{})) == Nil{} : List<&2, T>}:
124	  match k:
125	    case 0n:
126	      {==}
127	    case 1n+j:
128	      somes_rep(T, j)
129	
130	def lay_rep(-T: Data, +k: Nat) -> {lay(T, SC.replicate(Maybe<&2, T>, k, None{}), 0n) == True{} : Bool}:
131	  match k:
132	    case 0n:
133	      {==}
134	    case 1n+j:
135	      nones_rep(T, j)
136	
137	def nones_lay0(-T: Data, +xs: List<&2, Maybe<&2, T>>, +h: {nones(T, xs) == True{} : Bool}) -> {lay(T, xs, 0n) == True{} : Bool}:
138	  match xs:
139	    case Nil{}:
140	      {==}
141	    case Con{None{}, r}:
142	      h
143	    case Con{Some{x}, r}:
144	      h
145	
146	def lay0_nones(-T: Data, +xs: List<&2, Maybe<&2, T>>, +h: {lay(T, xs, 0n) == True{} : Bool}) -> {nones(T, xs) == True{} : Bool}:
147	  match xs:
148	    case Nil{}:
149	      {==}
150	    case Con{None{}, r}:
151	      h
152	    case Con{Some{x}, r}:
153	      h
154	
155	def nones_append(-T: Data, +xs: List<&2, Maybe<&2, T>>, +ys: List<&2, Maybe<&2, T>>, +hx: {nones(T, xs) == True{} : Bool}, +hy: {nones(T, ys) == True{} : Bool}) -> {nones(T, SC.append(Maybe<&2, T>, xs, ys)) == True{} : Bool}:
156	  match xs:
157	    case Nil{}:
158	      hy
159	    case Con{None{}, +r}:
160	      nones_append(T, r, ys, hx, hy)
161	    case Con{Some{x}, r}:
162	      hx
163	
164	# ---- set ----
165	
166	def lay_set(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +i: Nat, +v: T, +h: {lay(T, xs, n) == True{} : Bool}, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {lay(T, SC.update(Maybe<&2, T>, xs, i, Some{v}), n) == True{} : Bool}:
167	  match xs n i:
168	    case Nil{} _ _:
169	      Empty.absurd({lay(T, Nil{}, n) == True{} : Bool}, L.true_not_false(lay(T, Nil{}, n), h, lay_nil_pos(T, n, i, hi)))
170	    case Con{None{}, r} 0n _:
171	      Empty.absurd({lay(T, SC.update(Maybe<&2, T>, Con{None{}, r}, i, Some{v}), 0n) == True{} : Bool}, N.lt_zero_absurd(i, hi))
172	    case Con{None{}, r} 1n+m _:
173	      Empty.absurd({lay(T, SC.update(Maybe<&2, T>, Con{None{}, r}, i, Some{v}), 1n+m) == True{} : Bool}, L.false_true(h))
174	    case Con{Some{x}, r} 0n _:
175	      Empty.absurd({lay(T, SC.update(Maybe<&2, T>, Con{Some{x}, r}, i, Some{v}), 0n) == True{} : Bool}, L.false_true(h))
176	    case Con{Some{x}, r} 1n+m 0n:
177	      h
178	    case Con{Some{x}, +r} 1n+m 1n+j:
179	      lay_set(T, r, m, j, v, h, hi)
180	
181	def somes_set(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +i: Nat, +v: T, +h: {lay(T, xs, n) == True{} : Bool}, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {somes(T, SC.update(Maybe<&2, T>, xs, i, Some{v})) == SC.update(T, somes(T, xs), i, v) : List<&2, T>}:
182	  match xs n i:
183	    case Nil{} _ _:
184	      Empty.absurd({Nil{} == Nil{} : List<&2, T>}, L.true_not_false(lay(T, Nil{}, n), h, lay_nil_pos(T, n, i, hi)))
185	    case Con{None{}, r} 0n _:
186	      Empty.absurd({somes(T, SC.update(Maybe<&2, T>, Con{None{}, r}, i, Some{v})) == SC.update(T, somes(T, r), i, v) : List<&2, T>}, N.lt_zero_absurd(i, hi))
187	    case Con{None{}, r} 1n+m _:
188	      Empty.absurd({somes(T, SC.update(Maybe<&2, T>, Con{None{}, r}, i, Some{v})) == SC.update(T, somes(T, r), i, v) : List<&2, T>}, L.false_true(h))
189	    case Con{Some{x}, r} 0n _:
190	      Empty.absurd({somes(T, SC.update(Maybe<&2, T>, Con{Some{x}, r}, i, Some{v})) == SC.update(T, Con{x, somes(T, r)}, i, v) : List<&2, T>}, L.false_true(h))
191	    case Con{Some{x}, r} 1n+m 0n:
192	      {==}
193	    case Con{Some{+x}, +r} 1n+m 1n+j:
194	      LL.cons_cong(T, x, somes(T, SC.update(Maybe<&2, T>, r, j, Some{v})), SC.update(T, somes(T, r), j, v), somes_set(T, r, m, j, v, h, hi))
195	
196	# ---- push (slot n is the first free one) ----
197	
198	def push_free(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +h: {lay(T, xs, n) == True{} : Bool}, +hn: {Nat.is_lt(n, SC.length(Maybe<&2, T>, xs)) == True{} : Bool}) -> {SC.nth(Maybe<&2, T>, xs, n) == Some{None{}} : Maybe<&2, Maybe<&2, T>>}:
199	  match xs n:
200	    case Nil{} _:
201	      Empty.absurd({None{} == Some{None{}} : Maybe<&2, Maybe<&2, T>>}, N.lt_zero_absurd(n, hn))
202	    case Con{None{}, r} 0n:
203	      {==}
204	    case Con{None{}, r} 1n+m:
205	      Empty.absurd({SC.nth(Maybe<&2, T>, r, m) == Some{None{}} : Maybe<&2, Maybe<&2, T>>}, L.false_true(h))
206	    case Con{Some{x}, r} 0n:
207	      Empty.absurd({Some{Some{x}} == Some{None{}} : Maybe<&2, Maybe<&2, T>>}, L.false_true(h))
208	    case Con{Some{x}, +r} 1n+m:
209	      push_free(T, r, m, h, hn)
210	
211	def lay_push(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +v: T, +h: {lay(T, xs, n) == True{} : Bool}, +hn: {Nat.is_lt(n, SC.length(Maybe<&2, T>, xs)) == True{} : Bool}) -> {lay(T, SC.update(Maybe<&2, T>, xs, n, Some{v}), 1n+n) == True{} : Bool}:
212	  match xs n:
213	    case Nil{} _:
214	      Empty.absurd({lay(T, Nil{}, 1n+n) == True{} : Bool}, N.lt_zero_absurd(n, hn))
215	    case Con{None{}, +r} 0n:
216	      nones_lay0(T, r, h)
217	    case Con{None{}, r} 1n+m:
218	      Empty.absurd({lay(T, Con{None{}, SC.update(Maybe<&2, T>, r, m, Some{v})}, 2n+m) == True{} : Bool}, L.false_true(h))
219	    case Con{Some{x}, r} 0n:
220	      Empty.absurd({lay(T, Con{Some{v}, r}, 1n) == True{} : Bool}, L.false_true(h))
221	    case Con{Some{x}, +r} 1n+m:
222	      lay_push(T, r, m, v, h, hn)
223	
224	def somes_push(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +v: T, +h: {lay(T, xs, n) == True{} : Bool}, +hn: {Nat.is_lt(n, SC.length(Maybe<&2, T>, xs)) == True{} : Bool}) -> {somes(T, SC.update(Maybe<&2, T>, xs, n, Some{v})) == SC.snoc(T, somes(T, xs), v) : List<&2, T>}:
225	  match xs n:
226	    case Nil{} _:
227	      Empty.absurd({Nil{} == Con{v, Nil{}} : List<&2, T>}, N.lt_zero_absurd(n, hn))
228	    case Con{None{}, +r} 0n:
229	      %Equal.sym(List<&2, T>, somes(T, r), Nil{}, nones_somes(T, r, h)) : {Con{v, _} == SC.snoc(T, _, v) : List<&2, T>}
230	      {==}
231	    case Con{None{}, r} 1n+m:
232	      Empty.absurd({somes(T, Con{None{}, SC.update(Maybe<&2, T>, r, m, Some{v})}) == SC.snoc(T, somes(T, r), v) : List<&2, T>}, L.false_true(h))
233	    case Con{Some{x}, r} 0n:
234	      Empty.absurd({Con{v, somes(T, r)} == SC.snoc(T, Con{x, somes(T, r)}, v) : List<&2, T>}, L.false_true(h))
235	    case Con{Some{+x}, +r} 1n+m:
236	      LL.cons_cong(T, x, somes(T, SC.update(Maybe<&2, T>, r, m, Some{v})), SC.snoc(T, somes(T, r), v), somes_push(T, r, m, v, h, hn))
237	
238	# ---- pop (slot m of a layout with m+1 items) ----
239	
240	def lay_pop(-T: Data, +xs: List<&2, Maybe<&2, T>>, +m: Nat, +h: {lay(T, xs, 1n+m) == True{} : Bool}) -> {lay(T, SC.update(Maybe<&2, T>, xs, m, None{}), m) == True{} : Bool}:
241	  match xs m:
242	    case Nil{} _:
243	      Empty.absurd({lay(T, Nil{}, m) == True{} : Bool}, L.false_true(h))
244	    case Con{None{}, r} _:
245	      Empty.absurd({lay(T, SC.update(Maybe<&2, T>, Con{None{}, r}, m, None{}), m) == True{} : Bool}, L.false_true(h))
246	    case Con{Some{x}, +r} 0n:
247	      lay0_nones(T, r, h)
248	    case Con{Some{x}, +r} 1n+k:
249	      lay_pop(T, r, k, h)
250	
251	def init_cons(-T: Data, +x: T, +ys: List<&2, T>, +k: Nat, +h: {SC.length(T, ys) == 1n+k : Nat}) -> {SC.init(T, Con{x, ys}) == Con{x, SC.init(T, ys)} : List<&2, T>}:
252	  match ys:
253	    case Nil{}:
254	      Empty.absurd({Nil{} == Con{x, Nil{}} : List<&2, T>}, N.zero_succ(k, h))
255	    case Con{y, t}:
256	      {==}
257	
258	def somes_pop(-T: Data, +xs: List<&2, Maybe<&2, T>>, +m: Nat, +h: {lay(T, xs, 1n+m) == True{} : Bool}) -> {somes(T, SC.update(Maybe<&2, T>, xs, m, None{})) == SC.init(T, somes(T, xs)) : List<&2, T>}:
259	  match xs m:
260	    case Nil{} _:
261	      Empty.absurd({Nil{} == Nil{} : List<&2, T>}, L.false_true(h))
262	    case Con{None{}, r} _:
263	      Empty.absurd({somes(T, SC.update(Maybe<&2, T>, Con{None{}, r}, m, None{})) == SC.init(T, somes(T, r)) : List<&2, T>}, L.false_true(h))
264	    case Con{Some{x}, +r} 0n:
265	      %Equal.sym(List<&2, T>, somes(T, r), Nil{}, nones_somes(T, r, lay0_nones(T, r, h))) : {_ == SC.init(T, Con{x, _}) : List<&2, T>}
266	      {==}
267	    case Con{Some{+x}, +r} 1n+k:
268	      Equal.trans(List<&2, T>, Con{x, somes(T, SC.update(Maybe<&2, T>, r, k, None{}))}, Con{x, SC.init(T, somes(T, r))}, SC.init(T, Con{x, somes(T, r)}),
269	        LL.cons_cong(T, x, somes(T, SC.update(Maybe<&2, T>, r, k, None{})), SC.init(T, somes(T, r)), somes_pop(T, r, k, h)),
270	        Equal.sym(List<&2, T>, SC.init(T, Con{x, somes(T, r)}), Con{x, SC.init(T, somes(T, r))}, init_cons(T, x, somes(T, r), k, lay_len(T, r, 1n+k, h))))
271	
272	# nth at the last position is last.
273	def nth_last(-T: Data, +ys: List<&2, T>, +m: Nat, +h: {SC.length(T, ys) == 1n+m : Nat}) -> {SC.nth(T, ys, m) == SC.last(T, ys) : Maybe<&2, T>}:
274	  match ys m:
275	    case Nil{} _:
276	      Empty.absurd({None{} == None{} : Maybe<&2, T>}, N.zero_succ(m, h))
277	    case Con{y, Nil{}} 0n:
278	      {==}
279	    case Con{y, Con{y2, t2}} 0n:
280	      Empty.absurd({Some{y} == SC.last(T, Con{y2, t2}) : Maybe<&2, T>}, N.succ_zero(SC.length(T, t2), N.succ_inj(1n+SC.length(T, t2), 0n, h)))
281	    case Con{y, Nil{}} 1n+k:
282	      Empty.absurd({SC.nth(T, Nil{}, k) == Some{y} : Maybe<&2, T>}, N.zero_succ(k, N.succ_inj(0n, 1n+k, h)))
283	    case Con{y, Con{+y2, +t2}} 1n+k:
284	      nth_last(T, Con{y2, t2}, k, N.succ_inj(1n+SC.length(T, t2), 1n+k, h))
285	
286	# ---- growth (append free slots) and clear ----
287	
288	def lay_grow(-T: Data, +xs: List<&2, Maybe<&2, T>>, +n: Nat, +k: Nat, +h: {lay(T, xs, n) == True{} : Bool}) -> {lay(T, SC.append(Maybe<&2, T>, xs, SC.replicate(Maybe<&2, T>, k, None{})), n) == True{} : Bool}:
289	  match xs n:
290	    case Nil{} 0n:
291	      lay_rep(T, k)
292	    case Nil{} 1n+m:
293	      Empty.absurd({lay(T, SC.replicate(Maybe<&2, T>, k, None{}), 1n+m) == True{} : Bool}, L.false_true(h))
294	    case Con{None{}, +r} 0n:
295	      nones_append(T, r, SC.replicate(Maybe<&2, T>, k, None{}), h, nones_rep(T, k))
296	    case Con{None{}, r} 1n+m:
297	      h
298	    case Con{Some{x}, r} 0n:
299	      h
300	    case Con{Some{x}, +r} 1n+m:
301	      lay_grow(T, r, m, k, h)
302	
303	def somes_grow(-T: Data, +xs: List<&2, Maybe<&2, T>>, +k: Nat) -> {somes(T, SC.append(Maybe<&2, T>, xs, SC.replicate(Maybe<&2, T>, k, None{}))) == somes(T, xs) : List<&2, T>}:
304	  match xs:
305	    case Nil{}:
306	      somes_rep(T, k)
307	    case Con{None{}, +r}:
308	      somes_grow(T, r, k)
309	    case Con{Some{+x}, +r}:
310	      LL.cons_cong(T, x, somes(T, SC.append(Maybe<&2, T>, r, SC.replicate(Maybe<&2, T>, k, None{}))), somes(T, r), somes_grow(T, r, k))