-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathLambdaCore.lam
126 lines (96 loc) · 4.3 KB
/
LambdaCore.lam
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
module LambdaCore
import Lambda
import LamTranslator
import LamParsec
--booleans
tr = La.Lb.a;
fl = La.Lb.b;
--
iF = Lp.La.Lb.p a b;
oR = Lp.Lq.p p q;
anD = Lp.Lq.p q p;
noT = Lm.La.Lb.m b a;
--lisp functions car is head cdr is tail
cons = #pr;
car = Lp.p #tr;
cdr = Lp.p #fl;
nil = Lx.#tr;
nul = Lp.p (Lx.Ly.#fl);
appnd = #y (Lg.La.Lb.#nul a b (#pr (#car a) (g (#cdr a) b)));
len = #y (Lg.Lc.Lx.#nul x c (g (#sucs c) (#cdr x))) #zero;
idx = Lx.Li. #car (i #cdr x);
last = #y (Lg.Lx.#nul x #nil (#nul (#cdr x) (#car x) (g (#cdr x))));
rvrs = #y (Lg.La.Ll.#nul l a (g (#pr (#car l) a) (#cdr l))) #nil;
fold = Lf.Le.Lx.#y (Lg.Ly.#nul y e (f (#car y) (g (#cdr y)))) x;
ins = #y (Lf.La.Las.#iF (#oR (#nul as) (#lte a (#car as))) (#pr a as) (#pr (#car as) (f a (#cdr as))));
insort = #y (Lf.Las.Lbs.(#nul as) bs (f (#cdr as) (#ins (#car as) bs)));
insert = Ll.#fold #ins #nil l;
--pair functions pr is also cons for pairList
pr = Lx.Ly.Lp.p x y;
frst = Lp.p #tr;
scnd = Lp.p #fl;
--Y combinator
y = Lg.(Lx.g (x x)) (Lx.g (x x));
--some church numerals
zero = Lf.Lx.x;
one = Lf.Lx.f x;
two = Lf.Lx.f (f x);
three = Lf.Lx.f (f (f x));
four = Lf.Lx.f (f (f (f x)));
five = Lf.Lx.f (f (f (f (f x))));
--church numeral operations
sucs = Ln.Lf.Lx.f (n f x);
prdc = Ln.Lf.Lx.n (Lg.Lh.h (g f)) (Lu.x) (Lu.u);
isZr = Ln.n (Lx.#fl) #tr;
subt = Lm.Ln.n #prdc m;
plus = Lm.Ln.Lf.Lx.m f (n f x);
mult = Lm.Ln.Lf.m (n f);
exp = Lm.Ln.n m;
lte = Lm.Ln.#isZr (#subt m n);
eq = Lm.Ln.#anD (#lte m n) (#lte n m);
gt = Lm.Ln.#noT (#lte m n);
lt = Lm.Ln.#anD (#lte m n) (#noT (#eq m n));
--casE matches a pattern to a list of pattern value pairs and returns a value
cas = Li.Lcs.#y #cs i cs;
cs = Lf.Li.Lp.(#eq (#frst (#car p)) i) (#scnd (#car p)) (f i (#cdr p));
casE = #y (Lf.Li.Lps.(#eq (#frst (#car ps)) i) (#scnd (#car ps)) (f i (#cdr ps)));
--set functions
--union unions two already sorted lists outputs a sorted list
sss = Lxs.Lys.(Lx.Ly.(Lx.Ly.#lt x y) x y (#one) ((Lx.Ly.#eq x y) x y (#two) (#three))) (#car xs) (#car ys);
unHd = #y (Lf.Lxs.Lys.Lac.(Lx.Ly.(#nul xs) (#insort ys ac) ((#nul ys) (#insort xs ac) ((Lx.Ly.#lt x y) x y (f (#cdr xs) ys (#ins x ac)) ((Lx.Ly.#eq x y) x y (f (#cdr xs) (#cdr ys) (#ins x ac)) (f xs (#cdr ys) (#ins y ac)))))) (#car xs) (#car ys));
union = Lxs.Lys.#unHd xs ys #nil;
--set difference
dfHd = #y (Lf.Lxs.Lys.Lac.(Lx.Ly.(#nul xs) ac ((#nul ys) xs ((Lx.Ly.#lt x y) x y (f (#cdr xs) ys (#ins x ac)) ((Lx.Ly.#eq x y) x y (f (#cdr xs) (#cdr ys) ac) (f xs (#cdr ys) ac))))) (#car xs) (#car ys));
diff = Lxs.Lys.#dfHd xs ys #nil;
--Core
subb = #y (Lf.Lm.Lx.Lval.#casE (#frst val) #cases);
cases = #cons (#pr #three #varC) (#cons (#pr #two #appC) (#cons (#pr #one #lamC) #nil));
varC = #eq (#scnd x) (#scnd val) m val;
appC = #pr #two (#pr (f m x (#frst (#scnd val))) (f m x (#scnd (#scnd val))));
lamC = #eq (#scnd x) (#frst (#scnd val)) val (#pr #one (#pr (#frst (#scnd val)) (f m x (#scnd (#scnd val)))));
cbV = #y (Lf.Lexp.#casE (#frst exp) #patterns);
patterns = #cons (#pr #three #varCbv) (#cons (#pr #two #appCbv) (#cons (#pr #one #lamCbv) #nil));
varCbv = exp;
lamCbv = exp;
appCbv = (Lei.(#eq (#frst ei) #one) #lamCase #owCase) (#cbV (#frst (#scnd exp)));
lamCase = (Leii.#cbV (#subb eii (#pr #three (#frst (#scnd ei))) (#scnd (#scnd ei)))) (#cbV (#scnd (#scnd exp)));
owCase = (Leii.#pr #two (#pr ei eii)) (#cbV (#scnd (#scnd exp)));
--test stuff
ptrn = #pr #zero #tr;
ptrni = #pr #one #fl;
test = #casE #zero #tst;
tst = #cons #ptrn (#cons #ptrni #nil);
lista = #cons #one (#cons #two #nil);
listb = #cons #two (#cons #three #nil);
listc = #cons #two (#cons #three #nil);
duplist = #cons #zero (#cons #zero (#cons #one (#cons #one #nil)));
list = #pr #five (#pr #three (#pr #four (#pr #two (#pr #one (#pr #zero (#pr #three (#pr #four (#pr #one (#pr #five (#pr #zero (#pr #two #nil)))))))))));
lis = #cons #three (#cons #two #nil);
ppen = Las.Lb.Lscs.#appnd as (#appnd (#pr b #nil) scs);
sing = #pr #one #nil;
tet = #pr #one (#pr #two (#pr #three (#pr five (#pr #four #nil))));
tat = #pr #four (#pr #three (#pr #two (#pr #one #nil)));
tot = #pr #zero (#pr #one (#pr #three (#pr #four #nil)));
mann = #insort #mane #mane;
mane = #insort #list (#insort #list #nil);
man = #insert #lis;