src/float/num.bend

bend-lawful-stdlib@0.1.0.0 · 49 lines · 8 definitions

1import Base
2import bend-lawful-stdlib@0.1.0.0/src/float/format.bend as Fmt
3
4# num.bend: the contract a float implementation meets.
5#
6#   import ./num.bend as Num
7#
8# An implementation is a carrier type T, the exact value each T stands
9# for, and its operations. It is correctly rounded for its format when
10# each operation's result stands for the spec result on the operands'
11# values (AddOk, MulOk). Hardware F32 and the software SF32 are both
12# implementations over the carrier F32 (see sf32.bend); anyone can add
13# another carrier, format or algorithm, and code written against Impl
14# works with all of them.
15
16type Impl<-T: Data> is Type:
17  Impl{fmt: Fmt.Format, value: T -> Fmt.Val, add: T -> T -> T, mul: T -> T -> T}
18
19def Impl.fmt(-T: Data, i: Impl<T>) -> Fmt.Format:
20  match i:
21    case Impl{fmt, value, add, mul}:
22      fmt
23
24def Impl.value(-T: Data, i: Impl<T>, x: T) -> Fmt.Val:
25  match i:
26    case Impl{fmt, value, add, mul}:
27      value(x)
28
29def Impl.add(-T: Data, i: Impl<T>, a: T, b: T) -> T:
30  match i:
31    case Impl{fmt, value, add, mul}:
32      add(a, b)
33
34def Impl.mul(-T: Data, i: Impl<T>, a: T, b: T) -> T:
35  match i:
36    case Impl{fmt, value, add, mul}:
37      mul(a, b)
38
39# add is correctly rounded at a and b
40def AddOk(~T: Data, ~i: Impl<T>, a: T, b: T) -> Type:
41  {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}
42
43# mul is correctly rounded at a and b
44def MulOk(~T: Data, ~i: Impl<T>, a: T, b: T) -> Type:
45  {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}
46
47# an implementation that is correctly rounded everywhere
48type Correct<-T: Data, -i: Impl<T>> is Type:
49  Correct{add: @a: T -> @b: T -> AddOk(~T, ~i, a, b), mul: @a: T -> @b: T -> MulOk(~T, ~i, a, b)}