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 (err rest : false) (val rest : true) result

resultIsErr result =
  matchResult (err 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)))

-- This module has no list matcher, so `triage` is used directly: a cons is a
-- Fork, which is why the cons case sits in the fork slot, exactly as in
-- `matchList` in lib/list.tri.
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))))

isZero? = triage true (_ : false) (_ _ : false)

add = y (self x y :
  triage
    y
    (_ : succ y)
    (_ _ : succ (self (pred x) y))
    x)

sub = 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))))

gte? = a b :
  lte? b a

lt? = a b :
  and? (lte? a b) (not? (equal? a b))

gt? = a b :
  lt? b a

mul = y (self a b :
  ifLazy
    (isZero? b)
    (_ : 0)
    (_ : add a (self a (pred b))))

div = y (self a b :
  ifLazy
    (isZero? b)
    (_ : 0)
    (_ : ifLazy
      (lt? a b)
      (_ : 0)
      (_ : succ (self (sub a b) b))))

mod = y (self a b :
  ifLazy
    (isZero? b)
    (_ : 0)
    (_ : ifLazy
      (lt? a b)
      (_ : a)
      (_ : self (sub a b) b)))

-- ---------------------------------------------------------------------------
-- 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)