def integral

bend-collections-laws-crypto@1.0.0.0 · spec/math/f64.bend:325

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/math/f64.bend as F

325# the integer magnitude of (-1)^s * m * 2^-k, k >= 1, in each direction: the
326# integer part high(k, m), plus one when the discarded low(k, m) is nonzero
327# and the direction is away from zero (floor of a negative, ceil of a
328# positive), or to nearest with ties to even (rne)
329def integral(m: F.RMode, +s: Bool, +n: Nat, +k: Nat) -> Nat:
330  match m:
331    case F.Trunc{}:
332      C.high(k, n)
333    case F.Floor{}:
334      Nat.add(C.high(k, n), b2n(Bool.and(s, Bool.not(Nat.is_eq(C.low(k, n), 0n)))))
335    case F.Ceil{}:
336      Nat.add(C.high(k, n), b2n(Bool.and(Bool.not(s), Bool.not(Nat.is_eq(C.low(k, n), 0n)))))
337    case F.Even{}:
338      rne(n, k)