tricu

float-finite-product-quotient.tri (4359B)

---

 -- Benchmark-only finite signed multiplication and nonzero-divisor division.
 -- Checked interface matches finite.tri; error 3 rejects a zero divisor.
 !import native_math as N
 !import kernels as K
 !import fast as F
 !import finite as B
 !import adders as A
 !export *
 check operation a b = K.lazy (_ : t t 2)
   (_ : K.lazy (_ : t t 1) (_ : t (t t) (operation a b))
     (K.either (N.equal (B.exponent a) 2047) (N.equal (B.exponent b) 2047)))
   (K.either (N.gte a 18446744073709551616) (N.gte b 18446744073709551616))
 product kernel a b = let da = B.decode a in let db = B.decode b in
   let negative = K.xor (B.sign da) (B.sign db) in K.lazy
     (_ : B.zero negative)
     (_ : B.signed negative (F.selective (N.subtract (N.add (B.scale da) (B.scale db)) 2304)
       (kernel (B.mant da) (B.mant db))))
     (K.either (N.zero (B.mant da)) (N.zero (B.mant db)))
 nativeProduct = product N.multiply
 orderedProduct = product A.orderedMultiply
 -- Exact control: divide a 109-bit numerator by the normalized divisor.
 nativeQuotient a b = N.divMod (F.shiftPositive 56 a) b
 -- Produce the exact quotient/remainder by consuming 56 fractional bits.
 -- Initial quotient is 0 or 1 because 1/2 < a/b < 2.
 walk count divisor q r = K.lazy (_ : t q r)
   (_ : K.lazy (_ : t (F.shiftPositive count q) 0)
     (_ : let shifted = F.zeros1 r in K.lazy
       (_ : walk (N.predecessor count) divisor (K.node t q) shifted)
       (_ : walk (N.predecessor count) divisor (N.successor (K.node t q)) (N.subtract shifted divisor))
       (N.lt shifted divisor)) (N.zero r)) (N.zero count)
 boundedQuotient a b = K.lazy (_ : walk 56 b 0 a)
   (_ : walk 56 b 1 (N.subtract a b)) (N.lt a b)
 -- Round-to-odd retains the discarded rational remainder. At least three
 -- working bits survive normalization, so this only feeds immediate final RNE.
 jam split = let q = K.head split in K.lazy (_ : q)
   (_ : K.choose q (N.successor q) (N.zero (K.tail split))) (N.odd q)
 quotient kernel a b = let da = B.decode a in let db = B.decode b in
   let negative = K.xor (B.sign da) (B.sign db) in K.lazy
     (_ : B.zero negative)
     (_ : B.signed negative (F.selective (N.subtract (N.add 2248 (B.scale da)) (B.scale db))
       (jam (kernel (B.mant da) (B.mant db))))) (N.zero (B.mant da))
 -- Range/nonfinite checks precede division-by-zero rejection; error codes are
 -- domain errors in this finite-input test interface.
 checkedQuotient kernel a b = let result = check (quotient kernel) a b in K.lazy
   (_ : K.lazy (_ : t t 3) (_ : result) (N.zero (B.mant (B.decode b))))
   (_ : result) (K.head result)
 nativeMultiplyOne x = check nativeProduct (K.head x) (K.tail x)
 orderedMultiplyOne x = check orderedProduct (K.head x) (K.tail x)
 nativeDivideOne x = checkedQuotient nativeQuotient (K.head x) (K.tail x)
 boundedDivideOne x = checkedQuotient boundedQuotient (K.head x) (K.tail x)
 nativeMultiplies xs = K.map nativeMultiplyOne xs
 orderedMultiplies xs = K.map orderedMultiplyOne xs
 nativeDivides xs = K.map nativeDivideOne xs
 boundedDivides xs = K.map boundedDivideOne xs
 nativeRawOne x = nativeQuotient (K.head x) (K.tail x)
 boundedRawOne x = boundedQuotient (K.head x) (K.tail x)
 nativeRaw xs = K.map nativeRawOne xs
 boundedRaw xs = K.map boundedRawOne xs
 spin x = spin x
 productZeroDemand x = product (spin x) 0 1
 quotientZeroDemand x = quotient (spin x) 0 1
 jamOddDemand x = jam (t 7 (spin x))
 rangeDemand x = check nativeProduct 18446744073709551616 (spin x)
 walkExactDemand x = walk 56 (spin x) 1 0
 -- Negative rounding controls: separate precision/quantum cuts and dropped remainder.
 truncateKernel a b = t (K.head (boundedQuotient a b)) 0
 truncateDivideOne x = checkedQuotient truncateKernel (K.head x) (K.tail x)
 truncateDivides xs = K.map truncateDivideOne xs
 doubleProduct a b = let da = B.decode a in let db = B.decode b in
   let n = N.multiply (B.mant da) (B.mant db) in
   let cut = N.subtract (K.width n) 53 in let first = K.roundL cut n in
   let result = F.selective (N.add cut (N.subtract (N.add (B.scale da) (B.scale db)) 2304)) (K.head first) in
   let ix = K.either (K.tail first) (K.head (K.tail result)) in
     B.signed (K.xor (B.sign da) (B.sign db))
       (t (K.head result) (t ix (K.both ix (N.lt (K.head result) 4503599627370496))))
 doubleProductOne x = check doubleProduct (K.head x) (K.tail x)
 doubleProducts xs = K.map doubleProductOne xs
 divisionRejectDemand x = checkedQuotient (spin x) 1 0