tricu

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

float-boundary.tri (1917B)

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