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)
id    = \a : 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)
)

matchList = \a b : triage a _ b

matchPair = \a   : triage _ _ a

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

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

or? = (\x y : 
	matchBool 
  	(matchBool (t t) (t t) y)
  	(matchBool (t t) 0 y)
  	x)
xor? = matchBool id not?

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

lExist? = y (\self x : matchList
  false
  (\h z : or? (equal? x h) (self x z)))

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

succ = y (\self :
  triage
    1
    t
    (triage
      (t (t t))
      (\_ tail : t t (self tail))
      t))

length = y (\self : matchList
  0
  (\_ tail : succ (self tail)))

reverse = y (\self : matchList
  t
  (\head tail : append (self tail) (pair head t)))

snoc = y (\self x : matchList
  (pair x t)
  (\h z : pair h (self x z)))

count = y (\self x : matchList
  0
  (\h z : matchBool 
    (succ (self x z))
    (self x z)
    (equal? x h)))

last = y (\self : matchList
  t
  (\hd tl : matchBool
    hd
    (self tl)
    (emptyList? tl)))

all? = y (\self pred : matchList
  true
  (\h z : and? (pred h) (self pred z)))

any? = y (\self pred : matchList
  false
  (\h z : or? (pred h) (self pred z)))

unique_ = y (\self seen : matchList
  t
  (\head rest : matchBool
    (self seen rest)
    (pair head (self (pair head seen) rest))
    (lExist? head seen)))
unique = \xs : unique_ t xs

intersect = \xs ys : filter (\x : lExist? x ys) xs
union     = \xs ys : unique (append xs ys)