1	import Base
2	import ./fold.bend as Chain
3	import ../../../src/containers/internal/intrusive_list.bend as L
4	import ../../../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.
9	def ignore_link(~S: Type, ~V: Data, s: S, n: List<&2, V>, m: Maybe<&2, List<&2, V>>) -> S:
10	  s
11	
12	def 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	
17	def 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	
23	def 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	
28	def 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	
33	def 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{}))