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 ./setters.bend as SE
6	
7	# The mirror's attach and rotations as functions of the node list and the
8	# root: attach links a child under a parent (or makes it the root), a
9	# rotation relinks the node, its child, the child's inner subtree and the
10	# parent. (source: tools/generators/tm_hand/rotm.src)
11	
12	
13	def rootq(+q: Nat, +root: Nat, +y: Nat) -> Nat:
14	  match q:
15	    case 0n:
16	      y
17	    case 1n+j:
18	      root
19	
20	def attn(-K: Data, +nl: List<&2, M.Node<K>>, +q: Nat, +y: Nat, +dir: Bool) -> List<&2, M.Node<K>>:
21	  match q:
22	    case 0n:
23	      nl
24	    case 1n+j:
25	      match dir:
26	        case True{}:
27	          SE.setl(K, nl, 1n+j, y)
28	        case False{}:
29	          SE.setr(K, nl, 1n+j, y)
30	
31	def attach_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>, +q: Nat, +y: Nat, +dir: Bool) -> {MI.attach(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, q, y, dir) == ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, attn(K, nl, q, y, dir), y, q), pl, tg, fl} : ST.Sh<K, V>}:
32	  match q dir:
33	    case 0n True{}:
34	      SE.set_parent_m(~K, ~V, ~cmp, n, y, lo, hi, free, l, d, nl, pl, tg, fl, y, 0n)
35	    case 0n False{}:
36	      SE.set_parent_m(~K, ~V, ~cmp, n, y, lo, hi, free, l, d, nl, pl, tg, fl, y, 0n)
37	    case 1n+j True{}:
38	      %Equal.sym(ST.Sh<K, V>, MI.set_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, y), ST.SH{n, root, lo, hi, free, l, d, SE.setl(K, nl, 1n+j, y), pl, tg, fl}, SE.set_left_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, 1n+j, y)) : {MI.set_parent(~K, ~V, ~cmp, _, y, 1n+j) == ST.SH{n, root, lo, hi, free, l, d, SE.setp(K, SE.setl(K, nl, 1n+j, y), y, 1n+j), pl, tg, fl} : ST.Sh<K, V>}
39	      SE.set_parent_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setl(K, nl, 1n+j, y), pl, tg, fl, y, 1n+j)
40	    case 1n+j False{}:
41	      %Equal.sym(ST.Sh<K, V>, MI.set_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, y), ST.SH{n, root, lo, hi, free, l, d, SE.setr(K, nl, 1n+j, y), pl, tg, fl}, SE.set_right_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, 1n+j, y)) : {MI.set_parent(~K, ~V, ~cmp, _, y, 1n+j) == ST.SH{n, root, lo, hi, free, l, d, SE.setp(K, SE.setr(K, nl, 1n+j, y), y, 1n+j), pl, tg, fl} : ST.Sh<K, V>}
42	      SE.set_parent_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setr(K, nl, 1n+j, y), pl, tg, fl, y, 1n+j)
43	
44	
45	# the left rotation's writes: x's right := b, b's parent := x, the parent's
46	# child (or the root) := y, y's parent := q, y's left := x, x's parent := y
47	def rotl_nl(-K: Data, +nl: List<&2, M.Node<K>>, +x: Nat, +y: Nat, +b: Nat, +q: Nat, +dir: Bool) -> List<&2, M.Node<K>>:
48	  SE.setp(K, SE.setl(K, SE.setp(K, attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y)
49	
50	def rotl_body(~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>, +x: Nat, +y: Nat, +b: Nat, +q: Nat, +dir: Bool) -> {MI.set_parent(~K, ~V, ~cmp, MI.set_left(~K, ~V, ~cmp, MI.attach(~K, ~V, ~cmp, MI.set_parent(~K, ~V, ~cmp, MI.set_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, x, b), b, x), q, y, dir), y, x), x, y) == ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, rotl_nl(K, nl, x, y, b, q, dir), pl, tg, fl} : ST.Sh<K, V>}:
51	  %Equal.sym(ST.Sh<K, V>, MI.set_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, x, b), ST.SH{n, root, lo, hi, free, l, d, SE.setr(K, nl, x, b), pl, tg, fl}, SE.set_right_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, x, b)) : {MI.set_parent(~K, ~V, ~cmp, MI.set_left(~K, ~V, ~cmp, MI.attach(~K, ~V, ~cmp, MI.set_parent(~K, ~V, ~cmp, _, b, x), q, y, dir), y, x), x, y) == ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, SE.setl(K, SE.setp(K, attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), pl, tg, fl} : ST.Sh<K, V>}
52	  %Equal.sym(ST.Sh<K, V>, MI.set_parent(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setr(K, nl, x, b), pl, tg, fl}, b, x), ST.SH{n, root, lo, hi, free, l, d, SE.setp(K, SE.setr(K, nl, x, b), b, x), pl, tg, fl}, SE.set_parent_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setr(K, nl, x, b), pl, tg, fl, b, x)) : {MI.set_parent(~K, ~V, ~cmp, MI.set_left(~K, ~V, ~cmp, MI.attach(~K, ~V, ~cmp, _, q, y, dir), y, x), x, y) == ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, SE.setl(K, SE.setp(K, attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), pl, tg, fl} : ST.Sh<K, V>}
53	  %Equal.sym(ST.Sh<K, V>, MI.attach(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setp(K, SE.setr(K, nl, x, b), b, x), pl, tg, fl}, q, y, dir), ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), pl, tg, fl}, attach_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setp(K, SE.setr(K, nl, x, b), b, x), pl, tg, fl, q, y, dir)) : {MI.set_parent(~K, ~V, ~cmp, MI.set_left(~K, ~V, ~cmp, _, y, x), x, y) == ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, SE.setl(K, SE.setp(K, attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), pl, tg, fl} : ST.Sh<K, V>}
54	  %Equal.sym(ST.Sh<K, V>, MI.set_left(~K, ~V, ~cmp, ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), pl, tg, fl}, y, x), ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setl(K, SE.setp(K, attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), pl, tg, fl}, SE.set_left_m(~K, ~V, ~cmp, n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), pl, tg, fl, y, x)) : {MI.set_parent(~K, ~V, ~cmp, _, x, y) == ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, SE.setl(K, SE.setp(K, attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), pl, tg, fl} : ST.Sh<K, V>}
55	  SE.set_parent_m(~K, ~V, ~cmp, n, rootq(q, root, y), lo, hi, free, l, d, SE.setl(K, SE.setp(K, attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), pl, tg, fl, x, y)
56	
57	
58	# the right rotation: x's left := b, b's parent := x, the parent's child (or
59	# the root) := y, y's parent := q, y's right := x, x's parent := y
60	def rotr_nl(-K: Data, +nl: List<&2, M.Node<K>>, +x: Nat, +y: Nat, +b: Nat, +q: Nat, +dir: Bool) -> List<&2, M.Node<K>>:
61	  SE.setp(K, SE.setr(K, SE.setp(K, attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y)
62	
63	def rotr_body(~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>, +x: Nat, +y: Nat, +b: Nat, +q: Nat, +dir: Bool) -> {MI.set_parent(~K, ~V, ~cmp, MI.set_right(~K, ~V, ~cmp, MI.attach(~K, ~V, ~cmp, MI.set_parent(~K, ~V, ~cmp, MI.set_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, x, b), b, x), q, y, dir), y, x), x, y) == ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, rotr_nl(K, nl, x, y, b, q, dir), pl, tg, fl} : ST.Sh<K, V>}:
64	  %Equal.sym(ST.Sh<K, V>, MI.set_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, x, b), ST.SH{n, root, lo, hi, free, l, d, SE.setl(K, nl, x, b), pl, tg, fl}, SE.set_left_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, x, b)) : {MI.set_parent(~K, ~V, ~cmp, MI.set_right(~K, ~V, ~cmp, MI.attach(~K, ~V, ~cmp, MI.set_parent(~K, ~V, ~cmp, _, b, x), q, y, dir), y, x), x, y) == ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, SE.setr(K, SE.setp(K, attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), pl, tg, fl} : ST.Sh<K, V>}
65	  %Equal.sym(ST.Sh<K, V>, MI.set_parent(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setl(K, nl, x, b), pl, tg, fl}, b, x), ST.SH{n, root, lo, hi, free, l, d, SE.setp(K, SE.setl(K, nl, x, b), b, x), pl, tg, fl}, SE.set_parent_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setl(K, nl, x, b), pl, tg, fl, b, x)) : {MI.set_parent(~K, ~V, ~cmp, MI.set_right(~K, ~V, ~cmp, MI.attach(~K, ~V, ~cmp, _, q, y, dir), y, x), x, y) == ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, SE.setr(K, SE.setp(K, attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), pl, tg, fl} : ST.Sh<K, V>}
66	  %Equal.sym(ST.Sh<K, V>, MI.attach(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setp(K, SE.setl(K, nl, x, b), b, x), pl, tg, fl}, q, y, dir), ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), pl, tg, fl}, attach_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setp(K, SE.setl(K, nl, x, b), b, x), pl, tg, fl, q, y, dir)) : {MI.set_parent(~K, ~V, ~cmp, MI.set_right(~K, ~V, ~cmp, _, y, x), x, y) == ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, SE.setr(K, SE.setp(K, attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), pl, tg, fl} : ST.Sh<K, V>}
67	  %Equal.sym(ST.Sh<K, V>, MI.set_right(~K, ~V, ~cmp, ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), pl, tg, fl}, y, x), ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setr(K, SE.setp(K, attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), pl, tg, fl}, SE.set_right_m(~K, ~V, ~cmp, n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), pl, tg, fl, y, x)) : {MI.set_parent(~K, ~V, ~cmp, _, x, y) == ST.SH{n, rootq(q, root, y), lo, hi, free, l, d, SE.setp(K, SE.setr(K, SE.setp(K, attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), pl, tg, fl} : ST.Sh<K, V>}
68	  SE.set_parent_m(~K, ~V, ~cmp, n, rootq(q, root, y), lo, hi, free, l, d, SE.setr(K, SE.setp(K, attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), pl, tg, fl, x, y)
69	
70	# the mirror's rotations over nodes read from the list
71	def rotate_left_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>, +x: Nat) -> {MI.rotate_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, x) == ST.SH{n, rootq(M.node_parent(~K, ST.nd(K, nl, x)), root, M.node_right(~K, ST.nd(K, nl, x))), lo, hi, free, l, d, rotl_nl(K, nl, x, M.node_right(~K, ST.nd(K, nl, x)), M.node_left(~K, ST.nd(K, nl, M.node_right(~K, ST.nd(K, nl, x)))), M.node_parent(~K, ST.nd(K, nl, x)), Nat.is_eq(M.node_left(~K, ST.nd(K, nl, M.node_parent(~K, ST.nd(K, nl, x)))), x)), pl, tg, fl} : ST.Sh<K, V>}:
72	  rotl_body(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, x, M.node_right(~K, ST.nd(K, nl, x)), M.node_left(~K, ST.nd(K, nl, M.node_right(~K, ST.nd(K, nl, x)))), M.node_parent(~K, ST.nd(K, nl, x)), Nat.is_eq(M.node_left(~K, ST.nd(K, nl, M.node_parent(~K, ST.nd(K, nl, x)))), x))
73	
74	def rotate_right_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>, +x: Nat) -> {MI.rotate_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, x) == ST.SH{n, rootq(M.node_parent(~K, ST.nd(K, nl, x)), root, M.node_left(~K, ST.nd(K, nl, x))), lo, hi, free, l, d, rotr_nl(K, nl, x, M.node_left(~K, ST.nd(K, nl, x)), M.node_right(~K, ST.nd(K, nl, M.node_left(~K, ST.nd(K, nl, x)))), M.node_parent(~K, ST.nd(K, nl, x)), Nat.is_eq(M.node_left(~K, ST.nd(K, nl, M.node_parent(~K, ST.nd(K, nl, x)))), x)), pl, tg, fl} : ST.Sh<K, V>}:
75	  rotr_body(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, x, M.node_left(~K, ST.nd(K, nl, x)), M.node_right(~K, ST.nd(K, nl, M.node_left(~K, ST.nd(K, nl, x)))), M.node_parent(~K, ST.nd(K, nl, x)), Nat.is_eq(M.node_left(~K, ST.nd(K, nl, M.node_parent(~K, ST.nd(K, nl, x)))), x))