1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../../spec/lib/common.bend as SC
5	import ../../../src/containers/balanced_search_tree.bend as M
6	import ./state.bend as ST
7	import ./mirror.bend as MI
8	import ./tree.bend as TR
9	import ./path.bend as P
10	import ./nbr.bend as NB
11	import ../../lib/nat_list.bend as NL
12	
13	# Navigation (floor, ceiling, lower, higher): the loop descends by
14	# comparison keeping the best candidate, which along the path is the first
15	# id after (upward) or the last before (downward) the current subtree; at an
16	# equal key it answers the node (inclusive) or its neighbour. The loop is
17	# the ghost navigation gnav. (source: tools/generators/tm_hand/nav.src)
18	
19	
20	def gnav(~K: Data, ~cmp: K -> K -> Cmp, t: ST.Tr, +c: List<&2, P.Fr>, +nl: List<&2, M.Node<K>>, +k: K, +h: Bool, +incl: Bool) -> Nat:
21	  match t:
22	    case ST.TE{}:
23	      ST.pk(Nat, h, ST.fst0(P.after(c)), ST.last0(P.before(c)))
24	    case ST.TN{+i, +l, +r}:
25	      TR.pk3(Nat, TR.kc(~K, ~cmp, k, ST.nd(K, nl, i)), gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl), gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl), ST.pk(Nat, incl, i, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))))
26	
27	
28	# the candidate after a step left / right
29	def best_l(+h: Bool, +i: Nat, +a: Nat, +b: Nat) -> {M.pick(Nat, h, i, ST.pk(Nat, h, a, b)) == ST.pk(Nat, h, i, b) : Nat}:
30	  match h:
31	    case True{}:
32	      {==}
33	    case False{}:
34	      {==}
35	
36	def best_r(+h: Bool, +i: Nat, +a: Nat, +b: Nat) -> {M.pick(Nat, h, ST.pk(Nat, h, a, b), i) == ST.pk(Nat, h, a, i) : Nat}:
37	  match h:
38	    case True{}:
39	      {==}
40	    case False{}:
41	      {==}
42	
43	def nav_eq(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l0: Nat, +d0: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +i: Nat, +h: Bool, +incl: Bool, +v: Nat, +e: {MI.neighbor(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, i, h) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, v) : ST.Sh<K, V> & Nat}) -> {MI.nav_equal(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, i, h, incl) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, ST.pk(Nat, incl, i, v)) : ST.Sh<K, V> & Nat}:
44	  match incl:
45	    case True{}:
46	      {==}
47	    case False{}:
48	      e
49	
50	
51	def nav_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l0: Nat, +d0: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +c: List<&2, P.Fr>, +i: Nat, +l: ST.Tr, +r: ST.Tr, +k: K, +h: Bool, +incl: Bool, +g: Nat, +cc: Bool, +a: Nat, +b: Nat, +q: Nat, +key: K, +ea: {a == ST.rid(l) : Nat}, +eb: {b == ST.rid(r) : Nat}, +ihl: {MI.nav_loop(~K, ~V, ~cmp, g, k, h, incl, ST.rid(l), ST.pk(Nat, h, i, ST.last0(P.before(c))), MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, ST.rid(l), k)) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl)) : ST.Sh<K, V> & Nat}, +ihr: {MI.nav_loop(~K, ~V, ~cmp, g, k, h, incl, ST.rid(r), ST.pk(Nat, h, ST.fst0(P.after(c)), i), MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, ST.rid(r), k)) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl)) : ST.Sh<K, V> & Nat}, +ne: {MI.neighbor(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, i, h) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))) : ST.Sh<K, V> & Nat}, +o: Cmp) -> {MI.nav_loop(~K, ~V, ~cmp, 1n+g, k, h, incl, i, ST.pk(Nat, h, ST.fst0(P.after(c)), ST.last0(P.before(c))), (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, (M.N{cc, a, b, q, key}, o))) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, TR.pk3(Nat, o, gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl), gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl), ST.pk(Nat, incl, i, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))))) : ST.Sh<K, V> & Nat}:
52	  match o:
53	    case LT{}:
54	      %Equal.sym(Nat, a, ST.rid(l), ea) : {MI.nav_loop(~K, ~V, ~cmp, g, k, h, incl, _, M.pick(Nat, h, i, ST.pk(Nat, h, ST.fst0(P.after(c)), ST.last0(P.before(c)))), MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, _, k)) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl)) : ST.Sh<K, V> & Nat}
55	      %Equal.sym(Nat, M.pick(Nat, h, i, ST.pk(Nat, h, ST.fst0(P.after(c)), ST.last0(P.before(c)))), ST.pk(Nat, h, i, ST.last0(P.before(c))), best_l(h, i, ST.fst0(P.after(c)), ST.last0(P.before(c)))) : {MI.nav_loop(~K, ~V, ~cmp, g, k, h, incl, ST.rid(l), _, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, ST.rid(l), k)) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl)) : ST.Sh<K, V> & Nat}
56	      ihl
57	    case GT{}:
58	      %Equal.sym(Nat, b, ST.rid(r), eb) : {MI.nav_loop(~K, ~V, ~cmp, g, k, h, incl, _, M.pick(Nat, h, ST.pk(Nat, h, ST.fst0(P.after(c)), ST.last0(P.before(c))), i), MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, _, k)) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl)) : ST.Sh<K, V> & Nat}
59	      %Equal.sym(Nat, M.pick(Nat, h, ST.pk(Nat, h, ST.fst0(P.after(c)), ST.last0(P.before(c))), i), ST.pk(Nat, h, ST.fst0(P.after(c)), i), best_r(h, i, ST.fst0(P.after(c)), ST.last0(P.before(c)))) : {MI.nav_loop(~K, ~V, ~cmp, g, k, h, incl, ST.rid(r), _, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, ST.rid(r), k)) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl)) : ST.Sh<K, V> & Nat}
60	      ihr
61	    case EQ{}:
62	      nav_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l0, d0, nl, pl, tg, fl, i, h, incl, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l)))), ne)
63	
64	def nav_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l0: Nat, +d0: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +c: List<&2, P.Fr>, +i: Nat, +l: ST.Tr, +r: ST.Tr, +k: K, +h: Bool, +incl: Bool, +g: Nat, +x: M.Node<K>, +hx: {ST.is_node(K, x, ST.rid(l), ST.rid(r), P.top(c)) == True{} : Bool}, +ihl: {MI.nav_loop(~K, ~V, ~cmp, g, k, h, incl, ST.rid(l), ST.pk(Nat, h, i, ST.last0(P.before(c))), MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, ST.rid(l), k)) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl)) : ST.Sh<K, V> & Nat}, +ihr: {MI.nav_loop(~K, ~V, ~cmp, g, k, h, incl, ST.rid(r), ST.pk(Nat, h, ST.fst0(P.after(c)), i), MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, ST.rid(r), k)) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl)) : ST.Sh<K, V> & Nat}, +ne: {MI.neighbor(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, i, h) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))) : ST.Sh<K, V> & Nat}) -> {MI.nav_loop(~K, ~V, ~cmp, 1n+g, k, h, incl, i, ST.pk(Nat, h, ST.fst0(P.after(c)), ST.last0(P.before(c))), MI.probe_node(~K, ~V, ~cmp, i, k, (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, x))) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, TR.pk3(Nat, TR.kc(~K, ~cmp, k, x), gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl), gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl), ST.pk(Nat, incl, i, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))))) : ST.Sh<K, V> & Nat}:
65	  match x:
66	    case M.Free{fx}:
67	      Empty.absurd({MI.nav_loop(~K, ~V, ~cmp, 1n+g, k, h, incl, i, ST.pk(Nat, h, ST.fst0(P.after(c)), ST.last0(P.before(c))), MI.probe_node(~K, ~V, ~cmp, i, k, (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, M.Free{fx}))) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, TR.pk3(Nat, EQ{}, gnav(~K, ~cmp, l, Con{P.FR{i, True{}, r}, c}, nl, k, h, incl), gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl), ST.pk(Nat, incl, i, ST.pk(Nat, h, ST.fst0(SC.append(Nat, ST.ids(r), P.after(c))), ST.last0(SC.append(Nat, P.before(c), ST.ids(l))))))) : ST.Sh<K, V> & Nat}, L.false_true(hx))
68	    case M.N{+cc, +a, +b, +q, +key}:
69	      +ha = L.and_left(Nat.is_eq(a, ST.rid(l)), Bool.and(Nat.is_eq(b, ST.rid(r)), Nat.is_eq(q, P.top(c))), hx)
70	      +hb = L.and_left(Nat.is_eq(b, ST.rid(r)), Nat.is_eq(q, P.top(c)), L.and_right(Nat.is_eq(a, ST.rid(l)), Bool.and(Nat.is_eq(b, ST.rid(r)), Nat.is_eq(q, P.top(c))), hx))
71	      nav_c(~K, ~V, ~cmp, n, root, lo, hi, free, l0, d0, nl, pl, tg, fl, c, i, l, r, k, h, incl, g, cc, a, b, q, key, N.eq_from_is_eq(a, ST.rid(l), ha), N.eq_from_is_eq(b, ST.rid(r), hb), ihl, ihr, ne, cmp(k, key))
72	
73	
74	# the loop from a subtree the path leads to is the ghost navigation
75	def nav_ptr(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l0: Nat, +d0: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +f: Nat, +c: List<&2, P.Fr>, +t: ST.Tr, +k: K, +h: Bool, +incl: Bool, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c)))) == True{} : Bool}, +hid: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hn: {n == SC.length(Nat, ST.ids(tg)) : Nat}, +hf: {Nat.is_lt(TR.ht(t), f) == True{} : Bool}) -> {MI.nav_loop(~K, ~V, ~cmp, f, k, h, incl, ST.rid(t), ST.pk(Nat, h, ST.fst0(P.after(c)), ST.last0(P.before(c))), MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, ST.rid(t), k)) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, gnav(~K, ~cmp, t, c, nl, k, h, incl)) : ST.Sh<K, V> & Nat}:
76	  match f t:
77	    case 0n +t:
78	      Empty.absurd({MI.nav_loop(~K, ~V, ~cmp, 0n, k, h, incl, ST.rid(t), ST.pk(Nat, h, ST.fst0(P.after(c)), ST.last0(P.before(c))), MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, ST.rid(t), k)) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, gnav(~K, ~cmp, t, c, nl, k, h, incl)) : ST.Sh<K, V> & Nat}, L.true_not_false(Nat.is_lt(TR.ht(t), 0n), hf, N.not_lt_zero(TR.ht(t))))
79	    case 1n+g ST.TE{}:
80	      {==}
81	    case 1n+g ST.TN{+i, +l, +r}:
82	      +el = P.ids_l(c, i, l, r)
83	      +er = P.ids_r(c, i, l, r)
84	      +ihl = nav_ptr(~K, ~V, ~cmp, n, root, lo, hi, free, l0, d0, nl, pl, tg, fl, g, Con{P.FR{i, True{}, r}, c}, l, k, h, incl, Pair.snd({P.ctxok(~K, Con{P.FR{i, True{}, r}, c}, ST.rid(l), nl) == True{} : Bool}, {ST.rep(~K, l, i, nl) == True{} : Bool}, P.ok_l(~K, nl, c, i, l, r, hr, hok)), Pair.fst({P.ctxok(~K, Con{P.FR{i, True{}, r}, c}, ST.rid(l), nl) == True{} : Bool}, {ST.rep(~K, l, i, nl) == True{} : Bool}, P.ok_l(~K, nl, c, i, l, r, hr, hok)), L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), SC.append(Nat, P.before(Con{P.FR{i, True{}, r}, c}), SC.append(Nat, ST.ids(l), P.after(Con{P.FR{i, True{}, r}, c}))), el, hnd), Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), SC.append(Nat, P.before(Con{P.FR{i, True{}, r}, c}), SC.append(Nat, ST.ids(l), P.after(Con{P.FR{i, True{}, r}, c}))), hid, el), hn, TR.ht_l(i, l, r, g, hf))
85	      +ihr0 = nav_ptr(~K, ~V, ~cmp, n, root, lo, hi, free, l0, d0, nl, pl, tg, fl, g, Con{P.FR{i, False{}, l}, c}, r, k, h, incl, Pair.snd({P.ctxok(~K, Con{P.FR{i, False{}, l}, c}, ST.rid(r), nl) == True{} : Bool}, {ST.rep(~K, r, i, nl) == True{} : Bool}, P.ok_r(~K, nl, c, i, l, r, hr, hok)), Pair.fst({P.ctxok(~K, Con{P.FR{i, False{}, l}, c}, ST.rid(r), nl) == True{} : Bool}, {ST.rep(~K, r, i, nl) == True{} : Bool}, P.ok_r(~K, nl, c, i, l, r, hr, hok)), L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), SC.append(Nat, P.before(Con{P.FR{i, False{}, l}, c}), SC.append(Nat, ST.ids(r), P.after(Con{P.FR{i, False{}, l}, c}))), er, hnd), Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), P.after(c))), SC.append(Nat, P.before(Con{P.FR{i, False{}, l}, c}), SC.append(Nat, ST.ids(r), P.after(Con{P.FR{i, False{}, l}, c}))), hid, er), hn, TR.ht_r(i, l, r, g, hf))
86	      +ihr = L.subst(Nat, z => {MI.nav_loop(~K, ~V, ~cmp, g, k, h, incl, ST.rid(r), ST.pk(Nat, h, ST.fst0(P.after(c)), z), MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, ST.rid(r), k)) == (ST.SH{n, root, lo, hi, free, l0, d0, nl, pl, tg, fl}, gnav(~K, ~cmp, r, Con{P.FR{i, False{}, l}, c}, nl, k, h, incl)) : ST.Sh<K, V> & Nat}, ST.last0(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(l), Con{i, Nil{}}))), i, NB.last0_end(P.before(c), ST.ids(l), i), ihr0)
87	      +ne = NB.neighbor_m(~K, ~V, ~cmp, n, root, lo, hi, free, l0, d0, nl, pl, tg, fl, c, i, l, r, hr, hok, hnd, hid, hn, h)
88	      nav_node(~K, ~V, ~cmp, n, root, lo, hi, free, l0, d0, nl, pl, tg, fl, c, i, l, r, k, h, incl, g, ST.nd(K, nl, i), TR.rep_node(~K, i, l, r, P.top(c), nl, hr), ihl, ihr, ne)