proofs/containers/intrusive_doubly_linked_list/fold.bend source

proofs/containers/intrusive_doubly_linked_list/fold.bend on the hub · documented module

import Baseimport ../../../src/containers/internal/intrusive_list.bend as Limport ../../../src/containers/types/intrusive_doubly_linked_list.bend as E# 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.def cursor(-V: Data, +xs: List<&2, V>) -> Maybe<&2, List<&2, V>>:  match xs:    case Nil{}: None{}    case Con{v, rest}: Some{Con{v, rest}}def next(~S: Type, ~V: Data, s: S, node: List<&2, V>) -> S & Maybe<&2, List<&2, V>>:  match node:    case Nil{}: (s, None{})    case Con{v, rest}: (s, cursor(V, rest))def value(~S: Type, ~V: Data, ~zero: V, s: S, node: List<&2, V>) -> S & V:  match node:    case Nil{}: (s, zero)    case Con{v, rest}: (s, v)def get(~S: Type, ~V: Data, s: S, h: List<&2, V>) -> S & Maybe<&2, List<&2, V>>:  (s, cursor(V, h))def model(~S: Type, ~V: Data, ~A: Type, ~C: Data, ~fn: S -> C -> A -> V -> S & A, xs: List<&2, V>, +c: C, r: S & A) -> S & Result<&2, &1, E.Error, A>:  match xs r:    case Nil{} Tuple{s, acc}: (s, Done{acc})    case Con{v, rest} Tuple{s, acc}: model(~S, ~V, ~A, ~C, ~fn, rest, c, fn(s, c, acc, v))def refinement(~S: Type, ~V: Data, ~A: Type, ~C: Data, ~zero: V, ~fn: S -> C -> A -> V -> S & A, +xs: List<&2, V>, +c: C, r: S & A) -> {L.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, L.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) : S & Result<&2, &1, E.Error, A>}:  match xs r:    case Nil{} Tuple{s, acc}: {==}    case Con{v, rest} Tuple{s, acc}:      refinement(~S, ~V, ~A, ~C, ~zero, ~fn, rest, c, fn(s, c, acc, v))def fold_left_refines(~S: Type, ~V: Data, ~A: Type, ~C: Data, ~zero: V, ~fn: S -> C -> A -> V -> S & A, +xs: List<&2, V>, +c: C, s: S, acc: A) -> {L.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)) : S & Result<&2, &1, E.Error, A>}:  refinement(~S, ~V, ~A, ~C, ~zero, ~fn, xs, c, (s, acc))