spec/containers/intrusive_doubly_linked_list/programs.bend

bend-collections-laws-containers@1.0.0.0 · 45 lines · 0 definitions

1import Base
2
3# Independent write programs. These describe field updates and root hooks,
4# without importing the implementation or its generated helpers.
5type Edit<-N: Data, -I: Data> is Data:
6  Next{node: N, link: Maybe<&2, N>}
7  Prev{node: N, link: Maybe<&2, N>}
8  Head{root: I, link: Maybe<&2, N>}
9  Nonempty{root: I, node: N}
10
11def remove(-N: Data, -I: Data, +root: I, +node: N, +before: Maybe<&2, N>, +after: Maybe<&2, N>) -> List<&2, Edit<N, I>>:
12  match before after:
13    case None{} None{}:
14      Con{Head{root, None{}}, Con{Next{node, None{}}, Nil{}}}
15    case None{} Some{+q}:
16      Con{Prev{q, None{}}, Con{Head{root, Some{q}}, Con{Next{node, None{}}, Nil{}}}}
17    case Some{p} None{}:
18      Con{Next{p, None{}}, Con{Prev{node, None{}}, Con{Next{node, None{}}, Nil{}}}}
19    case Some{p} Some{+q}:
20      Con{Prev{q, Some{p}}, Con{Next{p, Some{q}}, Con{Prev{node, None{}}, Con{Next{node, None{}}, Nil{}}}}}
21
22def prepend(-N: Data, -I: Data, root: I, +node: N, head: Maybe<&2, N>) -> List<&2, Edit<N, I>>:
23  match head:
24    case None{}:
25      Con{Next{node, None{}}, Con{Nonempty{root, node}, Nil{}}}
26    case Some{+h}:
27      Con{Next{node, Some{h}}, Con{Prev{h, Some{node}}, Con{Nonempty{root, node}, Nil{}}}}
28
29def apply(~S: Type, ~N: Data, ~I: Data, ~sn: S -> N -> Maybe<&2, N> -> S, ~sp: S -> N -> Maybe<&2, N> -> S, ~sh: S -> I -> Maybe<&2, N> -> S, ~sf: S -> I -> N -> S, s: S, e: Edit<N, I>) -> S:
30  match e:
31    case Next{n, m}: sn(s, n, m)
32    case Prev{n, m}: sp(s, n, m)
33    case Head{i, m}: sh(s, i, m)
34    case Nonempty{i, n}: sf(s, i, n)
35
36def run(~S: Type, ~N: Data, ~I: Data, ~sn: S -> N -> Maybe<&2, N> -> S, ~sp: S -> N -> Maybe<&2, N> -> S, ~sh: S -> I -> Maybe<&2, N> -> S, ~sf: S -> I -> N -> S, edits: List<&2, Edit<N, I>>, s: S) -> S:
37  match edits:
38    case Nil{}: s
39    case Con{e, rest}: run(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf, rest, apply(~S, ~N, ~I, ~sn, ~sp, ~sh, ~sf, s, e))
40
41# Exact ordered callback sequence for clear; no writes on the empty list.
42def clear_order(-N: Data, nodes: List<&2, N>) -> List<&2, N>:
43  match nodes:
44    case Nil{}: Nil{}
45    case Con{h, rest}: List.append(&2, N, rest, Con{h, Nil{}})