1	import Base
2	import ./bin.bend as Bin
3	
4	# format.bend: what IEEE float operations mean, for any binary format.
5	#
6	#   import ./format.bend as Fmt
7	#
8	# A value is exact: m * 2^(e - 300) with m a binary natural, plus signed
9	# zeros, infinities and NaN. A Format says how many mantissa bits there
10	# are and which exponents exist; round fits an exact value into a format
11	# (to nearest, ties to even). The spec_ functions are the IEEE 754
12	# operations on values: the exact result, then round. Every NaN is the
13	# same value, so NaN bit patterns (which differ between backends) never
14	# reach a law.
15	#
16	# The exponent is a Nat offset by 300, which covers every binary32 value
17	# and every product of two, and keeps exponents small enough for the
18	# checker's unary Nat.
19	
20	type Val is Data:
21	  Z{neg: Bool}
22	  Inf{neg: Bool}
23	  NaN{}
24	  Fin{neg: Bool, m: Bin.Bin, e: Nat}
25	
26	# p: mantissa bits; emin, emax: lowest and highest exponent (offset by
27	# 300) of a mantissa's last bit
28	type Format is Data:
29	  Format{p: Nat, emin: Nat, emax: Nat}
30	
31	# binary32: 24 bits; smallest subnormal 2^-149; largest 2^104 * (2^24 - 1)
32	def binary32() -> Format:
33	  Format{24n, 151n, 404n}
34	
35	# the same value with its low zero bits moved into the exponent and its
36	# high zero bits dropped, so that equal values are equal terms
37	def strip(neg: Bool, m: Bin.Bin, e: Nat) -> Val:
38	  match m:
39	    case Bin.BZ{}:
40	      Z{neg}
41	    case Bin.B0{r}:
42	      strip(neg, r, 1n+e)
43	    case Bin.B1{r}:
44	      Fin{neg, Bin.B1{Bin.trim(r)}, e}
45	
46	def canon(v: Val) -> Val:
47	  match v:
48	    case Z{neg}:
49	      Z{neg}
50	    case Inf{neg}:
51	      Inf{neg}
52	    case NaN{}:
53	      NaN{}
54	    case Fin{neg, m, e}:
55	      strip(neg, m, e)
56	
57	# Rounding
58	# --------
59	
60	def over.go(neg: Bool, m: Bin.Bin, e: Nat, zero: Bool, big: Bool) -> Val:
61	  match zero big:
62	    case True{} big:
63	      Z{neg}
64	    case False{} True{}:
65	      Inf{neg}
66	    case False{} False{}:
67	      Fin{neg, m, e}
68	
69	def over(+top: Nat, neg: Bool, +m: Bin.Bin, +e: Nat) -> Val:
70	  over.go(neg, m, e, Bin.is_zero(m), Nat.is_gt(Nat.add(e, Bin.len(m)), top))
71	
72	def round.up(q: Bin.Bin, up: Bool) -> Bin.Bin:
73	  match up:
74	    case True{}:
75	      Bin.inc(q)
76	    case False{}:
77	      q
78	
79	def round.fin(+top: Nat, neg: Bool, +t: Nat, qrs: Bin.Bin & Bool & Bool) -> Val:
80	  (+q, r, s) = qrs
81	  over(top, neg, round.up(q, Bool.and(r, Bool.or(s, Bin.odd(q)))), t)
82	
83	def round.go(+top: Nat, neg: Bool, m: Bin.Bin, +e: Nat, +t: Nat, exact: Bool) -> Val:
84	  match exact:
85	    case True{}:
86	      over(top, neg, m, e)
87	    case False{}:
88	      round.fin(top, neg, t, Bin.shr(Nat.sub(t, e), m, False{}, False{}))
89	
90	# the float of format f nearest to (-1)^neg * m * 2^(e - 300), ties to even
91	def round(f: Format, neg: Bool, +m: Bin.Bin, +e: Nat) -> Val:
92	  Format{+p, emin, emax} = f
93	  +t = Nat.max(Nat.sub(Nat.add(e, Bin.len(m)), p), emin)
94	  round.go(Nat.add(emax, p), neg, m, e, t, Nat.is_le(t, e))
95	
96	# Addition
97	# --------
98	
99	# add two finite values once their mantissas share the exponent e
100	def add.fin.cmp(f: Format, na: Bool, nb: Bool, a: Bin.Bin, b: Bin.Bin, e: Nat, c: Cmp) -> Val:
101	  match c:
102	    case LT{}:
103	      round(f, nb, Bin.sub(b, a), e)
104	    case EQ{}:
105	      Z{False{}}
106	    case GT{}:
107	      round(f, na, Bin.sub(a, b), e)
108	
109	def add.fin.signs(f: Format, na: Bool, nb: Bool, +a: Bin.Bin, +b: Bin.Bin, e: Nat, differ: Bool) -> Val:
110	  match differ:
111	    case False{}:
112	      round(f, na, Bin.add(a, b), e)
113	    case True{}:
114	      add.fin.cmp(f, na, nb, a, b, e, Bin.cmp(a, b))
115	
116	def add.fin.aligned(f: Format, +na: Bool, +nb: Bool, a: Bin.Bin, b: Bin.Bin, e: Nat) -> Val:
117	  add.fin.signs(f, na, nb, a, b, e, Bool.xor(na, nb))
118	
119	def add.fin.go(f: Format, na: Bool, a: Bin.Bin, +ea: Nat, nb: Bool, b: Bin.Bin, +eb: Nat, a_high: Bool) -> Val:
120	  match a_high:
121	    case True{}:
122	      add.fin.aligned(f, na, nb, Bin.shl(a, Nat.sub(ea, eb)), b, eb)
123	    case False{}:
124	      add.fin.aligned(f, na, nb, a, Bin.shl(b, Nat.sub(eb, ea)), ea)
125	
126	def add.fin(f: Format, na: Bool, a: Bin.Bin, +ea: Nat, b: Val) -> Val:
127	  match b:
128	    case Z{nb}:
129	      Fin{na, a, ea}
130	    case Inf{nb}:
131	      Inf{nb}
132	    case NaN{}:
133	      NaN{}
134	    case Fin{nb, mb, +eb}:
135	      add.fin.go(f, na, a, ea, nb, mb, eb, Nat.is_ge(ea, eb))
136	
137	def add.inf.go(na: Bool, differ: Bool) -> Val:
138	  match differ:
139	    case True{}:
140	      NaN{}
141	    case False{}:
142	      Inf{na}
143	
144	def add.inf(+na: Bool, b: Val) -> Val:
145	  match b:
146	    case Inf{+nb}:
147	      add.inf.go(na, Bool.xor(na, nb))
148	    case NaN{}:
149	      NaN{}
150	    case Z{nb}:
151	      Inf{na}
152	    case Fin{nb, mb, eb}:
153	      Inf{na}
154	
155	def add.zero(na: Bool, b: Val) -> Val:
156	  match b:
157	    case Z{nb}:
158	      Z{Bool.and(na, nb)}
159	    case Inf{nb}:
160	      Inf{nb}
161	    case NaN{}:
162	      NaN{}
163	    case Fin{nb, mb, eb}:
164	      Fin{nb, mb, eb}
165	
166	# IEEE addition: the exact sum, rounded; x + (-x) is +0
167	def spec_add(f: Format, a: Val, b: Val) -> Val:
168	  match a:
169	    case NaN{}:
170	      NaN{}
171	    case Inf{na}:
172	      add.inf(na, b)
173	    case Z{na}:
174	      add.zero(na, b)
175	    case Fin{na, ma, ea}:
176	      add.fin(f, na, ma, ea, b)
177	
178	def neg(v: Val) -> Val:
179	  match v:
180	    case Z{n}:
181	      Z{Bool.not(n)}
182	    case Inf{n}:
183	      Inf{Bool.not(n)}
184	    case NaN{}:
185	      NaN{}
186	    case Fin{n, m, e}:
187	      Fin{Bool.not(n), m, e}
188	
189	def spec_sub(f: Format, a: Val, b: Val) -> Val:
190	  spec_add(f, a, neg(b))
191	
192	# Multiplication
193	# --------------
194	
195	def mul.fin(f: Format, na: Bool, a: Bin.Bin, ea: Nat, b: Val) -> Val:
196	  match b:
197	    case Z{nb}:
198	      Z{Bool.xor(na, nb)}
199	    case Inf{nb}:
200	      Inf{Bool.xor(na, nb)}
201	    case NaN{}:
202	      NaN{}
203	    case Fin{nb, mb, eb}:
204	      round(f, Bool.xor(na, nb), Bin.mul(a, mb), Nat.sub(Nat.add(ea, eb), 300n))
205	
206	def mul.inf(na: Bool, b: Val) -> Val:
207	  match b:
208	    case Z{nb}:
209	      NaN{}
210	    case Inf{nb}:
211	      Inf{Bool.xor(na, nb)}
212	    case NaN{}:
213	      NaN{}
214	    case Fin{nb, mb, eb}:
215	      Inf{Bool.xor(na, nb)}
216	
217	def mul.zero(na: Bool, b: Val) -> Val:
218	  match b:
219	    case Z{nb}:
220	      Z{Bool.xor(na, nb)}
221	    case Inf{nb}:
222	      NaN{}
223	    case NaN{}:
224	      NaN{}
225	    case Fin{nb, mb, eb}:
226	      Z{Bool.xor(na, nb)}
227	
228	# IEEE multiplication: the exact product, rounded
229	def spec_mul(f: Format, a: Val, b: Val) -> Val:
230	  match a:
231	    case NaN{}:
232	      NaN{}
233	    case Inf{na}:
234	      mul.inf(na, b)
235	    case Z{na}:
236	      mul.zero(na, b)
237	    case Fin{na, ma, ea}:
238	      mul.fin(f, na, ma, ea, b)