1	import Base
2	import ./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.
6	type Stack<-T: Data> is Type:
7	  ST{items: List<&2, T>, count: Nat}
8	
9	def new(~T: Data) -> Stack<T>:
10	  ST{Nil{}, 0n}
11	
12	def length(~T: Data, s: Stack<T>) -> Stack<T> & Nat:
13	  ST{xs, +n} = s
14	  (ST{xs, n}, n)
15	
16	def push(~T: Data, s: Stack<T>, x: T) -> Stack<T>:
17	  ST{xs, n} = s
18	  ST{Con{x, xs}, 1n+n}
19	
20	def 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	
27	def 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	
34	def 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	
40	def obs_nat(~T: Data, r: Stack<T> & Nat) -> Stack<T> & E.Obs<T>:
41	  (q, n) = r
42	  (q, E.ONat{n})
43	
44	def 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	
48	def 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	
52	def 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	
65	def 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	
69	def 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	
73	def 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	
80	def 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	
84	def 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{})))