Adds support for several special characters in identifiers. Adds a demo for converting values to source code and another for checking equality. Updates the existing demo and tests to reflect new names for functions returning booleans.
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 = (\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)
|