tricu

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

9d35660dc220f72eb03bd57a02c9afaac7d3a911424fd558ab85d9142ea140f0.tri (1863B)

      1 -- Binary64 facade: checked word boundaries, trusted constructed values.
      2 !import native_math as N
      3 !import binary64_kernels as K
      4 !import binary64_working as W
      5 !import binary64_chains as C
      6 !export add
      7 !export addBits
      8 !export clearFlags
      9 !export divide
     10 !export divideBits
     11 !export divideByZero
     12 !export flags
     13 !export fromBits
     14 !export fromBitsC
     15 !export inexact
     16 !export invalid
     17 !export mergeFlags
     18 !export multiply
     19 !export multiplyBits
     20 !export overflow
     21 !export subtract
     22 !export subtractBits
     23 !export toBits
     24 !export underflow
     25 !export value
     26 !export word?
     27 
     28 isLeaf x = K.triage (t t) (_ : t) (_ _ : t) x
     29 isBit x = K.triage (t t) (child : isLeaf child) (_ _ : t) x
     30 wordWalk fuel previous x = K.lazy (_ : K.both previous (isLeaf x))
     31   (_ : K.triage previous (_ : t)
     32     (bit rest : K.lazy (_ : wordWalk (N.predecessor fuel) bit rest)
     33       (_ : t) (isBit bit)) x) (N.zero fuel)
     34 isWord x = wordWalk 64 (t t) x
     35 ok x rest = t (t t) (t x rest)
     36 err rest = t t (t "binary64 word" rest)
     37 word? x rest = K.lazy (_ : ok x rest) (_ : err rest) (isWord x)
     38 fromBitsC x rest = K.lazy (_ : ok (W.fromWord x) rest) (_ : err rest) (isWord x)
     39 fromBits x = fromBitsC x t
     40 toBits x = W.toWord x
     41 add a b = W.step 0 a b
     42 subtract a b = W.step 1 a b
     43 multiply a b = W.step 2 a b
     44 divide a b = W.step 3 a b
     45 value reply = K.head reply
     46 flags reply = K.tail reply
     47 clearFlags = t t (t t (t t (t t t)))
     48 mergeFlags a b = C.flagsOr a b
     49 invalid f = K.head f
     50 divideByZero f = K.head (K.tail f)
     51 overflow f = K.head (C.drop2 f)
     52 underflow f = K.head (C.drop3 f)
     53 inexact f = C.drop4 f
     54 checked op a b = K.lazy
     55   (_ : K.lazy
     56     (_ : let reply = W.step op (W.fromWord a) (W.fromWord b) in
     57       ok (t (W.toWord (value reply)) (flags reply)) t)
     58     (_ : err t) (isWord b))
     59   (_ : err t) (isWord a)
     60 addBits a b = checked 0 a b
     61 subtractBits a b = checked 1 a b
     62 multiplyBits a b = checked 2 a b
     63 divideBits a b = checked 3 a b