float-pipelines.tri (7490B)
1 -- Natural-significand pipelines with rounded products and exponent increments. 2 !import native_math as N 3 !import kernels as K 4 !import layouts as L 5 !export * 6 triage leaf stem fork = t (t leaf stem) fork 7 choose = K.choose 8 lazy = K.lazy 9 head = K.head 10 tail = K.tail 11 map = K.map 12 either = K.either 13 both = K.both 14 not = K.not 15 -- Radix 256, least-significant canonical octet first; empty zero. 16 -- The highest limb is nonzero; each octet uses its canonical natural encoding. 17 consLimb bit rest = lazy (_ : choose t (t bit rest) (N.zero rest)) (_ : t bit rest) (N.zero bit) 18 low8 x = L.join8 x t 19 fromNatural x = triage t (_ : t) (_ _ : t (low8 x) (fromNatural (L.drop8 x))) x 20 toNatural xs = triage t (_ : t) (a b : L.join8 a (toNatural b)) xs 21 increment xs = triage (t 1 t) (_ : t 1 t) 22 (a b : lazy (_ : t 0 (increment b)) (_ : t (N.successor a) b) (N.equal a 255)) xs 23 addCarry a b carry = triage 24 (lazy (_ : increment b) (_ : b) carry) 25 (_ : b) 26 (av ar : triage (lazy (_ : increment a) (_ : a) carry) (_ : a) 27 (bv br : let total = N.add (N.add av bv) (choose 1 0 carry) in 28 t (low8 total) (addCarry ar br (N.odd (L.drop8 total)))) b) a 29 add a b = addCarry a b t 30 -- Subtraction requires a >= b. Canonicalize high zero limbs while rebuilding. 31 subtractBorrow a b borrow = triage t (_ : t) 32 (av ar : let bv = N.add (head b) (choose 1 0 borrow) in 33 let under = N.lt av bv in 34 consLimb (N.subtract (choose (N.add 256 av) av under) bv) 35 (subtractBorrow ar (tail b) under)) a 36 subtract a b = subtractBorrow a b t 37 multiplyDigit digit xs carry = triage (fromNatural carry) (_ : fromNatural carry) 38 (a b : let total = N.add (N.multiply digit a) carry in 39 consLimb (low8 total) (multiplyDigit digit b (L.drop8 total))) xs 40 multiply a b = triage t (_ : t) 41 (digit rest : add (multiplyDigit digit a 0) (consLimb 0 (multiply a rest))) b 42 -- Width only traverses the limb spine plus the highest octet's bit spine. 43 width xs = triage 0 (_ : 0) 44 (a b : lazy (_ : K.width a) (_ : N.add 8 (width b)) (N.zero b)) xs 45 -- Consume whole limbs first, stopping at the end even for enormous counts. 46 dropLimbs count xs sticky = lazy (_ : t xs sticky) 47 (_ : triage (t t sticky) (_ : t t sticky) 48 (a b : dropLimbs (N.predecessor count) b (either sticky (not (N.zero a)))) xs) (N.zero count) 49 shiftLeft count n = lazy (_ : n) 50 (_ : K.node t (shiftLeft (N.predecessor count) n)) (N.zero count) 51 -- Residual shift is 1..7 (also used with 1 for the guard bit). 52 shiftResidual count xs = triage t (_ : t) 53 (a b : let lower = head (K.shiftL count a) in 54 let upper = L.takeBits count (head b) in 55 consLimb (N.add lower (shiftLeft (N.subtract 8 count) upper)) 56 (shiftResidual count b)) xs 57 shift count xs = let whole = L.drop1 (L.drop2 count) in 58 let residual = L.join2 count (L.join1 (L.drop2 count) t) in 59 let dropped = dropLimbs whole xs t in 60 lazy (_ : dropped) 61 (_ : let rest = head dropped in 62 t (shiftResidual residual rest) 63 (either (tail dropped) (not (N.zero (L.takeBits residual (head rest)))))) (N.zero residual) 64 roundSplit count xs = lazy (_ : t xs t) 65 (_ : let split = shift (N.predecessor count) xs in let rest = head split in 66 let guard = N.odd (head rest) in let quotient = shiftResidual 1 rest in 67 t (choose (increment quotient) quotient (both guard (either (tail split) (N.odd (head quotient))))) 68 (either guard (tail split))) (N.zero count) 69 -- Direct rounding extracts guard/sticky from the boundary octet once. 70 roundFinish quotient guard sticky = t 71 (choose (increment quotient) quotient (both guard (either sticky (N.odd (head quotient))))) 72 (either guard sticky) 73 round count xs = lazy (_ : t xs t) 74 (_ : let whole = L.drop1 (L.drop2 count) in 75 let residual = L.join2 count (L.join1 (L.drop2 count) t) in 76 lazy 77 (_ : let dropped = dropLimbs (N.predecessor whole) xs t in 78 let rest = head dropped in let boundary = head rest in 79 roundFinish (tail rest) (N.odd (L.drop1 (L.drop2 (L.drop4 boundary)))) 80 (either (tail dropped) (not (N.zero (L.low7 boundary))))) 81 (_ : let dropped = dropLimbs whole xs t in 82 let rest = head dropped in let boundary = head rest in 83 let lowCount = N.predecessor residual in 84 roundFinish (shiftResidual residual rest) (N.odd (head (K.shiftL lowCount boundary))) 85 (either (tail dropped) (not (N.zero (L.takeBits lowCount boundary))))) (N.zero residual)) (N.zero count) 86 limbRoundSplit xs = map (x : roundSplit (head x) (tail x)) xs 87 -- Round exact natural to at most 53 significant bits. Output (shift, (m, inexact)). 88 -- Renormalize a carry into bit 54 by an exact shift. 89 finishL n = let cut = N.subtract (K.width n) 53 in let rounded = K.roundL cut n in 90 let m = head rounded in lazy 91 (_ : t (N.successor cut) (t (tail m) (tail rounded))) 92 (_ : t cut rounded) (N.odd (L.drop1 (L.drop52 m))) 93 finishB n = let cut = N.subtract (width n) 53 in let rounded = round cut n in 94 let m = head rounded in lazy 95 (_ : t (N.successor cut) (t (shiftResidual 1 m) (tail rounded))) 96 (_ : t cut rounded) (N.odd (L.drop1 (L.drop4 (head (L.drop2 (L.drop4 m)))))) 97 lsbAdd xs = map (x : finishL (N.add (head x) (tail x))) xs 98 limbAdd xs = map (x : finishB (add (head x) (tail x))) xs 99 lsbSubtract xs = map (x : finishL (N.subtract (head x) (tail x))) xs 100 limbSubtract xs = map (x : finishB (subtract (head x) (tail x))) xs 101 lsbMultiply xs = map (x : finishL (N.multiply (head x) (tail x))) xs 102 limbMultiply xs = map (x : finishB (multiply (head x) (tail x))) xs 103 limbShift xs = map (x : shift (head x) (tail x)) xs 104 limbRound xs = map (x : round (head x) (tail x)) xs 105 limbWidths xs = map width xs 106 limbToNatural xs = map toNatural xs 107 naturalToLimb xs = map fromNatural xs 108 -- Three individually rounded multiplies; collect all exponent increments and 109 -- inexact flags across the significand chain. 110 chainL a b = let first = finishL (N.multiply a b) in 111 let second = finishL (N.multiply (head (tail first)) b) in 112 let third = finishL (N.multiply (head (tail second)) b) in 113 t (N.add (head first) (N.add (head second) (head third))) 114 (t (head (tail third)) (either (tail (tail first)) (either (tail (tail second)) (tail (tail third))))) 115 chainB a b = let first = finishB (multiply a b) in 116 let second = finishB (multiply (head (tail first)) b) in 117 let third = finishB (multiply (head (tail second)) b) in 118 t (N.add (head first) (N.add (head second) (head third))) 119 (t (head (tail third)) (either (tail (tail first)) (either (tail (tail second)) (tail (tail third))))) 120 lsbChain xs = map (x : chainL (head x) (tail x)) xs 121 limbChain xs = map (x : chainB (head x) (tail x)) xs 122 -- Bounded exact-alignment controls: callers constrain gap to 0..54 here. 123 -- Larger-gap bounds are exercised by the aligned-quantize workers. 124 prependLimbs count xs = lazy (_ : xs) 125 (_ : consLimb 0 (prependLimbs (N.predecessor count) xs)) (N.zero count) 126 leftB count xs = let residual = L.join2 count (L.join1 (L.drop2 count) t) in 127 prependLimbs (L.drop1 (L.drop2 count)) (multiplyDigit (shiftLeft residual 1) xs 0) 128 lsbAlignedAdd xs = map (x : let ab = tail x in 129 finishL (N.add (shiftLeft (head x) (head ab)) (tail ab))) xs 130 limbAlignedAdd xs = map (x : let ab = tail x in 131 finishB (add (leftB (head x) (head ab)) (tail ab))) xs 132 lsbAlignedSubtract xs = map (x : let ab = tail x in 133 finishL (N.subtract (shiftLeft (head x) (head ab)) (tail ab))) xs 134 limbAlignedSubtract xs = map (x : let ab = tail x in 135 finishB (subtract (leftB (head x) (head ab)) (tail ab))) xs 136 lsbRound xs = K.lsbRound xs