proofs/containers/balanced_search_tree/rotm.bend
bend-collections-laws-containers@1.0.0.0 · 75 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
3import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
4import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
5import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/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
13def rootq(+q: Nat, +root: Nat, +y: Nat) -> Nat:
14 match q:
15 case 0n:
16 y
17 case 1n+j:
18 root
19
20def 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
31def 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
47def 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
50def 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
60def 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
63def 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
71def 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
74def 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))