spec/containers/intrusive_doubly_linked_list/main.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/main.bend as Main

3 imports

import Base
import ./model.bend as G
import ./programs.bend as W

Templates

template Prepend.valid source · line 38 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @-reflex:(@x:N -> {eq(x, x) == True{} : Bool}) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+xs:List<&2, N> -> @+rsame:{req(r, r) == True{} : Bool} -> @+away:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, xs) -> @+detached:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, g, n) == None{} : Maybe<&2, N>} -> @+valid:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, g, r, xs) -> Type

Prepend: a detached non-member n becomes the first member.

template Prepend.other_roots source · line 42 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-req:(@_:R -> @_:R -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+x:R -> @+neq:{req(r, x) == False{} : Bool} -> Type

Prepend: every other root reads what it read before.

template Prepend.frame source · line 46 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-req:(@_:R -> @_:R -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> Type

Prepend: everything else the application owns is unchanged.

template Delete.first source · line 50 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @-reflex:(@x:N -> {eq(x, x) == True{} : Bool}) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+xs:List<&2, N> -> @+rsame:{req(r, r) == True{} : Bool} -> @+valid:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, g, r, n <> xs) -> Type

Delete the first member.

template Delete.inner source · line 54 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @-reflex:(@x:N -> {eq(x, x) == True{} : Bool}) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+a:List<&2, N> -> @+p:N -> @+b:List<&2, N> -> @+valid:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, g, r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [p]), n <> b)) -> Type

Delete a member after the prefix a ++ [p].

template Delete.other_roots source · line 58 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+x:R -> @+neq:{req(r, x) == False{} : Bool} -> Type

Delete: every other root reads what it read before.

template Delete.frame source · line 62 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> Type

Delete: everything else the application owns is unchanged.

template Delete.detached source · line 66 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+same:{eq(n, n) == True{} : Bool} -> Type

Delete: the removed entity no longer links forward (it can join another list).

template First.head source · line 70 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+xs:List<&2, N> -> @+valid:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, g, r, xs) -> Type

First: a valid list's root reads its first member.