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 mirror result's answer mapped: a refinement with the value v found
10	# gives one with the value's presence (changed_value) or its entry
11	# (entry_value). (source: tools/generators/tm_hand/mokx.src)
12	
13	
14	def cv_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m0: S.Model<K, V>, +m: ST.Sh<K, V>, +v: V, +sh2: ST.Sh<K, V>, +o: Maybe<&2, V>, +h1: {(ST.real(~K, ~V, ~cmp, m), Some{v}) == (ST.real(~K, ~V, ~cmp, sh2), o) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}, r: {(m0, Some{v}) == (ST.model(~K, ~V, ~cmp, sh2), o) : S.Model<K, V> & Maybe<&2, V>} & {ST.good(~K, ~V, ~cmp, sh2) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Bool, (m0, True{}), MI.changed_value(~K, ~V, ~cmp, (m, Some{v}))):
15	  match r:
16	    case Tuple{h2, hg}:
17	      +e1 = L.pair_fst(M.TreeMap<K, V, cmp>, Maybe<&2, V>, ST.real(~K, ~V, ~cmp, m), Some{v}, ST.real(~K, ~V, ~cmp, sh2), o, h1)
18	      +e2 = L.pair_fst(S.Model<K, V>, Maybe<&2, V>, m0, Some{v}, ST.model(~K, ~V, ~cmp, sh2), o, h2)
19	      (sh2, (True{}, (L.pair_eq(M.TreeMap<K, V, cmp>, Bool, ST.real(~K, ~V, ~cmp, m), True{}, ST.real(~K, ~V, ~cmp, sh2), True{}, e1, {==}), (L.pair_eq(S.Model<K, V>, Bool, m0, True{}, ST.model(~K, ~V, ~cmp, sh2), True{}, e2, {==}), hg))))
20	
21	# the value found: the answer is that something changed
22	def cv_mok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m0: S.Model<K, V>, +m: ST.Sh<K, V>, +v: V, p: OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (m0, Some{v}), (m, Some{v}))) -> OK.MOK(~K, ~V, ~cmp, Bool, (m0, True{}), MI.changed_value(~K, ~V, ~cmp, (m, Some{v}))):
23	  match p:
24	    case Tuple{+sh2, Tuple{+o, Tuple{+h1, r}}}:
25	      cv_r(~K, ~V, ~cmp, m0, m, v, sh2, o, h1, r)
26	
27	def ev_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m0: S.Model<K, V>, +m: ST.Sh<K, V>, +k: K, +v: V, +sh2: ST.Sh<K, V>, +o: Maybe<&2, V>, +h1: {(ST.real(~K, ~V, ~cmp, m), Some{v}) == (ST.real(~K, ~V, ~cmp, sh2), o) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}, r: {(m0, Some{v}) == (ST.model(~K, ~V, ~cmp, sh2), o) : S.Model<K, V> & Maybe<&2, V>} & {ST.good(~K, ~V, ~cmp, sh2) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, (m0, Some{M.Entry{k, v}}), MI.entry_value(~K, ~V, ~cmp, Some{k}, (m, Some{v}))):
28	  match r:
29	    case Tuple{h2, hg}:
30	      +e1 = L.pair_fst(M.TreeMap<K, V, cmp>, Maybe<&2, V>, ST.real(~K, ~V, ~cmp, m), Some{v}, ST.real(~K, ~V, ~cmp, sh2), o, h1)
31	      +e2 = L.pair_fst(S.Model<K, V>, Maybe<&2, V>, m0, Some{v}, ST.model(~K, ~V, ~cmp, sh2), o, h2)
32	      (sh2, (Some{M.Entry{k, v}}, (L.pair_eq(M.TreeMap<K, V, cmp>, Maybe<&2, M.Entry<K, V>>, ST.real(~K, ~V, ~cmp, m), Some{M.Entry{k, v}}, ST.real(~K, ~V, ~cmp, sh2), Some{M.Entry{k, v}}, e1, {==}), (L.pair_eq(S.Model<K, V>, Maybe<&2, M.Entry<K, V>>, m0, Some{M.Entry{k, v}}, ST.model(~K, ~V, ~cmp, sh2), Some{M.Entry{k, v}}, e2, {==}), hg))))
33	
34	# the value found: the answer is its entry
35	def ev_mok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m0: S.Model<K, V>, +m: ST.Sh<K, V>, +k: K, +v: V, p: OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (m0, Some{v}), (m, Some{v}))) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, (m0, Some{M.Entry{k, v}}), MI.entry_value(~K, ~V, ~cmp, Some{k}, (m, Some{v}))):
36	  match p:
37	    case Tuple{+sh2, Tuple{+o, Tuple{+h1, r}}}:
38	      ev_r(~K, ~V, ~cmp, m0, m, k, v, sh2, o, h1, r)