tricu

97d703664739df908db963ab2f722b62ea14fa7175351e8ad788c97c5ec20621.tri (22024B)

---

 !export *
 -- 1.  t  t      a b       -> a
 -- 2.  t (t a)   b c       -> a c (b c)
 -- 3a. t (t a b) c t       -> a
 -- 3b. t (t a b) c (t u)   -> b u
 -- 3c. t (t a b) c (t u v) -> c u v
 
 false = t
 _     = t
 true  = t t
 id a = a
 const a b = a
 pair  = t
 if cond then else = t (t else (t t then)) t cond
 
 y = ((mut wait fun : wait mut (x : fun (wait mut x)))
      (x : x x)
      (a0 a1 a2 : t (t a0) (t t a2) a1))
 
 compose f g x = f (g x)
 
 triage leaf stem fork = t (t leaf stem) fork
 test   = triage "Leaf" (_ : "Stem") (_ _ : "Fork")
 
 matchBool = (ot of : triage
   of
   (_ : ot)
   (_ _ : ot)
 )
 
 lAnd = (triage
   (_     : false)
   (_ x   : x)
   (_ _ x : x))
 
 lOr = (triage
   (x     : x)
   (_ _   : true)
   (_ _ _ : true))
 
 matchPair a = triage _ _ a
 
 fst p = matchPair takeFirst p
   where takeFirst a b = a
 snd p = matchPair takeSecond p
   where takeSecond a b = b
 
 resultIsOk result =
   matchResult (errR rest : false) (val rest : true) result
 
 resultIsErr result =
   matchResult (errR rest : true) (val rest : false) result
 
 not? = matchBool false true
 and? = matchBool id (_ : false)
 
 or? = (x z : 
   matchBool 
     (matchBool true true z)
     (matchBool true false z)
     x)
 
 xor? = (x z : 
   matchBool 
     (matchBool false true z)
     (matchBool true false z)
     x)
 
 equal? = y (self : triage
   (triage
     true
     (_   : false)
     (_ _ : false))
   (ax :
     triage
       false
       (self ax)
       (_ _ : false))
   (ax ay :
     triage
       false
       (_ : false)
       (bx by : lAnd (self ax bx) (self ay by))))
 
 succ = y (self :
   triage
     1
     t
     (triage
       (t (t t))
       (_ tail : t t (self tail))
       t))
 
 ok value rest = pair true (pair value rest)
 err msg rest = pair false (pair msg rest)
 
 matchResult errCase okCase result =
   matchPair
     (tag payload :
       matchPair
         (value rest :
           matchBool
             (okCase value rest)
             (errCase value rest)
             tag)
         payload)
     result
 
 -- ---------------------------------------------------------------------------
 -- Maybe / Option type
 -- ---------------------------------------------------------------------------
 
 nothing = t
 just x = t x
 
 matchMaybe nothingCase justCase maybe =
   triage
     nothingCase
     justCase
     (_ _ : nothingCase)
     maybe
 
 maybe default f m = matchMaybe default f m
 maybeMap f m = matchMaybe nothing (x : just (f x)) m
 maybeBind m f = matchMaybe nothing f m
 maybeOr default m = matchMaybe default id m
 maybe? = matchMaybe false (_ : true)
 
 -- ---------------------------------------------------------------------------
 -- Lazy eliminators
 --
 -- A strict eliminator evaluates both branches because they are ordinary
 -- arguments. Give a branch that recurses, looks something up, or builds
 -- structure to one of these instead: it becomes a thunk and only the selected
 -- branch is ever applied.
 -- ---------------------------------------------------------------------------
 
 lazyBool = (thenK elseK cond :
   ((chosen : chosen t)
    (matchBool
      thenK
      elseK
      cond)))
 
 -- `triage` selects a thunk directly: a cons is a Fork, so the cons case sits
 -- in the fork slot, exactly as in `matchList` below.
 lazyList = (nilK consK xs :
   ((chosen : chosen t)
    (triage
      nilK
      _
      (h r : (_ : consK h r))
      xs)))
 
 lazyMaybe = (noneK someK m :
   ((chosen : chosen t)
    (matchMaybe
      noneK
      (x : (_ : someK x))
      m)))
 
 lazyResult = (errK okK result :
   ((chosen : chosen t)
    (matchResult
      (code rest : (_ : errK code rest))
      (value rest : (_ : okK value rest))
      result)))
 
 -- ---------------------------------------------------------------------------
 -- Basic arithmetic
 -- ---------------------------------------------------------------------------
 
 ifLazy = (cond thenK elseK :
   matchBool
     (thenK t)
     (elseK t)
     cond)
 
 andLazy? = (a bK :
   ifLazy
     a
     bK
     (_ : false))
 
 pred_ = y (self : triage
   0
   0
   (bit rest :
     ifLazy
       bit
       (_ : matchBool
         (t t rest)
         0
         rest)
       (_ : t (t t) (self rest))))
 
 pred @nat? =@nat? pred_
 
 isZero_? = triage true (_ : false) (_ _ : false)
 
 isZero? @nat? =@bool? isZero_?
 
 add @nat? @nat? =@nat? (y (self x y :
   triage
     y
     (_ : succ y)
     (_ _ : succ (self (pred_ x) y))
     x))
 
 sub @nat? @nat? =@nat? y (self a b :
   ifLazy
     (isZero_? b)
     (_ : a)
     (_ : self (pred_ a) (pred_ b)))
 
 lte_? = y (self a b :
   ifLazy
     (isZero_? a)
     (_ : true)
     (_ :
       ifLazy
         (isZero_? b)
         (_ : false)
         (_ : self (pred_ a) (pred_ b))))
 
 lte? @nat? @nat? =@bool? lte_?
 
 gte_? = a b : lte_? b a
 
 gte? @nat? @nat? =@bool? gte_?
 
 lt_? = a b : and? (lte_? a b) (not? (equal? a b))
 
 lt? @nat? @nat? =@bool? lt_?
 
 gt_? = a b : lt_? b a
 
 gt? @nat? @nat? =@bool? gt_?
 
 mul @nat? @nat? =@nat? y (self a b :
   ifLazy
     (isZero_? b)
     (_ : 0)
     (_ : add a (self a (pred_ b))))
 
 div @nat? @nat? =@nat? y (self a b :
   ifLazy
     (isZero_? b)
     (_ : 0)
     (_ : ifLazy
       (lt_? a b)
       (_ : 0)
       (_ : succ (self (sub a b) b))))
 
 mod @nat? @nat? =@nat? y (self a b :
   ifLazy
     (isZero_? b)
     (_ : 0)
     (_ : ifLazy
       (lt_? a b)
       (_ : a)
       (_ : self (sub a b) b)))
 
 pow @nat? @nat? =@nat? y (self a b :
   ifLazy
     (isZero_? b)
     (_ : 1)
     (_ : mul a (self a (pred_ b))))
 
 even? n = (triage
   true
   (_ : false)
   (bit _ : isZero_? bit)
   n)
 
 odd? = (n : not? (even? n))
 
 min @nat? @nat? =@nat? (a b : ifLazy (lte_? a b) (_ : a) (_ : b))
 
 max @nat? @nat? =@nat? (a b : ifLazy (lte_? a b) (_ : b) (_ : a))
 
 -- ---------------------------------------------------------------------------
 -- Result combinators
 -- ---------------------------------------------------------------------------
 
 mapResult = (f result :
   matchResult
     (code rest : err code rest)
     (value rest : ok (f value) rest)
     result)
 
 bindResult = (result f :
   matchResult
     (code rest : err code rest)
     (value rest : f value rest)
     result)
 
 resultOr = (default result :
   matchResult
     (_ _ : default)
     (value _ : value)
     result)
 
 resultMapErr = (f result :
   matchResult
     (code rest : err (f code) rest)
     (value rest : ok value rest)
     result)
 
 -- ---------------------------------------------------------------------------
 -- List
 -- ---------------------------------------------------------------------------
 
 matchList = a b : triage a _ b
 
 emptyList? = matchList true (_ _ : false)
 head xs@(nonEmptyListOf anyC) =@anyC matchList t (h _ : h) xs
 tail xs@(nonEmptyListOf anyC) =@(listOf anyC) matchList t (_ r : r) xs
 
 append_ self xs ys =
   matchList
     ys
     (h r : pair h (self r ys))
     xs
 append = xs ys : y append_ xs ys
 
 lExist?_ self x xs =
   matchList
     false
     (h r : or? (equal? x h) (self x r))
     xs
 lExist? = x xs : y lExist?_ x xs
 
 map_ self l f =
   matchList
     t
     (h r : pair (f h) (self r f))
     l
 map = f l : y map_ l f
 
 filter_ self l f =
   matchList
     t
     (h r :
       matchBool
         (pair h (self r f))
         (self r f)
         (f h))
     l
 filter = f l : y filter_ l f
 
 foldl_ self l f acc =
   matchList
     acc
     (h r : self r f (f acc h))
     l
 foldl = f x l : y foldl_ l f x
 
 foldr_ self l f x =
   matchList
     x
     (h r : f (self r f x) h)
     l
 foldr = f x l : y foldr_ l f x
 
 length_ self xs =
   matchList
     0
     (_ r : succ (self r))
     xs
 length @(listOf anyC) =@nat? y length_
 
 reverse_ self xs acc =
   matchList
     acc
     (h r : self r (pair h acc))
     xs
 reverse = xs : y reverse_ xs t
 
 snoc_ self x xs =
   matchList
     (pair x t)
     (h r : pair h (self x r))
     xs
 snoc = x xs : y snoc_ x xs
 
 count_ self x xs =
   matchList
     0
     (h r :
       matchBool
         (succ (self x r))
         (self x r)
         (equal? x h))
     xs
 count = x xs : y count_ x xs
 
 last_ self xs =
   matchList
     t
     (h r :
       matchBool
         h
         (self r)
         (emptyList? r))
     xs
 last @(nonEmptyListOf anyC) =@anyC y last_
 
 all?_ self pred xs =
   matchList
     true
     (h r : and? (pred h) (self pred r))
     xs
 all? = pred xs : y all?_ pred xs
 
 any?_ self pred xs =
   matchList
     false
     (h r : or? (pred h) (self pred r))
     xs
 any? = pred xs : y any?_ pred xs
 
 intersect = xs ys : filter (x : lExist? x ys) xs
 
 nth_ self xs n i =
   matchList
     t
     (h r :
       matchBool
         h
         (self r n (succ i))
         (equal? i n))
     xs
 nth = n xs : y nth_ xs n 0
 
 headMaybe = matchList nothing (h _ : just h)
 
 lastMaybe_ self xs =
   matchList
     nothing
     (h r :
       matchBool
         (just h)
         (self r)
         (emptyList? r))
     xs
 lastMaybe = xs : y lastMaybe_ xs
 
 nthMaybe_ self xs n i =
   matchList
     nothing
     (h r :
       matchBool
         (just h)
         (self r n (succ i))
         (equal? i n))
     xs
 nthMaybe = n xs : y nthMaybe_ xs n 0
 
 take_ self xs n i =
   matchList
     t
     (h r :
       matchBool
         t
         (pair h (self r n (succ i)))
         (equal? i n))
     xs
 take = n xs : y take_ xs n 0
 
 drop_ self xs n i =
   matchBool
     xs
     (matchList
       t
       (_ r : self r n (succ i))
       xs)
     (equal? i n)
 drop = n xs : y drop_ xs n 0
 
 splitAt = n xs : pair (take n xs) (drop n xs)
 
 concatMap_ self f xs =
   matchList
     t
     (h r : append (f h) (self f r))
     xs
 concatMap = f xs : y concatMap_ f xs
 
 find_ self pred xs =
   matchList
     nothing
     (h r :
       matchBool
         (just h)
         (self pred r)
         (pred h))
     xs
 find = pred xs : y find_ pred xs
 
 partition_ self pred xs trues falses =
   matchList
     (pair (reverse trues) (reverse falses))
     (h r :
       matchBool
         (self pred r (pair h trues) falses)
         (self pred r trues (pair h falses))
         (pred h))
     xs
 partition = pred xs : y partition_ pred xs t t
 
 strLength = length
 strAppend = append
 strEq? = equal?
 strEmpty? = emptyList?
 
 startsWith?_ self prefix input =
   matchList
     true
     (ph pr :
       matchList
         false
         (sh sr :
           matchBool
             (self pr sr)
             false
             (equal? ph sh))
         input)
     prefix
 startsWith? = prefix input : y startsWith?_ prefix input
 
 endsWith? = prefix str : startsWith? (reverse prefix) (reverse str)
 
 contains?_ self needle haystack =
   matchBool
     true
     (matchList
       false
       (_ r : self needle r)
       haystack)
     (startsWith? needle haystack)
 contains? = needle haystack : y contains?_ needle haystack
 
 sum @(listOf nat?) =@nat? foldl (acc x : add x acc) 0
 product @(listOf nat?) =@nat? foldl (acc x : mul x acc) 1
 
 -- ---------------------------------------------------------------------------
 -- Generic separators
 --
 -- `lines`, `unlines`, `words` and `unwords` at the bottom of this section are
 -- the byte-valued special cases of these primitives.
 --
 -- Joining takes any separator; splitting takes one byte. Separators are removed
 -- rather than kept, and empty fields are preserved.
 -- ---------------------------------------------------------------------------
 
 takeWhile_ self xs f =
   lazyList
     (_ : t)
     (h r :
       lazyBool
         (_ : pair h (self r f))
         (_ : t)
         (f h))
     xs
 takeWhile = f xs : y takeWhile_ xs f
 
 dropWhile_ self xs f =
   lazyList
     (_ : t)
     (h r :
       lazyBool
         (_ : self r f)
         (_ : pair h r)
         (f h))
     xs
 dropWhile = f xs : y dropWhile_ xs f
 
 -- Byte-level whitespace only: space and horizontal tab (HTTP OWS).
 spaceByte? = b : equal? b 32
 tabByte?   = b : equal? b 9
 trimByte?  = b : or? (spaceByte? b) (tabByte? b)
 
 trim = xs : dropWhile trimByte? (reverse (dropWhile trimByte? (reverse xs)))
 
 intercalate_ self xs sep =
   lazyList
     (_ : t)
     (h r :
       lazyBool
         (_ : h)
         (_ : append h (append sep (self r sep)))
         (emptyList? r))
     xs
 intercalate = sep xs : y intercalate_ xs sep
 
 -- Separator after every field, including the last one. Line-oriented formats
 -- want this: `joinSuffix "\n" xs` terminates the final line while
 -- `intercalate "\n" xs` does not.
 joinSuffix_ self xs sep =
   lazyList
     (_ : t)
     (h r : append (append h sep) (self r sep))
     xs
 joinSuffix = sep xs : y joinSuffix_ xs sep
 
 -- Split on a single byte. 
 -- Empty fields are preserved: `splitOnByte 58 "a::b"` is ["a" "" "b"].
 splitByte_ self str byte acc current =
   lazyList
     (_ : map reverse (reverse (pair current acc)))
     (h r :
       lazyBool
         (_ : self r byte (pair current acc) t)
         (_ : self r byte acc (pair h current))
         (equal? h byte))
     str
 splitOnByte = byte str : y splitByte_ str byte t t
 
 -- Every one of these keeps its arguments bound: partially applying a
 -- multi-argument function at the top level leaves a fixed point exposed.
 lines   = str : splitOnByte 10 str
 unlines = xs : joinSuffix "\n" xs
 
 -- Runs of separators collapse: empty fields are dropped.
 words   = str : filter (w : not? (emptyList? w)) (splitOnByte 32 str)
 unwords = xs : intercalate " " xs
 
 zipWith_ self f xs ys =
   matchList
     t
     (xh xt :
       matchList
         t
         (yh yt : pair (f xh yh) (self f xt yt))
         ys)
     xs
 zipWith = f xs ys : y zipWith_ f xs ys
 
 -- ---------------------------------------------------------------------------
 -- Core contract type
 --
 -- A contract is an ordinary tricu function: Tree -> Tree -> Result Tree Tree.
 -- The second argument is the conventional "rest" slot. On success a contract
 -- returns the checked value wrapped in the standard ok shape; on failure it
 -- returns a diagnostic wrapped in the standard err shape.
 --
 -- The contract kernel is a globally configurable function selected by the
 -- runner. It decides whether to accept the contract result, replace it, log
 -- it, or transform the diagnostic. The default kernel is the identity on the
 -- contract Result.
 --
 -- The runner may rebind 'kernel' to a different kernel before evaluating
 -- user code (e.g. via --contract-kernel).
 -- ---------------------------------------------------------------------------
 
 contractOk = (value : (rest : ok value rest))
 contractErr = (msg : (rest : err msg rest))
 
 -- Default contract kernel. Return the contract Result unchanged.
 defaultKernel = (contract value result :
   matchResult
     (msg rest : err msg rest)
     (v rest : ok v rest)
     result)
 
 -- The active kernel. The runner may rebind this name to a different kernel
 -- before evaluating user code (e.g. via --contract-kernel). Internally,
 -- withContract dispatches through this binding, so rebinding 'kernel' changes
 -- the behaviour of every contract boundary in the program.
 kernel = defaultKernel
 
 -- Skip-everything kernel. Resume with the original value on failure.
 skipKernel = (contract value result :
   matchResult
     (msg rest : ok value rest)
     (v rest : ok v rest)
     result)
 
 -- Apply a contract and pass the raw Result to the kernel.
 withContract = (contract value :
   kernel contract value (contract value t))
 
 -- Apply a contract and return the checked value or the diagnostic message.
 check contract value =
   matchResult
     (msg _ : msg)
     (v _ : v)
     (withContract contract value)
 
 -- Apply a contract and return the raw Result (kernel is bypassed).
 checkContract = (contract value : contract value t)
 
 -- ---------------------------------------------------------------------------
 -- Basic contracts
 -- ---------------------------------------------------------------------------
 
 -- Any value passes.
 anyC = (value : contractOk value)
 
 -- Always fails with the supplied message.
 neverC = (msg : (value : contractErr msg))
 
 -- Build a contract from a predicate that inspects only the value.
 guardC = (msg predicate value rest :
   lazyBool
     (_ : contractOk value rest)
     (_ : contractErr msg rest)
     (predicate value))
 
 -- Structural natural-number predicate.
 -- A natural is either Leaf (0) or Fork bit rest where bit is Leaf (even)
 -- or Stem Leaf (odd) and rest is itself a natural.
 isNat? = y (self n :
   triage
     true
     (_ : false)
     (bit r :
       triage
         (self r)
         (_ : self r)
         (_ _ : false)
         bit)
     n)
 
 -- Natural number contract.
 nat? = guardC "not a natural number" isNat?
 
 -- Non-zero natural number contract.
 nonZero? = guardC "non-zero" (n : and? (isNat? n) (not? (isZero_? n)))
 
 -- Boolean contract.
 bool? = guardC "not a boolean" (b : or? (equal? b true) (equal? b false))
 
 -- ---------------------------------------------------------------------------
 -- Contract combinators
 -- ---------------------------------------------------------------------------
 
 andC = (c1 c2 value rest :
   matchResult
     (msg _ : contractErr msg rest)
     (v _ : c2 v rest)
     (c1 value rest))
 
 orC = (c1 c2 value rest :
   matchResult
     (msg _ : c2 value rest)
     (v _ : contractOk v rest)
     (c1 value rest))
 
 notC = (c value rest :
   matchResult
     (msg _ : contractOk value rest)
     (_ _ : contractErr "notC: predicate succeeded" rest)
     (c value rest))
 
 mapC = (f c value rest :
   matchResult
     (msg _ : contractErr msg rest)
     (v _ : contractOk (f v) rest)
     (c value rest))
 
 bindC = (c f value rest :
   matchResult
     (msg _ : contractErr msg rest)
     (v _ : f v value rest)
     (c value rest))
 
 -- ---------------------------------------------------------------------------
 -- Collection contracts
 -- ---------------------------------------------------------------------------
 
 listOf = (c value rest :
   y (self orig xs :
     matchList
       (contractOk orig rest)
       (h r :
         matchResult
           (msg _ : contractErr msg rest)
           (_ _ : self orig r)
           (c h rest))
       xs) value value)
 
 nonEmptyListOf = (c :
   andC (guardC "empty list" (xs : not? (emptyList? xs))) (listOf c))
 
 pairOf = (c1 c2 p rest :
   matchPair
     (a b :
       matchResult
         (msg _ : contractErr msg rest)
         (a' _ :
           matchResult
             (msg _ : contractErr msg rest)
             (b' _ : contractOk (pair a' b') rest)
             (c2 b rest))
         (c1 a rest))
     p)
 
 -- ---------------------------------------------------------------------------
 -- Higher-order function contracts
 --
 -- These return a Result-wrapped proxy. The proxy itself is a contract: it
 -- checks arguments on the way in and results on the way out.
 -- ---------------------------------------------------------------------------
 
 fnContract = (argC resC f rest :
   contractOk
     (x : (rest1 :
       matchResult
         (msg _ : contractErr msg rest1)
         (x' _ :
           matchResult
             (msg _ : contractErr msg rest1)
             (y _ : contractOk y rest1)
             (withContract resC (f x')))
         (withContract argC x)))
     rest)
 
 fn2 = (arg1C arg2C resC f rest :
   contractOk
     (x : (rest1 :
       matchResult
         (msg _ : contractErr msg rest1)
         (x' _ :
           contractOk
             (y : (rest2 :
               matchResult
                 (msg _ : contractErr msg rest2)
                 (y' _ :
                   matchResult
                     (msg _ : contractErr msg rest2)
                     (z _ : contractOk z rest2)
                     (withContract resC (f x' y')))
                 (withContract arg2C y)))
             rest1)
         (withContract arg1C x)))
     rest)
 
 -- ---------------------------------------------------------------------------
 -- Interaction-tree effect layer
 --
 -- These constructors and combinators layer catchable, composable failures on
 -- top of the core Result contracts. They reuse the same tags as tricu IO:
 --   0 = pureE
 --   1 = bindE
 --   2 = exceptE
 -- ---------------------------------------------------------------------------
 
 pureE = (value : pair 0 value)
 bindE = (action k : pair 1 (pair action k))
 exceptE = (tag value k : pair 2 (pair tag (pair value k)))
 
 pureM = pureE
 bindM = bindE
 
 -- Lift a contract failure into an interaction tree.
 checkM = (contract value :
   matchResult
     (msg _ : exceptE "contract" msg (_ : pureE t))
     (checked _ : pureE checked)
     (contract value t))
 
 -- Lift a pure function into the interaction tree.
 liftM = (f : (x : pureE (f x)))
 
 -- Interpret a pure interaction tree into a Result.
 runM = (tree :
   run tree
   where run =
           y (self tree :
             matchPair
               (op payload :
                 matchBool
                   -- pureE
                   (contractOk (snd tree) t)
                   (matchBool
                     -- bindE
                     (matchPair
                       (action k :
                         matchResult
                           (msg _ : contractErr msg t)
                           (v _ : self (k v))
                           (self action))
                       payload)
                     -- exceptE
                     (matchPair
                       (tag pair :
                         matchPair
                           (value k :
                             contractErr value t)
                           pair)
                       payload)
                     (equal? op 1))
                   (equal? op 0))
               tree))
 
 -- Handle matching exceptE nodes by applying the handler to the value and the
 -- resumption continuation. Non-matching exceptions are left in place.
 handleM = (tag handler tree :
   handle tree
   where handle =
           y (self tree :
             matchPair
               (op payload :
                 matchBool
                   -- pureE
                   tree
                   (matchBool
                     -- bindE
                     (matchPair
                       (action k :
                         bindE (self action) (v : self (k v)))
                       payload)
                     -- exceptE
                     (matchPair
                       (et pair :
                         matchPair
                           (value k :
                             matchBool
                               (self (handler value k))
                               tree
                               (equal? et tag))
                           pair)
                       payload)
                     (equal? op 1))
                   (equal? op 0))
               tree))