Some special characters in ids; new demos
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.
This commit is contained in:
107
lib/base.tri
107
lib/base.tri
@ -1,22 +1,25 @@
|
||||
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)
|
||||
_ = 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)
|
||||
pair = t
|
||||
test = triage "Leaf" (\_ : "Stem") (\_ _ : "Fork")
|
||||
|
||||
matchBool = (\ot of : triage
|
||||
of
|
||||
@ -36,58 +39,58 @@ matchPair = (\op : triage
|
||||
op
|
||||
)
|
||||
|
||||
not = matchBool false true
|
||||
and = matchBool id (\z : false)
|
||||
if = (\cond then else : t (t else (t t then)) t cond)
|
||||
test = triage "Leaf" (\z : "Stem") (\a b : "Fork")
|
||||
not? = matchBool false true
|
||||
and? = matchBool id (\_ : false)
|
||||
emptyList? = matchList true (\_ _ : false)
|
||||
|
||||
emptyList = matchList true (\y z : false)
|
||||
head = matchList t (\hd tl : hd)
|
||||
tail = matchList t (\hd tl : tl)
|
||||
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
|
||||
(\x : false)
|
||||
(\_ x : x)
|
||||
(\_ : false)
|
||||
(\_ x : x)
|
||||
(\_ _ x : x)
|
||||
)
|
||||
|
||||
lOr = (triage
|
||||
(\x : x)
|
||||
(\_ _ : true)
|
||||
(\_ _ x : true)
|
||||
(\x : x)
|
||||
(\_ _ : true)
|
||||
(\_ _ _ : true)
|
||||
)
|
||||
|
||||
hmap = y (\self :
|
||||
map_ = y (\self :
|
||||
matchList
|
||||
(\f : t)
|
||||
(\hd tl f : pair
|
||||
(f hd)
|
||||
(self tl f)))
|
||||
map = (\f l : hmap l f)
|
||||
(\_ : t)
|
||||
(\head tail f : pair (f head) (self tail f)))
|
||||
map = (\f l : map_ l f)
|
||||
|
||||
equal = y (\self : triage
|
||||
equal? = y (\self : triage
|
||||
(triage
|
||||
true
|
||||
(\z : false)
|
||||
(\y z : false))
|
||||
(\ax : triage
|
||||
false
|
||||
(self ax)
|
||||
(\y z : false))
|
||||
(\ax ay : triage
|
||||
false
|
||||
(\z : false)
|
||||
(\bx by : lAnd (self ax bx) (self ay by))))
|
||||
(\_ : false)
|
||||
(\_ _ : false))
|
||||
(\ax :
|
||||
triage
|
||||
false
|
||||
(self ax)
|
||||
(\_ _ : false))
|
||||
(\ax ay :
|
||||
triage
|
||||
false
|
||||
(\_ : false)
|
||||
(\bx by : lAnd (self ax bx) (self ay by))))
|
||||
|
||||
hfilter = y (\self : matchList (\f : t) (\hd tl f : matchBool (t hd) i (f hd) (self tl f)))
|
||||
filter = (\f l : hfilter l f)
|
||||
filter_ = y (\self : matchList
|
||||
(\_ : t)
|
||||
(\head tail f : matchBool (t head) i (f head) (self tail f)))
|
||||
filter = (\f l : filter_ l f)
|
||||
|
||||
hfoldl = y (\self f l x : matchList (\acc : acc) (\hd tl acc : self f tl (f acc hd)) l x)
|
||||
foldl = (\f x l : hfoldl f l x)
|
||||
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)
|
||||
|
||||
hfoldr = y (\self x f l : matchList x (\hd tl : f (self x f tl) hd) l)
|
||||
foldr = (\f x l : hfoldr x f l)
|
||||
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)
|
||||
|
Reference in New Issue
Block a user