tricu

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

float-significands.tri (6710B)

      1 -- Unsigned significand kernels for binary64 component benchmarks.
      2 !import native_math as N
      3 !export *
      4 triage leaf stem fork = t (t leaf stem) fork
      5 choose yes no value = triage no (_ : yes) (_ _ : yes) value
      6 lazy yes no value = choose yes no value t
      7 head value = triage t (_ : t) (a _ : a) value
      8 tail value = triage t (_ : t) (_ b : b) value
      9 both a b = choose b t a
     10 either a b = choose (t t) b a
     11 not value = choose t (t t) value
     12 xor a b = choose (not b) b a
     13 map f xs = triage t (_ : t) (a b : t (f a) (map f b)) xs
     14 node bit rest = choose (t bit rest) (choose t (t bit rest) (N.zero rest)) bit
     15 reverseInto xs acc = triage acc (_ : acc) (a b : reverseInto b (t a acc)) xs
     16 reverse xs = reverseInto xs t
     17 width xs = triage 0 (_ : 0) (_ rest : N.successor (width rest)) xs
     18 anyBit xs = triage t (_ : t) (bit rest : either bit (anyBit rest)) xs
     19 -- LSB-first canonical naturals. Return (quotient, discardedNonzero).
     20 shiftL k x = shiftWalk k x t
     21 shiftWalk k x sticky = lazy (_ : t x sticky)
     22   (_ : triage (t t sticky) (_ : t t sticky)
     23     (bit rest : shiftWalk (N.predecessor k) rest (either sticky bit)) x) (N.zero k)
     24 roundL k x = lazy (_ : t x t) (_ : roundWalk k x t) (N.zero k)
     25 roundWalk k x sticky = triage (t t sticky) (_ : t t sticky)
     26   (bit rest : lazy
     27     (_ : t (choose (N.successor rest) rest (both bit (either sticky (N.odd rest)))) (either sticky bit))
     28     (_ : roundWalk (N.predecessor k) rest (either sticky bit)) (N.equal k 1)) x
     29 -- MSB-first canonical bit lists (empty zero, first bit 1 otherwise).
     30 -- Cached variants take width explicitly; it is a trusted internal invariant.
     31 shiftM k x = shiftMW (width x) k x
     32 shiftMW w k x = lazy (_ : t x t)
     33   (_ : lazy (_ : t t (anyBit x))
     34     (_ : splitPrefix (N.subtract w k) x) (N.gte k w)) (N.zero k)
     35 splitPrefix keep x = lazy (_ : t t (anyBit x))
     36   (_ : let next = splitPrefix (N.predecessor keep) (tail x) in
     37     t (t (head x) (head next)) (tail next)) (N.zero keep)
     38 roundM k x = roundMW (width x) k x
     39 roundMW w k x = lazy (_ : t x t)
     40   (_ : lazy (_ : t t (anyBit x))
     41     (_ : let rounded = roundPrefix (N.subtract w k) x t in
     42       t (choose (t (t t) (head (tail rounded))) (head (tail rounded)) (head rounded))
     43         (tail (tail rounded))) (N.gt k w)) (N.zero k)
     44 -- Return (carry, (retained bits, inexact)); propagate increment towards the MSB.
     45 roundPrefix keep x previous = lazy
     46   (_ : let guard = head x in let sticky = anyBit (tail x) in
     47     t (both guard (either sticky previous)) (t t (either guard sticky)))
     48   (_ : let bit = head x in let next = roundPrefix (N.predecessor keep) (tail x) bit in
     49     t (both bit (head next))
     50       (t (t (xor bit (head next)) (head (tail next))) (tail (tail next)))) (N.zero keep)
     51 -- Wire arguments: (shiftCount, payload); cached payload: (width, bits).
     52 lsbShiftOne x = shiftL (head x) (tail x)
     53 lsbRoundOne x = roundL (head x) (tail x)
     54 msbShiftOne x = shiftM (head x) (tail x)
     55 msbRoundOne x = roundM (head x) (tail x)
     56 msbCachedShiftOne x = shiftMW (head (tail x)) (head x) (tail (tail x))
     57 msbCachedRoundOne x = roundMW (head (tail x)) (head x) (tail (tail x))
     58 lsbShift xs = map lsbShiftOne xs
     59 lsbRound xs = map lsbRoundOne xs
     60 msbShift xs = map msbShiftOne xs
     61 msbRound xs = map msbRoundOne xs
     62 msbCachedShift xs = map msbCachedShiftOne xs
     63 msbCachedRound xs = map msbCachedRoundOne xs
     64 -- Charge width-cache construction inside each invocation.
     65 msbBuildCachedShiftOne x = let bits = tail x in msbCachedShiftOne (t (head x) (t (width bits) bits))
     66 msbBuildCachedRoundOne x = let bits = tail x in msbCachedRoundOne (t (head x) (t (width bits) bits))
     67 msbBuildCachedShift xs = map msbBuildCachedShiftOne xs
     68 msbBuildCachedRound xs = map msbBuildCachedRoundOne xs
     69 -- Round after each shift in the working-representation chain.
     70 -- The independent oracle follows each rounded step.
     71 chainL k x = let a = head (roundL k x) in
     72   let b = head (roundL k a) in head (roundL k b)
     73 chainM k x = let a = head (roundM k x) in
     74   let b = head (roundM k a) in head (roundM k b)
     75 -- Cache rebuild is charged at every stage in this control.
     76 chainCachedM k x = let a = head (roundMW (head x) k (tail x)) in
     77   let b = head (roundMW (width a) k a) in head (roundMW (width b) k b)
     78 lsbChain xs = map (x : chainL (head x) (tail x)) xs
     79 msbChain xs = map (x : chainM (head x) (tail x)) xs
     80 msbCachedChain xs = map (x : chainCachedM (head x) (tail x)) xs
     81 -- Conversion controls consume the runtime-supplied inputs.
     82 lsbToMsb xs = map reverse xs
     83 msbToLsb xs = map reverse xs
     84 widths xs = map width xs
     85 -- At k=0, the sticky projection leaves the significand opaque.
     86 spin x = spin x
     87 zeroShiftDemand x = tail (shiftL 0 (spin x))
     88 zeroRoundDemand x = tail (roundL 0 (spin x))
     89 zeroMsbDemand x = tail (roundM 0 (spin x))
     90 -- Finish a huge-count shift at the end of the finite significand.
     91 hugeShift x = shiftL x 1
     92 hugeRound x = roundL x 1
     93 -- Derive the result width from the retained count and carry.
     94 roundMC w k x = lazy (_ : t (t w x) t)
     95   (_ : lazy (_ : t (t 0 t) (anyBit x))
     96     (_ : let keep = N.subtract w k in let rounded = roundPrefix keep x t in
     97       let carry = head rounded in let bits = head (tail rounded) in
     98       t (t (choose (N.successor keep) keep carry) (choose (t (t t) bits) bits carry))
     99         (tail (tail rounded))) (N.gt k w)) (N.zero k)
    100 msbMaintainedRoundOne x = roundMC (head (tail x)) (head x) (tail (tail x))
    101 msbMaintainedRound xs = map msbMaintainedRoundOne xs
    102 chainMaintainedM k x = let a = head (roundMC (head x) k (tail x)) in
    103   let b = head (roundMC (head a) k (tail a)) in
    104   tail (head (roundMC (head b) k (tail b)))
    105 msbMaintainedChain xs = map (x : chainMaintainedM (head x) (tail x)) xs
    106 -- Cached width can also cap LSB work for large alignment gaps.
    107 shiftLW w k x = lazy (_ : t t (not (N.zero w))) (_ : shiftL k x) (N.gte k w)
    108 roundLW w k x = lazy (_ : t t (not (N.zero w))) (_ : roundL k x) (N.gt k w)
    109 lsbCachedShiftOne x = shiftLW (head (tail x)) (head x) (tail (tail x))
    110 lsbCachedRoundOne x = roundLW (head (tail x)) (head x) (tail (tail x))
    111 lsbCachedShift xs = map lsbCachedShiftOne xs
    112 lsbCachedRound xs = map lsbCachedRoundOne xs
    113 lsbBuildCachedRoundOne x = let bits = tail x in roundLW (width bits) (head x) bits
    114 lsbBuildCachedRound xs = map lsbBuildCachedRoundOne xs
    115 -- Exact odd-significand normalization: (removed powers of two, significand).
    116 normalizeL x = triage (t 0 t) (_ : t 0 t)
    117   (bit rest : lazy (_ : t 0 x)
    118     (_ : let next = normalizeL rest in t (N.successor (head next)) (tail next)) bit) x
    119 normalizeM x = triage (t 0 t) (_ : t 0 t)
    120   (bit rest : let next = normalizeM rest in
    121     lazy (_ : t (N.successor (head next)) t)
    122       (_ : t (head next) (t bit (tail next))) (both (not bit) (N.zero (tail next)))) x
    123 lsbNormalize xs = map (x : normalizeL (tail x)) xs
    124 msbNormalize xs = map (x : normalizeM (tail x)) xs