tricu

An interpreted language for exploring Tree Calculus
Log | Files | Refs | README | LICENSE

505c81c87fee684b23a8cc74bc2e1b4e7819ed022c33951093b063f2388615f2.tri (3725B)

      1 !export compare
      2 !export equal
      3 !export lt
      4 !export lte
      5 !export gt
      6 !export gte
      7 !export inRange
      8 !export minimum
      9 !export maximum
     10 !export zero
     11 !export odd
     12 !export even
     13 !export successor
     14 !export predecessor
     15 !export add
     16 !export subtract
     17 !export multiply
     18 !export decimal
     19 !export ascii
     20 !export digit
     21 !export letter
     22 !export lowerHex
     23 !export printable
     24 -- Canonical natural numbers only. No validation or contracts on this path.
     25 -- Self-contained native module; explicit fixed points support both backends.
     26 
     27 triage leaf stem fork = t (t leaf stem) fork
     28 choose yes no value = triage no (_ : yes) (_ _ : yes) value
     29 lazy yes no value = choose yes no value t
     30 not value = choose t (t t) value
     31 both a b = choose b t a
     32 either a b = choose (t t) b a
     33 xor a b = choose (not b) b a
     34 fix = ((mut wait fun : wait mut (x : fun (wait mut x)))
     35   (x : x x)
     36   (a b c : t (t a) (t t c) b))
     37 
     38 -- Ordering: Leaf = equal, Stem Leaf = less, Fork Leaf Leaf = greater.
     39 bitOrder a b = choose (choose t (t t t) b) (choose (t t) t b) a
     40 compareStep self a b = (triage
     41   (triage t (_ : t) (_ _ : t t) b)
     42   (_ : t)
     43   (abit ar : triage (t t t) (_ : t)
     44     (bbit br : triage (bitOrder abit bbit) (_ : t t) (_ _ : t t t)
     45       (self ar br)) b)
     46   a)
     47 compare a b = fix compareStep a b
     48 isEqual order = triage (t t) (_ : t) (_ _ : t) order
     49 isLess order = triage t (_ : t t) (_ _ : t) order
     50 isGreater order = triage t (_ : t) (_ _ : t t) order
     51 -- Equality may stop at the first differing low bit; ordering cannot.
     52 equalStep self a b = (triage
     53   (zero b)
     54   (_ : t)
     55   (abit ar : triage t (_ : t)
     56     (bbit br : lazy (_ : t) (_ : self ar br) (xor abit bbit)) b)
     57   a)
     58 equal a b = fix equalStep a b
     59 lt a b = isLess (compare a b)
     60 lte a b = not (isGreater (compare a b))
     61 gt a b = isGreater (compare a b)
     62 gte a b = not (isLess (compare a b))
     63 inRange value low high = both (gte value low) (lte value high)
     64 minimum a b = choose b a (gt a b)
     65 maximum a b = choose a b (gt a b)
     66 zero value = triage (t t) (_ : t) (_ _ : t) value
     67 odd value = triage t (_ : t) (bit rest : bit) value
     68 even value = not (odd value)
     69 
     70 -- Discard a redundant high zero bit when rebuilding after subtraction.
     71 node bit rest = choose (t bit rest) (choose t (t bit rest) (zero rest)) bit
     72 double value = node t value
     73 succStep self value = (triage (t (t t) t) (_ : t)
     74   (bit rest : triage (t (t t) rest) (_ : t t (self rest)) (_ _ : t) bit) value)
     75 successor value = fix succStep value
     76 predStep self value = (triage t (_ : t)
     77   (bit rest : lazy (_ : node t rest) (_ : t (t t) (self rest)) bit) value)
     78 predecessor value = fix predStep value
     79 
     80 carry a b c = either (both a b) (both c (xor a b))
     81 addStep self a b c = (triage
     82   (lazy (_ : successor b) (_ : b) c)
     83   (_ : t)
     84   (abit ar : triage
     85     (lazy (_ : successor a) (_ : a) c)
     86     (_ : t)
     87     (bbit br : t (xor (xor abit bbit) c) (self ar br (carry abit bbit c))) b)
     88   a)
     89 add a b = fix addStep a b t
     90 
     91 borrow a b c = either (both (not a) b) (both c (not (xor a b)))
     92 subStep self a b c = (triage t (_ : t)
     93   (abit ar : triage
     94     (lazy (_ : predecessor a) (_ : a) c)
     95     (_ : t)
     96     (bbit br : node (xor (xor abit bbit) c) (self ar br (borrow abit bbit c))) b)
     97   a)
     98 subtract a b = lazy (_ : t) (_ : fix subStep a b t) (lt a b)
     99 
    100 mulStep self b a = (triage t (_ : t)
    101   (bit rest : lazy
    102     (_ : add a (double (self rest a)))
    103     (_ : double (self rest a)) bit)
    104   b)
    105 multiply a b = fix mulStep b a
    106 -- Decimal accumulation: value * 10 + digit (digit must be 0..9).
    107 decimal value digit = add (add (double (double (double value))) (double value)) digit
    108 
    109 ascii value = lte value 127
    110 digit value = inRange value 48 57
    111 letter value = either (inRange value 65 90) (inRange value 97 122)
    112 lowerHex value = either (digit value) (inRange value 97 102)
    113 printable value = inRange value 32 126