forked from sorear/metamath-turing-machines
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathlam_loader.nql
240 lines (222 loc) · 16.8 KB
/
lam_loader.nql
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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
/*
Haskell code:
data Term = Lam Term | App Term Term | Var Int
type Env = [Value]
data Value = Closure Env Term | Reflect
eval :: Term -> Env -> Value
eval e (Lam x) = Closure e x
eval e (App f x) = vapp (eval e f) (eval e x)
eval e (Var n) = e !! n
vapp :: Value -> Value -> Value
vapp Reflect !_ = Reflect
vapp (Closure e t) v = eval (v:e) t
quote :: Value -> ()
quote Reflect = ()
quote (Closure e t) = eval (Reflect:e) t
Data representations:
Lam t = (0,t)
App f x = (1,(f,x))
Var n = (2,n)
[] :: Env = 0
(x:xs) :: Env = (x,xs) (overlaps [] but that's fine)
Reflect = 0
Closure e t = (e,t)+1
Program stack entries (input lstacktop->output lstacktop):
0 = x -> quote x (and exit if x==0==Reflect)
(0,e)+1 = t -> eval e t
(1,(e,x))+1 = f -> vapp f (eval e x)
(2,(e,t))+1 = x -> vapp (Closure e t) x
(3,_)+1 = x -> Reflect
Reductions (lstacktop # rstacktop rstack...):
Reflect # 0 -> halt
(Closure e t) # 0 -> Reflect # (2,(e,t))+1 (-> t # (0,(0,e))+1)
(Lam t) # (0,e)+1 -> (Closure e t) #
(App f x) # (0,e)+1 -> f # (0,e)+1 (1,(e,x))+1
(Var n) # (0,e)+1 -> e!!n #
Reflect # (1,(e,x))+1 -> x # (0,e)+1 (3,_)+1
(Closure e t) # (1,(e',x))+1 -> x # (0,e')+1 (2,(e,t))+1
x # (2,(e,t))+1 -> t # (0,(x,e))+1
x # (3,_)+1 -> Reflect #
*/
/* Cantor pair manipulation proctions */
/* zeros in1, in2 */
proc pair(out, in1, in2) {
builtin_pair(out, in1, in2);
}
proc pair_inc(out, in1, in2) {
builtin_pair(out, in1, in2);
out = out + 1;
}
/* zeros in */
proc unpair(out1, out2, in) {
builtin_unpair(out1, out2, in);
}
proc unpair_dec(out1, out2, in) {
in = in - 1;
unpair(out1, out2, in);
}
global lstacktop;
global rstack;
global rstacktop;
global t2;
global t3;
/* Stack manipulation */
proc rstack_push() {
pair(rstack, rstack, rstacktop);
}
proc rstack_pop() {
unpair(rstack, rstacktop, rstack);
}
/* Constructors for Term */
proc push_lam() {
t2 = 0;
pair(rstacktop, t2, rstacktop);
}
/* rstack=((...,x),f)->(...,App f x) */
proc push_app() {
t2 = rstacktop;
rstack_pop();
pair(rstacktop, t2, rstacktop);
t2 = t2 + 1;
pair(rstacktop, t2, rstacktop);
}
proc push_var(v) {
rstack_push();
rstacktop = 2;
pair(rstacktop, rstacktop, v);
}
/* e !! n, all operands distinct */
proc index_list(e, n, out) {
/* decz n = (n-- == 0) */
while(!decz n){
unpair(out, e, e);
}
unpair(out, e, e);
}
/* t2 is 0 after this only at the beginning or the end */
proc stackszero() {
t2 = 0;
if(lstacktop > 0){
t2 = t2 + 1;
}
if(rstacktop > 0){
t2 = t2 + 1;
}
}
proc main() {
/* first iteration? */
stackszero();
if(t2 == 0){
/* push the program */
push_var(t2); push_var(t2); push_app(); push_var(t2); push_var(t2); push_var(t2); t2 = t2 + 6; push_var(t2); t2 = t2 + 1; push_var(t2); push_lam(); push_app(); t2 = t2 + 10; push_var(t2); t2 = t2 + 2; push_var(t2); push_app(); push_app(); push_lam(); push_app(); push_lam(); push_lam(); push_lam(); push_lam(); push_app(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); t2 = t2 + 1; push_var(t2); t2 = t2 + 2; push_var(t2); t2 = t2 + 7; push_var(t2); t2 = t2 + 3; push_var(t2); push_app(); t2 = t2 + 2; push_var(t2); push_app(); t2 = t2 + 1; push_var(t2); push_var(t2); push_app(); push_app(); push_lam(); push_lam(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); push_app(); push_var(t2); push_lam(); push_app(); push_lam(); push_app(); push_var(t2); push_app(); push_var(t2); push_var(t2); push_var(t2); push_lam(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); t2 = t2 + 1; push_var(t2); push_lam(); push_lam(); push_app(); push_lam(); push_lam(); push_lam(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); push_var(t2); push_lam(); push_lam(); push_app(); push_lam(); push_lam(); push_lam(); push_lam(); push_app(); push_lam(); push_app(); push_var(t2); push_lam(); push_lam(); push_app(); push_lam(); push_app(); push_lam(); push_app(); push_var(t2); push_lam(); push_lam(); push_app(); push_app(); t2 = t2 + 1; push_var(t2); push_app(); push_lam(); push_var(t2); push_var(t2); push_app(); push_lam(); push_var(t2); t2 = t2 + 5; push_var(t2); t2 = t2 + 2; push_var(t2); push_app(); t2 = t2 + 4; push_var(t2); t2 = t2 + 4; push_var(t2); push_app(); t2 = t2 + 1; push_var(t2); push_app(); push_var(t2); push_app(); push_app(); push_lam(); push_lam(); push_lam(); push_app(); push_lam(); push_lam(); push_app(); push_lam(); push_app(); push_lam(); push_lam(); t2 = t2 + 1; push_var(t2); t2 = t2 + 3; push_var(t2); t2 = t2 + 11; push_var(t2); t2 = t2 + 8; push_var(t2); push_app(); t2 = t2 + 5; push_var(t2); push_app(); t2 = t2 + 2; push_var(t2); push_app(); t2 = t2 + 1; push_var(t2); push_var(t2); t2 = t2 + 2; push_var(t2); push_app(); t2 = t2 + 1; push_var(t2); push_app(); push_lam(); push_lam(); push_lam(); push_var(t2); push_var(t2); t2 = t2 + 4; push_var(t2); push_app(); t2 = t2 + 6; push_var(t2); push_app(); push_lam(); push_app(); t2 = t2 + 8; push_var(t2); push_var(t2); push_var(t2); push_lam(); push_lam(); push_app(); push_app(); push_lam(); push_app(); t2 = t2 + 7; push_var(t2); push_var(t2); push_var(t2); push_lam(); push_lam(); push_app(); push_app(); push_lam(); push_app(); push_lam(); push_app(); push_app(); push_var(t2); push_lam(); push_app(); t2 = t2 + 12; push_var(t2); t2 = t2 + 6; push_var(t2); push_app(); t2 = t2 + 1; push_var(t2); t2 = t2 + 13; push_var(t2); t2 = t2 + 2; push_var(t2); push_lam(); push_app(); t2 = t2 + 6; push_var(t2); push_app(); push_var(t2); t2 = t2 + 2; push_var(t2); push_app(); t2 = t2 + 1; push_var(t2); push_app(); push_lam(); push_lam(); push_lam(); push_var(t2); t2 = t2 + 10; push_var(t2); push_app(); t2 = t2 + 1; push_var(t2); t2 = t2 + 12; push_var(t2); push_app(); t2 = t2 + 8; push_var(t2); push_app(); push_app(); t2 = t2 + 1; push_var(t2); t2 = t2 + 11; push_var(t2); push_app(); t2 = t2 + 8; push_var(t2); push_app(); push_app(); push_lam(); push_lam(); t2 = t2 + 2; push_var(t2); push_var(t2); push_app(); t2 = t2 + 2; push_var(t2); t2 = t2 + 1; push_var(t2); push_lam(); push_app(); push_lam(); push_lam(); push_lam(); push_app(); push_var(t2); push_lam(); push_lam(); push_app(); push_var(t2); push_lam(); push_lam(); push_app(); t2 = t2 + 2; push_var(t2); push_var(t2); push_lam(); push_lam(); push_app(); t2 = t2 + 6; push_var(t2); t2 = t2 + 4; push_var(t2); push_app(); push_app(); t2 = t2 + 3; push_var(t2); push_app(); push_lam(); push_lam(); push_lam(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); push_var(t2); push_app(); push_app(); push_lam(); push_lam(); push_lam(); push_app(); push_app(); push_lam(); push_app(); push_lam(); push_app(); push_lam(); push_lam(); push_app(); push_var(t2); push_lam(); push_lam(); push_app(); push_var(t2); push_lam(); push_lam(); push_app(); t2 = t2 + 4; push_var(t2); push_var(t2); t2 = t2 + 2; push_var(t2); push_app(); t2 = t2 + 1; push_var(t2); push_app(); push_lam(); push_lam(); push_lam(); push_var(t2); t2 = t2 + 2; push_var(t2); push_app(); t2 = t2 + 5; push_var(t2); push_var(t2); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); t2 = t2 + 1; push_var(t2); push_lam(); push_lam(); push_app(); t2 = t2 + 3; push_var(t2); push_app(); push_app(); t2 = t2 + 7; push_var(t2); push_app(); push_app(); t2 = t2 + 1; push_var(t2); t2 = t2 + 5; push_var(t2); push_app(); t2 = t2 + 3; push_var(t2); push_app(); t2 = t2 + 6; push_var(t2); push_app(); push_app(); push_lam(); push_lam(); t2 = t2 + 2; push_var(t2); t2 = t2 + 1; push_var(t2); t2 = t2 + 8; push_var(t2); push_app(); push_lam(); push_lam(); push_app(); t2 = t2 + 5; push_var(t2); t2 = t2 + 3; push_var(t2); push_app(); push_app(); t2 = t2 + 5; push_var(t2); push_var(t2); t2 = t2 + 1; push_var(t2); push_app(); t2 = t2 + 5; push_var(t2); push_app(); push_lam(); push_app(); push_lam(); push_app(); push_lam(); push_lam(); push_lam(); push_lam(); push_lam(); push_lam(); push_lam(); push_app(); push_app(); push_lam(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); push_var(t2); push_var(t2); push_var(t2); t2 = t2 + 5; push_var(t2); push_app(); t2 = t2 + 7; push_var(t2); push_app(); push_lam(); push_app(); t2 = t2 + 5; push_var(t2); push_var(t2); push_var(t2); push_lam(); push_lam(); push_app(); push_app(); push_lam(); push_app(); push_var(t2); t2 = t2 + 1; push_var(t2); push_lam(); push_lam(); push_app(); push_lam(); push_app(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); push_app(); push_lam(); push_app(); push_var(t2); push_app(); push_app(); push_app(); push_app(); push_lam(); push_lam(); t2 = t2 + 10; push_var(t2); t2 = t2 + 1; push_var(t2); push_app(); push_var(t2); push_lam(); push_lam(); push_lam(); push_lam(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); push_lam(); push_lam(); push_lam(); push_app(); push_var(t2); push_lam(); push_lam(); push_lam(); push_app(); push_app(); push_app(); push_var(t2); push_lam(); push_app(); push_lam(); push_lam(); push_lam(); push_app(); push_lam(); push_lam(); push_lam(); push_app(); push_lam(); push_lam(); push_app(); push_lam(); t2 = t2 + 4; push_var(t2); t2 = t2 + 1; push_var(t2); push_var(t2); push_app(); push_var(t2); t2 = t2 + 1; push_var(t2); push_app(); t2 = t2 + 1; push_var(t2); push_lam(); push_lam(); push_app(); push_app(); push_lam(); push_lam(); push_app(); t2 = t2 + 2; push_var(t2); t2 = t2 + 1; push_var(t2); push_app(); push_app(); t2 = t2 + 2; push_var(t2); push_var(t2); push_app(); push_app(); push_lam(); push_lam(); push_app(); push_lam(); push_var(t2); push_var(t2); push_app(); push_lam(); t2 = t2 + 3; push_var(t2); t2 = t2 + 4; push_var(t2); t2 = t2 + 8; push_var(t2); t2 = t2 + 7; push_var(t2); push_app(); t2 = t2 + 1; push_var(t2); push_app(); t2 = t2 + 2; push_var(t2); t2 = t2 + 5; push_var(t2); push_var(t2); t2 = t2 + 1; push_var(t2); push_app(); t2 = t2 + 10; push_var(t2); t2 = t2 + 1; push_var(t2); t2 = t2 + 11; push_var(t2); t2 = t2 + 1; push_var(t2); push_app(); push_var(t2); push_app(); push_app(); push_lam(); push_lam(); push_app(); t2 = t2 + 2; push_var(t2); push_var(t2); t2 = t2 + 12; push_var(t2); push_var(t2); push_var(t2); push_lam(); push_lam(); push_app(); push_lam(); push_app(); push_app(); push_lam(); push_lam(); push_lam(); push_app(); push_app(); t2 = t2 + 7; push_var(t2); push_app(); push_app(); push_lam(); push_app(); push_lam(); push_app(); t2 = t2 + 3; push_var(t2); t2 = t2 + 8; push_var(t2); t2 = t2 + 7; push_var(t2); push_app(); push_var(t2); push_app(); t2 = t2 + 5; push_var(t2); push_app(); push_app(); push_app(); push_app(); push_app(); push_lam(); push_lam(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); t2 = t2 + 2; push_var(t2); push_var(t2); t2 = t2 + 1; push_var(t2); push_app(); t2 = t2 + 4; push_var(t2); push_app(); push_lam(); push_app(); push_app(); push_lam(); push_app(); push_var(t2); t2 = t2 + 5; push_var(t2); t2 = t2 + 1; push_var(t2); push_app(); t2 = t2 + 1; push_var(t2); t2 = t2 + 2; push_var(t2); t2 = t2 + 3; push_var(t2); push_app(); push_app(); push_app(); push_app(); push_lam(); push_app(); push_lam(); push_var(t2); push_var(t2); push_lam(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); push_app(); push_lam(); push_lam(); push_app(); push_lam(); push_var(t2); t2 = t2 + 1; push_var(t2); push_lam(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); push_app(); push_lam(); push_lam(); push_app(); push_lam(); push_lam(); push_lam(); push_lam(); push_var(t2); push_var(t2); push_app(); push_app(); push_lam(); push_app(); push_var(t2); push_lam(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); push_var(t2); push_app(); push_app(); push_var(t2); push_lam(); push_lam(); push_app(); push_lam(); push_app(); push_lam(); push_var(t2); push_var(t2); push_var(t2); push_app(); push_lam(); push_var(t2); push_var(t2); t2 = t2 + 4; push_var(t2); push_app(); push_lam(); push_lam(); push_lam(); push_app(); t2 = t2 + 3; push_var(t2); t2 = t2 + 3; push_var(t2); push_app(); t2 = t2 + 1; push_var(t2); push_app(); push_app(); push_lam(); push_lam(); t2 = t2 + 1; push_var(t2); push_var(t2); push_var(t2); push_lam(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); push_app(); push_lam(); push_app(); push_lam(); push_app(); push_lam(); push_lam(); push_app(); push_var(t2); push_lam(); push_app(); push_app(); push_lam(); push_app(); push_lam(); push_var(t2); push_var(t2); push_app(); push_lam(); t2 = t2 + 1; push_var(t2); t2 = t2 + 3; push_var(t2); t2 = t2 + 10; push_var(t2); t2 = t2 + 5; push_var(t2); push_app(); t2 = t2 + 2; push_var(t2); push_app(); t2 = t2 + 8; push_var(t2); t2 = t2 + 4; push_var(t2); push_app(); t2 = t2 + 1; push_var(t2); push_app(); push_app(); push_var(t2); push_lam(); push_lam(); push_app(); push_lam(); push_lam(); push_lam(); push_app(); t2 = t2 + 3; push_var(t2); push_app(); push_lam(); push_lam(); push_lam(); push_app(); push_var(t2); t2 = t2 + 4; push_var(t2); push_lam(); push_lam(); push_lam(); push_app(); t2 = t2 + 1; push_var(t2); push_lam(); push_lam(); push_app(); push_app(); push_lam(); push_lam(); push_lam(); push_var(t2); push_var(t2); push_app(); push_app(); push_lam(); push_app(); push_lam(); push_app(); push_app(); push_var(t2); push_app(); push_lam(); t2 = t2 + 1; push_var(t2); t2 = t2 + 1; push_var(t2); t2 = t2 + 1; push_var(t2); push_var(t2); push_app(); push_app(); push_app(); push_lam(); push_lam(); push_app();
builtin_move(lstacktop, rstacktop);
/* 1 = (0,0)+1 = eval [] */
rstacktop = rstacktop + 1;
}
/* apply a reduction */
if(decz rstacktop){
/* 0 = quote */
if(!decz lstacktop){
/* (Closure e t) # 0 -> Reflect # (2,(e,t))+1 */
/* lstacktop = (e,t) */
t2 = 2;
pair_inc(rstacktop, t2, lstacktop);
/* lstacktop = 0 */
}
/* Reflect # 0 -> halt is handled elsewhere */
}else{
unpair(t2, rstacktop, rstacktop);
switch(t2){
case 0:
/* 0 = eval */
unpair(t2, lstacktop, lstacktop);
switch(t2){
case 0:
/* (Lam t) # (0,e)+1 -> (Closure e t) # */
/* lstacktop = t, rstacktop = e */
pair_inc(lstacktop, rstacktop, lstacktop);
/* lstacktop = (e,t)+1 = (Closure e t) */
rstack_pop();
break;
case 1:
/* (App f x) # (0,e)+1 -> f # (0,e)+1 (1,(e,x))+1 */
/* lstacktop = (f,x), rstacktop = e */
unpair(lstacktop, t2, lstacktop);
/* lstacktop = f, t2 = x */
t3 = rstacktop;
pair(t2, t3, t2);
/* t2 = (e,x) */
t3 = 1;
pair_inc(t2, t3, t2);
pair(rstack, rstack, t2);
/* rstack = (1,(e,x))+1 ... */
/* t2 = 0 */
pair_inc(rstacktop, t2, rstacktop);
/* rstacktop = (0,e)+1 */
break;
default:
/* (Var n) # (0,e)+1 -> e!!n # */
/* lstacktop = n, rstacktop = e */
builtin_move(t2, lstacktop);
index_list(rstacktop, t2, lstacktop);
/* lstacktop = e !! n */
rstack_pop();
break;
}
break;
case 1:
/* 1 = vapp eval */
if(decz lstacktop){
/* Reflect # (1,(e,x))+1 -> x # (0,e)+1 (3,_)+1 */
/* lstacktop = 0, rstacktop = (e,x) */
unpair(rstacktop, lstacktop, rstacktop);
/* lstacktop = x, rstacktop = e */
/* t2 = 1 */
t2 = t2 + 9;
/* t2 = (3,0)+1 */
pair(rstack, rstack, t2);
/* rstack = (3,0)+1 ... */
/* t2 = 0 */
pair_inc(rstacktop, t2, rstacktop);
/* rstacktop = (0,e)+1 */
}else{
/* (Closure e t) # (1,(e',x))+1 -> x # (0,e')+1 (2,(e,t))+1 */
/* lstacktop = (e,t), rstacktop = (e',x) */
t2 = 2;
pair_inc(t2, t2, lstacktop);
/* t2 = (2,(e,t))+1 */
pair(rstack, rstack, t2);
/* rstack = (2,(e,t))+1 ... */
/* t2 = 0 */
unpair(rstacktop, lstacktop, rstacktop);
/* lstacktop = x, rstacktop = e' */
pair_inc(rstacktop, t2, rstacktop);
/* rstacktop = (0,e')+1 */
}
break;
case 2:
/* 2 = vapp Closure */
/* x # (2,(e,t))+1 -> t # (0,(x,e))+1 */
/* lstacktop = x, rstacktop = (e,t) */
builtin_move(t2, lstacktop);
/* t2 = x */
unpair(rstacktop, lstacktop, rstacktop);
/* lstacktop = t, rstacktop = e */
pair(rstacktop, t2, rstacktop);
/* rstacktop = (x,e) */
/* t2 = 0 */
pair_inc(rstacktop, t2, rstacktop);
/* rstacktop = (0,(x,e))+1 */
break;
default:
/* 3 = const Reflect */
lstacktop = 0;
break;
}
}
/* done? */
stackszero();
if(t2 == 0){
return;
}
}