spec/containers/doubly_linked_list.bend source
spec/containers/doubly_linked_list.bend on the hub · documented module
import Baseimport ../lib/common.bend as Cimport ../../src/containers/types/doubly_linked_list.bend as Eimport ../lib/sequence.bend as V# Independent model of the doubly linked list with generational handles.## A list is its elements' ids in order, and for every id ever issued its value# (None once removed) and its generation. Removed ids are kept on a stack and# reissued last-removed first; an id whose generation reached 2^32 - 1 is# retired instead (never reissued). A new id, when none is free, is the next# one, at generation 0. A handle names the list's tag, an id and a# generation: it is foreign when the tag differs, and stale when its id is# not live or its generation is not the id's current one.## Nothing here refers to the arenas, links or free chain of the# implementation.type DS<-T: Data> is Data: DS{tag: U32, order: List<&2, Nat>, vals: List<&2, Maybe<&2, T>>, gens: List<&2, U32>, free: List<&2, Nat>}def pick_list(+b: Bool, xs: List<&2, Nat>, ys: List<&2, Nat>) -> List<&2, Nat>: match b: case True{}: xs case False{}: ysdef pick_maybe(+b: Bool, x: Maybe<&2, Nat>, y: Maybe<&2, Nat>) -> Maybe<&2, Nat>: match b: case True{}: x case False{}: ydef cons_some(-T: Data, m: Maybe<&2, T>, xs: List<&2, T>) -> List<&2, T>: match m: case None{}: xs case Some{v}: Con{v, xs}def maybe_done(-T: Data, e: E.Error, m: Maybe<&2, T>) -> Result<&2, &2, E.Error, T>: match m: case None{}: Fail{e} case Some{v}: Done{v}def gen_of(+gens: List<&2, U32>, +i: Nat) -> U32: match gens i: case Nil{} _: 0 case Con{g, t} 0n: g case Con{g, t} 1n+p: gen_of(t, p)def val_of(-T: Data, +vals: List<&2, Maybe<&2, T>>, +i: Nat) -> Maybe<&2, T>: match vals i: case Nil{} _: None{} case Con{v, t} 0n: v case Con{v, t} 1n+p: val_of(T, t, p)def handle(+tag: U32, +gens: List<&2, U32>, +i: Nat) -> E.Handle: E.H{tag, U32.from_nat(i), gen_of(gens, i)}# ---- validity ----def live_gen(-T: Data, m: Maybe<&2, T>, +same: Bool) -> Maybe<&2, E.Error>: match m same: case None{} _: Some{E.StaleHandle{}} case Some{v} True{}: None{} case Some{v} False{}: Some{E.StaleHandle{}}def valid_own(-T: Data, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +i: Nat, +g: U32, mine: Bool) -> Maybe<&2, E.Error>: match mine: case False{}: Some{E.ForeignHandle{}} case True{}: live_gen(T, val_of(T, vals, i), U32.is_eq(gen_of(gens, i), g))# None when h names a live element of the list at its current generationdef validate(-T: Data, +s: DS<T>, +h: E.Handle) -> Maybe<&2, E.Error>: match s h: case DS{+tag, +order, +vals, +gens, +free} E.H{+owner, +id, +g}: valid_own(T, vals, gens, U32.to_nat(id), g, U32.is_eq(owner, tag))# ---- positions in the order ----def ins_before(xs: List<&2, Nat>, +i: Nat, +n: Nat) -> List<&2, Nat>: match xs: case Nil{}: Nil{} case Con{+x, +t}: pick_list(Nat.is_eq(x, i), Con{n, Con{x, t}}, Con{x, ins_before(t, i, n)})def ins_after(xs: List<&2, Nat>, +i: Nat, +n: Nat) -> List<&2, Nat>: match xs: case Nil{}: Nil{} case Con{+x, +t}: pick_list(Nat.is_eq(x, i), Con{x, Con{n, t}}, Con{x, ins_after(t, i, n)})def delete(xs: List<&2, Nat>, +i: Nat) -> List<&2, Nat>: match xs: case Nil{}: Nil{} case Con{+x, +t}: pick_list(Nat.is_eq(x, i), t, Con{x, delete(t, i)})def first(xs: List<&2, Nat>) -> Maybe<&2, Nat>: match xs: case Nil{}: None{} case Con{x, t}: Some{x}# the element after idef after(xs: List<&2, Nat>, +i: Nat) -> Maybe<&2, Nat>: match xs: case Nil{}: None{} case Con{+x, +t}: pick_maybe(Nat.is_eq(x, i), first(t), after(t, i))# the element before i (p: the element before the list)def before(xs: List<&2, Nat>, +i: Nat, p: Maybe<&2, Nat>) -> Maybe<&2, Nat>: match xs: case Nil{}: None{} case Con{+x, +t}: pick_maybe(Nat.is_eq(x, i), p, before(t, i, Some{x}))def values(-T: Data, +vals: List<&2, Maybe<&2, T>>, xs: List<&2, Nat>) -> List<&2, T>: match xs: case Nil{}: Nil{} case Con{+x, +t}: cons_some(T, val_of(T, vals, x), values(T, vals, t))# ---- issuing an id ----# the id a new element takes, the list with the id reserveddef alloc(-T: Data, s: DS<T>) -> DS<T> & Nat: match s: case DS{+tag, +order, +vals, +gens, free}: match free: case Con{+i, rest}: (DS{tag, order, vals, gens, rest}, i) case Nil{}: (DS{tag, order, C.snoc(Maybe<&2, T>, vals, None{}), C.snoc(U32, gens, 0), Nil{}}, C.length(Maybe<&2, T>, vals))# where a new element goestype Pos is Data: PFront{} PBack{} PBefore{i: Nat} PAfter{i: Nat}def place_order(pos: Pos, xs: List<&2, Nat>, +n: Nat) -> List<&2, Nat>: match pos: case PFront{}: Con{n, xs} case PBack{}: C.snoc(Nat, xs, n) case PBefore{+i}: ins_before(xs, i, n) case PAfter{+i}: ins_after(xs, i, n)# store x at the reserved id n and place n in the orderdef place(-T: Data, s: DS<T>, +n: Nat, x: T, pos: Pos) -> DS<T> & E.Handle: match s: case DS{+tag, order, +vals, +gens, free}: (DS{tag, place_order(pos, order, n), C.update(Maybe<&2, T>, vals, n, Some{x}), gens, free}, handle(tag, gens, n))def inserted(-T: Data, r: DS<T> & Nat, x: T, pos: Pos) -> DS<T> & E.Handle: match r: case Tuple{s, +n}: place(T, s, n, x, pos)def push_front(-T: Data, s: DS<T>, x: T) -> DS<T> & E.Handle: inserted(T, alloc(T, s), x, PFront{})def push_back(-T: Data, s: DS<T>, x: T) -> DS<T> & E.Handle: inserted(T, alloc(T, s), x, PBack{})# ---- removal ----def retire(+gens: List<&2, U32>, +i: Nat, +free: List<&2, Nat>, +g: U32, exhausted: Bool) -> List<&2, U32> & List<&2, Nat>: match exhausted: case True{}: (gens, free) case False{}: (C.update(U32, gens, i, U32.inc(g)), Con{i, free})def 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>: match r: case Tuple{gens, free}: (DS{tag, delete(order, i), C.update(Maybe<&2, T>, vals, i, None{}), gens, free}, E.OVal{Done{v}})def 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>: match m: case Some{+v}: removed(T, tag, order, vals, i, v, retire(gens, i, free, gen_of(gens, i), U32.is_eq(gen_of(gens, i), 4294967295))) case None{}: (DS{tag, order, vals, gens, free}, E.OVal{Fail{E.StaleHandle{}}})def remove_live(-T: Data, s: DS<T>, +i: Nat) -> DS<T> & E.Obs<T>: match s: case DS{+tag, +order, +vals, +gens, +free}: remove_m(T, tag, order, vals, gens, free, i, val_of(T, vals, i))# ---- one operation on a valid handle ----def get_live(-T: Data, s: DS<T>, +i: Nat) -> DS<T> & E.Obs<T>: match s: case DS{+tag, +order, +vals, +gens, +free}: (DS{tag, order, vals, gens, free}, E.OVal{maybe_done(T, E.StaleHandle{}, val_of(T, vals, i))})def set_live(-T: Data, s: DS<T>, +i: Nat, x: T) -> DS<T> & E.Obs<T>: match s: case DS{+tag, +order, +vals, +gens, +free}: (DS{tag, order, C.update(Maybe<&2, T>, vals, i, Some{x}), gens, free}, E.OUnit{Done{Unit{}}})def nbr(+tag: U32, +gens: List<&2, U32>, m: Maybe<&2, Nat>) -> Maybe<&2, E.Handle>: match m: case None{}: None{} case Some{+j}: Some{handle(tag, gens, j)}def next_live(-T: Data, s: DS<T>, +i: Nat) -> DS<T> & E.Obs<T>: match s: case DS{+tag, +order, +vals, +gens, +free}: (DS{tag, order, vals, gens, free}, E.ONbr{Done{nbr(tag, gens, after(order, i))}})def prev_live(-T: Data, s: DS<T>, +i: Nat) -> DS<T> & E.Obs<T>: match s: case DS{+tag, +order, +vals, +gens, +free}: (DS{tag, order, vals, gens, free}, E.ONbr{Done{nbr(tag, gens, before(order, i, None{}))}})def ins_obs(-T: Data, r: DS<T> & E.Handle) -> DS<T> & E.Obs<T>: match r: case Tuple{s, h}: (s, E.OInsert{Done{h}})def live_op(-T: Data, s: DS<T>, +op: E.Op<T>, +i: Nat) -> DS<T> & E.Obs<T>: match op: case E.InsertBefore{h, x}: ins_obs(T, inserted(T, alloc(T, s), x, PBefore{i})) case E.InsertAfter{h, x}: ins_obs(T, inserted(T, alloc(T, s), x, PAfter{i})) case E.Remove{h}: remove_live(T, s, i) case E.Get{h}: get_live(T, s, i) case E.Set{h, x}: set_live(T, s, i, x) case E.Next{h}: next_live(T, s, i) case E.Prev{h}: prev_live(T, s, i) case E.Length{}: (s, E.ONat{0n}) case E.PushFront{x}: (s, E.ONat{0n}) case E.PushBack{x}: (s, E.ONat{0n}) case E.ToList{}: (s, E.ONat{0n})# the observation of op failing with e (the list is unchanged)def failed(-T: Data, op: E.Op<T>, e: E.Error) -> E.Obs<T>: match op: case E.InsertBefore{h, x}: E.OInsert{Fail{e}} case E.InsertAfter{h, x}: E.OInsert{Fail{e}} case E.Remove{h}: E.OVal{Fail{e}} case E.Get{h}: E.OVal{Fail{e}} case E.Set{h, x}: E.OUnit{Fail{e}} case E.Next{h}: E.ONbr{Fail{e}} case E.Prev{h}: E.ONbr{Fail{e}} case E.Length{}: E.ONat{0n} case E.PushFront{x}: E.ONat{0n} case E.PushBack{x}: E.ONat{0n} case E.ToList{}: E.ONat{0n}def handle_id(+h: E.Handle) -> Nat: match h: case E.H{+owner, +id, +g}: U32.to_nat(id)def checked(-T: Data, +s: DS<T>, +op: E.Op<T>, +h: E.Handle, m: Maybe<&2, E.Error>) -> DS<T> & E.Obs<T>: match m: case Some{e}: (s, failed(T, op, e)) case None{}: live_op(T, s, op, handle_id(h))def with_handle(-T: Data, +s: DS<T>, +op: E.Op<T>, +h: E.Handle) -> DS<T> & E.Obs<T>: checked(T, s, op, h, validate(T, s, h))def len_of(-T: Data, s: DS<T>) -> Nat: match s: case DS{+tag, +order, +vals, +gens, +free}: C.length(Nat, order)def list_of(-T: Data, s: DS<T>) -> List<&2, T>: match s: case DS{+tag, +order, +vals, +gens, +free}: values(T, vals, order)def pushed(-T: Data, r: DS<T> & E.Handle) -> DS<T> & E.Obs<T>: match r: case Tuple{s, h}: (s, E.OHandle{h})def step(-T: Data, +s: DS<T>, op: E.Op<T>) -> DS<T> & E.Obs<T>: match op: case E.Length{}: (s, E.ONat{len_of(T, s)}) case E.PushFront{x}: pushed(T, push_front(T, s, x)) case E.PushBack{x}: pushed(T, push_back(T, s, x)) case E.InsertBefore{+h, +x}: with_handle(T, s, E.InsertBefore{h, x}, h) case E.InsertAfter{+h, +x}: with_handle(T, s, E.InsertAfter{h, x}, h) case E.Remove{+h}: with_handle(T, s, E.Remove{h}, h) case E.Get{+h}: with_handle(T, s, E.Get{h}, h) case E.Set{+h, +x}: with_handle(T, s, E.Set{h, x}, h) case E.Next{+h}: with_handle(T, s, E.Next{h}, h) case E.Prev{+h}: with_handle(T, s, E.Prev{h}, h) case E.ToList{}: (s, E.OList{list_of(T, s)})def empty(-T: Data, +tag: U32) -> DS<T>: DS{tag, Nil{}, Nil{}, Nil{}, Nil{}}def cons_obs(-T: Data, o: E.Obs<T>, r: DS<T> & List<&2, E.Obs<T>>) -> DS<T> & List<&2, E.Obs<T>>: match r: case Tuple{m, os}: (m, Con{o, os})def run(-T: Data, ops: List<&2, E.Op<T>>, +s: DS<T>) -> DS<T> & List<&2, E.Obs<T>>: match ops: case Nil{}: (s, Nil{}) case Con{+op, rest}: 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))))# ---- contract (SPARK formal containers) ----# Each `<Subprogram>.<clause>` definition below states one Post clause of# that SPARK subprogram, as a proposition on this model; the table names the# clauses. proofs/containers/doubly_linked_list/ proves every clause under its clause name,# and its `impl` lemma carries them to the implementation.## Contracts of the doubly linked list in the style of SPARK's formal doubly# linked lists (SPARKlib src/spark-containers-formal-doubly_linked_lists.ads,# AdaCore/SPARKlib 46ec319; model predicates in spec/lib/sequence.bend).# SPARK's cursors are our handles; Has_Element (Container, Position) is# S.validate (s, h) = None; Positions is the order (the ids of the live# elements, first to last: a handle's position is the index of its id);# Model is S.list_of (the values along the order). Position clauses are# stated on the order, split at the handle's id: order = a ++ [id] ++ b# with id not in a (fsplit), so Position (h) = Length (a). A valid handle's# id is in the order in every good list (doubly_linked_list/hlive.src,# mem_of), which is the premise of fsplit. Each lemma is one Post clause of# step; `impl` (via P.step_ok) carries every clause to the implementation.## SPARK subprogram (.ads line) ours clauses# Length (78) length length_result, length_frame# Empty_List (71) new new_empty# Has_Element (1814) validate has_element (definition), valid_live# Element (419) get get_frame, get_element# Replace_Element (430) set set_positions, set_element, set_others, set_gens# Prepend (836) push_front push_front_positions, push_front_first, push_front_length# Append (905) push_back push_back_positions, push_back_last, push_back_length# Insert Before (523) insert_before insert_before_equal, insert_before_at,# insert_before_shifted, insert_before_length# Insert after (Next (Before)) insert_after insert_after_equal, insert_after_at,# insert_after_shifted, insert_after_length# Delete (978) remove remove_equal, remove_shifted, remove_length,# remove_result, remove_stale# Next (1614) next next_result, next_position, next_frame# Previous (1652) prev prev_result, prev_first, prev_position, prev_frame# iteration (Iter_Model) to_list to_list_model, to_list_frame# implementation D.step impl# Not in this API: "=", Is_Empty, Clear, Assign/Copy/Move, Reference,# Insert with Count, Delete with Count, Delete_First/Delete_Last,# First/First_Element/Last/Last_Element (the ends are reached by the# handles push returns), Reverse_Elements, Swap, Swap_Links, Splice, Find,# Reverse_Find, Contains. SPARK's Pre (Has_Element) is a defensive check:# a foreign or stale handle returns ForeignHandle / StaleHandle and changes# nothing (the refinement proof's failed case).def nx(-T: Data, +s: DS<T>, +op: E.Op<T>) -> DS<T>: Pair.fst(DS<T>, E.Obs<T>, step(T, s, op))def ob(-T: Data, +s: DS<T>, +op: E.Op<T>) -> E.Obs<T>: Pair.snd(DS<T>, E.Obs<T>, step(T, s, op))def ord(-T: Data, s: DS<T>) -> List<&2, Nat>: match s: case DS{tag, order, vals, gens, free}: orderdef vls(-T: Data, s: DS<T>) -> List<&2, Maybe<&2, T>>: match s: case DS{tag, order, vals, gens, free}: valsdef gns(-T: Data, s: DS<T>) -> List<&2, U32>: match s: case DS{tag, order, vals, gens, free}: gens# Has_Element (Container, Position)def has_of(m: Maybe<&2, E.Error>) -> Bool: match m: case None{}: True{} case Some{e}: False{}def has_element(-T: Data, +s: DS<T>, +h: E.Handle) -> Bool: has_of(validate(T, s, h))# Previous: the last element of a, or p when a is emptydef lastm(xs: List<&2, Nat>, p: Maybe<&2, Nat>) -> Maybe<&2, Nat>: match xs: case Nil{}: p case Con{+x, t}: lastm(t, Some{x})# ---- the order split at a live id ----def FSplit(+i: Nat, +xs: List<&2, Nat>) -> Type: 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}>># Next (1614)def Next.next_position(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>) -> Type: {C.nth(Nat, C.append(Nat, a, Con{i, b}), 1n+C.length(Nat, a)) == first(b) : Maybe<&2, Nat>}# Previous (1652)def Previous.prev_position(+t: List<&2, Nat>, +x: Nat, +i: Nat, +b: List<&2, Nat>, +p: Maybe<&2, Nat>) -> Type: {lastm(Con{x, t}, p) == C.nth(Nat, C.append(Nat, Con{x, t}, Con{i, b}), C.length(Nat, t)) : Maybe<&2, Nat>}# Has_Element (1814)def 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: Sigma<&1, &1, T, v => {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}># Length (78)def Length.length_result(-T: Data, +s: DS<T>) -> Type: {ob(T, s, E.Length{}) == E.ONat{len_of(T, s)} : E.Obs<T>}# Length (78)def Length.length_frame(-T: Data, +s: DS<T>) -> Type: {nx(T, s, E.Length{}) == s : DS<T>}# iteration (Iter_Model)def Iteration.to_list_model(-T: Data, +s: DS<T>) -> Type: {ob(T, s, E.ToList{}) == E.OList{list_of(T, s)} : E.Obs<T>}# iteration (Iter_Model)def Iteration.to_list_frame(-T: Data, +s: DS<T>) -> Type: {nx(T, s, E.ToList{}) == s : DS<T>}# Empty_List (71)def Empty_List.new_empty(-T: Data, +tag: U32) -> Type: {len_of(T, empty(T, tag)) == 0n : Nat}# Element (419)def 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: {nx(T, DS{tag, order, vals, gens, free}, E.Get{h}) == DS{tag, order, vals, gens, free} : DS<T>}# Element (419)def 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: {ob(T, DS{tag, order, vals, gens, free}, E.Get{h}) == E.OVal{Done{v}} : E.Obs<T>}# Replace_Element (430)def 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: {ord(T, nx(T, DS{tag, order, vals, gens, free}, E.Set{h, x})) == order : List<&2, Nat>}# Replace_Element (430)def 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: {gns(T, nx(T, DS{tag, order, vals, gens, free}, E.Set{h, x})) == gens : List<&2, U32>}# Replace_Element (430)def 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: {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>}# Replace_Element (430)def 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: {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>}# Prepend (836)def 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: V.RangeShifted(Nat, order, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushFront{x})), 0n, C.length(Nat, order), 1n)# Prepend (836)def 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: {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>}# Prepend (836)def 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: {C.length(Nat, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushFront{x}))) == 1n+C.length(Nat, order) : Nat}# Append (905)def 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: V.EqualPrefix(Nat, order, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushBack{x})))# Append (905)def 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: {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>}# Append (905)def 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: {C.length(Nat, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushBack{x}))) == 1n+C.length(Nat, order) : Nat}# Insert Before (523)def 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: 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))# Insert Before (523)def 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: {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>}# Insert Before (523)def 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: 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)# Insert Before (523)def 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: {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}# Insert after (Next (Before))def 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: 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))# Insert after (Next (Before))def 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: {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>}# Insert after (Next (Before))def 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: 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)# Insert after (Next (Before))def 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: {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}# Delete (978)def 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: {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>}# Delete (978)def 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: 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))# Delete (978)def 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: 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)# Delete (978)def 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: {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}# Delete (978)def 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: {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}# Next (1614)def 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: {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>}# Next (1614)def 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: {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>}# Previous (1652)def 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: {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>}# Previous (1652)def 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: {ob(T, DS{tag, Con{handle_id(h), b}, vals, gens, free}, E.Prev{h}) == E.ONbr{Done{None{}}} : E.Obs<T>}# Previous (1652)def 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: {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>}