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 (a b : a) p
snd = p : matchPair (a b : b) p

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)

-- ---------------------------------------------------------------------------
-- Basic arithmetic
-- ---------------------------------------------------------------------------

pred = y (self : triage
  0
  (_ : 0)
  (bit rest :
    matchBool
      (matchBool
        0
        (pair 0 rest)
        (equal? rest 0))
      (matchBool
        0
        (pair 1 (self rest))
        (equal? rest 0))
      bit))

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 :
  matchBool
    a
    (self (pred a) (pred b))
    (isZero? b))

lt? = a b : not? (isZero? (sub b a))
lte? = a b : isZero? (sub a b)

mul = y (self a b :
  matchBool
    0
    (add a (self a (pred b)))
    (isZero? 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)