src/float/num.bend source

src/float/num.bend on the hub · documented module

import Baseimport ./format.bend as Fmt# num.bend: the contract a float implementation meets.##   import ./num.bend as Num## An implementation is a carrier type T, the exact value each T stands# for, and its operations. It is correctly rounded for its format when# each operation's result stands for the spec result on the operands'# values (AddOk, MulOk). Hardware F32 and the software SF32 are both# implementations over the carrier F32 (see sf32.bend); anyone can add# another carrier, format or algorithm, and code written against Impl# works with all of them.type Impl<-T: Data> is Type:  Impl{fmt: Fmt.Format, value: T -> Fmt.Val, add: T -> T -> T, mul: T -> T -> T}def Impl.fmt(-T: Data, i: Impl<T>) -> Fmt.Format:  match i:    case Impl{fmt, value, add, mul}:      fmtdef Impl.value(-T: Data, i: Impl<T>, x: T) -> Fmt.Val:  match i:    case Impl{fmt, value, add, mul}:      value(x)def Impl.add(-T: Data, i: Impl<T>, a: T, b: T) -> T:  match i:    case Impl{fmt, value, add, mul}:      add(a, b)def Impl.mul(-T: Data, i: Impl<T>, a: T, b: T) -> T:  match i:    case Impl{fmt, value, add, mul}:      mul(a, b)# add is correctly rounded at a and bdef AddOk(~T: Data, ~i: Impl<T>, a: T, b: T) -> Type:  {Fmt.canon(Impl.value(T, i, Impl.add(T, i, a, b))) == Fmt.canon(Fmt.spec_add(Impl.fmt(T, i), Impl.value(T, i, a), Impl.value(T, i, b))) : Fmt.Val}# mul is correctly rounded at a and bdef MulOk(~T: Data, ~i: Impl<T>, a: T, b: T) -> Type:  {Fmt.canon(Impl.value(T, i, Impl.mul(T, i, a, b))) == Fmt.canon(Fmt.spec_mul(Impl.fmt(T, i), Impl.value(T, i, a), Impl.value(T, i, b))) : Fmt.Val}# an implementation that is correctly rounded everywheretype Correct<-T: Data, -i: Impl<T>> is Type:  Correct{add: @a: T -> @b: T -> AddOk(~T, ~i, a, b), mul: @a: T -> @b: T -> MulOk(~T, ~i, a, b)}