def keys_sorted.go

bend-kit-collections@0.1.4.1 · PROOF.bend:179

import Base
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws
import bend-kit-collections@0.1.4.1/omap.bend as O

179def keys_sorted.go(
180  ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, t: O.OMap<K, V>, +lb: Maybe<&2, K>,
181  +acc: List<&2, K>,
182  +bt: {Laws.bounded(~K, ~V, ~cmp, t, lb, head(K, acc)) == True{} : Bool},
183  lt: {lt_m(~K, ~cmp, lb, head(K, acc)) == True{} : Bool},
184  sa: {Laws.sorted(~K, ~cmp, acc) == True{} : Bool}
185) -> {sfrom(~K, ~cmp, lb, O.OMap.keys.go(K, V, t, acc)) == True{} : Bool}:
186  match t:
187    case O.OTip{}:
188      sfrom.base(~K, ~cmp, lb, acc, lt, sa)
189    case O.OBin{s, +k, v, +lo, +hi}:
190      +A = Laws.above(~K, ~cmp, lb, k)
191      +B = Laws.below(~K, ~cmp, head(K, acc), k)
192      +L = Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k})
193      +H = Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, head(K, acc))
194      ih = keys_sorted.go(~K, ~V, ~cmp, hi, Some{k}, acc, c4.d(A, B, L, H, bt),
195        lt_m.some(~K, ~cmp, head(K, acc), k, c4.b(A, B, L, H, bt)), sa)
196      keys_sorted.go(~K, ~V, ~cmp, lo, lb, k <> O.OMap.keys.go(K, V, hi, acc),
197        c4.c(A, B, L, H, bt), c4.a(A, B, L, H, bt), ih)