tricu

float-quantize.tri (2393B)

---

 -- Positive binary64 quantization benchmark.
 -- Exact input n * 2^(scale-2304), n and scale canonical naturals.
 -- RNE output: (IEEE magnitude bits, (inexact, storedTiny)).
 -- storedTiny means inexact with a stored zero/subnormal magnitude.
 !import native_math as N
 !import kernels as K
 !import pipelines as P
 !export *
 max a b = K.choose a b (N.gte a b)
 min a b = K.choose a b (N.lte a b)
 answer bits inexact tiny = t bits (t inexact (K.both inexact tiny))
 infinity = 9218868437227405312
 encode scale m inexact = K.lazy
   (_ : answer infinity (t t) t)
   (_ : K.lazy (_ : answer m inexact (t t))
     (_ : answer (N.add (P.shiftLeft 52 (N.successor (N.subtract scale 1230)))
                        (N.subtract m 4503599627370496)) inexact t)
     (N.lt m 4503599627370496)) (N.gt scale 3275)
 normalize scale m inexact = K.lazy
   (_ : answer 0 inexact (t t))
   (_ : let pad = min (N.subtract 53 (K.width m)) (N.subtract scale 1230) in
     encode (N.subtract scale pad) (P.shiftLeft pad m) inexact) (N.zero m)
 carry scale m inexact = K.lazy
   (_ : normalize (N.successor scale) (K.tail m) inexact)
   (_ : normalize scale m inexact) (N.gt (K.width m) 53)
 quantize scale n = K.lazy (_ : answer 0 t (t t))
   (_ : let cut = max (N.subtract (K.width n) 53) (N.subtract 1230 scale) in
     let rounded = K.roundL cut n in
     carry (N.add scale cut) (K.head rounded) (K.tail rounded)) (N.zero n)
 one x = quantize (K.head x) (K.tail x)
 quantized xs = K.map one xs
 -- Demand control: a zero result is independent of scale.
 spin x = spin x
 zeroDemand x = quantize (spin x) 0
 -- Near alignment passes the EXACT intermediate directly to the quantizer.
 -- Preconditions: normalized a,b; gap 0..54; a>=b for gap-zero subtraction.
 nearAdd x = let scale = K.head x in let rest = K.tail x in
   let gap = K.head rest in let ab = K.tail rest in
   quantize scale (N.add (P.shiftLeft gap (K.head ab)) (K.tail ab))
 nearSubtract x = let scale = K.head x in let rest = K.tail x in
   let gap = K.head rest in let ab = K.tail rest in
   quantize scale (N.subtract (P.shiftLeft gap (K.head ab)) (K.tail ab))
 nearAdds xs = K.map nearAdd xs
 nearSubtracts xs = K.map nearSubtract xs
 -- Negative rounding control: apply separate precision and quantum cuts.
 doubleRoundOne x = let first = P.finishL (K.tail x) in
   quantize (N.add (K.head x) (K.head first)) (K.head (K.tail first))
 doubleRoundControl xs = K.map doubleRoundOne xs