1 import Base 2 import ../../lib/order.bend as O 3 import ../../../spec/containers/balanced_search_tree/main.bend as S 4 import ../../../src/containers/balanced_search_tree.bend as M 5 import ./state.bend as ST 6 import ./mirror.bend as MI 7 import ./ends.bend as EN 8 import ./navm.bend as NM 9 import ./ord.bend as OR 10 import ./cur.bend as CU 11 import ./vsp.bend as VS 12 13 # A view's first and last entries and its searches: the mirror starts at the 14 # bound (or searches from the key, when inside the view) and checks the entry 15 # found against the range; the specification searches the entries within. 16 # (source: tools/generators/tm_hand/vnav.src) 17 18 19 # ---- the entry at a bound ---- 20 21 def rsf_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lw: M.Bound) -> {MI.entry_snapshot(~K, ~V, ~cmp, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lw, True{})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, VS.fal(~K, ~V, ~cmp, lw, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh & Maybe<&2, M.Entry>}: 22 match lw: 23 case M.Unbounded{}: 24 %Equal.sym(Maybe<&2, M.Entry>, VS.fal(~K, ~V, ~cmp, M.Unbounded{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.head(M.Entry, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.fal_u(~K, ~V, ~cmp, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : {MI.entry_snapshot(~K, ~V, ~cmp, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Unbounded{}, True{})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _) : ST.Sh & Maybe<&2, M.Entry>} 25 EN.first_entry_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg) 26 case M.Inclusive{+x}: 27 %Equal.sym(Maybe<&2, M.Entry>, VS.fal(~K, ~V, ~cmp, M.Inclusive{x}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.first_where(~K, ~V, ~cmp, x, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.fal_i(~K, ~V, ~cmp, x, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : {MI.entry_snapshot(~K, ~V, ~cmp, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Inclusive{x}, True{})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _) : ST.Sh & Maybe<&2, M.Entry>} 28 NM.nav_entry_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, x, True{}, True{}, hg) 29 case M.Exclusive{+x}: 30 %Equal.sym(Maybe<&2, M.Entry>, VS.fal(~K, ~V, ~cmp, M.Exclusive{x}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.first_where(~K, ~V, ~cmp, x, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.fal_x(~K, ~V, ~cmp, x, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : {MI.entry_snapshot(~K, ~V, ~cmp, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Exclusive{x}, True{})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _) : ST.Sh & Maybe<&2, M.Entry>} 31 NM.nav_entry_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, x, True{}, False{}, hg) 32 33 def rsb_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +up: M.Bound) -> {MI.entry_snapshot(~K, ~V, ~cmp, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, up, False{})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, VS.lbu(~K, ~V, ~cmp, up, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{})) : ST.Sh & Maybe<&2, M.Entry>}: 34 match up: 35 case M.Unbounded{}: 36 %Equal.sym(Maybe<&2, M.Entry>, VS.lbu(~K, ~V, ~cmp, M.Unbounded{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), S.last(M.Entry, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Equal.trans(Maybe<&2, M.Entry>, VS.lbu(~K, ~V, ~cmp, M.Unbounded{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), OR.orm(M.Entry, S.last(M.Entry, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}), S.last(M.Entry, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.lbu_u(~K, ~V, ~cmp, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), OR.orm_none(M.Entry, S.last(M.Entry, ST.ents(~K, ~V, ST.ids(tg), nl, pl))))) : {MI.entry_snapshot(~K, ~V, ~cmp, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Unbounded{}, False{})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _) : ST.Sh & Maybe<&2, M.Entry>} 37 EN.last_entry_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg) 38 case M.Inclusive{+y}: 39 %Equal.sym(Maybe<&2, M.Entry>, VS.lbu(~K, ~V, ~cmp, M.Inclusive{y}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), S.last_where(~K, ~V, ~cmp, y, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), VS.lbu_i(~K, ~V, ~cmp, y, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{})) : {MI.entry_snapshot(~K, ~V, ~cmp, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Inclusive{y}, False{})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _) : ST.Sh & Maybe<&2, M.Entry>} 40 NM.nav_entry_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, y, False{}, True{}, hg) 41 case M.Exclusive{+y}: 42 %Equal.sym(Maybe<&2, M.Entry>, VS.lbu(~K, ~V, ~cmp, M.Exclusive{y}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), S.last_where(~K, ~V, ~cmp, y, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), VS.lbu_x(~K, ~V, ~cmp, y, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{})) : {MI.entry_snapshot(~K, ~V, ~cmp, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Exclusive{y}, False{})) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _) : ST.Sh & Maybe<&2, M.Entry>} 43 NM.nav_entry_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, y, False{}, False{}, hg) 44 45 # ---- the entry found, checked against the range ---- 46 47 48 def ver_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +s: ST.Sh, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +en: M.Entry, +b: Bool) -> {MI.view_entry_checked(~K, ~V, ~cmp, s, lo2, hi2, d2, en, b) == (MI.MV{s, lo2, hi2, d2}, S.pick(Maybe<&2, M.Entry>, b, Some{en}, None{})) : MI.MView & Maybe<&2, M.Entry>}: 49 match b: 50 case True{}: 51 {==} 52 case False{}: 53 {==} 54 55 def ver_eq(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +s: ST.Sh, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +m: Maybe<&2, M.Entry>) -> {MI.view_entry_result(~K, ~V, ~cmp, lo2, hi2, d2, (s, m)) == (MI.MV{s, lo2, hi2, d2}, VS.chk(~K, ~V, ~cmp, lo2, hi2, m)) : MI.MView & Maybe<&2, M.Entry>}: 56 match m: 57 case None{}: 58 {==} 59 case Some{M.Entry{+k, +v}}: 60 %Equal.sym(Bool, M.in_range(~K, ~V, ~cmp, k, lo2, hi2), S.in_range(~K, ~cmp, k, lo2, hi2), CU.inr_eq(~K, ~V, ~cmp, k, lo2, hi2)) : {MI.view_entry_checked(~K, ~V, ~cmp, s, lo2, hi2, d2, M.Entry{k, v}, _) == (MI.MV{s, lo2, hi2, d2}, VS.chk(~K, ~V, ~cmp, lo2, hi2, Some{M.Entry{k, v}})) : MI.MView & Maybe<&2, M.Entry>} 61 ver_b(~K, ~V, ~cmp, s, lo2, hi2, d2, M.Entry{k, v}, S.in_range(~K, ~cmp, k, lo2, hi2)) 62 63 # a snapshot known, its check the specification's answer 64 def vres(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +s: ST.Sh, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, -r: ST.Sh & Maybe<&2, M.Entry>, +m: Maybe<&2, M.Entry>, +o: Maybe<&2, M.Entry>, +hr: {r == (s, m) : ST.Sh & Maybe<&2, M.Entry>}, +ho: {o == VS.chk(~K, ~V, ~cmp, lo2, hi2, m) : Maybe<&2, M.Entry>}) -> {MI.view_entry_result(~K, ~V, ~cmp, lo2, hi2, d2, r) == (MI.MV{s, lo2, hi2, d2}, o) : MI.MView & Maybe<&2, M.Entry>}: 65 %Equal.sym(ST.Sh & Maybe<&2, M.Entry>, r, (s, m), hr) : {MI.view_entry_result(~K, ~V, ~cmp, lo2, hi2, d2, _) == (MI.MV{s, lo2, hi2, d2}, o) : MI.MView & Maybe<&2, M.Entry>} 66 %Equal.sym(Maybe<&2, M.Entry>, o, VS.chk(~K, ~V, ~cmp, lo2, hi2, m), ho) : {MI.view_entry_result(~K, ~V, ~cmp, lo2, hi2, d2, (s, m)) == (MI.MV{s, lo2, hi2, d2}, _) : MI.MView & Maybe<&2, M.Entry>} 67 ver_eq(~K, ~V, ~cmp, s, lo2, hi2, d2, m) 68 69 # ---- first and last ---- 70 71 72 def vx_up(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +up: Bool) -> {MI.view_entry_result(~K, ~V, ~cmp, lo2, hi2, d2, MI.entry_snapshot(~K, ~V, ~cmp, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.pick(M.Bound, up, lo2, hi2), up))) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, M.Entry>, up, S.head(M.Entry, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.last(M.Entry, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))))) : MI.MView & Maybe<&2, M.Entry>}: 73 match up: 74 case True{}: 75 vres(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2, MI.entry_snapshot(~K, ~V, ~cmp, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{})), VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.head(M.Entry, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), rsf_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2), VS.first_within(~K, ~V, ~cmp, ~o, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))) 76 case False{}: 77 vres(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2, MI.entry_snapshot(~K, ~V, ~cmp, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{})), VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), S.last(M.Entry, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), rsb_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, hi2), VS.last_within(~K, ~V, ~cmp, ~o, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))) 78 79 80 def vx_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +first: Bool) -> {MI.view_extreme(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, first) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, M.Entry>, S.pick(Bool, d2, Bool.not(first), first), S.head(M.Entry, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.last(M.Entry, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))))) : MI.MView & Maybe<&2, M.Entry>}: 81 match d2: 82 case True{}: 83 vx_up(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, True{}, Bool.not(first)) 84 case False{}: 85 vx_up(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, False{}, first) 86 87 # ---- searches ---- 88 89 90 def vn_t(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +k: K, +incl: Bool, +a: Bool, +ha: {S.above_lower(~K, ~cmp, k, lo2) == a : Bool}) -> {MI.view_entry_result(~K, ~V, ~cmp, lo2, hi2, d2, MI.entry_snapshot(~K, ~V, ~cmp, MI.view_nav_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, True{}, incl, a))) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.nav(~K, ~V, ~cmp, k, True{}, incl, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView & Maybe<&2, M.Entry>}: 91 match a: 92 case True{}: 93 vres(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2, MI.entry_snapshot(~K, ~V, ~cmp, MI.navigate(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, True{}, incl)), S.first_where(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), NM.nav_entry_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, True{}, incl, hg), VS.fw_within(~K, ~V, ~cmp, ~o, lo2, hi2, k, incl, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ha)) 94 case False{}: 95 vres(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2, MI.entry_snapshot(~K, ~V, ~cmp, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{})), VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), rsf_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2), Equal.trans(Maybe<&2, M.Entry>, S.first_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.head(M.Entry, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), VS.chk(~K, ~V, ~cmp, lo2, hi2, VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), VS.fw_below(~K, ~V, ~cmp, ~o, lo2, hi2, k, incl, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ha), VS.first_within(~K, ~V, ~cmp, ~o, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))) 96 97 def vn_f(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +k: K, +incl: Bool, +b: Bool, +hb: {S.below_upper(~K, ~cmp, k, hi2) == b : Bool}) -> {MI.view_entry_result(~K, ~V, ~cmp, lo2, hi2, d2, MI.entry_snapshot(~K, ~V, ~cmp, MI.view_nav_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, False{}, incl, b))) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.nav(~K, ~V, ~cmp, k, False{}, incl, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView & Maybe<&2, M.Entry>}: 98 match b: 99 case True{}: 100 vres(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2, MI.entry_snapshot(~K, ~V, ~cmp, MI.navigate(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, False{}, incl)), S.last_where(~K, ~V, ~cmp, k, incl, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}), NM.nav_entry_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, False{}, incl, hg), VS.lw_within(~K, ~V, ~cmp, ~o, lo2, hi2, k, incl, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), hb)) 101 case False{}: 102 vres(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2, MI.entry_snapshot(~K, ~V, ~cmp, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{})), VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}), rsb_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, hi2), Equal.trans(Maybe<&2, M.Entry>, S.last_where(~K, ~V, ~cmp, k, incl, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}), S.last(M.Entry, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), VS.chk(~K, ~V, ~cmp, lo2, hi2, VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{})), VS.lw_above(~K, ~V, ~cmp, ~o, lo2, hi2, k, incl, ST.ents(~K, ~V, ST.ids(tg), nl, pl), hb), VS.last_within(~K, ~V, ~cmp, ~o, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))) 103 104 def vn_up(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +k: K, +incl: Bool, +up: Bool) -> {MI.view_entry_result(~K, ~V, ~cmp, lo2, hi2, d2, MI.entry_snapshot(~K, ~V, ~cmp, MI.view_nav_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, up, incl, M.pick(Bool, up, M.above_lower(~K, ~V, ~cmp, k, lo2), M.below_upper(~K, ~V, ~cmp, k, hi2))))) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.nav(~K, ~V, ~cmp, k, up, incl, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView & Maybe<&2, M.Entry>}: 105 match up: 106 case True{}: 107 %Equal.sym(Bool, M.above_lower(~K, ~V, ~cmp, k, lo2), S.above_lower(~K, ~cmp, k, lo2), CU.al_eq(~K, ~V, ~cmp, k, lo2)) : {MI.view_entry_result(~K, ~V, ~cmp, lo2, hi2, d2, MI.entry_snapshot(~K, ~V, ~cmp, MI.view_nav_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, True{}, incl, _))) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.nav(~K, ~V, ~cmp, k, True{}, incl, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView & Maybe<&2, M.Entry>} 108 vn_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, d2, k, incl, S.above_lower(~K, ~cmp, k, lo2), {==}) 109 case False{}: 110 %Equal.sym(Bool, M.below_upper(~K, ~V, ~cmp, k, hi2), S.below_upper(~K, ~cmp, k, hi2), CU.bu_eq(~K, ~V, ~cmp, k, hi2)) : {MI.view_entry_result(~K, ~V, ~cmp, lo2, hi2, d2, MI.entry_snapshot(~K, ~V, ~cmp, MI.view_nav_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, False{}, incl, _))) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.nav(~K, ~V, ~cmp, k, False{}, incl, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView & Maybe<&2, M.Entry>} 111 vn_f(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, d2, k, incl, S.below_upper(~K, ~cmp, k, hi2), {==}) 112 113 114 def vn_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +k: K, +higher: Bool, +incl: Bool) -> {MI.view_nav(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, higher, incl) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.nav(~K, ~V, ~cmp, k, S.pick(Bool, d2, Bool.not(higher), higher), incl, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView & Maybe<&2, M.Entry>}: 115 match d2: 116 case True{}: 117 vn_up(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, True{}, k, incl, Bool.not(higher)) 118 case False{}: 119 vn_up(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, False{}, k, incl, higher) 120