spec/containers/intrusive_doubly_linked_list/model.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/model.bend as Model
1 import
import Base
Types
type Binding source · line 16 · raw
@-K:Data -> @-V:Data -> Data
Proof-only finite maps. New bindings shadow old ones; no storage layout, allocation strategy, machine integer width or payload type is assumed.
Binding@-K:Data -> @-V:Data -> @key:K -> @value:V -> Binding<K, V>
type Graph source · line 29 · raw
@-N:Data -> @-R:Data -> @-P:Data -> Data
Graph@-N:Data -> @-R:Data -> @-P:Data -> @nexts:List<&2, Binding<N, Maybe<&2, N>>> -> @prevs:List<&2, Binding<N, Maybe<&2, N>>> -> @roots:List<&2, Binding<R, Maybe<&2, N>>> -> @frame:P -> Graph<N, R, P>
Definitions
def both source · line 3 · raw
@-A:Data -> @-B:Data -> Data
def left source · line 6 · raw
@-A:Data -> @-B:Data -> @p:both(A, B) -> A
def right source · line 10 · raw
@-A:Data -> @-B:Data -> @p:both(A, B) -> B
Templates
template choose source · line 19 · raw
@-V:Data -> @b:Bool -> @yes:V -> @no:V -> V
template lookup source · line 24 · raw
@-K:Data -> @-V:Data -> @-eq:(@_:K -> @_:K -> Bool) -> @+key:K -> @xs:List<&2, Binding<K, V>> -> @+default:V -> V
template next source · line 32 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @g:Graph<N, R, P> -> @n:N -> Maybe<&2, N>
template prev source · line 36 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @g:Graph<N, R, P> -> @n:N -> Maybe<&2, N>
template head source · line 40 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:R -> @_:R -> Bool) -> @g:Graph<N, R, P> -> @r:R -> Maybe<&2, N>
template frame source · line 44 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @g:Graph<N, R, P> -> P
template sn source · line 48 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @g:Graph<N, R, P> -> @n:N -> @v:Maybe<&2, N> -> Graph<N, R, P>
template sp source · line 52 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @g:Graph<N, R, P> -> @n:N -> @v:Maybe<&2, N> -> Graph<N, R, P>
template sh source · line 56 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @g:Graph<N, R, P> -> @r:R -> @v:Maybe<&2, N> -> Graph<N, R, P>
template first source · line 60 · raw
@-N:Data -> @xs:List<&2, N> -> @d:Maybe<&2, N> -> Maybe<&2, N>
template last source · line 65 · raw
@-N:Data -> @xs:List<&2, N> -> @d:Maybe<&2, N> -> Maybe<&2, N>
template append source · line 70 · raw
@-N:Data -> @xs:List<&2, N> -> @+ys:List<&2, N> -> List<&2, N>
template away source · line 77 · raw
@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+n:N -> @xs:List<&2, N> -> Data
Away records disjoint identities in both directions. A lawful equality is reflexive and agrees with identity; the algorithm does not execute it.
template unique source · line 82 · raw
@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @xs:List<&2, N> -> Data
template segment source · line 90 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:Graph<N, R, P> -> @p:Maybe<&2, N> -> @xs:List<&2, N> -> @+q:Maybe<&2, N> -> Data
A segment states BOTH links of EVERY member, with explicit external ends. With unique(xs), segment(g,None,xs,None) describes an acyclic reciprocal chain, rather than merely an ordered write trace.
template valid source · line 95 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @+g:Graph<N, R, P> -> @r:R -> @+xs:List<&2, N> -> Data
template disjoint source · line 98 · raw
@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @xs:List<&2, N> -> @+ys:List<&2, N> -> Data
template optional_prev source · line 103 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @g:Graph<N, R, P> -> @at:Maybe<&2, N> -> @v:Maybe<&2, N> -> Graph<N, R, P>
template attach source · line 108 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @g:Graph<N, R, P> -> @r:R -> @+n:N -> @+h:Maybe<&2, N> -> Graph<N, R, P>
template cut_left source · line 111 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @g:Graph<N, R, P> -> @r:R -> @+n:N -> @p:Maybe<&2, N> -> @q:Maybe<&2, N> -> Graph<N, R, P>
template cut source · line 116 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @g:Graph<N, R, P> -> @r:R -> @+n:N -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> Graph<N, R, P>
template prepend source · line 119 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @-req:(@_:R -> @_:R -> Bool) -> @+g:Graph<N, R, P> -> @+r:R -> @n:N -> Graph<N, R, P>
template remove source · line 122 · raw
@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:Graph<N, R, P> -> @r:R -> @+n:N -> Graph<N, R, P>