tricu

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

base.tri (21889B)


      1 false = t
      2 _     = t
      3 true  = t t
      4 id a = a
      5 const a b = a
      6 pair  = t
      7 if cond then else = t (t else (t t then)) t cond
      8 
      9 y = ((mut wait fun : wait mut (x : fun (wait mut x)))
     10      (x : x x)
     11      (a0 a1 a2 : t (t a0) (t t a2) a1))
     12 
     13 compose f g x = f (g x)
     14 
     15 triage leaf stem fork = t (t leaf stem) fork
     16 test   = triage "Leaf" (_ : "Stem") (_ _ : "Fork")
     17 
     18 matchBool = (ot of : triage
     19   of
     20   (_ : ot)
     21   (_ _ : ot)
     22 )
     23 
     24 lAnd = (triage
     25   (_     : false)
     26   (_ x   : x)
     27   (_ _ x : x))
     28 
     29 lOr = (triage
     30   (x     : x)
     31   (_ _   : true)
     32   (_ _ _ : true))
     33 
     34 matchPair a = triage _ _ a
     35 
     36 fst p = matchPair takeFirst p
     37   where takeFirst a b = a
     38 snd p = matchPair takeSecond p
     39   where takeSecond a b = b
     40 
     41 resultIsOk result =
     42   matchResult (errR rest : false) (val rest : true) result
     43 
     44 resultIsErr result =
     45   matchResult (errR rest : true) (val rest : false) result
     46 
     47 not? = matchBool false true
     48 and? = matchBool id (_ : false)
     49 
     50 or? = (x z : 
     51   matchBool 
     52     (matchBool true true z)
     53     (matchBool true false z)
     54     x)
     55 
     56 xor? = (x z : 
     57   matchBool 
     58     (matchBool false true z)
     59     (matchBool true false z)
     60     x)
     61 
     62 equal? = y (self : triage
     63   (triage
     64     true
     65     (_   : false)
     66     (_ _ : false))
     67   (ax :
     68     triage
     69       false
     70       (self ax)
     71       (_ _ : false))
     72   (ax ay :
     73     triage
     74       false
     75       (_ : false)
     76       (bx by : lAnd (self ax bx) (self ay by))))
     77 
     78 succ = y (self :
     79   triage
     80     1
     81     t
     82     (triage
     83       (t (t t))
     84       (_ tail : t t (self tail))
     85       t))
     86 
     87 ok value rest = pair true (pair value rest)
     88 err msg rest = pair false (pair msg rest)
     89 
     90 matchResult errCase okCase result =
     91   matchPair
     92     (tag payload :
     93       matchPair
     94         (value rest :
     95           matchBool
     96             (okCase value rest)
     97             (errCase value rest)
     98             tag)
     99         payload)
    100     result
    101 
    102 -- ---------------------------------------------------------------------------
    103 -- Maybe / Option type
    104 -- ---------------------------------------------------------------------------
    105 
    106 nothing = t
    107 just x = t x
    108 
    109 matchMaybe nothingCase justCase maybe =
    110   triage
    111     nothingCase
    112     justCase
    113     (_ _ : nothingCase)
    114     maybe
    115 
    116 maybe default f m = matchMaybe default f m
    117 maybeMap f m = matchMaybe nothing (x : just (f x)) m
    118 maybeBind m f = matchMaybe nothing f m
    119 maybeOr default m = matchMaybe default id m
    120 maybe? = matchMaybe false (_ : true)
    121 
    122 -- ---------------------------------------------------------------------------
    123 -- Lazy eliminators
    124 --
    125 -- A strict eliminator evaluates both branches because they are ordinary
    126 -- arguments. Give a branch that recurses, looks something up, or builds
    127 -- structure to one of these instead: it becomes a thunk and only the selected
    128 -- branch is ever applied.
    129 -- ---------------------------------------------------------------------------
    130 
    131 lazyBool = (thenK elseK cond :
    132   ((chosen : chosen t)
    133    (matchBool
    134      thenK
    135      elseK
    136      cond)))
    137 
    138 -- This module has no list matcher, so `triage` is used directly: a cons is a
    139 -- Fork, which is why the cons case sits in the fork slot, exactly as in
    140 -- `matchList` in lib/list.tri.
    141 lazyList = (nilK consK xs :
    142   ((chosen : chosen t)
    143    (triage
    144      nilK
    145      _
    146      (h r : (_ : consK h r))
    147      xs)))
    148 
    149 lazyMaybe = (noneK someK m :
    150   ((chosen : chosen t)
    151    (matchMaybe
    152      noneK
    153      (x : (_ : someK x))
    154      m)))
    155 
    156 lazyResult = (errK okK result :
    157   ((chosen : chosen t)
    158    (matchResult
    159      (code rest : (_ : errK code rest))
    160      (value rest : (_ : okK value rest))
    161      result)))
    162 
    163 -- ---------------------------------------------------------------------------
    164 -- Basic arithmetic
    165 -- ---------------------------------------------------------------------------
    166 
    167 ifLazy = (cond thenK elseK :
    168   matchBool
    169     (thenK t)
    170     (elseK t)
    171     cond)
    172 
    173 andLazy? = (a bK :
    174   ifLazy
    175     a
    176     bK
    177     (_ : false))
    178 
    179 pred_ = y (self : triage
    180   0
    181   0
    182   (bit rest :
    183     ifLazy
    184       bit
    185       (_ : matchBool
    186         (t t rest)
    187         0
    188         rest)
    189       (_ : t (t t) (self rest))))
    190 
    191 pred @nat? =@nat? pred_
    192 
    193 isZero_? = triage true (_ : false) (_ _ : false)
    194 
    195 isZero? @nat? =@bool? isZero_?
    196 
    197 add @nat? @nat? =@nat? (y (self x y :
    198   triage
    199     y
    200     (_ : succ y)
    201     (_ _ : succ (self (pred_ x) y))
    202     x))
    203 
    204 sub @nat? @nat? =@nat? y (self a b :
    205   ifLazy
    206     (isZero_? b)
    207     (_ : a)
    208     (_ : self (pred_ a) (pred_ b)))
    209 
    210 lte_? = y (self a b :
    211   ifLazy
    212     (isZero_? a)
    213     (_ : true)
    214     (_ :
    215       ifLazy
    216         (isZero_? b)
    217         (_ : false)
    218         (_ : self (pred_ a) (pred_ b))))
    219 
    220 lte? @nat? @nat? =@bool? lte_?
    221 
    222 gte_? = a b : lte_? b a
    223 
    224 gte? @nat? @nat? =@bool? gte_?
    225 
    226 lt_? = a b : and? (lte_? a b) (not? (equal? a b))
    227 
    228 lt? @nat? @nat? =@bool? lt_?
    229 
    230 gt_? = a b : lt_? b a
    231 
    232 gt? @nat? @nat? =@bool? gt_?
    233 
    234 mul @nat? @nat? =@nat? y (self a b :
    235   ifLazy
    236     (isZero_? b)
    237     (_ : 0)
    238     (_ : add a (self a (pred_ b))))
    239 
    240 div @nat? @nat? =@nat? y (self a b :
    241   ifLazy
    242     (isZero_? b)
    243     (_ : 0)
    244     (_ : ifLazy
    245       (lt_? a b)
    246       (_ : 0)
    247       (_ : succ (self (sub a b) b))))
    248 
    249 mod @nat? @nat? =@nat? y (self a b :
    250   ifLazy
    251     (isZero_? b)
    252     (_ : 0)
    253     (_ : ifLazy
    254       (lt_? a b)
    255       (_ : a)
    256       (_ : self (sub a b) b)))
    257 
    258 pow @nat? @nat? =@nat? y (self a b :
    259   ifLazy
    260     (isZero_? b)
    261     (_ : 1)
    262     (_ : mul a (self a (pred_ b))))
    263 
    264 even? n = (triage
    265   true
    266   (_ : false)
    267   (bit _ : isZero_? bit)
    268   n)
    269 
    270 odd? = (n : not? (even? n))
    271 
    272 min @nat? @nat? =@nat? (a b : ifLazy (lte_? a b) (_ : a) (_ : b))
    273 
    274 max @nat? @nat? =@nat? (a b : ifLazy (lte_? a b) (_ : b) (_ : a))
    275 
    276 -- ---------------------------------------------------------------------------
    277 -- Result combinators
    278 -- ---------------------------------------------------------------------------
    279 
    280 mapResult = (f result :
    281   matchResult
    282     (code rest : err code rest)
    283     (value rest : ok (f value) rest)
    284     result)
    285 
    286 bindResult = (result f :
    287   matchResult
    288     (code rest : err code rest)
    289     (value rest : f value rest)
    290     result)
    291 
    292 resultOr = (default result :
    293   matchResult
    294     (_ _ : default)
    295     (value _ : value)
    296     result)
    297 
    298 resultMapErr = (f result :
    299   matchResult
    300     (code rest : err (f code) rest)
    301     (value rest : ok value rest)
    302     result)
    303 
    304 -- ---------------------------------------------------------------------------
    305 -- List
    306 -- ---------------------------------------------------------------------------
    307 
    308 matchList = a b : triage a _ b
    309 
    310 emptyList? = matchList true (_ _ : false)
    311 head xs@(nonEmptyListOf anyC) =@anyC matchList t (h _ : h) xs
    312 tail xs@(nonEmptyListOf anyC) =@(listOf anyC) matchList t (_ r : r) xs
    313 
    314 append_ self xs ys =
    315   matchList
    316     ys
    317     (h r : pair h (self r ys))
    318     xs
    319 append = xs ys : y append_ xs ys
    320 
    321 lExist?_ self x xs =
    322   matchList
    323     false
    324     (h r : or? (equal? x h) (self x r))
    325     xs
    326 lExist? = x xs : y lExist?_ x xs
    327 
    328 map_ self l f =
    329   matchList
    330     t
    331     (h r : pair (f h) (self r f))
    332     l
    333 map = f l : y map_ l f
    334 
    335 filter_ self l f =
    336   matchList
    337     t
    338     (h r :
    339       matchBool
    340         (pair h (self r f))
    341         (self r f)
    342         (f h))
    343     l
    344 filter = f l : y filter_ l f
    345 
    346 foldl_ self l f acc =
    347   matchList
    348     acc
    349     (h r : self r f (f acc h))
    350     l
    351 foldl = f x l : y foldl_ l f x
    352 
    353 foldr_ self l f x =
    354   matchList
    355     x
    356     (h r : f (self r f x) h)
    357     l
    358 foldr = f x l : y foldr_ l f x
    359 
    360 length_ self xs =
    361   matchList
    362     0
    363     (_ r : succ (self r))
    364     xs
    365 length @(listOf anyC) =@nat? y length_
    366 
    367 reverse_ self xs acc =
    368   matchList
    369     acc
    370     (h r : self r (pair h acc))
    371     xs
    372 reverse = xs : y reverse_ xs t
    373 
    374 snoc_ self x xs =
    375   matchList
    376     (pair x t)
    377     (h r : pair h (self x r))
    378     xs
    379 snoc = x xs : y snoc_ x xs
    380 
    381 count_ self x xs =
    382   matchList
    383     0
    384     (h r :
    385       matchBool
    386         (succ (self x r))
    387         (self x r)
    388         (equal? x h))
    389     xs
    390 count = x xs : y count_ x xs
    391 
    392 last_ self xs =
    393   matchList
    394     t
    395     (h r :
    396       matchBool
    397         h
    398         (self r)
    399         (emptyList? r))
    400     xs
    401 last @(nonEmptyListOf anyC) =@anyC y last_
    402 
    403 all?_ self pred xs =
    404   matchList
    405     true
    406     (h r : and? (pred h) (self pred r))
    407     xs
    408 all? = pred xs : y all?_ pred xs
    409 
    410 any?_ self pred xs =
    411   matchList
    412     false
    413     (h r : or? (pred h) (self pred r))
    414     xs
    415 any? = pred xs : y any?_ pred xs
    416 
    417 intersect = xs ys : filter (x : lExist? x ys) xs
    418 
    419 nth_ self xs n i =
    420   matchList
    421     t
    422     (h r :
    423       matchBool
    424         h
    425         (self r n (succ i))
    426         (equal? i n))
    427     xs
    428 nth = n xs : y nth_ xs n 0
    429 
    430 headMaybe = matchList nothing (h _ : just h)
    431 
    432 lastMaybe_ self xs =
    433   matchList
    434     nothing
    435     (h r :
    436       matchBool
    437         (just h)
    438         (self r)
    439         (emptyList? r))
    440     xs
    441 lastMaybe = xs : y lastMaybe_ xs
    442 
    443 nthMaybe_ self xs n i =
    444   matchList
    445     nothing
    446     (h r :
    447       matchBool
    448         (just h)
    449         (self r n (succ i))
    450         (equal? i n))
    451     xs
    452 nthMaybe = n xs : y nthMaybe_ xs n 0
    453 
    454 take_ self xs n i =
    455   matchList
    456     t
    457     (h r :
    458       matchBool
    459         t
    460         (pair h (self r n (succ i)))
    461         (equal? i n))
    462     xs
    463 take = n xs : y take_ xs n 0
    464 
    465 drop_ self xs n i =
    466   matchBool
    467     xs
    468     (matchList
    469       t
    470       (_ r : self r n (succ i))
    471       xs)
    472     (equal? i n)
    473 drop = n xs : y drop_ xs n 0
    474 
    475 splitAt = n xs : pair (take n xs) (drop n xs)
    476 
    477 concatMap_ self f xs =
    478   matchList
    479     t
    480     (h r : append (f h) (self f r))
    481     xs
    482 concatMap = f xs : y concatMap_ f xs
    483 
    484 find_ self pred xs =
    485   matchList
    486     nothing
    487     (h r :
    488       matchBool
    489         (just h)
    490         (self pred r)
    491         (pred h))
    492     xs
    493 find = pred xs : y find_ pred xs
    494 
    495 partition_ self pred xs trues falses =
    496   matchList
    497     (pair (reverse trues) (reverse falses))
    498     (h r :
    499       matchBool
    500         (self pred r (pair h trues) falses)
    501         (self pred r trues (pair h falses))
    502         (pred h))
    503     xs
    504 partition = pred xs : y partition_ pred xs t t
    505 
    506 strLength = length
    507 strAppend = append
    508 strEq? = equal?
    509 strEmpty? = emptyList?
    510 
    511 startsWith?_ self prefix input =
    512   matchList
    513     true
    514     (ph pr :
    515       matchList
    516         false
    517         (sh sr :
    518           matchBool
    519             (self pr sr)
    520             false
    521             (equal? ph sh))
    522         input)
    523     prefix
    524 startsWith? = prefix input : y startsWith?_ prefix input
    525 
    526 endsWith? = prefix str : startsWith? (reverse prefix) (reverse str)
    527 
    528 contains?_ self needle haystack =
    529   matchBool
    530     true
    531     (matchList
    532       false
    533       (_ r : self needle r)
    534       haystack)
    535     (startsWith? needle haystack)
    536 contains? = needle haystack : y contains?_ needle haystack
    537 
    538 sum @(listOf nat?) =@nat? foldl (acc x : add x acc) 0
    539 product @(listOf nat?) =@nat? foldl (acc x : mul x acc) 1
    540 
    541 -- ---------------------------------------------------------------------------
    542 -- Generic separators
    543 --
    544 -- `lines`, `unlines`, `words` and `unwords` at the bottom of this section are
    545 -- the byte-valued special cases of these primitives.
    546 --
    547 -- Joining takes any separator; splitting takes one byte. Separators are removed
    548 -- rather than kept, and empty fields are preserved.
    549 -- ---------------------------------------------------------------------------
    550 
    551 takeWhile_ self xs f =
    552   lazyList
    553     (_ : t)
    554     (h r :
    555       lazyBool
    556         (_ : pair h (self r f))
    557         (_ : t)
    558         (f h))
    559     xs
    560 takeWhile = f xs : y takeWhile_ xs f
    561 
    562 dropWhile_ self xs f =
    563   lazyList
    564     (_ : t)
    565     (h r :
    566       lazyBool
    567         (_ : self r f)
    568         (_ : pair h r)
    569         (f h))
    570     xs
    571 dropWhile = f xs : y dropWhile_ xs f
    572 
    573 -- Byte-level whitespace only: space and horizontal tab (HTTP OWS).
    574 spaceByte? = b : equal? b 32
    575 tabByte?   = b : equal? b 9
    576 trimByte?  = b : or? (spaceByte? b) (tabByte? b)
    577 
    578 trim = xs : dropWhile trimByte? (reverse (dropWhile trimByte? (reverse xs)))
    579 
    580 intercalate_ self xs sep =
    581   lazyList
    582     (_ : t)
    583     (h r :
    584       lazyBool
    585         (_ : h)
    586         (_ : append h (append sep (self r sep)))
    587         (emptyList? r))
    588     xs
    589 intercalate = sep xs : y intercalate_ xs sep
    590 
    591 -- Separator after every field, including the last one. Line-oriented formats
    592 -- want this: `joinSuffix "\n" xs` terminates the final line while
    593 -- `intercalate "\n" xs` does not.
    594 joinSuffix_ self xs sep =
    595   lazyList
    596     (_ : t)
    597     (h r : append (append h sep) (self r sep))
    598     xs
    599 joinSuffix = sep xs : y joinSuffix_ xs sep
    600 
    601 -- Split on a single byte. 
    602 -- Empty fields are preserved: `splitOnByte 58 "a::b"` is ["a" "" "b"].
    603 splitByte_ self str byte acc current =
    604   lazyList
    605     (_ : map reverse (reverse (pair current acc)))
    606     (h r :
    607       lazyBool
    608         (_ : self r byte (pair current acc) t)
    609         (_ : self r byte acc (pair h current))
    610         (equal? h byte))
    611     str
    612 splitOnByte = byte str : y splitByte_ str byte t t
    613 
    614 -- Every one of these keeps its arguments bound: partially applying a
    615 -- multi-argument function at the top level leaves a fixed point exposed.
    616 lines   = str : splitOnByte 10 str
    617 unlines = xs : joinSuffix "\n" xs
    618 
    619 -- Runs of separators collapse: empty fields are dropped.
    620 words   = str : filter (w : not? (emptyList? w)) (splitOnByte 32 str)
    621 unwords = xs : intercalate " " xs
    622 
    623 zipWith_ self f xs ys =
    624   matchList
    625     t
    626     (xh xt :
    627       matchList
    628         t
    629         (yh yt : pair (f xh yh) (self f xt yt))
    630         ys)
    631     xs
    632 zipWith = f xs ys : y zipWith_ f xs ys
    633 
    634 -- ---------------------------------------------------------------------------
    635 -- Core contract type
    636 --
    637 -- A contract is an ordinary tricu function: Tree -> Tree -> Result Tree Tree.
    638 -- The second argument is the conventional "rest" slot. On success a contract
    639 -- returns the checked value wrapped in the standard ok shape; on failure it
    640 -- returns a diagnostic wrapped in the standard err shape.
    641 --
    642 -- The contract kernel is a globally configurable function selected by the
    643 -- runner. It decides whether to accept the contract result, replace it, log
    644 -- it, or transform the diagnostic. The default kernel is the identity on the
    645 -- contract Result.
    646 --
    647 -- The runner may rebind 'kernel' to a different kernel before evaluating
    648 -- user code (e.g. via --contract-kernel).
    649 -- ---------------------------------------------------------------------------
    650 
    651 contractOk = (value : (rest : ok value rest))
    652 contractErr = (msg : (rest : err msg rest))
    653 
    654 -- Default contract kernel. Return the contract Result unchanged.
    655 defaultKernel = (contract value result :
    656   matchResult
    657     (msg rest : err msg rest)
    658     (v rest : ok v rest)
    659     result)
    660 
    661 -- The active kernel. The runner may rebind this name to a different kernel
    662 -- before evaluating user code (e.g. via --contract-kernel). Internally,
    663 -- withContract dispatches through this binding, so rebinding 'kernel' changes
    664 -- the behaviour of every contract boundary in the program.
    665 kernel = defaultKernel
    666 
    667 -- Skip-everything kernel. Resume with the original value on failure.
    668 skipKernel = (contract value result :
    669   matchResult
    670     (msg rest : ok value rest)
    671     (v rest : ok v rest)
    672     result)
    673 
    674 -- Apply a contract and pass the raw Result to the kernel.
    675 withContract = (contract value :
    676   kernel contract value (contract value t))
    677 
    678 -- Apply a contract and return the checked value or the diagnostic message.
    679 check contract value =
    680   matchResult
    681     (msg _ : msg)
    682     (v _ : v)
    683     (withContract contract value)
    684 
    685 -- Apply a contract and return the raw Result (kernel is bypassed).
    686 checkContract = (contract value : contract value t)
    687 
    688 -- ---------------------------------------------------------------------------
    689 -- Basic contracts
    690 -- ---------------------------------------------------------------------------
    691 
    692 -- Any value passes.
    693 anyC = (value : contractOk value)
    694 
    695 -- Always fails with the supplied message.
    696 neverC = (msg : (value : contractErr msg))
    697 
    698 -- Build a contract from a predicate that inspects only the value.
    699 guardC = (msg predicate value rest :
    700   lazyBool
    701     (_ : contractOk value rest)
    702     (_ : contractErr msg rest)
    703     (predicate value))
    704 
    705 -- Structural natural-number predicate.
    706 -- A natural is either Leaf (0) or Fork bit rest where bit is Leaf (even)
    707 -- or Stem Leaf (odd) and rest is itself a natural.
    708 isNat? = y (self n :
    709   triage
    710     true
    711     (_ : false)
    712     (bit r :
    713       triage
    714         (self r)
    715         (_ : self r)
    716         (_ _ : false)
    717         bit)
    718     n)
    719 
    720 -- Natural number contract.
    721 nat? = guardC "not a natural number" isNat?
    722 
    723 -- Non-zero natural number contract.
    724 nonZero? = guardC "non-zero" (n : and? (isNat? n) (not? (isZero_? n)))
    725 
    726 -- Boolean contract.
    727 bool? = guardC "not a boolean" (b : or? (equal? b true) (equal? b false))
    728 
    729 -- ---------------------------------------------------------------------------
    730 -- Contract combinators
    731 -- ---------------------------------------------------------------------------
    732 
    733 andC = (c1 c2 value rest :
    734   matchResult
    735     (msg _ : contractErr msg rest)
    736     (v _ : c2 v rest)
    737     (c1 value rest))
    738 
    739 orC = (c1 c2 value rest :
    740   matchResult
    741     (msg _ : c2 value rest)
    742     (v _ : contractOk v rest)
    743     (c1 value rest))
    744 
    745 notC = (c value rest :
    746   matchResult
    747     (msg _ : contractOk value rest)
    748     (_ _ : contractErr "notC: predicate succeeded" rest)
    749     (c value rest))
    750 
    751 mapC = (f c value rest :
    752   matchResult
    753     (msg _ : contractErr msg rest)
    754     (v _ : contractOk (f v) rest)
    755     (c value rest))
    756 
    757 bindC = (c f value rest :
    758   matchResult
    759     (msg _ : contractErr msg rest)
    760     (v _ : f v value rest)
    761     (c value rest))
    762 
    763 -- ---------------------------------------------------------------------------
    764 -- Collection contracts
    765 -- ---------------------------------------------------------------------------
    766 
    767 listOf = (c value rest :
    768   y (self orig xs :
    769     matchList
    770       (contractOk orig rest)
    771       (h r :
    772         matchResult
    773           (msg _ : contractErr msg rest)
    774           (_ _ : self orig r)
    775           (c h rest))
    776       xs) value value)
    777 
    778 nonEmptyListOf = (c :
    779   andC (guardC "empty list" (xs : not? (emptyList? xs))) (listOf c))
    780 
    781 pairOf = (c1 c2 p rest :
    782   matchPair
    783     (a b :
    784       matchResult
    785         (msg _ : contractErr msg rest)
    786         (a' _ :
    787           matchResult
    788             (msg _ : contractErr msg rest)
    789             (b' _ : contractOk (pair a' b') rest)
    790             (c2 b rest))
    791         (c1 a rest))
    792     p)
    793 
    794 -- ---------------------------------------------------------------------------
    795 -- Higher-order function contracts
    796 --
    797 -- These return a Result-wrapped proxy. The proxy itself is a contract: it
    798 -- checks arguments on the way in and results on the way out.
    799 -- ---------------------------------------------------------------------------
    800 
    801 fnContract = (argC resC f rest :
    802   contractOk
    803     (x : (rest1 :
    804       matchResult
    805         (msg _ : contractErr msg rest1)
    806         (x' _ :
    807           matchResult
    808             (msg _ : contractErr msg rest1)
    809             (y _ : contractOk y rest1)
    810             (withContract resC (f x')))
    811         (withContract argC x)))
    812     rest)
    813 
    814 fn2 = (arg1C arg2C resC f rest :
    815   contractOk
    816     (x : (rest1 :
    817       matchResult
    818         (msg _ : contractErr msg rest1)
    819         (x' _ :
    820           contractOk
    821             (y : (rest2 :
    822               matchResult
    823                 (msg _ : contractErr msg rest2)
    824                 (y' _ :
    825                   matchResult
    826                     (msg _ : contractErr msg rest2)
    827                     (z _ : contractOk z rest2)
    828                     (withContract resC (f x' y')))
    829                 (withContract arg2C y)))
    830             rest1)
    831         (withContract arg1C x)))
    832     rest)
    833 
    834 -- ---------------------------------------------------------------------------
    835 -- Interaction-tree effect layer
    836 --
    837 -- These constructors and combinators layer catchable, composable failures on
    838 -- top of the core Result contracts. They reuse the same tags as tricu IO:
    839 --   0 = pureE
    840 --   1 = bindE
    841 --   2 = exceptE
    842 -- ---------------------------------------------------------------------------
    843 
    844 pureE = (value : pair 0 value)
    845 bindE = (action k : pair 1 (pair action k))
    846 exceptE = (tag value k : pair 2 (pair tag (pair value k)))
    847 
    848 pureM = pureE
    849 bindM = bindE
    850 
    851 -- Lift a contract failure into an interaction tree.
    852 checkM = (contract value :
    853   matchResult
    854     (msg _ : exceptE "contract" msg (_ : pureE t))
    855     (checked _ : pureE checked)
    856     (contract value t))
    857 
    858 -- Lift a pure function into the interaction tree.
    859 liftM = (f : (x : pureE (f x)))
    860 
    861 -- Interpret a pure interaction tree into a Result.
    862 runM = (tree :
    863   run tree
    864   where run =
    865           y (self tree :
    866             matchPair
    867               (op payload :
    868                 matchBool
    869                   -- pureE
    870                   (contractOk (snd tree) t)
    871                   (matchBool
    872                     -- bindE
    873                     (matchPair
    874                       (action k :
    875                         matchResult
    876                           (msg _ : contractErr msg t)
    877                           (v _ : self (k v))
    878                           (self action))
    879                       payload)
    880                     -- exceptE
    881                     (matchPair
    882                       (tag pair :
    883                         matchPair
    884                           (value k :
    885                             contractErr value t)
    886                           pair)
    887                       payload)
    888                     (equal? op 1))
    889                   (equal? op 0))
    890               tree))
    891 
    892 -- Handle matching exceptE nodes by applying the handler to the value and the
    893 -- resumption continuation. Non-matching exceptions are left in place.
    894 handleM = (tag handler tree :
    895   handle tree
    896   where handle =
    897           y (self tree :
    898             matchPair
    899               (op payload :
    900                 matchBool
    901                   -- pureE
    902                   tree
    903                   (matchBool
    904                     -- bindE
    905                     (matchPair
    906                       (action k :
    907                         bindE (self action) (v : self (k v)))
    908                       payload)
    909                     -- exceptE
    910                     (matchPair
    911                       (et pair :
    912                         matchPair
    913                           (value k :
    914                             matchBool
    915                               (self (handler value k))
    916                               tree
    917                               (equal? et tag))
    918                           pair)
    919                       payload)
    920                     (equal? op 1))
    921                   (equal? op 0))
    922               tree))