97 lines
1.8 KiB
Plaintext
97 lines
1.8 KiB
Plaintext
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 = (\leaf stem fork : t (t leaf stem) fork)
|
|
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)
|