1	import Base
2	import ../../../src/containers/balanced_search_tree.bend as M
3	import ./state.bend as ST
4	import ./mirror.bend as MI
5	import ./tree.bend as TR
6	import ./nbr.bend as NB
7	
8	# The extremes the deletion reads: from an id the mirror's walk is the
9	# node-list walk, so from a node the path leads to it reaches the first
10	# (backward) or last (forward) id of its subtree, and refreshing the ends
11	# puts the tree's first and last ids in the header.
12	# (source: tools/generators/tm_hand/xtr.src)
13	
14	
15	def ext_eq(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fuel: Nat, +fw: Bool, +id: Nat, +next: Nat) -> {MI.extreme_loop(~K, ~V, ~cmp, fuel, fw, id, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, next)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, MI.ext_loop(~K, fuel, nl, fw, id, next)) : ST.Sh<K, V> & Nat}:
16	  match fuel next:
17	    case 0n 0n:
18	      {==}
19	    case 0n 1n+j:
20	      {==}
21	    case 1n+f 0n:
22	      {==}
23	    case 1n+f 1n+j:
24	      ext_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, f, fw, 1n+j, M.child(~K, ST.nd(K, nl, 1n+j), fw))
25	
26	def extreme_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +fw: Bool) -> {MI.extreme(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, fw) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, MI.ext_loop(~K, 1n+n, nl, fw, id, M.child(~K, ST.nd(K, nl, id), fw))) : ST.Sh<K, V> & Nat}:
27	  ext_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, 1n+n, fw, id, M.child(~K, ST.nd(K, nl, id), fw))
28	
29	
30	# refreshing the ends of a linked tree
31	def refresh_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +t: ST.Tr, +hr: {ST.rep(~K, t, 0n, nl) == True{} : Bool}, +hf: {Nat.is_lt(TR.ht(t), 1n+n) == True{} : Bool}) -> {MI.refresh_ends(~K, ~V, ~cmp, ST.SH{n, ST.rid(t), lo, hi, free, l, d, nl, pl, tg, fl}) == ST.SH{n, ST.rid(t), ST.fst0(ST.ids(t)), ST.last0(ST.ids(t)), free, l, d, nl, pl, tg, fl} : ST.Sh<K, V>}:
32	  match t:
33	    case ST.TE{}:
34	      {==}
35	    case ST.TN{+j, +a, +b}:
36	      %Equal.sym(ST.Sh<K, V> & Nat, MI.extreme(~K, ~V, ~cmp, ST.SH{n, j, lo, hi, free, l, d, nl, pl, tg, fl}, j, False{}), (ST.SH{n, j, lo, hi, free, l, d, nl, pl, tg, fl}, MI.ext_loop(~K, 1n+n, nl, False{}, j, M.child(~K, ST.nd(K, nl, j), False{}))), extreme_m(~K, ~V, ~cmp, n, j, lo, hi, free, l, d, nl, pl, tg, fl, j, False{})) : {MI.refresh_ends_2(~K, ~V, ~cmp, j, _) == ST.SH{n, j, ST.fst0(ST.ids(ST.TN{j, a, b})), ST.last0(ST.ids(ST.TN{j, a, b})), free, l, d, nl, pl, tg, fl} : ST.Sh<K, V>}
37	      %Equal.sym(Nat, MI.ext_loop(~K, 1n+n, nl, False{}, j, M.child(~K, ST.nd(K, nl, j), False{})), ST.fst0(ST.ids(ST.TN{j, a, b})), NB.ext_l(~K, nl, 1n+n, j, a, b, 0n, hr, hf)) : {MI.refresh_ends_2(~K, ~V, ~cmp, j, (ST.SH{n, j, lo, hi, free, l, d, nl, pl, tg, fl}, _)) == ST.SH{n, j, ST.fst0(ST.ids(ST.TN{j, a, b})), ST.last0(ST.ids(ST.TN{j, a, b})), free, l, d, nl, pl, tg, fl} : ST.Sh<K, V>}
38	      %Equal.sym(ST.Sh<K, V> & Nat, MI.extreme(~K, ~V, ~cmp, ST.SH{n, j, lo, hi, free, l, d, nl, pl, tg, fl}, j, True{}), (ST.SH{n, j, lo, hi, free, l, d, nl, pl, tg, fl}, MI.ext_loop(~K, 1n+n, nl, True{}, j, M.child(~K, ST.nd(K, nl, j), True{}))), extreme_m(~K, ~V, ~cmp, n, j, lo, hi, free, l, d, nl, pl, tg, fl, j, True{})) : {MI.refresh_ends_3(~K, ~V, ~cmp, ST.fst0(ST.ids(ST.TN{j, a, b})), _) == ST.SH{n, j, ST.fst0(ST.ids(ST.TN{j, a, b})), ST.last0(ST.ids(ST.TN{j, a, b})), free, l, d, nl, pl, tg, fl} : ST.Sh<K, V>}
39	      %Equal.sym(Nat, MI.ext_loop(~K, 1n+n, nl, True{}, j, M.child(~K, ST.nd(K, nl, j), True{})), ST.last0(ST.ids(ST.TN{j, a, b})), NB.ext_r(~K, nl, 1n+n, j, a, b, 0n, hr, hf)) : {MI.refresh_ends_3(~K, ~V, ~cmp, ST.fst0(ST.ids(ST.TN{j, a, b})), (ST.SH{n, j, lo, hi, free, l, d, nl, pl, tg, fl}, _)) == ST.SH{n, j, ST.fst0(ST.ids(ST.TN{j, a, b})), ST.last0(ST.ids(ST.TN{j, a, b})), free, l, d, nl, pl, tg, fl} : ST.Sh<K, V>}
40	      {==}