tricu

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

float-chains.tri (6042B)

      1 -- Chain benchmark over canonical 64-bit words and private caches.
      2 -- Input (initialWord, (operandPool, [(opcode,poolIndex), ...])). Opcodes 0..3.
      3 -- Output (finalWord, OR of all five flags); round after every operation.
      4 !import native_math as N
      5 !import kernels as K
      6 !import layouts as L
      7 !import fast as F
      8 !import adders as A
      9 !import finite as B
     10 !import product_quotient as P
     11 !import ieee as I
     12 !export *
     13 drop2 x = K.tail (K.tail x)
     14 drop3 x = K.tail (drop2 x)
     15 drop4 x = K.tail (drop3 x)
     16 flagsOr a b = t (K.either (K.head a) (K.head b))
     17   (t (K.either (K.head (K.tail a)) (K.head (K.tail b)))
     18     (t (K.either (K.head (drop2 a)) (K.head (drop2 b)))
     19       (t (K.either (K.head (drop3 a)) (K.head (drop3 b)))
     20         (K.either (drop4 a) (drop4 b)))))
     21 at index xs = K.lazy (_ : K.head xs) (_ : at (N.predecessor index) (K.tail xs)) (N.zero index)
     22 wordOp op a b = K.lazy (_ : I.add t a b)
     23   (_ : K.lazy (_ : I.add (t t) a b)
     24     (_ : K.lazy (_ : I.multiply a b) (_ : I.divide a b) (N.equal op 2)) (N.equal op 1)) (N.zero op)
     25 checkedStep op a b = K.tail (I.checked (wordOp op) a b)
     26 trustedStep op a b = K.lazy (_ : I.nanResult a b) (_ : wordOp op a b)
     27   (K.either (I.nanBit a) (I.nanBit b))
     28 wordWalk step pool instructions reply = K.triage reply (_ : reply)
     29   (instruction rest : let next = step (K.head instruction) (K.head reply) (at (K.tail instruction) pool) in
     30     wordWalk step pool rest (t (K.head next) (flagsOr (K.tail reply) (K.tail next)))) instructions
     31 wordChain step input = let initial = K.head input in let rest = K.tail input in
     32   wordWalk step (K.head rest) (K.tail rest) (I.exact initial)
     33 checked input = wordChain checkedStep input
     34 trusted input = wordChain trustedStep input
     35 -- Private lazy record: (word,(isNaN,(isInf,(isZero,normalizedRecord)))).
     36 -- Word, exponent, fraction and normalized fields are shared within the record.
     37 prepare word = let e = B.exponent word in let f = L.low52 word in
     38   let special = N.equal e 2047 in let zeroFraction = N.zero f in
     39   t word (t (K.both special (K.not zeroFraction))
     40     (t (K.both special zeroFraction)
     41       (t (K.both (N.zero e) zeroFraction)
     42         (t (B.signBit word) (K.lazy (_ : B.subnormal f)
     43           (_ : t (N.add e 1229) (F.pack 1 word)) (N.zero e))))))
     44 word x = K.head x
     45 nan x = K.head (K.tail x)
     46 inf x = K.head (drop2 x)
     47 zero x = K.head (drop3 x)
     48 decoded x = drop4 x
     49 sign x = B.sign (decoded x)
     50 finiteAdd subtract a b = let da = decoded a in let originalB = decoded b in
     51   let db = t (K.xor subtract (B.sign originalB)) (K.tail originalB) in K.lazy
     52     (_ : K.lazy (_ : I.exact (I.zero (K.both (B.sign da) (B.sign db))))
     53       (_ : I.exact (K.choose (B.flip (word b)) (word b) subtract)) (zero b))
     54     (_ : K.lazy (_ : I.exact (word a))
     55       (_ : I.lift (K.lazy (_ : B.ordered da db) (_ : B.ordered db da) (B.dominates da db)))
     56       (zero b)) (zero a)
     57 finiteProduct a b = let da = decoded a in let db = decoded b in
     58   let negative = K.xor (B.sign da) (B.sign db) in K.lazy
     59     (_ : I.exact (I.zero negative))
     60     (_ : B.signed negative (I.quantize (N.subtract (N.add (B.scale da) (B.scale db)) 2304)
     61       (A.orderedMultiply (B.mant da) (B.mant db)))) (K.either (zero a) (zero b))
     62 finiteQuotient a b = let da = decoded a in let db = decoded b in
     63   let negative = K.xor (B.sign da) (B.sign db) in K.lazy
     64     (_ : I.exact (I.zero negative))
     65     (_ : B.signed negative (I.quantize (N.subtract (N.add 2248 (B.scale da)) (B.scale db))
     66       (P.jam (P.boundedQuotient (B.mant da) (B.mant db))))) (zero a)
     67 add subtract a b = let sa = sign a in let sb = K.xor subtract (sign b) in K.lazy
     68   (_ : K.lazy (_ : I.invalidResult) (_ : I.exact (I.infinity (K.choose sa sb (inf a))))
     69     (K.both (K.both (inf a) (inf b)) (K.xor sa sb)))
     70   (_ : finiteAdd subtract a b) (K.either (inf a) (inf b))
     71 multiply a b = let negative = K.xor (sign a) (sign b) in K.lazy
     72   (_ : K.lazy (_ : I.invalidResult) (_ : I.exact (I.infinity negative)) (K.either (zero a) (zero b)))
     73   (_ : finiteProduct a b) (K.either (inf a) (inf b))
     74 divide a b = let negative = K.xor (sign a) (sign b) in K.lazy
     75   (_ : K.lazy (_ : I.invalidResult) (_ : I.exact (I.infinity negative)) (inf b))
     76   (_ : K.lazy (_ : I.exact (I.zero negative))
     77     (_ : K.lazy (_ : K.lazy (_ : I.invalidResult)
     78         (_ : I.answer (I.infinity negative) t (t t) t t t) (zero a))
     79       (_ : finiteQuotient a b) (zero b)) (inf b)) (inf a)
     80 cachedOp op a b = K.lazy (_ : add t a b)
     81   (_ : K.lazy (_ : add (t t) a b)
     82     (_ : K.lazy (_ : multiply a b) (_ : divide a b) (N.equal op 2)) (N.equal op 1)) (N.zero op)
     83 cachedStep op a b = K.lazy (_ : I.nanResult (word a) (word b)) (_ : cachedOp op a b)
     84   (K.either (nan a) (nan b))
     85 cachedWalk lookup pool instructions state flags = K.triage (t (word state) flags) (_ : t (word state) flags)
     86   (instruction rest : let next = cachedStep (K.head instruction) state (lookup (K.tail instruction) pool) in
     87     cachedWalk lookup pool rest (prepare (K.head next)) (flagsOr flags (K.tail next))) instructions
     88 cached input = let initial = K.head input in let rest = K.tail input in
     89   cachedWalk at (K.map prepare (K.head rest)) (K.tail rest) (prepare initial) (K.tail (I.exact initial))
     90 freshLookup index pool = prepare (at index pool)
     91 fresh input = let initial = K.head input in let rest = K.tail input in
     92   cachedWalk freshLookup (K.head rest) (K.tail rest) (prepare initial) (K.tail (I.exact initial))
     93 freshBatch xs = K.map fresh xs
     94 -- Cache only within each operation: isolates cross-operation pool reuse.
     95 localStep op a b = cachedStep op (prepare a) (prepare b)
     96 local input = wordChain localStep input
     97 checkedBatch xs = K.map checked xs
     98 trustedBatch xs = K.map trusted xs
     99 localBatch xs = K.map local xs
    100 cachedBatch xs = K.map cached xs
    101 spin x = spin x
    102 emptyChecked x = checked (t 9223372036854775808 (t (spin x) t))
    103 emptyCached x = cached (t 9223372036854775808 (t (spin x) t))
    104 unusedPool x = cached (t 4607182418800017408 (t (t 0 (spin x)) (t (t 0 0) t)))
    105 flagsOne x = flagsOr (K.head x) (K.tail x)
    106 mergeFlags xs = K.map flagsOne xs
    107 flagDemand x = K.head (flagsOr (t (t t) (spin x)) (t (spin x) (spin x)))