1	import Base
2	import ../../../spec/lib/common.bend as SC
3	import ../../../src/containers/deque.bend as DQ
4	
5	# The two-list deque DE{front, back, nf, nb} as a Data shadow: the two
6	# lists, with the counts their lengths (so the count invariant holds by
7	# construction).
8	#   model(sh) = front ++ reverse(back)   the elements, front first
9	
10	type Shadow<-T: Data> is Data:
11	  Sh{front: List<&2, T>, back: List<&2, T>}
12	
13	def initial(-T: Data) -> Shadow<T>:
14	  Sh{Nil{}, Nil{}}
15	
16	def real(-T: Data, sh: Shadow<T>) -> DQ.Deque<T>:
17	  match sh:
18	    case Sh{+f, +b}:
19	      DQ.DE{f, b, SC.length(T, f), SC.length(T, b)}
20	
21	def model(-T: Data, sh: Shadow<T>) -> List<&2, T>:
22	  match sh:
23	    case Sh{f, b}:
24	      SC.append(T, f, SC.reverse(T, b))
25	
26	def unreal(-T: Data, d: DQ.Deque<T>) -> Shadow<T>:
27	  DQ.DE{f, b, nf, nb} = d
28	  Sh{f, b}
29	
30	def unreal_real(-T: Data, +sh: Shadow<T>) -> {unreal(T, real(T, sh)) == sh : Shadow<T>}:
31	  match sh:
32	    case Sh{f, b}:
33	      {==}
34	
35	# a deque determines its shadow
36	def real_inj(-T: Data, +a: Shadow<T>, +b: Shadow<T>, +e: {real(T, a) == real(T, b) : DQ.Deque<T>}) -> {a == b : Shadow<T>}:
37	  Equal.trans(Shadow<T>, a, unreal(T, real(T, a)), b, Equal.sym(Shadow<T>, unreal(T, real(T, a)), a, unreal_real(T, a)),
38	    Equal.trans(Shadow<T>, unreal(T, real(T, a)), unreal(T, real(T, b)), b, Equal.cong(DQ.Deque<T>, Shadow<T>, d => unreal(T, d), real(T, a), real(T, b), e), unreal_real(T, b)))