1	import Base
2	import ../../lib/logic.bend as L
3	import ../../../spec/containers/balanced_search_tree/main.bend as S
4	import ../../../src/containers/balanced_search_tree.bend as M
5	import ./state.bend as ST
6	import ./mirror.bend as MI
7	import ./ok.bend as OK
8	
9	# A view's model and invariant, and the refinement of view results.
10	# (source: tools/generators/tm_hand/vdef.src)
11	
12	
13	# ---- a view's model and invariant ----
14	
15	def vmod(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: MI.MView<K, V>) -> S.View<K, V>:
16	  match w:
17	    case MI.MV{s, lo2, hi2, d2}:
18	      S.VW{ST.model(~K, ~V, ~cmp, s), lo2, hi2, d2}
19	
20	def vgood(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: MI.MView<K, V>) -> Bool:
21	  match w:
22	    case MI.MV{s, lo2, hi2, d2}:
23	      ST.good(~K, ~V, ~cmp, s)
24	
25	def vg_dg(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +w: MI.MView<K, V>, +h: {vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> {MI.dgv(K, V, w) == True{} : Bool}:
26	  match w:
27	    case MI.MV{+s, +lo2, +hi2, +d2}:
28	      OK.dg_good(~K, ~V, ~cmp, s, h)
29	
30	# a view refining a specification's
31	def VOK(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, sp: S.View<K, V>, r: M.View<K, V, cmp>) -> Type:
32	  Sigma<&1, &1, MI.MView<K, V>, w2 => {r == MI.rv(~K, ~V, ~cmp, w2) : M.View<K, V, cmp>} & ({sp == vmod(~K, ~V, ~cmp, w2) : S.View<K, V>} & {vgood(~K, ~V, ~cmp, w2) == True{} : Bool})>
33	
34	# a mirror view result refining a specification's
35	def VM(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Data, sp: S.View<K, V> & X, mir: MI.MView<K, V> & X) -> Type:
36	  Sigma<&1, &1, MI.MView<K, V>, w2 => Sigma<&1, &1, X, o => {MI.rvp(~K, ~V, ~cmp, X, mir) == (MI.rv(~K, ~V, ~cmp, w2), o) : M.View<K, V, cmp> & X} & ({sp == (vmod(~K, ~V, ~cmp, w2), o) : S.View<K, V> & X} & {vgood(~K, ~V, ~cmp, w2) == True{} : Bool})>>
37	
38	# an implementation view result refining a specification's
39	def VPOK(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Data, sp: S.View<K, V> & X, r: M.View<K, V, cmp> & X) -> Type:
40	  Sigma<&1, &1, MI.MView<K, V>, w2 => Sigma<&1, &1, X, o => {r == (MI.rv(~K, ~V, ~cmp, w2), o) : M.View<K, V, cmp> & X} & ({sp == (vmod(~K, ~V, ~cmp, w2), o) : S.View<K, V> & X} & {vgood(~K, ~V, ~cmp, w2) == True{} : Bool})>>
41	
42	def vm_pok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Data, -sp: S.View<K, V> & X, -mir: MI.MView<K, V> & X, -r: M.View<K, V, cmp> & X, +hs: {r == MI.rvp(~K, ~V, ~cmp, X, mir) : M.View<K, V, cmp> & X}, p: VM(~K, ~V, ~cmp, X, sp, mir)) -> VPOK(~K, ~V, ~cmp, X, sp, r):
43	  match p:
44	    case Tuple{+w2, Tuple{+o, Tuple{+h1, rest}}}:
45	      (w2, (o, (Equal.trans(M.View<K, V, cmp> & X, r, MI.rvp(~K, ~V, ~cmp, X, mir), (MI.rv(~K, ~V, ~cmp, w2), o), hs, h1), rest)))
46	
47	# a mirror result given exactly
48	def vm_exact(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Data, -sp: S.View<K, V> & X, -mir: MI.MView<K, V> & X, +w2: MI.MView<K, V>, +o: X, +hm: {mir == (w2, o) : MI.MView<K, V> & X}, +hs: {sp == (vmod(~K, ~V, ~cmp, w2), o) : S.View<K, V> & X}, +hg: {vgood(~K, ~V, ~cmp, w2) == True{} : Bool}) -> VM(~K, ~V, ~cmp, X, sp, mir):
49	  (w2, (o, (L.subst(MI.MView<K, V> & X, z => {MI.rvp(~K, ~V, ~cmp, X, z) == (MI.rv(~K, ~V, ~cmp, w2), o) : M.View<K, V, cmp> & X}, (w2, o), mir, Equal.sym(MI.MView<K, V> & X, mir, (w2, o), hm), {==}), (hs, hg))))
50