1	import Base
2	import ./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	
16	type Impl<-T: Data> is Type:
17	  Impl{fmt: Fmt.Format, value: T -> Fmt.Val, add: T -> T -> T, mul: T -> T -> T}
18	
19	def Impl.fmt(-T: Data, i: Impl<T>) -> Fmt.Format:
20	  match i:
21	    case Impl{fmt, value, add, mul}:
22	      fmt
23	
24	def 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	
29	def 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	
34	def 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
40	def 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
44	def 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
48	type 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)}