proofs/containers/intrusive_doubly_linked_list/clear.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/clear.bend as Clear

4 imports

import Base
import ./fold.bend as Chain
import ../../../src/containers/internal/intrusive_list.bend as L
import ../../../src/containers/types/intrusive_doubly_linked_list.bend as E

Templates

template ignore_link source · line 9 · raw

@-S:Type -> @-V:Data -> @s:S -> @n:List<&2, V> -> @m:Maybe<&2, List<&2, V>> -> S

Exact callback order for every finite chain under sufficient fuel. In this observer instance link stores are silent and root/post hooks may change arbitrary affine state. Detachment itself is checked separately.

template model source · line 12 · raw

@-S:Type -> @-V:Data -> @-C:Data -> @-post:(@_:S -> @_:C -> @_:List<&2, V> -> S) -> @+rest:List<&2, V> -> @head:List<&2, V> -> @+c:C -> @s:S -> Pair(S, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.Error, Unit>)

template clear_loop_order source · line 17 · raw

@-S:Type -> @-V:Data -> @-C:Data -> @-post:(@_:S -> @_:C -> @_:List<&2, V> -> S) -> @+rest:List<&2, V> -> @+head:List<&2, V> -> @+c:C -> @s:S -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/intrusive_list.clear_loop(S, List<&2, V>, C, s => n => 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/fold.next(S, V, s, n), s => n => m => ignore_link(S, V, s, n, m), s => n => m => ignore_link(S, V, s, n, m), post, 1n+List.length(&2, V, rest), head, c, (s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/fold.cursor(V, rest))) == model(S, V, C, post, rest, head, c, s) : Pair(S, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.Error, Unit>)}

template preflight_fits source · line 23 · raw

@-S:Type -> @-V:Data -> @+xs:List<&2, V> -> @-s:S -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/intrusive_list.chain_fits(S, List<&2, V>, s => n => 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/fold.next(S, V, s, n), List.length(&2, V, xs), (s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/fold.cursor(V, xs))) == (s, True{}) : Pair(S, Bool)}

template expected source · line 28 · raw

@-S:Type -> @-V:Data -> @-I:Data -> @-C:Data -> @-sh:(@_:S -> @_:I -> @_:Maybe<&2, List<&2, V>> -> S) -> @-post:(@_:S -> @_:C -> @_:List<&2, V> -> S) -> @+xs:List<&2, V> -> @i:I -> @c:C -> @s:S -> Pair(S, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.Error, Unit>)

template clear_list_order source · line 33 · raw

@-S:Type -> @-V:Data -> @-I:Data -> @-C:Data -> @-sh:(@_:S -> @_:I -> @_:Maybe<&2, List<&2, V>> -> S) -> @-post:(@_:S -> @_:C -> @_:List<&2, V> -> S) -> @+xs:List<&2, V> -> @+i:I -> @+c:C -> @s:S -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/intrusive_list.clear_list_as(S, List<&2, V>, List<&2, V>, I, C, s => h => 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/fold.get(S, V, s, h), s => n => 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/fold.next(S, V, s, n), s => n => m => ignore_link(S, V, s, n, m), s => n => m => ignore_link(S, V, s, n, m), sh, post, List.length(&2, V, xs), s, xs, i, c) == expected(S, V, I, C, sh, post, xs, i, c, s) : Pair(S, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.Error, Unit>)}