src/containers/queue.bend
bend-collections-laws-containers@1.0.0.0 · 99 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/types/queue.bend as E
3
4# Two-list FIFO queue: front ++ reverse(back). Reverse back only when front
5# is empty. Enqueue/dequeue/peek are amortized O(1) on consumed histories.
6# length is cached; to_list is O(n). Independent of the deque and DLL.
7type Queue<-T: Data> is Type:
8 QU{front: List<&2, T>, back: List<&2, T>, count: Nat}
9
10def new(~T: Data) -> Queue<T>:
11 QU{Nil{}, Nil{}, 0n}
12
13def length(~T: Data, q: Queue<T>) -> Queue<T> & Nat:
14 QU{f, b, +n} = q
15 (QU{f, b, n}, n)
16
17def enqueue(~T: Data, q: Queue<T>, x: T) -> Queue<T>:
18 QU{f, b, n} = q
19 QU{f, Con{x, b}, 1n+n}
20
21def ready(~T: Data, q: Queue<T>) -> Queue<T>:
22 match q:
23 case QU{Nil{}, b, n}:
24 QU{List.reverse(&2, T, b), Nil{}, n}
25 case QU{Con{x, f}, b, n}:
26 QU{Con{x, f}, b, n}
27
28def dequeue_ready(~T: Data, q: Queue<T>) -> Queue<T> & Result<&2, &2, E.Error, T>:
29 match q:
30 case QU{Nil{}, b, n}:
31 (QU{Nil{}, b, n}, Fail{E.EmptyQueue{}})
32 case QU{Con{x, f}, b, n}:
33 (QU{f, b, Nat.sub(n, 1n)}, Done{x})
34
35def peek_ready(~T: Data, q: Queue<T>) -> Queue<T> & Result<&2, &2, E.Error, T>:
36 match q:
37 case QU{Nil{}, b, n}:
38 (QU{Nil{}, b, n}, Fail{E.EmptyQueue{}})
39 case QU{Con{+x, f}, b, n}:
40 (QU{Con{x, f}, b, n}, Done{x})
41
42def dequeue(~T: Data, q: Queue<T>) -> Queue<T> & Result<&2, &2, E.Error, T>:
43 dequeue_ready(~T, ready(~T, q))
44
45def peek(~T: Data, q: Queue<T>) -> Queue<T> & Result<&2, &2, E.Error, T>:
46 peek_ready(~T, ready(~T, q))
47
48def to_list(~T: Data, q: Queue<T>) -> Queue<T> & List<&2, T>:
49 QU{+f, +b, n} = q
50 (QU{f, b, n}, List.append(&2, T, f, List.reverse(&2, T, b)))
51
52# ---- operation traces ----
53
54def obs_nat(~T: Data, r: Queue<T> & Nat) -> Queue<T> & E.Obs<T>:
55 (q, n) = r
56 (q, E.ONat{n})
57
58def obs_item(~T: Data, r: Queue<T> & Result<&2, &2, E.Error, T>) -> Queue<T> & E.Obs<T>:
59 (q, x) = r
60 (q, E.OItem{x})
61
62def obs_list(~T: Data, r: Queue<T> & List<&2, T>) -> Queue<T> & E.Obs<T>:
63 (q, xs) = r
64 (q, E.OList{xs})
65
66def step(~T: Data, q: Queue<T>, op: E.Op<T>) -> Queue<T> & E.Obs<T>:
67 match op:
68 case E.Length{}:
69 obs_nat(~T, length(~T, q))
70 case E.Enqueue{+x}:
71 (enqueue(~T, q, x), E.OUnit{})
72 case E.Dequeue{}:
73 obs_item(~T, dequeue(~T, q))
74 case E.Peek{}:
75 obs_item(~T, peek(~T, q))
76 case E.ToList{}:
77 obs_list(~T, to_list(~T, q))
78
79def record(~T: Data, acc: List<&2, E.Obs<T>>, r: Queue<T> & E.Obs<T>) -> Queue<T> & List<&2, E.Obs<T>>:
80 (q, o) = r
81 (q, Con{o, acc})
82
83def step_acc(~T: Data, op: E.Op<T>, st: Queue<T> & List<&2, E.Obs<T>>) -> Queue<T> & List<&2, E.Obs<T>>:
84 (q, acc) = st
85 record(~T, acc, step(~T, q, op))
86
87def run_acc(~T: Data, ops: List<&2, E.Op<T>>, st: Queue<T> & List<&2, E.Obs<T>>) -> Queue<T> & List<&2, E.Obs<T>>:
88 match ops:
89 case Nil{}:
90 st
91 case Con{op, rest}:
92 run_acc(~T, rest, step_acc(~T, op, st))
93
94def finish(~T: Data, st: Queue<T> & List<&2, E.Obs<T>>) -> Queue<T> & List<&2, E.Obs<T>>:
95 (q, acc) = st
96 (q, List.reverse(&2, E.Obs<T>, acc))
97
98def run(~T: Data, ops: List<&2, E.Op<T>>, q: Queue<T>) -> Queue<T> & List<&2, E.Obs<T>>:
99 finish(~T, run_acc(~T, ops, (q, Nil{})))