1	import Base
2	import ./bin.bend as Bin
3	import ./format.bend as Fmt
4	import ./num.bend as Num
5	
6	# sf32.bend: binary32 floats in software, and the two F32 implementations.
7	#
8	#   import ./sf32.bend as SF32
9	#   SF32.add(a, b)          # software IEEE add on F32 bit patterns
10	#   SF32.soft(), SF32.hard() # Num.Impl<F32>: software, and hardware
11	#
12	# decode and encode convert between F32 bits (sign, 8 exponent bits, 23
13	# mantissa bits) and exact values. The software operations are the spec
14	# itself: decode, exact operation and rounding, encode. They compute in
15	# the checker and give the same bits on every backend; they are also far
16	# slower than hardware. A faster algorithm can be another Num.Impl.
17	#
18	# hard() uses Base's F32.add and F32.mul, which the checker cannot
19	# compute. HardOk is the assumption that they are correctly rounded:
20	# a law that needs it takes ~ok: HardOk, and it stays a named hypothesis.
21	
22	def bits(x: F32) -> U32:
23	  match x:
24	    case F32{w}:
25	      U32{w}
26	
27	def of_bits(x: U32) -> F32:
28	  match x:
29	    case U32{w}:
30	      F32{w}
31	
32	# Decoding
33	# --------
34	# The fields are read off the word in one pass (23 mantissa bits, 8
35	# exponent bits, the sign), not with U32 shifts and masks: the checker
36	# evaluates a U32 operation bit by bit, and each shift costs a full pass.
37	
38	def decode.go(neg: Bool, e: Nat, f: Bin.Bin, top: Bool, low: Bool, fz: Bool) -> Fmt.Val:
39	  match top low fz:
40	    case True{} low True{}:
41	      Fmt.Inf{neg}
42	    case True{} low False{}:
43	      Fmt.NaN{}
44	    case False{} True{} True{}:
45	      Fmt.Z{neg}
46	    case False{} True{} False{}:
47	      Fmt.Fin{neg, f, 151n}
48	    case False{} False{} fz:
49	      Fmt.Fin{neg, Bin.add(f, Bin.pow2(23n)), Nat.add(e, 150n)}
50	
51	def decode.cls(neg: Bool, +e: Nat, +f: Bin.Bin) -> Fmt.Val:
52	  decode.go(neg, e, f, Nat.is_eq(e, 255n), Nat.is_eq(e, 0n), Bin.is_zero(f))
53	
54	def decode.sign(f: Bin.Bin, e: Bin.Bin, w: Word(1n)) -> Fmt.Val:
55	  match w:
56	    case WCon{s, t}:
57	      decode.cls(s, Bin.to_nat(e), f)
58	
59	def decode.exp(f: Bin.Bin, p: Bin.Bin & Word(1n)) -> Fmt.Val:
60	  (e, w) = p
61	  decode.sign(f, e, w)
62	
63	def decode.man(p: Bin.Bin & Word(9n)) -> Fmt.Val:
64	  (f, w) = p
65	  decode.exp(f, Bin.take(8n, 1n, w))
66	
67	# the exact value of a float
68	def decode(x: F32) -> Fmt.Val:
69	  match x:
70	    case F32{w}:
71	      decode.man(Bin.take(23n, 9n, w))
72	
73	# Encoding
74	# --------
75	
76	# the sign bit, as it sits above the 8 exponent bits
77	def sign(neg: Bool) -> Bin.Bin:
78	  match neg:
79	    case True{}:
80	      Bin.pow2(8n)
81	    case False{}:
82	      Bin.BZ{}
83	
84	# a word from its fields: 23 mantissa bits, then exponent and sign above
85	def word(frac: Bin.Bin, exp: Bin.Bin, neg: Bool) -> F32:
86	  F32{Bin.to_word(32n, Bin.add(Bin.low(23n, frac), Bin.shl(Bin.add(exp, sign(neg)), 23n)))}
87	
88	def first(r: Bin.Bin & Bool & Bool) -> Bin.Bin:
89	  (q, a, b) = r
90	  q
91	
92	# m moved to have its last bit at exponent t
93	def align(m: Bin.Bin, +e: Nat, +t: Nat, right: Bool) -> Bin.Bin:
94	  match right:
95	    case True{}:
96	      first(Bin.shr(Nat.sub(t, e), m, False{}, False{}))
97	    case False{}:
98	      Bin.shl(m, Nat.sub(e, t))
99	
100	def field(+t: Nat, normal: Bool) -> Bin.Bin:
101	  match normal:
102	    case True{}:
103	      Bin.of_nat(Nat.sub(t, 150n))
104	    case False{}:
105	      Bin.BZ{}
106	
107	def put(neg: Bool, t: Nat, +m: Bin.Bin) -> F32:
108	  word(m, field(t, Nat.is_eq(Bin.len(m), 24n)), neg)
109	
110	# a finite value that fits binary32, as bits: 24 mantissa bits when
111	# normal, fewer at the smallest exponent when subnormal
112	def encode.fin(neg: Bool, +m: Bin.Bin, +e: Nat) -> F32:
113	  +t = Nat.max(Nat.sub(Nat.add(e, Bin.len(m)), 24n), 151n)
114	  put(neg, t, align(m, e, t, Nat.is_ge(t, e)))
115	
116	def encode(v: Fmt.Val) -> F32:
117	  match v:
118	    case Fmt.Z{neg}:
119	      word(Bin.BZ{}, Bin.BZ{}, neg)
120	    case Fmt.Inf{neg}:
121	      word(Bin.BZ{}, Bin.of_nat(255n), neg)
122	    case Fmt.NaN{}:
123	      of_bits(2143289344) # 0x7FC00000, the quiet NaN
124	    case Fmt.Fin{neg, m, e}:
125	      encode.fin(neg, m, e)
126	
127	# Software operations
128	# -------------------
129	
130	def add(a: F32, b: F32) -> F32:
131	  encode(Fmt.spec_add(Fmt.binary32(), decode(a), decode(b)))
132	
133	def sub(a: F32, b: F32) -> F32:
134	  encode(Fmt.spec_sub(Fmt.binary32(), decode(a), decode(b)))
135	
136	def mul(a: F32, b: F32) -> F32:
137	  encode(Fmt.spec_mul(Fmt.binary32(), decode(a), decode(b)))
138	
139	# Implementations
140	# ---------------
141	
142	def soft() -> Num.Impl<F32>:
143	  Num.Impl{Fmt.binary32(), decode, add, mul}
144	
145	def hard() -> Num.Impl<F32>:
146	  Num.Impl{Fmt.binary32(), decode, F32.add, F32.mul}
147	
148	# the hardware assumption: Base's F32.add and F32.mul are correctly rounded
149	def HardOk() -> Type:
150	  Num.Correct<F32, hard()>