src/float/format.bend

bend-lawful-stdlib@0.1.0.0 · 238 lines · 26 definitions

1import Base
2import bend-lawful-stdlib@0.1.0.0/src/float/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
20type 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
28type 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)
32def 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
37def 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
46def 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
60def 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
69def 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
72def 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
79def 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
83def 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
91def 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
100def 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
109def 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
116def 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
119def 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
126def 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
137def add.inf.go(na: Bool, differ: Bool) -> Val:
138  match differ:
139    case True{}:
140      NaN{}
141    case False{}:
142      Inf{na}
143
144def 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
155def 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
167def 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
178def 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
189def spec_sub(f: Format, a: Val, b: Val) -> Val:
190  spec_add(f, a, neg(b))
191
192# Multiplication
193# --------------
194
195def 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
206def 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
217def 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
229def 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)