src/float/sf32.bend source
src/float/sf32.bend on the hub · documented module
import Baseimport ./bin.bend as Binimport ./format.bend as Fmtimport ./num.bend as Num# sf32.bend: binary32 floats in software, and the two F32 implementations.## import ./sf32.bend as SF32# SF32.add(a, b) # software IEEE add on F32 bit patterns# SF32.soft(), SF32.hard() # Num.Impl<F32>: software, and hardware## decode and encode convert between F32 bits (sign, 8 exponent bits, 23# mantissa bits) and exact values. The software operations are the spec# itself: decode, exact operation and rounding, encode. They compute in# the checker and give the same bits on every backend; they are also far# slower than hardware. A faster algorithm can be another Num.Impl.## hard() uses Base's F32.add and F32.mul, which the checker cannot# compute. HardOk is the assumption that they are correctly rounded:# a law that needs it takes ~ok: HardOk, and it stays a named hypothesis.def bits(x: F32) -> U32: match x: case F32{w}: U32{w}def of_bits(x: U32) -> F32: match x: case U32{w}: F32{w}# Decoding# --------# The fields are read off the word in one pass (23 mantissa bits, 8# exponent bits, the sign), not with U32 shifts and masks: the checker# evaluates a U32 operation bit by bit, and each shift costs a full pass.def decode.go(neg: Bool, e: Nat, f: Bin.Bin, top: Bool, low: Bool, fz: Bool) -> Fmt.Val: match top low fz: case True{} low True{}: Fmt.Inf{neg} case True{} low False{}: Fmt.NaN{} case False{} True{} True{}: Fmt.Z{neg} case False{} True{} False{}: Fmt.Fin{neg, f, 151n} case False{} False{} fz: Fmt.Fin{neg, Bin.add(f, Bin.pow2(23n)), Nat.add(e, 150n)}def decode.cls(neg: Bool, +e: Nat, +f: Bin.Bin) -> Fmt.Val: decode.go(neg, e, f, Nat.is_eq(e, 255n), Nat.is_eq(e, 0n), Bin.is_zero(f))def decode.sign(f: Bin.Bin, e: Bin.Bin, w: Word(1n)) -> Fmt.Val: match w: case WCon{s, t}: decode.cls(s, Bin.to_nat(e), f)def decode.exp(f: Bin.Bin, p: Bin.Bin & Word(1n)) -> Fmt.Val: (e, w) = p decode.sign(f, e, w)def decode.man(p: Bin.Bin & Word(9n)) -> Fmt.Val: (f, w) = p decode.exp(f, Bin.take(8n, 1n, w))# the exact value of a floatdef decode(x: F32) -> Fmt.Val: match x: case F32{w}: decode.man(Bin.take(23n, 9n, w))# Encoding# --------# the sign bit, as it sits above the 8 exponent bitsdef sign(neg: Bool) -> Bin.Bin: match neg: case True{}: Bin.pow2(8n) case False{}: Bin.BZ{}# a word from its fields: 23 mantissa bits, then exponent and sign abovedef word(frac: Bin.Bin, exp: Bin.Bin, neg: Bool) -> F32: F32{Bin.to_word(32n, Bin.add(Bin.low(23n, frac), Bin.shl(Bin.add(exp, sign(neg)), 23n)))}def first(r: Bin.Bin & Bool & Bool) -> Bin.Bin: (q, a, b) = r q# m moved to have its last bit at exponent tdef align(m: Bin.Bin, +e: Nat, +t: Nat, right: Bool) -> Bin.Bin: match right: case True{}: first(Bin.shr(Nat.sub(t, e), m, False{}, False{})) case False{}: Bin.shl(m, Nat.sub(e, t))def field(+t: Nat, normal: Bool) -> Bin.Bin: match normal: case True{}: Bin.of_nat(Nat.sub(t, 150n)) case False{}: Bin.BZ{}def put(neg: Bool, t: Nat, +m: Bin.Bin) -> F32: word(m, field(t, Nat.is_eq(Bin.len(m), 24n)), neg)# a finite value that fits binary32, as bits: 24 mantissa bits when# normal, fewer at the smallest exponent when subnormaldef encode.fin(neg: Bool, +m: Bin.Bin, +e: Nat) -> F32: +t = Nat.max(Nat.sub(Nat.add(e, Bin.len(m)), 24n), 151n) put(neg, t, align(m, e, t, Nat.is_ge(t, e)))def encode(v: Fmt.Val) -> F32: match v: case Fmt.Z{neg}: word(Bin.BZ{}, Bin.BZ{}, neg) case Fmt.Inf{neg}: word(Bin.BZ{}, Bin.of_nat(255n), neg) case Fmt.NaN{}: of_bits(2143289344) # 0x7FC00000, the quiet NaN case Fmt.Fin{neg, m, e}: encode.fin(neg, m, e)# Software operations# -------------------def add(a: F32, b: F32) -> F32: encode(Fmt.spec_add(Fmt.binary32(), decode(a), decode(b)))def sub(a: F32, b: F32) -> F32: encode(Fmt.spec_sub(Fmt.binary32(), decode(a), decode(b)))def mul(a: F32, b: F32) -> F32: encode(Fmt.spec_mul(Fmt.binary32(), decode(a), decode(b)))# Implementations# ---------------def soft() -> Num.Impl<F32>: Num.Impl{Fmt.binary32(), decode, add, mul}def hard() -> Num.Impl<F32>: Num.Impl{Fmt.binary32(), decode, F32.add, F32.mul}# the hardware assumption: Base's F32.add and F32.mul are correctly roundeddef HardOk() -> Type: Num.Correct<F32, hard()>