1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/order.bend as O 4 import ../../../spec/lib/common.bend as SC 5 import ../../../spec/containers/balanced_search_tree/main.bend as S 6 import ../../../src/containers/balanced_search_tree.bend as M 7 import ./state.bend as ST 8 import ./ord.bend as OR 9 import ./tree.bend as TR 10 11 # The ghost search finds the specification's value: over a subtree whose 12 # nodes link as the ghost tree says, have values, and list their entries in 13 # key order, the payload at the id the search returns is the lookup of the 14 # key in the subtree's entries. (source: tools/generators/tm_hand/find.src) 15 16 17 def sfound(s: M.Search) -> Nat: 18 match s: 19 case M.Search{+f, p, lf}: 20 f 21 22 def cons_m_app(-X: Data, +m: Maybe<&2, X>, +xs: List<&2, X>, +ys: List<&2, X>) -> {SC.append(X, ST.cons_m(X, m, xs), ys) == ST.cons_m(X, m, SC.append(X, xs, ys)) : List<&2, X>}: 23 match m: 24 case None{}: 25 {==} 26 case Some{x}: 27 {==} 28 29 def ents_app(~K: Data, ~V: Data, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>) -> {ST.ents(~K, ~V, SC.append(Nat, xs, ys), nl, pl) == SC.append(M.Entry, ST.ents(~K, ~V, xs, nl, pl), ST.ents(~K, ~V, ys, nl, pl)) : List<&2, M.Entry>}: 30 match xs: 31 case Nil{}: 32 {==} 33 case Con{+i, +t}: 34 %Equal.sym(List<&2, M.Entry>, SC.append(M.Entry, ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, t, nl, pl)), ST.ents(~K, ~V, ys, nl, pl)), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), SC.append(M.Entry, ST.ents(~K, ~V, t, nl, pl), ST.ents(~K, ~V, ys, nl, pl))), cons_m_app(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, t, nl, pl), ST.ents(~K, ~V, ys, nl, pl))) : {ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, SC.append(Nat, t, ys), nl, pl)) == _ : List<&2, M.Entry>} 35 %Equal.sym(List<&2, M.Entry>, ST.ents(~K, ~V, SC.append(Nat, t, ys), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, t, nl, pl), ST.ents(~K, ~V, ys, nl, pl)), ents_app(~K, ~V, t, ys, nl, pl)) : {ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), _) == ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), SC.append(M.Entry, ST.ents(~K, ~V, t, nl, pl), ST.ents(~K, ~V, ys, nl, pl))) : List<&2, M.Entry>} 36 {==} 37 38 def ord_app_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +xs: List<&2, M.Entry>, +ys: List<&2, M.Entry>, +h: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry, xs, ys)) == True{} : Bool}) -> {ST.ordered(~K, ~V, ~cmp, xs) == True{} : Bool}: 39 match xs: 40 case Nil{}: 41 {==} 42 case Con{+e, +t}: 43 match t: 44 case Nil{}: 45 {==} 46 case Con{+e2, +u}: 47 L.and_intro(Cmp.is_lt(cmp(S.key(K, V, e), S.key(K, V, e2))), ST.ordered(~K, ~V, ~cmp, Con{e2, u}), L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), S.key(K, V, e2))), ST.ordered(~K, ~V, ~cmp, Con{e2, SC.append(M.Entry, u, ys)}), h), ord_app_l(~K, ~V, ~cmp, Con{e2, u}, ys, L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), S.key(K, V, e2))), ST.ordered(~K, ~V, ~cmp, Con{e2, SC.append(M.Entry, u, ys)}), h))) 48 49 def ord_cons_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m: Maybe<&2, M.Entry>, +t: List<&2, M.Entry>, +h: {ST.ordered(~K, ~V, ~cmp, ST.cons_m(M.Entry, m, t)) == True{} : Bool}) -> {ST.ordered(~K, ~V, ~cmp, t) == True{} : Bool}: 50 match m: 51 case None{}: 52 h 53 case Some{+e}: 54 OR.ord_tail(~K, ~V, ~cmp, e, t, h) 55 56 57 def tf_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +left: Bool, +k: K, +key: K, +v: V, +hpi: {ST.pv(V, pl, i) == Some{v} : Maybe<&2, V>}, +ho: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry, ST.ents(~K, ~V, ST.ids(tl), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, ST.ids(tr), nl, pl)})) == True{} : Bool}, +ihl: {ST.pv(V, pl, sfound(TR.tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}))) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tl), nl, pl)) : Maybe<&2, V>}, +ihr: {ST.pv(V, pl, sfound(TR.tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}))) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tr), nl, pl)) : Maybe<&2, V>}, +cc: Cmp, +hcc: {cmp(k, key) == cc : Cmp}) -> {ST.pv(V, pl, sfound(TR.pk3(M.Search, cc, TR.tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}), TR.tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}), M.Search{i, p, left}))) == S.find(~K, ~V, ~cmp, k, SC.append(M.Entry, ST.ents(~K, ~V, ST.ids(tl), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, ST.ids(tr), nl, pl)})) : Maybe<&2, V>}: 58 match cc: 59 case LT{}: 60 %Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry, ST.ents(~K, ~V, ST.ids(tl), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, ST.ids(tr), nl, pl)})), S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tl), nl, pl)), OR.find_mid_lt(~K, ~V, ~cmp, ~o, k, ST.ents(~K, ~V, ST.ids(tl), nl, pl), M.Entry{key, v}, ST.ents(~K, ~V, ST.ids(tr), nl, pl), ho, hcc)) : {ST.pv(V, pl, sfound(TR.tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}))) == S.val_m(K, V, _) : Maybe<&2, V>} 61 ihl 62 case GT{}: 63 %Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry, ST.ents(~K, ~V, ST.ids(tl), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, ST.ids(tr), nl, pl)})), S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tr), nl, pl)), OR.find_mid_gt(~K, ~V, ~cmp, ~o, k, ST.ents(~K, ~V, ST.ids(tl), nl, pl), M.Entry{key, v}, ST.ents(~K, ~V, ST.ids(tr), nl, pl), ho, hcc)) : {ST.pv(V, pl, sfound(TR.tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}))) == S.val_m(K, V, _) : Maybe<&2, V>} 64 ihr 65 case EQ{}: 66 %Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry, ST.ents(~K, ~V, ST.ids(tl), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, ST.ids(tr), nl, pl)})), Some{M.Entry{key, v}}, OR.find_mid_eq(~K, ~V, ~cmp, ~o, k, ST.ents(~K, ~V, ST.ids(tl), nl, pl), M.Entry{key, v}, ST.ents(~K, ~V, ST.ids(tr), nl, pl), ho, hcc)) : {ST.pv(V, pl, i) == S.val_m(K, V, _) : Maybe<&2, V>} 67 hpi 68 69 def tf_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +left: Bool, +k: K, +x: M.Node, +m: Maybe<&2, V>, +hx: {ST.is_node(K, x, ST.rid(tl), ST.rid(tr), p) == True{} : Bool}, +hm: {ST.some2(V, m) == True{} : Bool}, +hpi: {ST.pv(V, pl, i) == m : Maybe<&2, V>}, +ho: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry, ST.ents(~K, ~V, ST.ids(tl), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, x, m), ST.ents(~K, ~V, ST.ids(tr), nl, pl)))) == True{} : Bool}, +ihl: {ST.pv(V, pl, sfound(TR.tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}))) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tl), nl, pl)) : Maybe<&2, V>}, +ihr: {ST.pv(V, pl, sfound(TR.tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}))) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tr), nl, pl)) : Maybe<&2, V>}) -> {ST.pv(V, pl, sfound(TR.pk3(M.Search, TR.kc(~K, ~cmp, k, x), TR.tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}), TR.tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}), M.Search{i, p, left}))) == S.find(~K, ~V, ~cmp, k, SC.append(M.Entry, ST.ents(~K, ~V, ST.ids(tl), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, x, m), ST.ents(~K, ~V, ST.ids(tr), nl, pl)))) : Maybe<&2, V>}: 70 match x m: 71 case M.Free{fx} _: 72 Empty.absurd({ST.pv(V, pl, sfound(TR.pk3(M.Search, EQ{}, TR.tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}), TR.tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}), M.Search{i, p, left}))) == S.find(~K, ~V, ~cmp, k, SC.append(M.Entry, ST.ents(~K, ~V, ST.ids(tl), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, M.Free{fx}, m), ST.ents(~K, ~V, ST.ids(tr), nl, pl)))) : Maybe<&2, V>}, L.false_true(hx)) 73 case M.N{c, a, b, q, +key} None{}: 74 Empty.absurd({ST.pv(V, pl, sfound(TR.pk3(M.Search, cmp(k, key), TR.tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}), TR.tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}), M.Search{i, p, left}))) == S.find(~K, ~V, ~cmp, k, SC.append(M.Entry, ST.ents(~K, ~V, ST.ids(tl), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, M.N{c, a, b, q, key}, None{}), ST.ents(~K, ~V, ST.ids(tr), nl, pl)))) : Maybe<&2, V>}, L.false_true(hm)) 75 case M.N{c, a, b, q, +key} Some{+v}: 76 tf_c(~K, ~V, ~cmp, ~o, nl, pl, i, tl, tr, p, left, k, key, v, hpi, ho, ihl, ihr, cmp(k, key), {==}) 77 78 79 def pay_parts(~V: Data, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +pl: List<&2, Maybe<&2, V>>, +h: {ST.pay(~V, ST.TN{i, tl, tr}, pl) == True{} : Bool}) -> {ST.some2(V, ST.pv(V, pl, i)) == True{} : Bool} & ({ST.pay(~V, tl, pl) == True{} : Bool} & {ST.pay(~V, tr, pl) == True{} : Bool}): 80 +h2 = L.and_right(ST.some2(V, ST.pv(V, pl, i)), Bool.and(ST.pay(~V, tl, pl), ST.pay(~V, tr, pl)), h) 81 (L.and_left(ST.some2(V, ST.pv(V, pl, i)), Bool.and(ST.pay(~V, tl, pl), ST.pay(~V, tr, pl)), h), (L.and_left(ST.pay(~V, tl, pl), ST.pay(~V, tr, pl), h2), L.and_right(ST.pay(~V, tl, pl), ST.pay(~V, tr, pl), h2))) 82 83 def pay_node(~V: Data, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +pl: List<&2, Maybe<&2, V>>, +h: {ST.pay(~V, ST.TN{i, tl, tr}, pl) == True{} : Bool}) -> {ST.some2(V, ST.pv(V, pl, i)) == True{} : Bool}: 84 L.and_left(ST.some2(V, ST.pv(V, pl, i)), Bool.and(ST.pay(~V, tl, pl), ST.pay(~V, tr, pl)), h) 85 86 def pay_l(~V: Data, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +pl: List<&2, Maybe<&2, V>>, +h: {ST.pay(~V, ST.TN{i, tl, tr}, pl) == True{} : Bool}) -> {ST.pay(~V, tl, pl) == True{} : Bool}: 87 L.and_left(ST.pay(~V, tl, pl), ST.pay(~V, tr, pl), L.and_right(ST.some2(V, ST.pv(V, pl, i)), Bool.and(ST.pay(~V, tl, pl), ST.pay(~V, tr, pl)), h)) 88 89 def pay_r(~V: Data, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +pl: List<&2, Maybe<&2, V>>, +h: {ST.pay(~V, ST.TN{i, tl, tr}, pl) == True{} : Bool}) -> {ST.pay(~V, tr, pl) == True{} : Bool}: 90 L.and_right(ST.pay(~V, tl, pl), ST.pay(~V, tr, pl), L.and_right(ST.some2(V, ST.pv(V, pl, i)), Bool.and(ST.pay(~V, tl, pl), ST.pay(~V, tr, pl)), h)) 91 92 93 # the entries of a node's subtree: the left ones, its own, the right ones 94 def ents_node(~K: Data, ~V: Data, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +i: Nat, +tl: ST.Tr, +tr: ST.Tr) -> {ST.ents(~K, ~V, ST.ids(ST.TN{i, tl, tr}), nl, pl) == SC.append(M.Entry, ST.ents(~K, ~V, ST.ids(tl), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, ST.ids(tr), nl, pl))) : List<&2, M.Entry>}: 95 ents_app(~K, ~V, ST.ids(tl), Con{i, ST.ids(tr)}, nl, pl) 96 97 # the value at the ghost search's id is the lookup of the key 98 def tfind(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +p: Nat, +left: Bool, +k: K, +hr: {ST.rep(~K, t, p, nl) == True{} : Bool}, +hp: {ST.pay(~V, t, pl) == True{} : Bool}, +ho: {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, ST.ids(t), nl, pl)) == True{} : Bool}) -> {ST.pv(V, pl, sfound(TR.tsearch(~K, ~V, ~cmp, t, nl, k, p, left))) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(t), nl, pl)) : Maybe<&2, V>}: 99 match t: 100 case ST.TE{}: 101 {==} 102 case ST.TN{+i, +tl, +tr}: 103 +ho2 = L.subst(List<&2, M.Entry>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(ST.TN{i, tl, tr}), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, ST.ids(tl), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, ST.ids(tr), nl, pl))), ents_node(~K, ~V, nl, pl, i, tl, tr), ho) 104 +ihl = tfind(~K, ~V, ~cmp, ~o, nl, pl, tl, i, True{}, k, TR.rep_l(~K, i, tl, tr, p, nl, hr), pay_l(~V, i, tl, tr, pl, hp), ord_app_l(~K, ~V, ~cmp, ST.ents(~K, ~V, ST.ids(tl), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, ST.ids(tr), nl, pl)), ho2)) 105 +ihr = tfind(~K, ~V, ~cmp, ~o, nl, pl, tr, i, False{}, k, TR.rep_r(~K, i, tl, tr, p, nl, hr), pay_r(~V, i, tl, tr, pl, hp), ord_cons_m(~K, ~V, ~cmp, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, ST.ids(tr), nl, pl), OR.ord_app_r(~K, ~V, ~cmp, ST.ents(~K, ~V, ST.ids(tl), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, ST.ids(tr), nl, pl)), ho2))) 106 %Equal.sym(List<&2, M.Entry>, ST.ents(~K, ~V, ST.ids(ST.TN{i, tl, tr}), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, ST.ids(tl), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i)), ST.ents(~K, ~V, ST.ids(tr), nl, pl))), ents_node(~K, ~V, nl, pl, i, tl, tr)) : {ST.pv(V, pl, sfound(TR.tsearch(~K, ~V, ~cmp, ST.TN{i, tl, tr}, nl, k, p, left))) == S.find(~K, ~V, ~cmp, k, _) : Maybe<&2, V>} 107 tf_node(~K, ~V, ~cmp, ~o, nl, pl, i, tl, tr, p, left, k, ST.nd(K, nl, i), ST.pv(V, pl, i), TR.rep_node(~K, i, tl, tr, p, nl, hr), pay_node(~V, i, tl, tr, pl, hp), {==}, ho2, ihl, ihr)