spec/containers/intrusive_doubly_linked_list/model.bend
bend-collections-laws-containers@1.0.0.0 · 123 lines · 0 definitions
1import Base
2
3def both(-A: Data, -B: Data) -> Data:
4 Sigma<&2,&2,A,_ => B>
5
6def left(-A: Data, -B: Data, p: both(A,B)) -> A:
7 (a,b) = p
8 a
9
10def right(-A: Data, -B: Data, p: both(A,B)) -> B:
11 (a,b) = p
12 b
13
14# Proof-only finite maps. New bindings shadow old ones; no storage layout,
15# allocation strategy, machine integer width or payload type is assumed.
16type Binding<-K: Data, -V: Data> is Data:
17 Binding{key: K, value: V}
18
19def choose(~V: Data, b: Bool, yes: V, no: V) -> V:
20 match b:
21 case True{}: yes
22 case False{}: no
23
24def lookup(~K: Data, ~V: Data, ~eq: K -> K -> Bool, +key: K, xs: List<&2, Binding<K, V>>, +default: V) -> V:
25 match xs:
26 case Nil{}: default
27 case Con{Binding{k, v}, rest}: choose(~V, eq(k, key), v, lookup(~K, ~V, ~eq, key, rest, default))
28
29type Graph<-N: Data, -R: Data, -P: Data> is Data:
30 Graph{nexts: List<&2, Binding<N, Maybe<&2, N>>>, prevs: List<&2, Binding<N, Maybe<&2, N>>>, roots: List<&2, Binding<R, Maybe<&2, N>>>, frame: P}
31
32def next(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, g: Graph<N,R,P>, n: N) -> Maybe<&2,N>:
33 Graph{ns, ps, rs, f} = g
34 lookup(~N, ~Maybe<&2,N>, ~eq, n, ns, None{})
35
36def prev(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, g: Graph<N,R,P>, n: N) -> Maybe<&2,N>:
37 Graph{ns, ps, rs, f} = g
38 lookup(~N, ~Maybe<&2,N>, ~eq, n, ps, None{})
39
40def head(~N: Data, ~R: Data, ~P: Data, ~eq: R -> R -> Bool, g: Graph<N,R,P>, r: R) -> Maybe<&2,N>:
41 Graph{ns, ps, rs, f} = g
42 lookup(~R, ~Maybe<&2,N>, ~eq, r, rs, None{})
43
44def frame(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>) -> P:
45 Graph{ns, ps, rs, f} = g
46 f
47
48def sn(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, n: N, v: Maybe<&2,N>) -> Graph<N,R,P>:
49 Graph{ns, ps, rs, f} = g
50 Graph{Con{Binding{n,v},ns}, ps, rs, f}
51
52def sp(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, n: N, v: Maybe<&2,N>) -> Graph<N,R,P>:
53 Graph{ns, ps, rs, f} = g
54 Graph{ns, Con{Binding{n,v},ps}, rs, f}
55
56def sh(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, r: R, v: Maybe<&2,N>) -> Graph<N,R,P>:
57 Graph{ns, ps, rs, f} = g
58 Graph{ns, ps, Con{Binding{r,v},rs}, f}
59
60def first(~N: Data, xs: List<&2,N>, d: Maybe<&2,N>) -> Maybe<&2,N>:
61 match xs:
62 case Nil{}: d
63 case Con{x, rest}: Some{x}
64
65def last(~N: Data, xs: List<&2,N>, d: Maybe<&2,N>) -> Maybe<&2,N>:
66 match xs:
67 case Nil{}: d
68 case Con{x, rest}: last(~N, rest, Some{x})
69
70def append(~N: Data, xs: List<&2,N>, +ys: List<&2,N>) -> List<&2,N>:
71 match xs:
72 case Nil{}: ys
73 case Con{x, rest}: Con{x, append(~N, rest, ys)}
74
75# Away records disjoint identities in both directions. A lawful equality is
76# reflexive and agrees with identity; the algorithm does not execute it.
77def away(~N: Data, ~eq: N -> N -> Bool, +n: N, xs: List<&2,N>) -> Data:
78 match xs:
79 case Nil{}: Unit
80 case Con{x, rest}: both(both({eq(n,x) == False{} : Bool}, {eq(x,n) == False{} : Bool}), away(~N, ~eq, n, rest))
81
82def unique(~N: Data, ~eq: N -> N -> Bool, xs: List<&2,N>) -> Data:
83 match xs:
84 case Nil{}: Unit
85 case Con{+x, +rest}: both(away(~N, ~eq, x, rest), unique(~N, ~eq, rest))
86
87# A segment states BOTH links of EVERY member, with explicit external ends.
88# With unique(xs), segment(g,None,xs,None) describes an acyclic reciprocal
89# chain, rather than merely an ordered write trace.
90def segment(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: Graph<N,R,P>, p: Maybe<&2,N>, xs: List<&2,N>, +q: Maybe<&2,N>) -> Data:
91 match xs:
92 case Nil{}: Unit
93 case Con{+x, +rest}: both({prev(~N,~R,~P,~eq,g,x) == p : Maybe<&2,N>}, both({next(~N,~R,~P,~eq,g,x) == first(~N,rest,q) : Maybe<&2,N>}, segment(~N,~R,~P,~eq,g,Some{x},rest,q)))
94
95def valid(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, +g: Graph<N,R,P>, r: R, +xs: List<&2,N>) -> Data:
96 both(unique(~N,~eq,xs), both({head(~N,~R,~P,~req,g,r) == first(~N,xs,None{}) : Maybe<&2,N>}, segment(~N,~R,~P,~eq,g,None{},xs,None{})))
97
98def disjoint(~N: Data, ~eq: N -> N -> Bool, xs: List<&2,N>, +ys: List<&2,N>) -> Data:
99 match xs:
100 case Nil{}: Unit
101 case Con{x,rest}: both(away(~N,~eq,x,ys),disjoint(~N,~eq,rest,ys))
102
103def optional_prev(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, at: Maybe<&2,N>, v: Maybe<&2,N>) -> Graph<N,R,P>:
104 match at:
105 case None{}: g
106 case Some{n}: sp(~N,~R,~P,g,n,v)
107
108def attach(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, r: R, +n: N, +h: Maybe<&2,N>) -> Graph<N,R,P>:
109 sh(~N,~R,~P,optional_prev(~N,~R,~P,sn(~N,~R,~P,g,n,h),h,Some{n}),r,Some{n})
110
111def cut_left(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, r: R, +n: N, p: Maybe<&2,N>, q: Maybe<&2,N>) -> Graph<N,R,P>:
112 match p:
113 case None{}: sn(~N,~R,~P,sh(~N,~R,~P,g,r,q),n,None{})
114 case Some{p}: sn(~N,~R,~P,sp(~N,~R,~P,sn(~N,~R,~P,g,p,q),n,None{}),n,None{})
115
116def cut(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, r: R, +n: N, +p: Maybe<&2,N>, +q: Maybe<&2,N>) -> Graph<N,R,P>:
117 cut_left(~N,~R,~P,optional_prev(~N,~R,~P,g,q,p),r,n,p,q)
118
119def prepend(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: Graph<N,R,P>, +r: R, n: N) -> Graph<N,R,P>:
120 attach(~N,~R,~P,g,r,n,head(~N,~R,~P,~req,g,r))
121
122def remove(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: Graph<N,R,P>, r: R, +n: N) -> Graph<N,R,P>:
123 cut(~N,~R,~P,g,r,n,prev(~N,~R,~P,~eq,g,n),next(~N,~R,~P,~eq,g,n))