tricu/lib/base.tri

false = t
_     = t
true  = t t
k     = t t
i     = t (t k) t
s     = t (t (k t)) t
m     = s i i
b     = s (k s) k
c     = s (s (k s) (s (k k) s)) (k k)
iC    = (\a b c : s a (k c) b)
iD    = b (b iC) iC
iE    = b (b iD) iC
yi    = (\i : b m (c b (i m)))
y     = yi iC
yC    = yi iD
yD    = yi iE
id    = (\a : a)
pair  = t
if    = (\cond then else : t (t else (t t then)) t cond)

triage = (\a b c : t (t a b) c)
test   = triage "Leaf" (\_ : "Stem") (\_ _ : "Fork")

matchBool = (\ot of : triage 
  of 
  (\_ : ot) 
  (\_ _ : ot)
)

matchList = (\oe oc : triage 
  oe 
  _ 
  oc
)

matchPair = (\op : triage 
  _ 
  _ 
  op
)

not? = matchBool false true
and? = matchBool id (\_ : false)
emptyList? = matchList true (\_ _ : false)

head = matchList t (\head _ : head)
tail = matchList t (\_ tail : tail)

lconcat = y (\self : matchList 
  (\k : k) 
  (\h r k : pair h (self r k)))

lAnd = (triage 
  (\_     : false) 
  (\_ x   : x) 
  (\_ _ x : x)
)

lOr = (triage 
  (\x     : x) 
  (\_ _   : true) 
  (\_ _ _ : true)
)

map_ = y (\self : 
  matchList 
    (\_ : t) 
    (\head tail f : pair (f head) (self tail f)))
map = (\f l : map_ l f)

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

filter_ = y (\self : matchList 
  (\_ : t) 
  (\head tail f : matchBool (t head) i (f head) (self tail f)))
filter  = (\f l : filter_ l f)

foldl_ = y (\self f l x : matchList (\acc : acc) (\head tail acc : self f tail (f acc head)) l x)
foldl  = (\f x l : foldl_ f l x)

foldr_ = y (\self x f l : matchList x (\head tail : f (self x f tail) head) l)
foldr  = (\f x l : foldr_ x f l)