src/queue.bend

bend-lawful-stdlib@0.1.0.0 · 95 lines · 10 definitions

1import Base
2import bend-lawful-stdlib@0.1.0.0/src/list.bend as List
3
4# queue.bend: a FIFO queue as two lists, specified by the list it holds.
5#
6#   import ./queue.bend as Q
7#
8# push conses onto rear; pop takes from front, and when front is empty the
9# reversed rear becomes the new front. Queue is linear (Type), so each
10# queue value is used once; then each element is reversed at most once and
11# every operation costs O(1) on average.
12#
13# model(q) is the list q holds. push_model and pop_model state push and
14# pop in terms of it.
15
16type Queue<-A: Data> is Type:
17  Queue{front: List<&2, A>, rear: List<&2, A>}
18
19def empty(-A: Data) -> Queue<A>:
20  Queue{Nil{}, Nil{}}
21
22def model(-A: Data, q: Queue<A>) -> List<&2, A>:
23  match q:
24    case Queue{f, r}:
25      List.append(&2, A, f, List.reverse(&2, A, r))
26
27def push(-A: Data, q: Queue<A>, x: A) -> Queue<A>:
28  match q:
29    case Queue{f, r}:
30      Queue{f, x <> r}
31
32# front is empty; f is the reversed rear
33def pop.rot(-A: Data, f: List<&2, A>) -> List.Step<&1, A, Queue<A>>:
34  match f:
35    case Nil{}:
36      List.Stop{}
37    case h <> t:
38      List.Next{h, Queue{t, Nil{}}}
39
40def pop(-A: Data, q: Queue<A>) -> List.Step<&1, A, Queue<A>>:
41  match q:
42    case Queue{Nil{}, r}:
43      pop.rot(A, List.reverse(&2, A, r))
44    case Queue{h <> t, r}:
45      List.Next{h, Queue{t, r}}
46
47# pop's result with the remaining queue replaced by its model
48def pop.model(-A: Data, s: List.Step<&1, A, Queue<A>>) -> List.Step<&2, A, List<&2, A>>:
49  match s:
50    case List.Stop{}:
51      List.Stop{}
52    case List.Next{x, q}:
53      List.Next{x, model(A, q)}
54
55# push appends x to the model.
56law push_model:
57  for -A: Data
58  for q: Queue<A>
59  for +x: A
60  {List.append(&2, A, model(A, q), [x]) == model(A, push(A, q, x)) : List<&2, A>}
61
62def push_model(A, q, x):
63  match q:
64    case Queue{+f, +r}:
65      %List.reverse_go(A, r, [x]) : {List.append(&2, A, List.append(&2, A, f, List.reverse(&2, A, r)), [x]) == List.append(&2, A, f, _) : List<&2, A>}
66      Equal.sym(List<&2, A>,
67        List.append(&2, A, f, List.append(&2, A, List.reverse(&2, A, r), [x])),
68        List.append(&2, A, List.append(&2, A, f, List.reverse(&2, A, r)), [x]),
69        List.append_assoc(A, f, List.reverse(&2, A, r), [x]))
70
71law pop_model.rot:
72  for -A: Data
73  for f: List<&2, A>
74  {List.uncons(A, f) == pop.model(A, pop.rot(A, f)) : List.Step<&2, A, List<&2, A>>}
75
76def pop_model.rot(A, f):
77  match f:
78    case Nil{}:
79      {==}
80    case h <> t:
81      %List.append_nil(A, t) : {List.Next{h, t} == List.Next{h, _} : List.Step<&2, A, List<&2, A>>}
82      {==}
83
84# pop returns the model's head and tail.
85law pop_model:
86  for -A: Data
87  for q: Queue<A>
88  {List.uncons(A, model(A, q)) == pop.model(A, pop(A, q)) : List.Step<&2, A, List<&2, A>>}
89
90def pop_model(A, q):
91  match q:
92    case Queue{Nil{}, r}:
93      pop_model.rot(A, List.reverse(&2, A, r))
94    case Queue{h <> t, r}:
95      {==}