1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/list.bend as LL
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 ./path.bend as P
8	
9	# A path plugged with a subtree: the tree it leads through. Its ids are the
10	# ids before, the subtree's, and after; it links as the ghost says when the
11	# subtree does below the path's parent and the path's frames do.
12	# (source: tools/generators/tm_hand/plug.src)
13	
14	
15	def plug(c: List<&2, P.Fr>, t: ST.Tr) -> ST.Tr:
16	  match c:
17	    case Nil{}:
18	      t
19	    case Con{f, u}:
20	      match f:
21	        case P.FR{+p, +lft, s}:
22	          match lft:
23	            case True{}:
24	              plug(u, ST.TN{p, t, s})
25	            case False{}:
26	              plug(u, ST.TN{p, s, t})
27	
28	def ids_plug(+c: List<&2, P.Fr>, +t: ST.Tr) -> {ST.ids(plug(c, t)) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}:
29	  match c:
30	    case Nil{}:
31	      Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(t), Nil{}), ST.ids(t), LL.append_nil(Nat, ST.ids(t)))
32	    case Con{P.FR{+p, +lft, +s}, +u}:
33	      match lft:
34	        case True{}:
35	          Equal.trans(List<&2, Nat>, ST.ids(plug(u, ST.TN{p, t, s})), SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(ST.TN{p, t, s}), P.after(u))), SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, u}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, u}))), ids_plug(u, ST.TN{p, t, s}), P.ids_l(u, p, t, s))
36	        case False{}:
37	          Equal.trans(List<&2, Nat>, ST.ids(plug(u, ST.TN{p, s, t})), SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(ST.TN{p, s, t}), P.after(u))), SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, u}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, u}))), ids_plug(u, ST.TN{p, s, t}), P.ids_r(u, p, s, t))
38	
39	
40	# the plugged tree links when the subtree and the path do
41	def rep_plug(~K: Data, +nl: List<&2, M.Node<K>>, +c: List<&2, P.Fr>, +t: ST.Tr, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hc: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}) -> {ST.rep(~K, plug(c, t), 0n, nl) == True{} : Bool}:
42	  match c:
43	    case Nil{}:
44	      hr
45	    case Con{P.FR{+p, +lft, +s}, +u}:
46	      match lft:
47	        case True{}:
48	          +hk = L.and_left(P.cok1(~K, P.FR{p, True{}, s}, ST.rid(t), P.top(u), nl), P.ctxok(~K, u, p, nl), hc)
49	          +hu = L.and_right(P.cok1(~K, P.FR{p, True{}, s}, ST.rid(t), P.top(u), nl), P.ctxok(~K, u, p, nl), hc)
50	          +h0 = L.and_left(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(u)), ST.rep(~K, s, p, nl)), hk)
51	          +h12 = L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(u)), ST.rep(~K, s, p, nl)), hk)
52	          +hn = L.and_left(ST.is_node(K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(u)), ST.rep(~K, s, p, nl), h12)
53	          +hs = L.and_right(ST.is_node(K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(u)), ST.rep(~K, s, p, nl), h12)
54	          rep_plug(~K, nl, u, ST.TN{p, t, s}, L.and_intro(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(u)), Bool.and(ST.rep(~K, t, p, nl), ST.rep(~K, s, p, nl))), h0, L.and_intro(ST.is_node(K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(u)), Bool.and(ST.rep(~K, t, p, nl), ST.rep(~K, s, p, nl)), hn, L.and_intro(ST.rep(~K, t, p, nl), ST.rep(~K, s, p, nl), hr, hs))), hu)
55	        case False{}:
56	          +hk = L.and_left(P.cok1(~K, P.FR{p, False{}, s}, ST.rid(t), P.top(u), nl), P.ctxok(~K, u, p, nl), hc)
57	          +hu = L.and_right(P.cok1(~K, P.FR{p, False{}, s}, ST.rid(t), P.top(u), nl), P.ctxok(~K, u, p, nl), hc)
58	          +h0 = L.and_left(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(u)), ST.rep(~K, s, p, nl)), hk)
59	          +h12 = L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(u)), ST.rep(~K, s, p, nl)), hk)
60	          +hn = L.and_left(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(u)), ST.rep(~K, s, p, nl), h12)
61	          +hs = L.and_right(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(u)), ST.rep(~K, s, p, nl), h12)
62	          rep_plug(~K, nl, u, ST.TN{p, s, t}, L.and_intro(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(u)), Bool.and(ST.rep(~K, s, p, nl), ST.rep(~K, t, p, nl))), h0, L.and_intro(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(u)), Bool.and(ST.rep(~K, s, p, nl), ST.rep(~K, t, p, nl)), hn, L.and_intro(ST.rep(~K, s, p, nl), ST.rep(~K, t, p, nl), hs, hr))), hu)