tricu

A lazy functional language based on Tree Calculus
Log | Files | Refs | README | LICENSE

float-finite.tri (3305B)

      1 -- Finite signed binary64 add/subtract over exact IEEE words.
      2 -- Inputs are canonical naturals; output (ok, payload). Success payload is
      3 -- (word, (inexact, storedTiny)); errors: 1 nonfinite, 2 out-of-range.
      4 -- storedTiny means inexact with a stored zero/subnormal magnitude.
      5 !import native_math as N
      6 !import kernels as K
      7 !import layouts as L
      8 !import fast as F
      9 !import quantize as Q
     10 !import near as H
     11 !export *
     12 exponent bits = L.low11 (L.drop52 bits)
     13 signBit bits = N.odd (L.drop11 (L.drop52 bits))
     14 -- Private normalized record (sign, (scale, significand)). Zero has mantissa 0.
     15 subnormal fraction = K.lazy (_ : t 1230 0)
     16   (_ : let pad = N.subtract 53 (K.width fraction) in
     17     t (N.subtract 1230 pad) (F.shiftSelective pad fraction)) (N.zero fraction)
     18 decode bits = let e = exponent bits in t (signBit bits)
     19   (K.lazy (_ : subnormal (L.low52 bits))
     20     (_ : t (N.add e 1229) (F.pack 1 bits)) (N.zero e))
     21 sign d = K.head d
     22 scale d = K.head (K.tail d)
     23 mant d = K.tail (K.tail d)
     24 -- Set a negative sign on an already nonnegative output word. The suffix is
     25 -- nonzero even for negative zero/subnormals, so fixed splicing is canonical.
     26 attach negative bits = K.choose (F.pack (N.add 2048 (L.drop52 bits)) bits) bits negative
     27 signed negative reply = t (attach negative (K.head reply)) (K.tail reply)
     28 exactWord bits = Q.answer bits t t
     29 zero negative = exactWord (K.choose 9223372036854775808 0 negative)
     30 -- Canonical low-63 extraction, needed only when flipping a negative raw word.
     31 low63 x = L.join32 x (L.join16 (L.drop32 x)
     32   (L.join8 (L.drop16 (L.drop32 x))
     33     (L.join4 (L.drop8 (L.drop16 (L.drop32 x)))
     34       (L.join2 (L.drop4 (L.drop8 (L.drop16 (L.drop32 x))))
     35         (L.join1 (L.drop2 (L.drop4 (L.drop8 (L.drop16 (L.drop32 x))))) t)))))
     36 flip bits = K.lazy (_ : low63 bits) (_ : attach (t t) bits) (signBit bits)
     37 dominates a b = K.either (N.gt (scale a) (scale b))
     38   (K.both (N.equal (scale a) (scale b)) (N.gte (mant a) (mant b)))
     39 ordered a b = let gap = N.subtract (scale a) (scale b) in K.lazy
     40   (_ : signed (sign a) (H.hybridAdd (scale a) gap (mant a) (mant b)))
     41   (_ : K.lazy (_ : zero t)
     42     (_ : signed (sign a) (H.hybridSubtract (scale a) gap (mant a) (mant b)))
     43     (K.both (N.zero gap) (N.equal (mant a) (mant b)))) (K.not (K.xor (sign a) (sign b)))
     44 operate subtract a b = let da = decode a in let originalB = decode b in
     45   let db = t (K.xor subtract (sign originalB)) (K.tail originalB) in K.lazy
     46     (_ : K.lazy (_ : zero (K.both (sign da) (sign db)))
     47       (_ : exactWord (K.choose (flip b) b subtract)) (N.zero (mant db)))
     48     (_ : K.lazy (_ : exactWord a)
     49       (_ : K.lazy (_ : ordered da db) (_ : ordered db da) (dominates da db))
     50       (N.zero (mant db))) (N.zero (mant da))
     51 checked subtract a b = K.lazy (_ : t t 2)
     52   (_ : K.lazy (_ : t t 1) (_ : t (t t) (operate subtract a b))
     53     (K.either (N.equal (exponent a) 2047) (N.equal (exponent b) 2047)))
     54   (K.either (N.gte a 18446744073709551616) (N.gte b 18446744073709551616))
     55 addOne x = checked t (K.head x) (K.tail x)
     56 subtractOne x = checked (t t) (K.head x) (K.tail x)
     57 adds xs = K.map addOne xs
     58 subtracts xs = K.map subtractOne xs
     59 decoded xs = K.map decode xs
     60 flipped xs = K.map flip xs
     61 -- An out-of-range first input wins before inspecting the second input.
     62 spin x = spin x
     63 rangeDemand x = checked t 18446744073709551616 (spin x)