a64b3f0829
tricu now allows defining terms in any order and will resolve dependencies to ensure that they're evaluated in the right order. Undefined terms are detected and throw errors during dependency ordering. For now we can't define top-level mutually recursive terms.
84 lines
1.7 KiB
Plaintext
84 lines
1.7 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)
|
|
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))
|
|
|
|
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)
|
|
|
|
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
|