float-ieee.tri (5309B)
1 -- Benchmark-only four basic binary64 operations, nearest/ties-to-even. 2 -- Checked reply: (ok, (word, (invalid,(divideByZero,(overflow,(underflow,inexact)))))). 3 -- Oversized canonical natural input: (False,2). Each reply carries its own flags. 4 !import native_math as N 5 !import kernels as K 6 !import layouts as L 7 !import fast as F 8 !import adders as A 9 !import finite as B 10 !import product_quotient as P 11 !export * 12 answer word invalid divideZero overflow underflow inexact = 13 t word (t invalid (t divideZero (t overflow (t underflow inexact)))) 14 exact word = answer word t t t t t 15 nanBit word = K.both (N.equal (B.exponent word) 2047) (K.not (N.zero (L.low52 word))) 16 infBit word = K.both (N.equal (B.exponent word) 2047) (N.zero (L.low52 word)) 17 zeroBit word = K.both (N.zero (B.exponent word)) (N.zero (L.low52 word)) 18 quietBit word = N.odd (L.drop1 (L.drop2 (L.drop16 (L.drop32 word)))) 19 signaling word = K.both (nanBit word) (K.not (quietBit word)) 20 quiet word = K.choose word (N.add word 2251799813685248) (quietBit word) 21 invalidResult = answer 9221120237041090560 (t t) t t t t 22 infinity negative = B.attach negative 9218868437227405312 23 zero negative = K.choose 9223372036854775808 0 negative 24 -- Only finite arithmetic reaches this adapter, so infinity implies overflow. 25 lift reply = let word = K.head reply in let flags = K.tail reply in 26 answer word t t (N.equal (B.exponent word) 2047) (K.tail flags) (K.head flags) 27 -- IEEE after-rounding tininess uses precision rounding with unbounded exponent. 28 -- The secondary round classifies tininess; a single combined cut determines 29 -- the stored value. 30 precisionTiny scale n = let cut = N.subtract (K.width n) 53 in 31 let rounded = K.head (K.roundL cut n) in 32 N.lte (N.add (N.add scale cut) (K.width rounded)) 1282 33 quantize scale n = let reply = F.selective scale n in let word = K.head reply in 34 let flags = K.tail reply in let ix = K.head flags in 35 let uf = K.either (K.tail flags) 36 (K.both (N.equal word 4503599627370496) (K.both ix (precisionTiny scale n))) in 37 answer word t t (N.equal (B.exponent word) 2047) uf ix 38 finiteProduct a b = let da = B.decode a in let db = B.decode b in 39 let negative = K.xor (B.sign da) (B.sign db) in K.lazy 40 (_ : exact (zero negative)) 41 (_ : B.signed negative (quantize (N.subtract (N.add (B.scale da) (B.scale db)) 2304) 42 (A.orderedMultiply (B.mant da) (B.mant db)))) 43 (K.either (N.zero (B.mant da)) (N.zero (B.mant db))) 44 finiteQuotient a b = let da = B.decode a in let db = B.decode b in 45 let negative = K.xor (B.sign da) (B.sign db) in K.lazy 46 (_ : exact (zero negative)) 47 (_ : B.signed negative (quantize (N.subtract (N.add 2248 (B.scale da)) (B.scale db)) 48 (P.jam (P.boundedQuotient (B.mant da) (B.mant db))))) (N.zero (B.mant da)) 49 -- NaN selection precedes subtraction's effective sign flip. 50 nanResult a b = answer (quiet (K.choose a b (nanBit a))) 51 (K.either (signaling a) (signaling b)) t t t t 52 checked operation a b = K.lazy (_ : t t 2) 53 (_ : t (t t) (K.lazy (_ : nanResult a b) (_ : operation a b) 54 (K.either (nanBit a) (nanBit b)))) 55 (K.either (N.gte a 18446744073709551616) (N.gte b 18446744073709551616)) 56 add subtract a b = let ia = infBit a in let ib = infBit b in 57 let sa = B.signBit a in let sb = K.xor subtract (B.signBit b) in K.lazy 58 (_ : K.lazy (_ : invalidResult) 59 (_ : exact (infinity (K.choose sa sb ia))) 60 (K.both (K.both ia ib) (K.xor sa sb))) 61 (_ : lift (B.operate subtract a b)) (K.either ia ib) 62 multiply a b = let negative = K.xor (B.signBit a) (B.signBit b) in K.lazy 63 (_ : K.lazy (_ : invalidResult) (_ : exact (infinity negative)) 64 (K.either (zeroBit a) (zeroBit b))) 65 (_ : finiteProduct a b) (K.either (infBit a) (infBit b)) 66 divide a b = let negative = K.xor (B.signBit a) (B.signBit b) in K.lazy 67 (_ : K.lazy (_ : invalidResult) (_ : exact (infinity negative)) (infBit b)) 68 (_ : K.lazy (_ : exact (zero negative)) 69 (_ : K.lazy 70 (_ : K.lazy (_ : invalidResult) 71 (_ : answer (infinity negative) t (t t) t t t) (zeroBit a)) 72 (_ : finiteQuotient a b) (zeroBit b)) (infBit b)) (infBit a) 73 addOne x = checked (add t) (K.head x) (K.tail x) 74 subtractOne x = checked (add (t t)) (K.head x) (K.tail x) 75 multiplyOne x = checked multiply (K.head x) (K.tail x) 76 divideOne x = checked divide (K.head x) (K.tail x) 77 adds xs = K.map addOne xs 78 subtracts xs = K.map subtractOne xs 79 multiplies xs = K.map multiplyOne xs 80 divides xs = K.map divideOne xs 81 -- Transport preserves the original word, including signaling and payload bits. 82 transport xs = xs 83 spin x = spin x 84 rangeDemand x = checked (spin x) 18446744073709551616 (spin x) 85 nanDemand x = checked (spin x) 9221120237041090561 9218868437227405313 86 -- A quiet left NaN determines the word; either signaling operand raises invalid. 87 nanWordDemand x = K.head (nanResult 9221120237041090561 (spin x)) 88 quantizeOne x = t (t t) (quantize (K.head x) (K.tail x)) 89 quantized xs = K.map quantizeOne xs 90 signalingDemand x = nanResult 9218868437227405313 (spin x) 91 -- Stored-exponent controls expose minimum-normal underflow flag differences. 92 storedMultiplyOne x = t (t t) (lift (P.orderedProduct (K.head x) (K.tail x))) 93 storedDivideOne x = t (t t) (lift (P.quotient P.boundedQuotient (K.head x) (K.tail x))) 94 storedMultiplies xs = K.map storedMultiplyOne xs 95 storedDivides xs = K.map storedDivideOne xs