1	import Base
2	import ../../../spec/lib/common.bend as SC
3	import ../../../src/containers/queue.bend as Q
4	
5	# The two-list queue QU{front, back, count} as a Data shadow: the two lists,
6	# with the count their total length.
7	#   model(sh) = front ++ reverse(back)   the elements, oldest first
8	
9	type Shadow<-T: Data> is Data:
10	  Sh{front: List<&2, T>, back: List<&2, T>}
11	
12	def initial(-T: Data) -> Shadow<T>:
13	  Sh{Nil{}, Nil{}}
14	
15	def real(-T: Data, sh: Shadow<T>) -> Q.Queue<T>:
16	  match sh:
17	    case Sh{+f, +b}:
18	      Q.QU{f, b, Nat.add(SC.length(T, f), SC.length(T, b))}
19	
20	def model(-T: Data, sh: Shadow<T>) -> List<&2, T>:
21	  match sh:
22	    case Sh{f, b}:
23	      SC.append(T, f, SC.reverse(T, b))
24	
25	def unreal(-T: Data, q: Q.Queue<T>) -> Shadow<T>:
26	  Q.QU{f, b, n} = q
27	  Sh{f, b}
28	
29	def unreal_real(-T: Data, +sh: Shadow<T>) -> {unreal(T, real(T, sh)) == sh : Shadow<T>}:
30	  match sh:
31	    case Sh{f, b}:
32	      {==}
33	
34	# a queue determines its shadow
35	def real_inj(-T: Data, +a: Shadow<T>, +b: Shadow<T>, +e: {real(T, a) == real(T, b) : Q.Queue<T>}) -> {a == b : Shadow<T>}:
36	  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)),
37	    Equal.trans(Shadow<T>, unreal(T, real(T, a)), unreal(T, real(T, b)), b, Equal.cong(Q.Queue<T>, Shadow<T>, d => unreal(T, d), real(T, a), real(T, b), e), unreal_real(T, b)))