1	import Base
2	import ../../../src/containers/stack.bend as D
3	import ../../../spec/containers/stack.bend as S
4	import ../../../spec/lib/common.bend as C
5	import ../../../src/containers/types/stack.bend as E
6	import ../../lib/nat.bend as N
7	import ../../lib/logic.bend as L
8	import ../../../spec/lib/sequence.bend as V
9	import ../../lib/sequence.bend as VL
10	
11	# Universal one-step refinement, including cached count preservation and
12	# empty errors. Concrete instances in STACK_COMPONENT_PROOF.bend.
13	def real(~T: Data, +xs: List<&2, T>) -> D.Stack<T>:
14	  D.ST{xs, C.length(T, xs)}
15	
16	def lift(~T: Data, r: List<&2, T> & E.Obs<T>) -> D.Stack<T> & E.Obs<T>:
17	  (xs, obs) = r
18	  (real(~T, xs), obs)
19	
20	def step_correct(~T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> {D.step(~T, real(~T, xs), op) == lift(~T, S.step(T, xs, op)) : D.Stack<T> & E.Obs<T>}:
21	  match xs op:
22	    case Nil{} E.Push{v}:
23	      {==}
24	    case Nil{} E.Length{}:
25	      {==}
26	    case Nil{} E.ToList{}:
27	      {==}
28	    case Nil{} E.Peek{}:
29	      {==}
30	    case Nil{} E.Pop{}:
31	      {==}
32	    case Con{+x, +tail} E.Push{v}:
33	      {==}
34	    case Con{+x, +tail} E.Length{}:
35	      {==}
36	    case Con{+x, +tail} E.ToList{}:
37	      {==}
38	    case Con{+x, +tail} E.Peek{}:
39	      {==}
40	    case Con{+x, +tail} E.Pop{}:
41	      Equal.cong(Nat, D.Stack<T> & E.Obs<T>, n => (D.ST{tail, n}, E.OItem{Done{x}}), Nat.sub(C.length(T, tail), 0n), C.length(T, tail), N.sub_zero(C.length(T, tail)))
42	
43	def constructor(~T: Data) -> {D.new(~T) == real(~T, Nil{}) : D.Stack<T>}:
44	  {==}
45	
46	# ==== the contract of stack (stated in spec/containers/stack.bend) ====================
47	
48	# ---- the implementation ----
49	def impl(~T: Data, +xs: List<&2, T>, +op: E.Op<T>, -Post: (D.Stack<T> & E.Obs<T>) -> Type, pf: Post(lift(~T, S.step(T, xs, op)))) -> Post(D.step(~T, real(~T, xs), op)):
50	  L.subst(D.Stack<T> & E.Obs<T>, Post, lift(~T, S.step(T, xs, op)), D.step(~T, real(~T, xs), op), Equal.sym(D.Stack<T> & E.Obs<T>, D.step(~T, real(~T, xs), op), lift(~T, S.step(T, xs, op)), step_correct(~T, xs, op)), pf)
51	
52	# ---- Length, iteration ----
53	def length_result(-T: Data, +xs: List<&2, T>) -> S.Length.length_result(T, xs):
54	  match xs:
55	    case Nil{}:
56	      {==}
57	    case Con{h, t}:
58	      {==}
59	
60	def length_frame(-T: Data, +xs: List<&2, T>) -> S.Length.length_frame(T, xs):
61	  match xs:
62	    case Nil{}:
63	      {==}
64	    case Con{h, t}:
65	      {==}
66	
67	def to_list_model(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_model(T, xs):
68	  match xs:
69	    case Nil{}:
70	      {==}
71	    case Con{h, t}:
72	      {==}
73	
74	def to_list_frame(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_frame(T, xs):
75	  match xs:
76	    case Nil{}:
77	      {==}
78	    case Con{h, t}:
79	      {==}
80	
81	# ---- Empty_Vector ----
82	def new_empty(-T: Data) -> S.Empty_Vector.new_empty(T):
83	  {==}
84	
85	def new_impl(~T: Data) -> {D.new(~T) == real(~T, Nil{}) : D.Stack<T>}:
86	  constructor(~T)
87	
88	# ---- Prepend: Length + 1, Element (First) = New_Item, Range_Shifted (Old, New, First, Last'Old, 1) ----
89	def push_length(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_length(T, xs, v):
90	  match xs:
91	    case Nil{}:
92	      {==}
93	    case Con{h, t}:
94	      {==}
95	
96	def push_first(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_first(T, xs, v):
97	  match xs:
98	    case Nil{}:
99	      {==}
100	    case Con{h, t}:
101	      {==}
102	
103	def push_is(-T: Data, +xs: List<&2, T>, +v: T) -> {S.nx(T, xs, E.Push{v}) == Con{v, xs} : List<&2, T>}:
104	  match xs:
105	    case Nil{}:
106	      {==}
107	    case Con{h, t}:
108	      {==}
109	
110	def push_shifted(-T: Data, +xs: List<&2, T>, +v: T) -> S.Prepend.push_shifted(T, xs, v):
111	  L.subst(List<&2, T>, z => V.RangeShifted(T, xs, z, 0n, C.length(T, xs), 1n), Con{v, xs}, S.nx(T, xs, E.Push{v}), Equal.sym(List<&2, T>, S.nx(T, xs, E.Push{v}), Con{v, xs}, push_is(T, xs, v)), VL.cons_shifted(T, xs, v))
112	
113	# ---- Delete_First: Length - 1, Range_Shifted (New, Old, First, Last, 1); pop returns First_Element'Old ----
114	def pop_length(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_length(T, h, t):
115	  {==}
116	
117	def pop_shifted(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_shifted(T, h, t):
118	  VL.tail_shifted(T, h, t)
119	
120	def pop_result(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.pop_result(T, h, t):
121	  {==}
122	
123	def pop_empty(-T: Data) -> S.Delete_First.pop_empty(T):
124	  {==}
125	
126	# ---- First_Element: Element (Model, First); nothing changes ----
127	def peek_first(-T: Data, +h: T, +t: List<&2, T>) -> S.First_Element.peek_first(T, h, t):
128	  ({==}, {==})
129	
130	def peek_frame(-T: Data, +xs: List<&2, T>) -> S.First_Element.peek_frame(T, xs):
131	  match xs:
132	    case Nil{}:
133	      {==}
134	    case Con{h, t}:
135	      {==}
136	
137	def peek_empty(-T: Data) -> S.First_Element.peek_empty(T):
138	  {==}