spec/containers/doubly_linked_list.bend
bend-collections-laws-containers@1.0.0.0 · 615 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-containers@1.0.0.0/src/containers/types/doubly_linked_list.bend as E
4import bend-collections-laws-containers@1.0.0.0/spec/lib/sequence.bend as V
5
6# Independent model of the doubly linked list with generational handles.
7#
8# A list is its elements' ids in order, and for every id ever issued its value
9# (None once removed) and its generation. Removed ids are kept on a stack and
10# reissued last-removed first; an id whose generation reached 2^32 - 1 is
11# retired instead (never reissued). A new id, when none is free, is the next
12# one, at generation 0. A handle names the list's tag, an id and a
13# generation: it is foreign when the tag differs, and stale when its id is
14# not live or its generation is not the id's current one.
15#
16# Nothing here refers to the arenas, links or free chain of the
17# implementation.
18
19type DS<-T: Data> is Data:
20 DS{tag: U32, order: List<&2, Nat>, vals: List<&2, Maybe<&2, T>>, gens: List<&2, U32>, free: List<&2, Nat>}
21
22def pick_list(+b: Bool, xs: List<&2, Nat>, ys: List<&2, Nat>) -> List<&2, Nat>:
23 match b:
24 case True{}:
25 xs
26 case False{}:
27 ys
28
29def pick_maybe(+b: Bool, x: Maybe<&2, Nat>, y: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
30 match b:
31 case True{}:
32 x
33 case False{}:
34 y
35
36def cons_some(-T: Data, m: Maybe<&2, T>, xs: List<&2, T>) -> List<&2, T>:
37 match m:
38 case None{}:
39 xs
40 case Some{v}:
41 Con{v, xs}
42
43def maybe_done(-T: Data, e: E.Error, m: Maybe<&2, T>) -> Result<&2, &2, E.Error, T>:
44 match m:
45 case None{}:
46 Fail{e}
47 case Some{v}:
48 Done{v}
49
50def gen_of(+gens: List<&2, U32>, +i: Nat) -> U32:
51 match gens i:
52 case Nil{} _:
53 0
54 case Con{g, t} 0n:
55 g
56 case Con{g, t} 1n+p:
57 gen_of(t, p)
58
59def val_of(-T: Data, +vals: List<&2, Maybe<&2, T>>, +i: Nat) -> Maybe<&2, T>:
60 match vals i:
61 case Nil{} _:
62 None{}
63 case Con{v, t} 0n:
64 v
65 case Con{v, t} 1n+p:
66 val_of(T, t, p)
67
68def handle(+tag: U32, +gens: List<&2, U32>, +i: Nat) -> E.Handle:
69 E.H{tag, U32.from_nat(i), gen_of(gens, i)}
70
71# ---- validity ----
72
73def live_gen(-T: Data, m: Maybe<&2, T>, +same: Bool) -> Maybe<&2, E.Error>:
74 match m same:
75 case None{} _:
76 Some{E.StaleHandle{}}
77 case Some{v} True{}:
78 None{}
79 case Some{v} False{}:
80 Some{E.StaleHandle{}}
81
82def valid_own(-T: Data, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +i: Nat, +g: U32, mine: Bool) -> Maybe<&2, E.Error>:
83 match mine:
84 case False{}:
85 Some{E.ForeignHandle{}}
86 case True{}:
87 live_gen(T, val_of(T, vals, i), U32.is_eq(gen_of(gens, i), g))
88
89# None when h names a live element of the list at its current generation
90def validate(-T: Data, +s: DS<T>, +h: E.Handle) -> Maybe<&2, E.Error>:
91 match s h:
92 case DS{+tag, +order, +vals, +gens, +free} E.H{+owner, +id, +g}:
93 valid_own(T, vals, gens, U32.to_nat(id), g, U32.is_eq(owner, tag))
94
95# ---- positions in the order ----
96
97def ins_before(xs: List<&2, Nat>, +i: Nat, +n: Nat) -> List<&2, Nat>:
98 match xs:
99 case Nil{}:
100 Nil{}
101 case Con{+x, +t}:
102 pick_list(Nat.is_eq(x, i), Con{n, Con{x, t}}, Con{x, ins_before(t, i, n)})
103
104def ins_after(xs: List<&2, Nat>, +i: Nat, +n: Nat) -> List<&2, Nat>:
105 match xs:
106 case Nil{}:
107 Nil{}
108 case Con{+x, +t}:
109 pick_list(Nat.is_eq(x, i), Con{x, Con{n, t}}, Con{x, ins_after(t, i, n)})
110
111def delete(xs: List<&2, Nat>, +i: Nat) -> List<&2, Nat>:
112 match xs:
113 case Nil{}:
114 Nil{}
115 case Con{+x, +t}:
116 pick_list(Nat.is_eq(x, i), t, Con{x, delete(t, i)})
117
118def first(xs: List<&2, Nat>) -> Maybe<&2, Nat>:
119 match xs:
120 case Nil{}:
121 None{}
122 case Con{x, t}:
123 Some{x}
124
125# the element after i
126def after(xs: List<&2, Nat>, +i: Nat) -> Maybe<&2, Nat>:
127 match xs:
128 case Nil{}:
129 None{}
130 case Con{+x, +t}:
131 pick_maybe(Nat.is_eq(x, i), first(t), after(t, i))
132
133# the element before i (p: the element before the list)
134def before(xs: List<&2, Nat>, +i: Nat, p: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
135 match xs:
136 case Nil{}:
137 None{}
138 case Con{+x, +t}:
139 pick_maybe(Nat.is_eq(x, i), p, before(t, i, Some{x}))
140
141def values(-T: Data, +vals: List<&2, Maybe<&2, T>>, xs: List<&2, Nat>) -> List<&2, T>:
142 match xs:
143 case Nil{}:
144 Nil{}
145 case Con{+x, +t}:
146 cons_some(T, val_of(T, vals, x), values(T, vals, t))
147
148# ---- issuing an id ----
149
150# the id a new element takes, the list with the id reserved
151def alloc(-T: Data, s: DS<T>) -> DS<T> & Nat:
152 match s:
153 case DS{+tag, +order, +vals, +gens, free}:
154 match free:
155 case Con{+i, rest}:
156 (DS{tag, order, vals, gens, rest}, i)
157 case Nil{}:
158 (DS{tag, order, C.snoc(Maybe<&2, T>, vals, None{}), C.snoc(U32, gens, 0), Nil{}}, C.length(Maybe<&2, T>, vals))
159
160# where a new element goes
161type Pos is Data:
162 PFront{}
163 PBack{}
164 PBefore{i: Nat}
165 PAfter{i: Nat}
166
167def place_order(pos: Pos, xs: List<&2, Nat>, +n: Nat) -> List<&2, Nat>:
168 match pos:
169 case PFront{}:
170 Con{n, xs}
171 case PBack{}:
172 C.snoc(Nat, xs, n)
173 case PBefore{+i}:
174 ins_before(xs, i, n)
175 case PAfter{+i}:
176 ins_after(xs, i, n)
177
178# store x at the reserved id n and place n in the order
179def place(-T: Data, s: DS<T>, +n: Nat, x: T, pos: Pos) -> DS<T> & E.Handle:
180 match s:
181 case DS{+tag, order, +vals, +gens, free}:
182 (DS{tag, place_order(pos, order, n), C.update(Maybe<&2, T>, vals, n, Some{x}), gens, free}, handle(tag, gens, n))
183
184def inserted(-T: Data, r: DS<T> & Nat, x: T, pos: Pos) -> DS<T> & E.Handle:
185 match r:
186 case Tuple{s, +n}:
187 place(T, s, n, x, pos)
188
189def push_front(-T: Data, s: DS<T>, x: T) -> DS<T> & E.Handle:
190 inserted(T, alloc(T, s), x, PFront{})
191
192def push_back(-T: Data, s: DS<T>, x: T) -> DS<T> & E.Handle:
193 inserted(T, alloc(T, s), x, PBack{})
194
195# ---- removal ----
196
197def retire(+gens: List<&2, U32>, +i: Nat, +free: List<&2, Nat>, +g: U32, exhausted: Bool) -> List<&2, U32> & List<&2, Nat>:
198 match exhausted:
199 case True{}:
200 (gens, free)
201 case False{}:
202 (C.update(U32, gens, i, U32.inc(g)), Con{i, free})
203
204def removed(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +i: Nat, +v: T, r: List<&2, U32> & List<&2, Nat>) -> DS<T> & E.Obs<T>:
205 match r:
206 case Tuple{gens, free}:
207 (DS{tag, delete(order, i), C.update(Maybe<&2, T>, vals, i, None{}), gens, free}, E.OVal{Done{v}})
208
209def remove_m(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +i: Nat, m: Maybe<&2, T>) -> DS<T> & E.Obs<T>:
210 match m:
211 case Some{+v}:
212 removed(T, tag, order, vals, i, v, retire(gens, i, free, gen_of(gens, i), U32.is_eq(gen_of(gens, i), 4294967295)))
213 case None{}:
214 (DS{tag, order, vals, gens, free}, E.OVal{Fail{E.StaleHandle{}}})
215
216def remove_live(-T: Data, s: DS<T>, +i: Nat) -> DS<T> & E.Obs<T>:
217 match s:
218 case DS{+tag, +order, +vals, +gens, +free}:
219 remove_m(T, tag, order, vals, gens, free, i, val_of(T, vals, i))
220
221# ---- one operation on a valid handle ----
222
223def get_live(-T: Data, s: DS<T>, +i: Nat) -> DS<T> & E.Obs<T>:
224 match s:
225 case DS{+tag, +order, +vals, +gens, +free}:
226 (DS{tag, order, vals, gens, free}, E.OVal{maybe_done(T, E.StaleHandle{}, val_of(T, vals, i))})
227
228def set_live(-T: Data, s: DS<T>, +i: Nat, x: T) -> DS<T> & E.Obs<T>:
229 match s:
230 case DS{+tag, +order, +vals, +gens, +free}:
231 (DS{tag, order, C.update(Maybe<&2, T>, vals, i, Some{x}), gens, free}, E.OUnit{Done{Unit{}}})
232
233def nbr(+tag: U32, +gens: List<&2, U32>, m: Maybe<&2, Nat>) -> Maybe<&2, E.Handle>:
234 match m:
235 case None{}:
236 None{}
237 case Some{+j}:
238 Some{handle(tag, gens, j)}
239
240def next_live(-T: Data, s: DS<T>, +i: Nat) -> DS<T> & E.Obs<T>:
241 match s:
242 case DS{+tag, +order, +vals, +gens, +free}:
243 (DS{tag, order, vals, gens, free}, E.ONbr{Done{nbr(tag, gens, after(order, i))}})
244
245def prev_live(-T: Data, s: DS<T>, +i: Nat) -> DS<T> & E.Obs<T>:
246 match s:
247 case DS{+tag, +order, +vals, +gens, +free}:
248 (DS{tag, order, vals, gens, free}, E.ONbr{Done{nbr(tag, gens, before(order, i, None{}))}})
249
250def ins_obs(-T: Data, r: DS<T> & E.Handle) -> DS<T> & E.Obs<T>:
251 match r:
252 case Tuple{s, h}:
253 (s, E.OInsert{Done{h}})
254
255def live_op(-T: Data, s: DS<T>, +op: E.Op<T>, +i: Nat) -> DS<T> & E.Obs<T>:
256 match op:
257 case E.InsertBefore{h, x}:
258 ins_obs(T, inserted(T, alloc(T, s), x, PBefore{i}))
259 case E.InsertAfter{h, x}:
260 ins_obs(T, inserted(T, alloc(T, s), x, PAfter{i}))
261 case E.Remove{h}:
262 remove_live(T, s, i)
263 case E.Get{h}:
264 get_live(T, s, i)
265 case E.Set{h, x}:
266 set_live(T, s, i, x)
267 case E.Next{h}:
268 next_live(T, s, i)
269 case E.Prev{h}:
270 prev_live(T, s, i)
271 case E.Length{}:
272 (s, E.ONat{0n})
273 case E.PushFront{x}:
274 (s, E.ONat{0n})
275 case E.PushBack{x}:
276 (s, E.ONat{0n})
277 case E.ToList{}:
278 (s, E.ONat{0n})
279
280# the observation of op failing with e (the list is unchanged)
281def failed(-T: Data, op: E.Op<T>, e: E.Error) -> E.Obs<T>:
282 match op:
283 case E.InsertBefore{h, x}:
284 E.OInsert{Fail{e}}
285 case E.InsertAfter{h, x}:
286 E.OInsert{Fail{e}}
287 case E.Remove{h}:
288 E.OVal{Fail{e}}
289 case E.Get{h}:
290 E.OVal{Fail{e}}
291 case E.Set{h, x}:
292 E.OUnit{Fail{e}}
293 case E.Next{h}:
294 E.ONbr{Fail{e}}
295 case E.Prev{h}:
296 E.ONbr{Fail{e}}
297 case E.Length{}:
298 E.ONat{0n}
299 case E.PushFront{x}:
300 E.ONat{0n}
301 case E.PushBack{x}:
302 E.ONat{0n}
303 case E.ToList{}:
304 E.ONat{0n}
305
306def handle_id(+h: E.Handle) -> Nat:
307 match h:
308 case E.H{+owner, +id, +g}:
309 U32.to_nat(id)
310
311def checked(-T: Data, +s: DS<T>, +op: E.Op<T>, +h: E.Handle, m: Maybe<&2, E.Error>) -> DS<T> & E.Obs<T>:
312 match m:
313 case Some{e}:
314 (s, failed(T, op, e))
315 case None{}:
316 live_op(T, s, op, handle_id(h))
317
318def with_handle(-T: Data, +s: DS<T>, +op: E.Op<T>, +h: E.Handle) -> DS<T> & E.Obs<T>:
319 checked(T, s, op, h, validate(T, s, h))
320
321def len_of(-T: Data, s: DS<T>) -> Nat:
322 match s:
323 case DS{+tag, +order, +vals, +gens, +free}:
324 C.length(Nat, order)
325
326def list_of(-T: Data, s: DS<T>) -> List<&2, T>:
327 match s:
328 case DS{+tag, +order, +vals, +gens, +free}:
329 values(T, vals, order)
330
331def pushed(-T: Data, r: DS<T> & E.Handle) -> DS<T> & E.Obs<T>:
332 match r:
333 case Tuple{s, h}:
334 (s, E.OHandle{h})
335
336def step(-T: Data, +s: DS<T>, op: E.Op<T>) -> DS<T> & E.Obs<T>:
337 match op:
338 case E.Length{}:
339 (s, E.ONat{len_of(T, s)})
340 case E.PushFront{x}:
341 pushed(T, push_front(T, s, x))
342 case E.PushBack{x}:
343 pushed(T, push_back(T, s, x))
344 case E.InsertBefore{+h, +x}:
345 with_handle(T, s, E.InsertBefore{h, x}, h)
346 case E.InsertAfter{+h, +x}:
347 with_handle(T, s, E.InsertAfter{h, x}, h)
348 case E.Remove{+h}:
349 with_handle(T, s, E.Remove{h}, h)
350 case E.Get{+h}:
351 with_handle(T, s, E.Get{h}, h)
352 case E.Set{+h, +x}:
353 with_handle(T, s, E.Set{h, x}, h)
354 case E.Next{+h}:
355 with_handle(T, s, E.Next{h}, h)
356 case E.Prev{+h}:
357 with_handle(T, s, E.Prev{h}, h)
358 case E.ToList{}:
359 (s, E.OList{list_of(T, s)})
360
361def empty(-T: Data, +tag: U32) -> DS<T>:
362 DS{tag, Nil{}, Nil{}, Nil{}, Nil{}}
363
364def cons_obs(-T: Data, o: E.Obs<T>, r: DS<T> & List<&2, E.Obs<T>>) -> DS<T> & List<&2, E.Obs<T>>:
365 match r:
366 case Tuple{m, os}:
367 (m, Con{o, os})
368
369def run(-T: Data, ops: List<&2, E.Op<T>>, +s: DS<T>) -> DS<T> & List<&2, E.Obs<T>>:
370 match ops:
371 case Nil{}:
372 (s, Nil{})
373 case Con{+op, rest}:
374 cons_obs(T, Pair.snd(DS<T>, E.Obs<T>, step(T, s, op)), run(T, rest, Pair.fst(DS<T>, E.Obs<T>, step(T, s, op))))
375
376# ---- contract (SPARK formal containers) ----
377# Each `<Subprogram>.<clause>` definition below states one Post clause of
378# that SPARK subprogram, as a proposition on this model; the table names the
379# clauses. proofs/containers/doubly_linked_list/ proves every clause under its clause name,
380# and its `impl` lemma carries them to the implementation.
381#
382# Contracts of the doubly linked list in the style of SPARK's formal doubly
383# linked lists (SPARKlib src/spark-containers-formal-doubly_linked_lists.ads,
384# AdaCore/SPARKlib 46ec319; model predicates in spec/lib/sequence.bend).
385# SPARK's cursors are our handles; Has_Element (Container, Position) is
386# S.validate (s, h) = None; Positions is the order (the ids of the live
387# elements, first to last: a handle's position is the index of its id);
388# Model is S.list_of (the values along the order). Position clauses are
389# stated on the order, split at the handle's id: order = a ++ [id] ++ b
390# with id not in a (fsplit), so Position (h) = Length (a). A valid handle's
391# id is in the order in every good list (doubly_linked_list/hlive.src,
392# mem_of), which is the premise of fsplit. Each lemma is one Post clause of
393# step; `impl` (via P.step_ok) carries every clause to the implementation.
394#
395# SPARK subprogram (.ads line) ours clauses
396# Length (78) length length_result, length_frame
397# Empty_List (71) new new_empty
398# Has_Element (1814) validate has_element (definition), valid_live
399# Element (419) get get_frame, get_element
400# Replace_Element (430) set set_positions, set_element, set_others, set_gens
401# Prepend (836) push_front push_front_positions, push_front_first, push_front_length
402# Append (905) push_back push_back_positions, push_back_last, push_back_length
403# Insert Before (523) insert_before insert_before_equal, insert_before_at,
404# insert_before_shifted, insert_before_length
405# Insert after (Next (Before)) insert_after insert_after_equal, insert_after_at,
406# insert_after_shifted, insert_after_length
407# Delete (978) remove remove_equal, remove_shifted, remove_length,
408# remove_result, remove_stale
409# Next (1614) next next_result, next_position, next_frame
410# Previous (1652) prev prev_result, prev_first, prev_position, prev_frame
411# iteration (Iter_Model) to_list to_list_model, to_list_frame
412# implementation D.step impl
413# Not in this API: "=", Is_Empty, Clear, Assign/Copy/Move, Reference,
414# Insert with Count, Delete with Count, Delete_First/Delete_Last,
415# First/First_Element/Last/Last_Element (the ends are reached by the
416# handles push returns), Reverse_Elements, Swap, Swap_Links, Splice, Find,
417# Reverse_Find, Contains. SPARK's Pre (Has_Element) is a defensive check:
418# a foreign or stale handle returns ForeignHandle / StaleHandle and changes
419# nothing (the refinement proof's failed case).
420
421def nx(-T: Data, +s: DS<T>, +op: E.Op<T>) -> DS<T>:
422 Pair.fst(DS<T>, E.Obs<T>, step(T, s, op))
423
424def ob(-T: Data, +s: DS<T>, +op: E.Op<T>) -> E.Obs<T>:
425 Pair.snd(DS<T>, E.Obs<T>, step(T, s, op))
426
427def ord(-T: Data, s: DS<T>) -> List<&2, Nat>:
428 match s:
429 case DS{tag, order, vals, gens, free}:
430 order
431
432def vls(-T: Data, s: DS<T>) -> List<&2, Maybe<&2, T>>:
433 match s:
434 case DS{tag, order, vals, gens, free}:
435 vals
436
437def gns(-T: Data, s: DS<T>) -> List<&2, U32>:
438 match s:
439 case DS{tag, order, vals, gens, free}:
440 gens
441
442# Has_Element (Container, Position)
443def has_of(m: Maybe<&2, E.Error>) -> Bool:
444 match m:
445 case None{}:
446 True{}
447 case Some{e}:
448 False{}
449
450def has_element(-T: Data, +s: DS<T>, +h: E.Handle) -> Bool:
451 has_of(validate(T, s, h))
452
453# Previous: the last element of a, or p when a is empty
454def lastm(xs: List<&2, Nat>, p: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
455 match xs:
456 case Nil{}:
457 p
458 case Con{+x, t}:
459 lastm(t, Some{x})
460
461# ---- the order split at a live id ----
462def FSplit(+i: Nat, +xs: List<&2, Nat>) -> Type:
463 Sigma<&1, &1, List<&2, Nat>, a => Sigma<&1, &1, List<&2, Nat>, b => {xs == C.append(Nat, a, Con{i, b}) : List<&2, Nat>} & {C.memn(i, a) == False{} : Bool}>>
464
465# Next (1614)
466def Next.next_position(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>) -> Type:
467 {C.nth(Nat, C.append(Nat, a, Con{i, b}), 1n+C.length(Nat, a)) == first(b) : Maybe<&2, Nat>}
468
469# Previous (1652)
470def Previous.prev_position(+t: List<&2, Nat>, +x: Nat, +i: Nat, +b: List<&2, Nat>, +p: Maybe<&2, Nat>) -> Type:
471 {lastm(Con{x, t}, p) == C.nth(Nat, C.append(Nat, Con{x, t}, Con{i, b}), C.length(Nat, t)) : Maybe<&2, Nat>}
472
473# Has_Element (1814)
474def Has_Element.valid_live(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
475 Sigma<&1, &1, T, v => {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}>
476
477# Length (78)
478def Length.length_result(-T: Data, +s: DS<T>) -> Type:
479 {ob(T, s, E.Length{}) == E.ONat{len_of(T, s)} : E.Obs<T>}
480
481# Length (78)
482def Length.length_frame(-T: Data, +s: DS<T>) -> Type:
483 {nx(T, s, E.Length{}) == s : DS<T>}
484
485# iteration (Iter_Model)
486def Iteration.to_list_model(-T: Data, +s: DS<T>) -> Type:
487 {ob(T, s, E.ToList{}) == E.OList{list_of(T, s)} : E.Obs<T>}
488
489# iteration (Iter_Model)
490def Iteration.to_list_frame(-T: Data, +s: DS<T>) -> Type:
491 {nx(T, s, E.ToList{}) == s : DS<T>}
492
493# Empty_List (71)
494def Empty_List.new_empty(-T: Data, +tag: U32) -> Type:
495 {len_of(T, empty(T, tag)) == 0n : Nat}
496
497# Element (419)
498def Element.get_frame(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
499 {nx(T, DS{tag, order, vals, gens, free}, E.Get{h}) == DS{tag, order, vals, gens, free} : DS<T>}
500
501# Element (419)
502def Element.get_element(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
503 {ob(T, DS{tag, order, vals, gens, free}, E.Get{h}) == E.OVal{Done{v}} : E.Obs<T>}
504
505# Replace_Element (430)
506def Replace_Element.set_positions(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
507 {ord(T, nx(T, DS{tag, order, vals, gens, free}, E.Set{h, x})) == order : List<&2, Nat>}
508
509# Replace_Element (430)
510def Replace_Element.set_gens(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
511 {gns(T, nx(T, DS{tag, order, vals, gens, free}, E.Set{h, x})) == gens : List<&2, U32>}
512
513# Replace_Element (430)
514def Replace_Element.set_element(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
515 {val_of(T, vls(T, nx(T, DS{tag, order, vals, gens, free}, E.Set{h, x})), handle_id(h)) == Some{x} : Maybe<&2, T>}
516
517# Replace_Element (430)
518def Replace_Element.set_others(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +j: Nat, +ne: {Nat.is_eq(handle_id(h), j) == False{} : Bool}) -> Type:
519 {val_of(T, vls(T, nx(T, DS{tag, order, vals, gens, free}, E.Set{h, x})), j) == val_of(T, vals, j) : Maybe<&2, T>}
520
521# Prepend (836)
522def Prepend.push_front_positions(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> Type:
523 V.RangeShifted(Nat, order, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushFront{x})), 0n, C.length(Nat, order), 1n)
524
525# Prepend (836)
526def Prepend.push_front_first(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> Type:
527 {C.nth(Nat, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushFront{x})), 0n) == Some{Pair.snd(DS<T>, Nat, alloc(T, DS{tag, order, vals, gens, free}))} : Maybe<&2, Nat>}
528
529# Prepend (836)
530def Prepend.push_front_length(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> Type:
531 {C.length(Nat, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushFront{x}))) == 1n+C.length(Nat, order) : Nat}
532
533# Append (905)
534def Append.push_back_positions(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> Type:
535 V.EqualPrefix(Nat, order, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushBack{x})))
536
537# Append (905)
538def Append.push_back_last(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> Type:
539 {C.nth(Nat, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushBack{x})), C.length(Nat, order)) == Some{Pair.snd(DS<T>, Nat, alloc(T, DS{tag, order, vals, gens, free}))} : Maybe<&2, Nat>}
540
541# Append (905)
542def Append.push_back_length(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> Type:
543 {C.length(Nat, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushBack{x}))) == 1n+C.length(Nat, order) : Nat}
544
545# Insert Before (523)
546def Insert.insert_before_equal(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
547 V.RangeEqual(Nat, C.append(Nat, a, Con{handle_id(h), b}), ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), 0n, C.length(Nat, a))
548
549# Insert Before (523)
550def Insert.insert_before_at(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
551 {C.nth(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), C.length(Nat, a)) == Some{Pair.snd(DS<T>, Nat, alloc(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}))} : Maybe<&2, Nat>}
552
553# Insert Before (523)
554def Insert.insert_before_shifted(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
555 V.RangeShifted(Nat, C.append(Nat, a, Con{handle_id(h), b}), ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), C.length(Nat, a), C.length(Nat, C.append(Nat, a, Con{handle_id(h), b})), 1n)
556
557# Insert Before (523)
558def Insert.insert_before_length(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
559 {C.length(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x}))) == 1n+C.length(Nat, C.append(Nat, a, Con{handle_id(h), b})) : Nat}
560
561# Insert after (Next (Before))
562def Insert.insert_after_equal(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
563 V.RangeEqual(Nat, C.append(Nat, a, Con{handle_id(h), b}), ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), 0n, 1n+C.length(Nat, a))
564
565# Insert after (Next (Before))
566def Insert.insert_after_at(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
567 {C.nth(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), 1n+C.length(Nat, a)) == Some{Pair.snd(DS<T>, Nat, alloc(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}))} : Maybe<&2, Nat>}
568
569# Insert after (Next (Before))
570def Insert.insert_after_shifted(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
571 V.RangeShifted(Nat, C.append(Nat, a, Con{handle_id(h), b}), ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), 1n+C.length(Nat, a), C.length(Nat, C.append(Nat, a, Con{handle_id(h), b})), 1n)
572
573# Insert after (Next (Before))
574def Insert.insert_after_length(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
575 {C.length(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x}))) == 1n+C.length(Nat, C.append(Nat, a, Con{handle_id(h), b})) : Nat}
576
577# Delete (978)
578def Delete.remove_result(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
579 {ob(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Remove{h}) == E.OVal{Done{v}} : E.Obs<T>}
580
581# Delete (978)
582def Delete.remove_equal(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
583 V.RangeEqual(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Remove{h})), C.append(Nat, a, Con{handle_id(h), b}), 0n, C.length(Nat, a))
584
585# Delete (978)
586def Delete.remove_shifted(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
587 V.RangeShifted(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Remove{h})), C.append(Nat, a, Con{handle_id(h), b}), C.length(Nat, a), C.length(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Remove{h}))), 1n)
588
589# Delete (978)
590def Delete.remove_length(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
591 {C.length(Nat, C.append(Nat, a, Con{handle_id(h), b})) == 1n+C.length(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Remove{h}))) : Nat}
592
593# Delete (978)
594def Delete.remove_stale(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
595 {has_element(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Remove{h}), h) == False{} : Bool}
596
597# Next (1614)
598def Next.next_result(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
599 {ob(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Next{h}) == E.ONbr{Done{nbr(tag, gens, first(b))}} : E.Obs<T>}
600
601# Next (1614)
602def Next.next_frame(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
603 {nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Next{h}) == DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free} : DS<T>}
604
605# Previous (1652)
606def Previous.prev_result(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
607 {ob(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Prev{h}) == E.ONbr{Done{nbr(tag, gens, lastm(a, None{}))}} : E.Obs<T>}
608
609# Previous (1652)
610def Previous.prev_first(-T: Data, +tag: U32, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, Con{handle_id(h), b}, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
611 {ob(T, DS{tag, Con{handle_id(h), b}, vals, gens, free}, E.Prev{h}) == E.ONbr{Done{None{}}} : E.Obs<T>}
612
613# Previous (1652)
614def Previous.prev_frame(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
615 {nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Prev{h}) == DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free} : DS<T>}