proofs/containers/intrusive_doubly_linked_list/fold.bend checks

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

3 imports

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

Definitions

def cursor source · line 9 · raw

@-V:Data -> @+xs:List<&2, V> -> Maybe<&2, List<&2, V>>

Sequence refinement of fold_left on a structurally represented chain. Callback state/accumulator are arbitrary affine Types. This establishes forward order and exact-once callbacks for every length, not just examples. Application array/handle adapters still need their own representation law.

Templates

template next source · line 14 · raw

@-S:Type -> @-V:Data -> @s:S -> @node:List<&2, V> -> Pair(S, Maybe<&2, List<&2, V>>)

template value source · line 19 · raw

@-S:Type -> @-V:Data -> @-zero:V -> @s:S -> @node:List<&2, V> -> Pair(S, V)

template get source · line 24 · raw

@-S:Type -> @-V:Data -> @s:S -> @h:List<&2, V> -> Pair(S, Maybe<&2, List<&2, V>>)

template model source · line 27 · raw

@-S:Type -> @-V:Data -> @-A:Type -> @-C:Data -> @-fn:(@_:S -> @_:C -> @_:A -> @_:V -> Pair(S, A)) -> @xs:List<&2, V> -> @+c:C -> @r:Pair(S, A) -> Pair(S, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.Error, A>)

@-S:Type -> @-V:Data -> @-A:Type -> @-C:Data -> @-zero:V -> @-fn:(@_:S -> @_:C -> @_:A -> @_:V -> Pair(S, A)) -> @+xs:List<&2, V> -> @+c:C -> @r:Pair(S, A) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/intrusive_list.fold_loop(S, List<&2, V>, V, A, C, s => n => next(S, V, s, n), s => n => value(S, V, zero, s, n), fn, List.length(&2, V, xs), c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/intrusive_list.fold_step_3(S, List<&2, V>, V, A, C, s => n => next(S, V, s, n), s => n => value(S, V, zero, s, n), fn, cursor(V, xs), r)) == model(S, V, A, C, fn, xs, c, r) : Pair(S, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.Error, A>)}

template fold_left_refines source · line 38 · raw

@-S:Type -> @-V:Data -> @-A:Type -> @-C:Data -> @-zero:V -> @-fn:(@_:S -> @_:C -> @_:A -> @_:V -> Pair(S, A)) -> @+xs:List<&2, V> -> @+c:C -> @s:S -> @acc:A -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/intrusive_list.fold_left(S, List<&2, V>, V, A, C, List<&2, V>, s => h => get(S, V, s, h), s => n => next(S, V, s, n), s => n => value(S, V, zero, s, n), fn, List.length(&2, V, xs), s, xs, c, acc) == model(S, V, A, C, fn, xs, c, (s, acc)) : Pair(S, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.Error, A>)}