src/containers/stack.bend
bend-collections-laws-containers@1.0.0.0 · 85 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/types/stack.bend as E
3
4# Stack over the native singly linked List, with a stored length.
5# Push/pop/peek/length O(1); to_list shares immutable Data elements/list.
6type Stack<-T: Data> is Type:
7 ST{items: List<&2, T>, count: Nat}
8
9def new(~T: Data) -> Stack<T>:
10 ST{Nil{}, 0n}
11
12def length(~T: Data, s: Stack<T>) -> Stack<T> & Nat:
13 ST{xs, +n} = s
14 (ST{xs, n}, n)
15
16def push(~T: Data, s: Stack<T>, x: T) -> Stack<T>:
17 ST{xs, n} = s
18 ST{Con{x, xs}, 1n+n}
19
20def pop(~T: Data, s: Stack<T>) -> Stack<T> & Result<&2, &2, E.Error, T>:
21 match s:
22 case ST{Nil{}, n}:
23 (ST{Nil{}, n}, Fail{E.EmptyStack{}})
24 case ST{Con{x, xs}, n}:
25 (ST{xs, Nat.sub(n, 1n)}, Done{x})
26
27def peek(~T: Data, s: Stack<T>) -> Stack<T> & Result<&2, &2, E.Error, T>:
28 match s:
29 case ST{Nil{}, n}:
30 (ST{Nil{}, n}, Fail{E.EmptyStack{}})
31 case ST{Con{+x, xs}, n}:
32 (ST{Con{x, xs}, n}, Done{x})
33
34def to_list(~T: Data, s: Stack<T>) -> Stack<T> & List<&2, T>:
35 ST{+xs, n} = s
36 (ST{xs, n}, xs)
37
38# ---- operation traces ----
39
40def obs_nat(~T: Data, r: Stack<T> & Nat) -> Stack<T> & E.Obs<T>:
41 (q, n) = r
42 (q, E.ONat{n})
43
44def obs_item(~T: Data, r: Stack<T> & Result<&2, &2, E.Error, T>) -> Stack<T> & E.Obs<T>:
45 (q, x) = r
46 (q, E.OItem{x})
47
48def obs_list(~T: Data, r: Stack<T> & List<&2, T>) -> Stack<T> & E.Obs<T>:
49 (q, xs) = r
50 (q, E.OList{xs})
51
52def step(~T: Data, q: Stack<T>, op: E.Op<T>) -> Stack<T> & E.Obs<T>:
53 match op:
54 case E.Length{}:
55 obs_nat(~T, length(~T, q))
56 case E.Push{+x}:
57 (push(~T, q, x), E.OUnit{})
58 case E.Pop{}:
59 obs_item(~T, pop(~T, q))
60 case E.Peek{}:
61 obs_item(~T, peek(~T, q))
62 case E.ToList{}:
63 obs_list(~T, to_list(~T, q))
64
65def record(~T: Data, acc: List<&2, E.Obs<T>>, r: Stack<T> & E.Obs<T>) -> Stack<T> & List<&2, E.Obs<T>>:
66 (q, o) = r
67 (q, Con{o, acc})
68
69def step_acc(~T: Data, op: E.Op<T>, st: Stack<T> & List<&2, E.Obs<T>>) -> Stack<T> & List<&2, E.Obs<T>>:
70 (q, acc) = st
71 record(~T, acc, step(~T, q, op))
72
73def run_acc(~T: Data, ops: List<&2, E.Op<T>>, st: Stack<T> & List<&2, E.Obs<T>>) -> Stack<T> & List<&2, E.Obs<T>>:
74 match ops:
75 case Nil{}:
76 st
77 case Con{op, rest}:
78 run_acc(~T, rest, step_acc(~T, op, st))
79
80def finish(~T: Data, st: Stack<T> & List<&2, E.Obs<T>>) -> Stack<T> & List<&2, E.Obs<T>>:
81 (q, acc) = st
82 (q, List.reverse(&2, E.Obs<T>, acc))
83
84def run(~T: Data, ops: List<&2, E.Op<T>>, q: Stack<T>) -> Stack<T> & List<&2, E.Obs<T>>:
85 finish(~T, run_acc(~T, ops, (q, Nil{})))