def chk_fit

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixgen.bend:32

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

32# the result r is low(w, n) and bad says n does not fit: Some n exactly
33# when n fits
34def chk_fit(~T: Data, ~val: T -> Nat, +w: Nat, +n: Nat, +r: T, +bad: Bool, +hb: {bad == Bool.not(C.fits(w, n)) : Bool}, +hv: {val(r) == C.low(w, n) : Nat}, +ok: Bool, +hok: {C.fits(w, n) == ok : Bool}) -> {SF.mval(~T, ~val, F.opt(T, bad, r)) == SF.keep(ok, n) : Maybe<&2, Nat>}:
35  match ok:
36    case True{}:
37      some_of(~T, ~val, bad, Equal.trans(Bool, bad, Bool.not(C.fits(w, n)), False{}, hb, bnot_eq(C.fits(w, n), True{}, hok)), r, n, Equal.trans(Nat, val(r), C.low(w, n), n, hv, WW.low_fit(w, n, hok)))
38    case False{}:
39      none_of(~T, ~val, bad, Equal.trans(Bool, bad, Bool.not(C.fits(w, n)), True{}, hb, bnot_eq(C.fits(w, n), False{}, hok)), r)