spec/containers/balanced_search_tree/main.bend source
spec/containers/balanced_search_tree/main.bend on the hub · documented module
import Baseimport ../../lib/common.bend as Cimport ../../../src/containers/balanced_search_tree.bend as Mimport ../../lib/order.bend as SO# Independent model of the indexed TreeMap: a limit exponent (at most# 2^limit entries) and the entries in key order under the comparator ~cmp.# Cursors name their next and current entries by key; views are the map with# a range and a direction. Nothing here refers to nodes, colours, links,# slots or the free list; only the neutral datatypes of the implementation# module (M.Entry, M.Rejected, M.Error, M.Bound) are used.type Model<-K: Data, -V: Data> is Data: TM{limit: Nat, es: List<&2, M.Entry<K, V>>}type Cursor<-K: Data, -V: Data> is Data: CR{map: Model<K, V>, next: Maybe<&2, K>, current: Maybe<&2, K>, lower: M.Bound<K>, upper: M.Bound<K>, forward: Bool}type View<-K: Data, -V: Data> is Data: VW{map: Model<K, V>, lower: M.Bound<K>, upper: M.Bound<K>, descending: Bool}type InvalidView<-K: Data, -V: Data> is Data: IV{map: Model<K, V>, error: M.Error}def pick(-T: Type, +b: Bool, x: T, y: T) -> T: match b: case True{}: x case False{}: ydef new(-K: Data, -V: Data) -> Model<K, V>: TM{31n, Nil{}}def with_limit(-K: Data, -V: Data, +k: Nat) -> Model<K, V>: TM{pick(Nat, Nat.is_lt(k, 31n), k, 31n), Nil{}}def key(-K: Data, -V: Data, e: M.Entry<K, V>) -> K: match e: case M.Entry{k, v}: kdef val(-K: Data, -V: Data, e: M.Entry<K, V>) -> V: match e: case M.Entry{k, v}: vdef keys(-K: Data, -V: Data, es: List<&2, M.Entry<K, V>>) -> List<&2, K>: match es: case Nil{}: Nil{} case Con{e, t}: Con{key(K, V, e), keys(K, V, t)}def is_eq(c: Cmp) -> Bool: match c: case EQ{}: True{} case _: False{}# ---- the entry of a key ----# the first entry whose key is equal to kdef find_e(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, es: List<&2, M.Entry<K, V>>) -> Maybe<&2, M.Entry<K, V>>: match es: case Nil{}: None{} case Con{+e, +t}: pick(Maybe<&2, M.Entry<K, V>>, is_eq(cmp(k, key(K, V, e))), Some{e}, find_e(~K, ~V, ~cmp, k, t))def val_m(-K: Data, -V: Data, m: Maybe<&2, M.Entry<K, V>>) -> Maybe<&2, V>: match m: case None{}: None{} case Some{e}: Some{val(K, V, e)}def key_m(-K: Data, -V: Data, m: Maybe<&2, M.Entry<K, V>>) -> Maybe<&2, K>: match m: case None{}: None{} case Some{e}: Some{key(K, V, e)}def find(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, es: List<&2, M.Entry<K, V>>) -> Maybe<&2, V>: val_m(K, V, find_e(~K, ~V, ~cmp, k, es))def is_some(-X: Data, m: Maybe<&2, X>) -> Bool: match m: case None{}: False{} case Some{x}: True{}# ---- changes ----# k, absent, inserted before the first entry with a greater keydef ins(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, es: List<&2, M.Entry<K, V>>) -> List<&2, M.Entry<K, V>>: match es: case Nil{}: Con{M.Entry{k, v}, Nil{}} case Con{+e, +t}: pick(List<&2, M.Entry<K, V>>, Cmp.is_lt(cmp(k, key(K, V, e))), Con{M.Entry{k, v}, Con{e, t}}, Con{e, ins(~K, ~V, ~cmp, k, v, t)})# the value of the first entry equal to k replaced (its key is kept)def set_val(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, es: List<&2, M.Entry<K, V>>) -> List<&2, M.Entry<K, V>>: match es: case Nil{}: Nil{} case Con{+e, +t}: pick(List<&2, M.Entry<K, V>>, is_eq(cmp(k, key(K, V, e))), Con{M.Entry{key(K, V, e), v}, t}, Con{e, set_val(~K, ~V, ~cmp, k, v, t)})# the first entry equal to k removeddef del(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, es: List<&2, M.Entry<K, V>>) -> List<&2, M.Entry<K, V>>: match es: case Nil{}: Nil{} case Con{+e, +t}: pick(List<&2, M.Entry<K, V>>, is_eq(cmp(k, key(K, V, e))), t, Con{e, del(~K, ~V, ~cmp, k, t)})# ---- ranges ----def ordering_ok(c: Cmp, inclusive: Bool) -> Bool: match c: case LT{}: True{} case EQ{}: inclusive case GT{}: False{}def above_lower(~K: Data, ~cmp: K -> K -> Cmp, +k: K, b: M.Bound<K>) -> Bool: match b: case M.Unbounded{}: True{} case M.Inclusive{lo}: ordering_ok(cmp(lo, k), True{}) case M.Exclusive{lo}: ordering_ok(cmp(lo, k), False{})def below_upper(~K: Data, ~cmp: K -> K -> Cmp, +k: K, b: M.Bound<K>) -> Bool: match b: case M.Unbounded{}: True{} case M.Inclusive{hi}: ordering_ok(cmp(k, hi), True{}) case M.Exclusive{hi}: ordering_ok(cmp(k, hi), False{})def in_range(~K: Data, ~cmp: K -> K -> Cmp, +k: K, lo: M.Bound<K>, hi: M.Bound<K>) -> Bool: Bool.and(above_lower(~K, ~cmp, k, lo), below_upper(~K, ~cmp, k, hi))# a view's bounds are valid when neither is past the otherdef bounds_valid(~K: Data, ~cmp: K -> K -> Cmp, lo: M.Bound<K>, hi: M.Bound<K>) -> Bool: match lo hi: case M.Unbounded{} _: True{} case _ M.Unbounded{}: True{} case M.Inclusive{a} M.Inclusive{b}: ordering_ok(cmp(a, b), True{}) case M.Inclusive{a} M.Exclusive{b}: ordering_ok(cmp(a, b), True{}) case M.Exclusive{a} M.Inclusive{b}: ordering_ok(cmp(a, b), True{}) case M.Exclusive{a} M.Exclusive{b}: ordering_ok(cmp(a, b), True{})def within(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo: M.Bound<K>, +hi: M.Bound<K>, es: List<&2, M.Entry<K, V>>) -> List<&2, M.Entry<K, V>>: match es: case Nil{}: Nil{} case Con{+e, +t}: pick(List<&2, M.Entry<K, V>>, in_range(~K, ~cmp, key(K, V, e), lo, hi), Con{e, within(~K, ~V, ~cmp, lo, hi, t)}, within(~K, ~V, ~cmp, lo, hi, t))def outside(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo: M.Bound<K>, +hi: M.Bound<K>, es: List<&2, M.Entry<K, V>>) -> List<&2, M.Entry<K, V>>: match es: case Nil{}: Nil{} case Con{+e, +t}: pick(List<&2, M.Entry<K, V>>, in_range(~K, ~cmp, key(K, V, e), lo, hi), outside(~K, ~V, ~cmp, lo, hi, t), Con{e, outside(~K, ~V, ~cmp, lo, hi, t)})# ---- order queries ----# the first entry e with keep(cmp(k, e.key))def first_where(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +inclusive: Bool, es: List<&2, M.Entry<K, V>>) -> Maybe<&2, M.Entry<K, V>>: match es: case Nil{}: None{} case Con{+e, +t}: pick(Maybe<&2, M.Entry<K, V>>, ordering_ok(cmp(k, key(K, V, e)), inclusive), Some{e}, first_where(~K, ~V, ~cmp, k, inclusive, t))# the last entry e below k (or equal, when inclusive)def last_where(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +inclusive: Bool, es: List<&2, M.Entry<K, V>>, +best: Maybe<&2, M.Entry<K, V>>) -> Maybe<&2, M.Entry<K, V>>: match es: case Nil{}: best case Con{+e, t}: last_where(~K, ~V, ~cmp, k, inclusive, t, pick(Maybe<&2, M.Entry<K, V>>, ordering_ok(cmp(key(K, V, e), k), inclusive), Some{e}, best))def head(-X: Data, xs: List<&2, X>) -> Maybe<&2, X>: match xs: case Nil{}: None{} case Con{x, t}: Some{x}def last(-X: Data, xs: List<&2, X>) -> Maybe<&2, X>: C.last(X, xs)# ceiling (higher: strict) when up, floor (lower: strict) otherwisedef nav(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +up: Bool, +inclusive: Bool, es: List<&2, M.Entry<K, V>>) -> Maybe<&2, M.Entry<K, V>>: match up: case True{}: first_where(~K, ~V, ~cmp, k, inclusive, es) case False{}: last_where(~K, ~V, ~cmp, k, inclusive, es, None{})# the key after (forward) or before kdef succ(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +forward: Bool, es: List<&2, M.Entry<K, V>>) -> Maybe<&2, K>: key_m(K, V, nav(~K, ~V, ~cmp, k, forward, False{}, es))# the first entry past a bound, in a directiondef start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, b: M.Bound<K>, +forward: Bool, es: List<&2, M.Entry<K, V>>) -> Maybe<&2, K>: match b forward: case M.Unbounded{} True{}: key_m(K, V, head(M.Entry<K, V>, es)) case M.Unbounded{} False{}: key_m(K, V, last(M.Entry<K, V>, es)) case M.Inclusive{+x} _: key_m(K, V, nav(~K, ~V, ~cmp, x, forward, True{}, es)) case M.Exclusive{+x} _: key_m(K, V, nav(~K, ~V, ~cmp, x, forward, False{}, es))# ---- the map ----def size(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Nat: match m: case TM{+l, +es}: (TM{l, es}, C.length(M.Entry<K, V>, es))def is_empty(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Bool: match m: case TM{+l, +es}: (TM{l, es}, Nat.is_eq(C.length(M.Entry<K, V>, es), 0n))def put_new(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V) -> Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>: pick(Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, Nat.is_lt(C.length(M.Entry<K, V>, es), C.pow2(l)), (TM{l, ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}), (TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}}))def put_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, old: Maybe<&2, V>) -> Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>: match old: case Some{+o}: (TM{l, set_val(~K, ~V, ~cmp, k, v, es)}, Done{Some{o}}) case None{}: put_new(~K, ~V, ~cmp, l, es, k, v)# k mapped to v: replaced when present, inserted when there is roomdef put(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, +v: V) -> Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>: match m: case TM{+l, +es}: put_at(~K, ~V, ~cmp, l, es, k, v, find(~K, ~V, ~cmp, k, es))def absent_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, old: Maybe<&2, V>) -> Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>: match old: case Some{+o}: (TM{l, es}, Done{Some{o}}) case None{}: put_new(~K, ~V, ~cmp, l, es, k, v)def put_if_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, +v: V) -> Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>: match m: case TM{+l, +es}: absent_at(~K, ~V, ~cmp, l, es, k, v, find(~K, ~V, ~cmp, k, es))def get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K) -> Model<K, V> & Maybe<&2, V>: match m: case TM{+l, +es}: (TM{l, es}, find(~K, ~V, ~cmp, k, es))def or_default(-V: Data, m: Maybe<&2, V>, fallback: V) -> V: match m: case None{}: fallback case Some{v}: vdef get_or_default(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, fallback: V) -> Model<K, V> & V: match m: case TM{+l, +es}: (TM{l, es}, or_default(V, find(~K, ~V, ~cmp, k, es), fallback))def contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K) -> Model<K, V> & Bool: match m: case TM{+l, +es}: (TM{l, es}, is_some(V, find(~K, ~V, ~cmp, k, es)))def remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K) -> Model<K, V> & Maybe<&2, V>: match m: case TM{+l, +es}: (TM{l, del(~K, ~V, ~cmp, k, es)}, find(~K, ~V, ~cmp, k, es))def replace_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, old: Maybe<&2, V>) -> Model<K, V> & Maybe<&2, V>: match old: case Some{+o}: (TM{l, set_val(~K, ~V, ~cmp, k, v, es)}, Some{o}) case None{}: (TM{l, es}, None{})def replace(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, +v: V) -> Model<K, V> & Maybe<&2, V>: match m: case TM{+l, +es}: replace_at(~K, ~V, ~cmp, l, es, k, v, find(~K, ~V, ~cmp, k, es))def any_value(~K: Data, ~V: Data, ~eq: V -> V -> Bool, +w: V, es: List<&2, M.Entry<K, V>>) -> Bool: match es: case Nil{}: False{} case Con{e, t}: Bool.or(eq(val(K, V, e), w), any_value(~K, ~V, ~eq, w, t))def contains_value(~K: Data, ~V: Data, ~eq: V -> V -> Bool, m: Model<K, V>, +w: V) -> Model<K, V> & Bool: match m: case TM{+l, +es}: (TM{l, es}, any_value(~K, ~V, ~eq, w, es))def remove_if_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +expected: V, old: Maybe<&2, V>) -> Model<K, V> & Bool: match old: case None{}: (TM{l, es}, False{}) case Some{o}: pick(Model<K, V> & Bool, eq(o, expected), (TM{l, del(~K, ~V, ~cmp, k, es)}, True{}), (TM{l, es}, False{}))def remove_if_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: Model<K, V>, +k: K, +expected: V) -> Model<K, V> & Bool: match m: case TM{+l, +es}: remove_if_at(~K, ~V, ~cmp, ~eq, l, es, k, expected, find(~K, ~V, ~cmp, k, es))def replace_if_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +expected: V, +replacement: V, old: Maybe<&2, V>) -> Model<K, V> & Bool: match old: case None{}: (TM{l, es}, False{}) case Some{o}: pick(Model<K, V> & Bool, eq(o, expected), (TM{l, set_val(~K, ~V, ~cmp, k, replacement, es)}, True{}), (TM{l, es}, False{}))def replace_if_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: Model<K, V>, +k: K, +expected: V, +replacement: V) -> Model<K, V> & Bool: match m: case TM{+l, +es}: replace_if_at(~K, ~V, ~cmp, ~eq, l, es, k, expected, replacement, find(~K, ~V, ~cmp, k, es))def clear(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V>: match m: case TM{+l, es}: TM{l, Nil{}}def first_entry(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Maybe<&2, M.Entry<K, V>>: match m: case TM{+l, +es}: (TM{l, es}, head(M.Entry<K, V>, es))def last_entry(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Maybe<&2, M.Entry<K, V>>: match m: case TM{+l, +es}: (TM{l, es}, last(M.Entry<K, V>, es))def first_key(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Maybe<&2, K>: match m: case TM{+l, +es}: (TM{l, es}, key_m(K, V, head(M.Entry<K, V>, es)))def last_key(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Maybe<&2, K>: match m: case TM{+l, +es}: (TM{l, es}, key_m(K, V, last(M.Entry<K, V>, es)))# lower/floor (up False) and ceiling/higher (up True) entriesdef nav_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, +up: Bool, +inclusive: Bool) -> Model<K, V> & Maybe<&2, M.Entry<K, V>>: match m: case TM{+l, +es}: (TM{l, es}, nav(~K, ~V, ~cmp, k, up, inclusive, es))def nav_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, +up: Bool, +inclusive: Bool) -> Model<K, V> & Maybe<&2, K>: match m: case TM{+l, +es}: (TM{l, es}, key_m(K, V, nav(~K, ~V, ~cmp, k, up, inclusive, es)))def poll_first_entry(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Maybe<&2, M.Entry<K, V>>: match m: case TM{+l, es}: match es: case Nil{}: (TM{l, Nil{}}, None{}) case Con{e, t}: (TM{l, t}, Some{e})def poll_last_entry(-K: Data, -V: Data, m: Model<K, V>) -> Model<K, V> & Maybe<&2, M.Entry<K, V>>: match m: case TM{+l, +es}: (TM{l, C.init(M.Entry<K, V>, es)}, last(M.Entry<K, V>, es))# ---- cursors ----def iterator(-K: Data, -V: Data, m: Model<K, V>) -> Cursor<K, V>: match m: case TM{+l, +es}: CR{TM{l, es}, key_m(K, V, head(M.Entry<K, V>, es)), None{}, M.Unbounded{}, M.Unbounded{}, True{}}def descending_iterator(-K: Data, -V: Data, m: Model<K, V>) -> Cursor<K, V>: match m: case TM{+l, +es}: CR{TM{l, es}, key_m(K, V, last(M.Entry<K, V>, es)), None{}, M.Unbounded{}, M.Unbounded{}, False{}}def next_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +current: Maybe<&2, K>, +lo: M.Bound<K>, +hi: M.Bound<K>, +forward: Bool, found: Maybe<&2, M.Entry<K, V>>) -> Cursor<K, V> & Maybe<&2, M.Entry<K, V>>: match found: case None{}: (CR{TM{l, es}, None{}, current, lo, hi, forward}, None{}) case Some{M.Entry{+k, +v}}: pick(Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, in_range(~K, ~cmp, k, lo, hi), (CR{TM{l, es}, succ(~K, ~V, ~cmp, k, forward, es), Some{k}, lo, hi, forward}, Some{M.Entry{k, v}}), (CR{TM{l, es}, None{}, current, lo, hi, forward}, None{}))def iterator_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: Cursor<K, V>) -> Cursor<K, V> & Maybe<&2, M.Entry<K, V>>: match c: case CR{TM{+l, +es}, next, +current, +lo, +hi, +forward}: match next: case None{}: (CR{TM{l, es}, None{}, current, lo, hi, forward}, None{}) case Some{+k}: next_at(~K, ~V, ~cmp, l, es, current, lo, hi, forward, find_e(~K, ~V, ~cmp, k, es))def iterator_has_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: Cursor<K, V>) -> Cursor<K, V> & Bool: match c: case CR{m, next, current, +lo, +hi, forward}: match next: case None{}: (CR{m, None{}, current, lo, hi, forward}, False{}) case Some{+k}: (CR{m, Some{k}, current, lo, hi, forward}, in_range(~K, ~cmp, k, lo, hi))def set_value_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, next: Maybe<&2, K>, +k: K, lo: M.Bound<K>, hi: M.Bound<K>, +forward: Bool, +v: V, old: Maybe<&2, V>) -> Cursor<K, V> & Result<&2, &2, M.Error, V>: match old: case None{}: (CR{TM{l, es}, next, Some{k}, lo, hi, forward}, Fail{M.NoCurrent{}}) case Some{o}: (CR{TM{l, set_val(~K, ~V, ~cmp, k, v, es)}, next, Some{k}, lo, hi, forward}, Done{o})def iterator_set_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: Cursor<K, V>, +v: V) -> Cursor<K, V> & Result<&2, &2, M.Error, V>: match c: case CR{TM{+l, +es}, next, current, lo, hi, +forward}: match current: case None{}: (CR{TM{l, es}, next, None{}, lo, hi, forward}, Fail{M.NoCurrent{}}) case Some{+k}: set_value_at(~K, ~V, ~cmp, l, es, next, k, lo, hi, forward, v, find(~K, ~V, ~cmp, k, es))def iterator_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: Cursor<K, V>) -> Cursor<K, V> & Maybe<&2, V>: match c: case CR{TM{+l, +es}, next, current, lo, hi, forward}: match current: case None{}: (CR{TM{l, es}, next, None{}, lo, hi, forward}, None{}) case Some{+k}: (CR{TM{l, del(~K, ~V, ~cmp, k, es)}, next, None{}, lo, hi, forward}, find(~K, ~V, ~cmp, k, es))def iterator_finish(-K: Data, -V: Data, c: Cursor<K, V>) -> Model<K, V>: match c: case CR{m, next, current, lo, hi, forward}: mdef key_result(-K: Data, -V: Data, r: Cursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> Cursor<K, V> & Maybe<&2, K>: match r: case Tuple{c2, m}: (c2, key_m(K, V, m))def value_result(-K: Data, -V: Data, r: Cursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> Cursor<K, V> & Maybe<&2, V>: match r: case Tuple{c2, m}: (c2, val_m(K, V, m))def iterator_next_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: Cursor<K, V>) -> Cursor<K, V> & Maybe<&2, K>: key_result(K, V, iterator_next(~K, ~V, ~cmp, c))def iterator_next_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: Cursor<K, V>) -> Cursor<K, V> & Maybe<&2, V>: value_result(K, V, iterator_next(~K, ~V, ~cmp, c))# ---- views ----def view_checked(-K: Data, -V: Data, m: Model<K, V>, lo: M.Bound<K>, hi: M.Bound<K>, valid: Bool) -> Result<&1, &1, InvalidView<K, V>, View<K, V>>: match valid: case True{}: Done{VW{m, lo, hi, False{}}} case False{}: Fail{IV{m, M.InvalidBounds{}}}def sub_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +lo: M.Bound<K>, +hi: M.Bound<K>) -> Result<&1, &1, InvalidView<K, V>, View<K, V>>: view_checked(K, V, m, lo, hi, bounds_valid(~K, ~cmp, lo, hi))def head_map(-K: Data, -V: Data, m: Model<K, V>, hi: M.Bound<K>) -> View<K, V>: VW{m, M.Unbounded{}, hi, False{}}def tail_map(-K: Data, -V: Data, m: Model<K, V>, lo: M.Bound<K>) -> View<K, V>: VW{m, lo, M.Unbounded{}, False{}}def descending_map(-K: Data, -V: Data, m: Model<K, V>) -> View<K, V>: VW{m, M.Unbounded{}, M.Unbounded{}, True{}}def view_reverse(-K: Data, -V: Data, w: View<K, V>) -> View<K, V>: match w: case VW{m, lo, hi, +d}: VW{m, lo, hi, Bool.not(d)}def view_finish(-K: Data, -V: Data, w: View<K, V>) -> Model<K, V>: match w: case VW{m, lo, hi, d}: mdef view_get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>, +k: K) -> View<K, V> & Maybe<&2, V>: match w: case VW{TM{+l, +es}, +lo, +hi, +d}: (VW{TM{l, es}, lo, hi, d}, pick(Maybe<&2, V>, in_range(~K, ~cmp, k, lo, hi), find(~K, ~V, ~cmp, k, es), None{}))def contained(-K: Data, -V: Data, r: View<K, V> & Maybe<&2, V>) -> View<K, V> & Bool: match r: case Tuple{w2, m}: (w2, is_some(V, m))def view_contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>, +k: K) -> View<K, V> & Bool: contained(K, V, view_get(~K, ~V, ~cmp, w, k))def rewrap_put(-K: Data, -V: Data, lo: M.Bound<K>, hi: M.Bound<K>, +d: Bool, r: Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>) -> View<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>: match r: case Tuple{m2, x}: (VW{m2, lo, hi, d}, x)def view_put_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, +v: V, lo: M.Bound<K>, hi: M.Bound<K>, +d: Bool, valid: Bool) -> View<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>: match valid: case True{}: rewrap_put(K, V, lo, hi, d, put(~K, ~V, ~cmp, m, k, v)) case False{}: (VW{m, lo, hi, d}, Fail{M.Rejected{M.OutOfRange{}, k, v}})def view_put(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>, +k: K, +v: V) -> View<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>: match w: case VW{m, +lo, +hi, +d}: view_put_at(~K, ~V, ~cmp, m, k, v, lo, hi, d, in_range(~K, ~cmp, k, lo, hi))def rewrap_val(-K: Data, -V: Data, lo: M.Bound<K>, hi: M.Bound<K>, +d: Bool, r: Model<K, V> & Maybe<&2, V>) -> View<K, V> & Maybe<&2, V>: match r: case Tuple{m2, x}: (VW{m2, lo, hi, d}, x)def view_remove_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: Model<K, V>, +k: K, lo: M.Bound<K>, hi: M.Bound<K>, +d: Bool, valid: Bool) -> View<K, V> & Maybe<&2, V>: match valid: case True{}: rewrap_val(K, V, lo, hi, d, remove(~K, ~V, ~cmp, m, k)) case False{}: (VW{m, lo, hi, d}, None{})def view_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>, +k: K) -> View<K, V> & Maybe<&2, V>: match w: case VW{m, +lo, +hi, +d}: view_remove_at(~K, ~V, ~cmp, m, k, lo, hi, d, in_range(~K, ~cmp, k, lo, hi))def view_size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>) -> View<K, V> & Nat: match w: case VW{TM{+l, +es}, +lo, +hi, +d}: (VW{TM{l, es}, lo, hi, d}, C.length(M.Entry<K, V>, within(~K, ~V, ~cmp, lo, hi, es)))def view_clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>) -> View<K, V>: match w: case VW{TM{+l, +es}, +lo, +hi, +d}: VW{TM{l, outside(~K, ~V, ~cmp, lo, hi, es)}, lo, hi, d}# the view's first (or last) entry in its own directiondef view_extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>, +first: Bool) -> View<K, V> & Maybe<&2, M.Entry<K, V>>: match w: case VW{TM{+l, +es}, +lo, +hi, +d}: (VW{TM{l, es}, lo, hi, d}, pick(Maybe<&2, M.Entry<K, V>>, pick(Bool, d, Bool.not(first), first), head(M.Entry<K, V>, within(~K, ~V, ~cmp, lo, hi, es)), last(M.Entry<K, V>, within(~K, ~V, ~cmp, lo, hi, es))))def view_first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>) -> View<K, V> & Maybe<&2, M.Entry<K, V>>: view_extreme(~K, ~V, ~cmp, w, True{})def view_last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>) -> View<K, V> & Maybe<&2, M.Entry<K, V>>: view_extreme(~K, ~V, ~cmp, w, False{})# the view's lower/floor (higher False) or ceiling/higher (higher True)# entry, in the view's own directiondef view_nav(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>, +k: K, +higher: Bool, +inclusive: Bool) -> View<K, V> & Maybe<&2, M.Entry<K, V>>: match w: case VW{TM{+l, +es}, +lo, +hi, +d}: (VW{TM{l, es}, lo, hi, d}, nav(~K, ~V, ~cmp, k, pick(Bool, d, Bool.not(higher), higher), inclusive, within(~K, ~V, ~cmp, lo, hi, es)))def view_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: View<K, V>) -> Cursor<K, V>: match w: case VW{TM{+l, +es}, +lo, +hi, +d}: CR{TM{l, es}, start(~K, ~V, ~cmp, pick(M.Bound<K>, d, hi, lo), Bool.not(d), es), None{}, lo, hi, Bool.not(d)}# the map's invariant: consecutive keys strictly increasing (SPARK's ordered# maps keep Keys (Container) sorted; Formal_Ordered_Maps, Formal_Model.K)def ordered(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, es: List<&2, M.Entry<K, V>>) -> Bool: match es: case Nil{}: True{} case Con{e, t}: match t: case Nil{}: True{} case Con{+e2, +u}: Bool.and(Cmp.is_lt(cmp(key(K, V, e), key(K, V, e2))), ordered(~K, ~V, ~cmp, Con{e2, u}))# ---- contract (SPARK formal containers) ----# Each `<Subprogram>.<clause>` definition below states one Post clause of# that SPARK subprogram, as a proposition on this model; the table names the# clauses. proofs/containers/balanced_search_tree/ proves every clause under its clause name,# and its `impl` lemma carries them to the implementation.## Contracts of the TreeMap in the style of SPARK's formal ordered maps# (SPARKlib src/full/spark-containers-formal-ordered_maps.ads, AdaCore/# SPARKlib master), stated on the independent model (this file: a limit and# the entries in key order). The refinement proof (proof.bend, api/capi/# vapi) shows the implementation returns exactly the model's result for# every operation, so each clause holds of the implementation.# Model (K) = S.find (K, es); keys are compared by ~cmp, a total order# (O.Order: flip, antisymmetry, transitivity); the entries are ordered# (ST.ordered), which is the model's invariant.## SPARK subprogram (.ads line) ours clauses# Empty_Map (101) new new_empty# Length (114), Is_Empty (425) size, is_empty size_value, is_empty_value# Clear (433) clear clear_empty# Element (Key) (1283), Find (1257) get, get_or_default get_value, get_or_default_value# Contains (1332) contains_key contains_value# Include (754) put put_present, put_absent, put_full,# put_found_present, put_found_absent,# find_set_other, find_ins_other (others unchanged),# set_length, ins_length# Insert (612/697, keeps a present key) put_if_absent put_if_absent_present, put_if_absent_absent# Replace (846) replace replace_present, replace_absent,# find_set_same, find_set_other# Exclude (884) / Delete (937) remove remove_present, remove_absent,# find_del_same (gone), find_del_other, del_length# First/First_Element/First_Key (1116-1137) first_value# Last/Last_Element/Last_Key (1148-1171) last_value# Floor (1291), Ceiling (1312) floor/ceiling/lower/higher (key, entry) nav_value# Delete_First (1037), Delete_Last (1077) poll_first/last_entry (model: S.poll_*; refinement: proof.bend)# Not in this API: "=", Assign/Copy/Move, Reference, Replace_Element and# Key/Element/Next/Previous by cursor (the map's cursors are its iterators,# whose steps the refinement proof relates to S.succ), Has_Element.# Include (754)def Include.find_ins_other(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +q: K, +hq: {is_eq(cmp(q, k)) == False{} : Bool}, +es: List<&2, M.Entry<K, V>>) -> Type: {find_e(~K, ~V, ~cmp, q, ins(~K, ~V, ~cmp, k, v, es)) == find_e(~K, ~V, ~cmp, q, es) : Maybe<&2, M.Entry<K, V>>}# Include (754)def Include.ins_length(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +es: List<&2, M.Entry<K, V>>) -> Type: {C.length(M.Entry<K, V>, ins(~K, ~V, ~cmp, k, v, es)) == 1n+C.length(M.Entry<K, V>, es) : Nat}# Replace (846)def Replace.find_set_same(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +e0: M.Entry<K, V>, +es: List<&2, M.Entry<K, V>>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type: {find(~K, ~V, ~cmp, k, set_val(~K, ~V, ~cmp, k, v, es)) == Some{v} : Maybe<&2, V>}# Include (754)def Include.find_set_other(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +v: V, +q: K, +hq: {is_eq(cmp(q, k)) == False{} : Bool}, +es: List<&2, M.Entry<K, V>>) -> Type: {find_e(~K, ~V, ~cmp, q, set_val(~K, ~V, ~cmp, k, v, es)) == find_e(~K, ~V, ~cmp, q, es) : Maybe<&2, M.Entry<K, V>>}# Include (754)def Include.set_length(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +es: List<&2, M.Entry<K, V>>) -> Type: {C.length(M.Entry<K, V>, set_val(~K, ~V, ~cmp, k, v, es)) == C.length(M.Entry<K, V>, es) : Nat}# Exclude (884) / Delete (937)def Exclude.find_del_other(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +q: K, +hq: {is_eq(cmp(q, k)) == False{} : Bool}, +es: List<&2, M.Entry<K, V>>) -> Type: {find_e(~K, ~V, ~cmp, q, del(~K, ~V, ~cmp, k, es)) == find_e(~K, ~V, ~cmp, q, es) : Maybe<&2, M.Entry<K, V>>}# Exclude (884) / Delete (937)def Exclude.find_del_same(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +es: List<&2, M.Entry<K, V>>, +hord: {ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> Type: {find_e(~K, ~V, ~cmp, k, del(~K, ~V, ~cmp, k, es)) == None{} : Maybe<&2, M.Entry<K, V>>}# Exclude (884) / Delete (937)def Exclude.del_length(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +e0: M.Entry<K, V>, +es: List<&2, M.Entry<K, V>>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type: {1n+C.length(M.Entry<K, V>, del(~K, ~V, ~cmp, k, es)) == C.length(M.Entry<K, V>, es) : Nat}# Empty_Map (101)def Empty_Map.new_empty(-K: Data, -V: Data) -> Type: {new(K, V) == TM{31n, Nil{}} : Model<K, V>}# Length (114), Is_Empty (425)def Length.size_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> Type: {size(K, V, TM{l, es}) == (TM{l, es}, C.length(M.Entry<K, V>, es)) : Model<K, V> & Nat}# Length (114), Is_Empty (425)def Length.is_empty_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> Type: {is_empty(K, V, TM{l, es}) == (TM{l, es}, Nat.is_eq(C.length(M.Entry<K, V>, es), 0n)) : Model<K, V> & Bool}# Clear (433)def Clear.clear_empty(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> Type: {clear(K, V, TM{l, es}) == TM{l, Nil{}} : Model<K, V>}# Element (Key) (1283), Find (1257)def Element.get_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K) -> Type: {get(~K, ~V, ~cmp, TM{l, es}, k) == (TM{l, es}, find(~K, ~V, ~cmp, k, es)) : Model<K, V> & Maybe<&2, V>}# Element (Key) (1283), Find (1257)def Element.get_or_default_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +d: V) -> Type: {get_or_default(~K, ~V, ~cmp, TM{l, es}, k, d) == (TM{l, es}, or_default(V, find(~K, ~V, ~cmp, k, es), d)) : Model<K, V> & V}# Contains (1332)def Contains.contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K) -> Type: {contains_key(~K, ~V, ~cmp, TM{l, es}, k) == (TM{l, es}, is_some(V, find(~K, ~V, ~cmp, k, es))) : Model<K, V> & Bool}# Include (754)def Include.put_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +e0: M.Entry<K, V>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type: {put(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, set_val(~K, ~V, ~cmp, k, v, es)}, Done{Some{val(K, V, e0)}}) : Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}# Include (754)def Include.put_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}, +hr: {Nat.is_lt(C.length(M.Entry<K, V>, es), C.pow2(l)) == True{} : Bool}) -> Type: {put(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}) : Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}# Include (754)def Include.put_full(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}, +hr: {Nat.is_lt(C.length(M.Entry<K, V>, es), C.pow2(l)) == False{} : Bool}) -> Type: {put(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}}) : Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}# Include (754)def Include.put_found_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +e0: M.Entry<K, V>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type: {find(~K, ~V, ~cmp, k, set_val(~K, ~V, ~cmp, k, v, es)) == Some{v} : Maybe<&2, V>}# Include (754)def Include.put_found_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}) -> Type: {find(~K, ~V, ~cmp, k, ins(~K, ~V, ~cmp, k, v, es)) == Some{v} : Maybe<&2, V>}# Insert (612/697, keeps a present key) put_if_absentdef Insert.put_if_absent_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +e0: M.Entry<K, V>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type: {put_if_absent(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, es}, Done{Some{val(K, V, e0)}}) : Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}# Insert (612/697, keeps a present key) put_if_absentdef Insert.put_if_absent_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}, +hr: {Nat.is_lt(C.length(M.Entry<K, V>, es), C.pow2(l)) == True{} : Bool}) -> Type: {put_if_absent(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}) : Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}# Replace (846)def Replace.replace_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +e0: M.Entry<K, V>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type: {replace(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, set_val(~K, ~V, ~cmp, k, v, es)}, Some{val(K, V, e0)}) : Model<K, V> & Maybe<&2, V>}# Replace (846)def Replace.replace_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}) -> Type: {replace(~K, ~V, ~cmp, TM{l, es}, k, v) == (TM{l, es}, None{}) : Model<K, V> & Maybe<&2, V>}# Exclude (884) / Delete (937)def Exclude.remove_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +e0: M.Entry<K, V>, +hp: {find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> Type: {remove(~K, ~V, ~cmp, TM{l, es}, k) == (TM{l, del(~K, ~V, ~cmp, k, es)}, Some{val(K, V, e0)}) : Model<K, V> & Maybe<&2, V>}# Exclude (884) / Delete (937)def Exclude.remove_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +ha: {find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}) -> Type: {remove(~K, ~V, ~cmp, TM{l, es}, k) == (TM{l, es}, None{}) : Model<K, V> & Maybe<&2, V>}# First/First_Element/First_Key (1116-1137)def First.first_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> Type: {first_entry(K, V, TM{l, es}) == (TM{l, es}, head(M.Entry<K, V>, es)) : Model<K, V> & Maybe<&2, M.Entry<K, V>>}# Last/Last_Element/Last_Key (1148-1171)def Last.last_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> Type: {last_entry(K, V, TM{l, es}) == (TM{l, es}, last(M.Entry<K, V>, es)) : Model<K, V> & Maybe<&2, M.Entry<K, V>>}# Floor (1291), Ceiling (1312)def Floor.nav_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +up: Bool, +inclusive: Bool) -> Type: {nav_entry(~K, ~V, ~cmp, TM{l, es}, k, up, inclusive) == (TM{l, es}, nav(~K, ~V, ~cmp, k, up, inclusive, es)) : Model<K, V> & Maybe<&2, M.Entry<K, V>>}