proofs/containers/intrusive_doubly_linked_list/clear.bend
bend-collections-laws-containers@1.0.0.0 · 38 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/fold.bend as Chain
3import bend-collections-laws-containers@1.0.0.0/src/containers/internal/intrusive_list.bend as L
4import bend-collections-laws-containers@1.0.0.0/src/containers/types/intrusive_doubly_linked_list.bend as E
5
6# Exact callback order for every finite chain under sufficient fuel.
7# In this observer instance link stores are silent and root/post hooks may
8# change arbitrary affine state. Detachment itself is checked separately.
9def ignore_link(~S: Type, ~V: Data, s: S, n: List<&2, V>, m: Maybe<&2, List<&2, V>>) -> S:
10 s
11
12def model(~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) -> S & Result<&2, &1, E.Error, Unit>:
13 match rest:
14 case Nil{}: (post(s, c, head), Done{Unit{}})
15 case Con{v, tail}: model(~S, ~V, ~C, ~post, tail, head, c, post(s, c, Con{v, tail}))
16
17def clear_loop_order(~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) -> {L.clear_loop(~S, ~List<&2, V>, ~C, ~(s => n => Chain.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, Chain.cursor(V, rest))) == model(~S, ~V, ~C, ~post, rest, head, c, s) : S & Result<&2, &1, E.Error, Unit>}:
18 match rest:
19 case Nil{}: {==}
20 case Con{v, tail}:
21 clear_loop_order(~S, ~V, ~C, ~post, tail, head, c, post(s, c, Con{v, tail}))
22
23def preflight_fits(~S: Type, ~V: Data, +xs: List<&2, V>, -s: S) -> {L.chain_fits(~S, ~List<&2, V>, ~(s => n => Chain.next(~S, ~V, s, n)), List.length(&2, V, xs), (s, Chain.cursor(V, xs))) == (s, True{}) : S & Bool}:
24 match xs:
25 case Nil{}: {==}
26 case Con{v, rest}: preflight_fits(~S, ~V, rest, s)
27
28def expected(~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) -> S & Result<&2, &1, E.Error, Unit>:
29 match xs:
30 case Nil{}: (s, Done{Unit{}})
31 case Con{v, rest}: model(~S, ~V, ~C, ~post, rest, Con{v, rest}, c, sh(s, i, None{}))
32
33def clear_list_order(~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) -> {L.clear_list_as(~S, ~List<&2, V>, ~List<&2, V>, ~I, ~C, ~(s => h => Chain.get(~S, ~V, s, h)), ~(s => n => Chain.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) : S & Result<&2, &1, E.Error, Unit>}:
34 match xs:
35 case Nil{}: {==}
36 case Con{v, rest}:
37 %Equal.sym(S & Bool, L.chain_fits(~S, ~List<&2, V>, ~(s => n => Chain.next(~S, ~V, s, n)), List.length(&2, V, Con{v, rest}), (s, Chain.cursor(V, Con{v, rest}))), (s, True{}), preflight_fits(~S, ~V, Con{v, rest}, s)) : {L.clear_checked(~S, ~List<&2, V>, ~List<&2, V>, ~I, ~C, ~(s => h => Chain.get(~S, ~V, s, h)), ~(s => n => Chain.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, 1n+List.length(&2, V, rest), Con{v, rest}, i, c, Some{Con{v, rest}}, _) == expected(~S, ~V, ~I, ~C, ~sh, ~post, Con{v, rest}, i, c, s) : S & Result<&2, &1, E.Error, Unit>}
38 clear_loop_order(~S, ~V, ~C, ~post, rest, Con{v, rest}, c, sh(s, i, None{}))