Lines Matching +defs:M1 +defs:OP
8 (IN-PACKAGE "M1")
10 (DEFUN M1::NEXT-INST (M1::S) (M1::NTH (M1::PC M1::S) (M1::PROGRAM M1::S)))
12 (DEFUN M1::EXECUTE-ICONST (M1::INST M1::S)
13 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S))
14 (M1::LOCALS M1::S)
15 (M1::PUSH (M1::ARG1 M1::INST)
16 (M1::STACK M1::S))
17 (M1::PROGRAM M1::S)))
19 (DEFUN M1::EXECUTE-ILOAD (M1::INST M1::S)
20 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S))
21 (M1::LOCALS M1::S)
22 (M1::PUSH (M1::NTH (M1::ARG1 M1::INST)
23 (M1::LOCALS M1::S))
24 (M1::STACK M1::S))
25 (M1::PROGRAM M1::S)))
28 M1::EXECUTE-IADD (M1::INST M1::S)
29 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S))
30 (M1::LOCALS M1::S)
31 (M1::PUSH (BINARY-+ (M1::TOP (M1::POP (M1::STACK M1::S)))
32 (M1::TOP (M1::STACK M1::S)))
33 (M1::POP (M1::POP (M1::STACK M1::S))))
34 (M1::PROGRAM M1::S)))
36 (DEFUN M1::EXECUTE-ISTORE (M1::INST M1::S)
37 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S))
38 (M1::UPDATE-NTH (M1::ARG1 M1::INST)
39 (M1::TOP (M1::STACK M1::S))
40 (M1::LOCALS M1::S))
41 (M1::POP (M1::STACK M1::S))
42 (M1::PROGRAM M1::S)))
45 M1::EXECUTE-ISUB (M1::INST M1::S)
46 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S))
47 (M1::LOCALS M1::S)
48 (M1::PUSH (BINARY-+ (M1::TOP (M1::POP (M1::STACK M1::S)))
49 (UNARY-- (M1::TOP (M1::STACK M1::S))))
50 (M1::POP (M1::POP (M1::STACK M1::S))))
51 (M1::PROGRAM M1::S)))
54 M1::EXECUTE-IMUL (M1::INST M1::S)
55 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S))
56 (M1::LOCALS M1::S)
57 (M1::PUSH (BINARY-* (M1::TOP (M1::POP (M1::STACK M1::S)))
58 (M1::TOP (M1::STACK M1::S)))
59 (M1::POP (M1::POP (M1::STACK M1::S))))
60 (M1::PROGRAM M1::S)))
62 (DEFUN M1::EXECUTE-GOTO (M1::INST M1::S)
63 (M1::MAKE-STATE (BINARY-+ (M1::ARG1 M1::INST)
64 (M1::PC M1::S))
65 (M1::LOCALS M1::S)
66 (M1::STACK M1::S)
67 (M1::PROGRAM M1::S)))
69 (DEFUN M1::EXECUTE-IFLE (M1::INST M1::S)
70 (M1::MAKE-STATE (IF (NOT (< '0 (M1::TOP (M1::STACK M1::S))))
71 (BINARY-+ (M1::ARG1 M1::INST)
72 (M1::PC M1::S))
73 (BINARY-+ '1 (M1::PC M1::S)))
74 (M1::LOCALS M1::S)
75 (M1::POP (M1::STACK M1::S))
76 (M1::PROGRAM M1::S)))
79 M1::DO-INST (M1::INST M1::S)
80 (IF (EQUAL (M1::OP-CODE M1::INST)
81 'M1::ICONST)
82 (M1::EXECUTE-ICONST M1::INST M1::S)
83 (IF (EQUAL (M1::OP-CODE M1::INST)
84 'M1::ILOAD)
85 (M1::EXECUTE-ILOAD M1::INST M1::S)
86 (IF (EQUAL (M1::OP-CODE M1::INST)
87 'M1::ISTORE)
88 (M1::EXECUTE-ISTORE M1::INST M1::S)
89 (IF (EQUAL (M1::OP-CODE M1::INST) 'M1::IADD)
90 (M1::EXECUTE-IADD M1::INST M1::S)
91 (IF (EQUAL (M1::OP-CODE M1::INST) 'M1::ISUB)
92 (M1::EXECUTE-ISUB M1::INST M1::S)
93 (IF (EQUAL (M1::OP-CODE M1::INST) 'M1::IMUL)
94 (M1::EXECUTE-IMUL M1::INST M1::S)
95 (IF (EQUAL (M1::OP-CODE M1::INST) 'M1::GOTO)
96 (M1::EXECUTE-GOTO M1::INST M1::S)
97 (IF (EQUAL (M1::OP-CODE M1::INST) 'M1::IFLE)
98 (M1::EXECUTE-IFLE M1::INST M1::S)
99 M1::S)))))))))
101 (DEFUN M1::STEP (M1::S) (M1::DO-INST (M1::NEXT-INST M1::S) M1::S))
103 (DEFUN M1::RUN (M1::SCHED M1::S)
104 (IF (ENDP M1::SCHED)
105 M1::S
106 (M1::RUN (CDR M1::SCHED)
107 (M1::STEP M1::S))))
109 (DEFTHM M1::FACTORIAL-EXAMPLE-0
110 (EQUAL (M1::RUN '(0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
115 (M1::MAKE-STATE '0
118 '((M1::ICONST 1)
119 (M1::ISTORE 1)
120 (M1::ILOAD 0)
121 (M1::IFLE 10)
122 (M1::ILOAD 0)
123 (M1::ILOAD 1)
124 (M1::IMUL)
125 (M1::ISTORE 1)
126 (M1::ILOAD 0)
127 (M1::ICONST 1)
128 (M1::ISUB)
129 (M1::ISTORE 0)
130 (M1::GOTO -10)
131 (M1::ILOAD 1)
132 (M1::HALT))))
135 ((M1::ICONST 1)
136 (M1::ISTORE 1)
137 (M1::ILOAD 0)
138 (M1::IFLE 10)
139 (M1::ILOAD 0)
140 (M1::ILOAD 1)
141 (M1::IMUL)
142 (M1::ISTORE 1)
143 (M1::ILOAD 0)
144 (M1::ICONST 1)
145 (M1::ISUB)
146 (M1::ISTORE 0)
147 (M1::GOTO -10)
148 (M1::ILOAD 1)
149 (M1::HALT)))))
151 (DEFUN M1::IFACT-LOOP-SCHED (M1::N)
152 (IF (ZP M1::N)
153 (M1::REPEAT '0 '4)
154 (M1::APP (M1::REPEAT '0 '11)
155 (M1::IFACT-LOOP-SCHED (BINARY-+ '-1 M1::N)))))
157 (DEFUN M1::IFACT-SCHED (M1::N)
158 (M1::APP (M1::REPEAT '0 '2)
159 (M1::IFACT-LOOP-SCHED M1::N)))
161 (DEFUN M1::! (M1::N)
162 (IF (ZP M1::N)
164 (BINARY-* M1::N (M1::! (BINARY-+ '-1 M1::N)))))
167 M1::TEST-IFACT (M1::N)
168 (M1::TOP (M1::STACK (M1::RUN (M1::IFACT-SCHED M1::N)
169 (M1::MAKE-STATE '0
170 (CONS M1::N (CONS '0 'NIL))
172 '((M1::ICONST 1)
173 (M1::ISTORE 1)
174 (M1::ILOAD 0)
175 (M1::IFLE 10)
176 (M1::ILOAD 0)
177 (M1::ILOAD 1)
178 (M1::IMUL)
179 (M1::ISTORE 1)
180 (M1::ILOAD 0)
181 (M1::ICONST 1)
182 (M1::ISUB)
183 (M1::ISTORE 0)
184 (M1::GOTO -10)
185 (M1::ILOAD 1)
186 (M1::HALT)))))))
188 (DEFTHM M1::FACTORIAL-EXAMPLE-1 (EQUAL (M1::TEST-IFACT '5) (M1::! '5)))
190 (DEFTHM M1::FACTORIAL-EXAMPLE-2
191 (EQUAL (M1::TEST-IFACT '1000)
192 (M1::! '1000)))
194 (DEFUN M1::EVEN-SCHED (M1::I)
195 (IF (ZP M1::I)
196 (M1::REPEAT '0 '4)
197 (IF (EQUAL M1::I '1)
198 (M1::REPEAT '0 '8)
199 (M1::APP (M1::REPEAT '0 '11)
200 (M1::EVEN-SCHED (BINARY-+ '-2 M1::I))))))
202 (DEFUN M1::TEST-EVEN (M1::I)
203 (M1::TOP (M1::STACK (M1::RUN (M1::EVEN-SCHED M1::I)
204 (M1::MAKE-STATE '0
205 (CONS M1::I 'NIL)
207 '((M1::ILOAD 0)
208 (M1::IFLE 12)
209 (M1::ILOAD 0)
210 (M1::ICONST 1)
211 (M1::ISUB)
212 (M1::IFLE 6)
213 (M1::ILOAD 0)
214 (M1::ICONST 2)
215 (M1::ISUB)
216 (M1::ISTORE 0)
217 (M1::GOTO -10)
218 (M1::ICONST 0)
219 (M1::HALT)
220 (M1::ICONST 1)
221 (M1::HALT)))))))
223 (DEFTHM M1::TEST-EVEN-THEOREM
224 (IF (EQUAL (M1::TEST-EVEN '18) '1)
225 (IF (EQUAL (M1::TEST-EVEN '19) '0)
226 (IF (EQUAL (M1::TEST-EVEN '235) '0)
227 (EQUAL (M1::TEST-EVEN '234) '1)
232 (DEFUN M1::COLLECT-AT-END (LIST M1::E)
233 (IF (M1::MEMBER M1::E LIST)
234 LIST (M1::APP LIST (CONS M1::E 'NIL))))
236 (DEFTHM M1::NTH-NIL (EQUAL (M1::NTH M1::N 'NIL) 'NIL))
238 (DEFTHM M1::ACL2-COUNT-NTH
240 (< (ACL2-COUNT (M1::NTH M1::N LIST))
243 (DEFUN M1::COLLECT-VARS-IN-EXPR
244 (M1::VARS M1::EXPR)
245 (IF (ATOM M1::EXPR)
246 (IF (SYMBOLP M1::EXPR)
247 (M1::COLLECT-AT-END M1::VARS M1::EXPR)
248 M1::VARS)
249 (M1::COLLECT-VARS-IN-EXPR
250 (M1::COLLECT-VARS-IN-EXPR M1::VARS (M1::NTH '0 M1::EXPR))
251 (M1::NTH '2 M1::EXPR))))
254 (DEFUN M1::COLLECT-VARS-IN-STMT*
255 (M1::VARS M1::STMT-LIST)
256 (IF (ENDP M1::STMT-LIST)
257 M1::VARS
258 (M1::COLLECT-VARS-IN-STMT*
259 (M1::COLLECT-VARS-IN-STMT M1::VARS (CAR M1::STMT-LIST))
260 (CDR M1::STMT-LIST))))
262 M1::COLLECT-VARS-IN-STMT
263 (M1::VARS M1::STMT)
264 (IF (EQUAL (M1::NTH '1 M1::STMT) 'M1::=)
265 (M1::COLLECT-VARS-IN-EXPR
266 (M1::COLLECT-AT-END M1::VARS (M1::NTH '0 M1::STMT))
267 (M1::NTH '2 M1::STMT))
268 (IF (EQUAL (M1::NTH '0 M1::STMT) 'M1::WHILE)
269 (M1::COLLECT-VARS-IN-STMT*
270 (M1::COLLECT-VARS-IN-EXPR M1::VARS (M1::NTH '1 M1::STMT))
271 (CDR (CDR M1::STMT)))
272 (IF (EQUAL (M1::NTH '0 M1::STMT)
273 'M1::RETURN)
274 (M1::COLLECT-VARS-IN-EXPR M1::VARS (M1::NTH '1 M1::STMT))
275 M1::VARS)))))
277 (DEFUN M1::OP! (M1::OP)
278 (IF (EQUAL M1::OP '+)
279 '((M1::IADD))
280 (IF (EQUAL M1::OP '-)
281 '((M1::ISUB))
282 (IF (EQUAL M1::OP '*)
283 '((M1::IMUL))
284 '((M1::ILLEGAL))))))
286 (DEFUN M1::ILOAD! (M1::VARS M1::VAR)
287 (CONS (CONS 'M1::ILOAD
288 (CONS (M1::INDEX M1::VAR M1::VARS)
292 (DEFUN M1::ICONST! (M1::N) (CONS (CONS 'M1::ICONST (CONS M1::N 'NIL)) 'NIL))
294 (DEFUN M1::EXPR! (M1::VARS M1::EXPR)
295 (IF (ATOM M1::EXPR)
296 (IF (SYMBOLP M1::EXPR)
297 (M1::ILOAD! M1::VARS M1::EXPR)
298 (M1::ICONST! M1::EXPR))
299 (M1::APP (M1::EXPR! M1::VARS (M1::NTH '0 M1::EXPR))
300 (M1::APP (M1::EXPR! M1::VARS (M1::NTH '2 M1::EXPR))
301 (M1::OP! (M1::NTH '1 M1::EXPR))))))
303 (DEFUN M1::IFLE! (M1::OFFSET)
304 (CONS (CONS 'M1::IFLE (CONS M1::OFFSET 'NIL))
307 (DEFUN M1::GOTO! (M1::OFFSET)
308 (CONS (CONS 'M1::GOTO (CONS M1::OFFSET 'NIL))
312 M1::WHILE! (M1::TEST-CODE M1::BODY-CODE)
313 (M1::APP
314 M1::TEST-CODE
315 (M1::APP
316 (M1::IFLE! (BINARY-+ '2 (M1::LEN M1::BODY-CODE)))
317 (M1::APP
318 M1::BODY-CODE
319 (M1::GOTO! (UNARY-- (BINARY-+ (M1::LEN M1::TEST-CODE)
321 (M1::LEN M1::BODY-CODE)))))))))
323 (DEFUN M1::TEST! (M1::VARS M1::TEST)
324 (IF (EQUAL (M1::NTH '1 M1::TEST) '>)
325 (IF (EQUAL (M1::NTH '2 M1::TEST) '0)
326 (M1::EXPR! M1::VARS (M1::NTH '0 M1::TEST))
327 (M1::APP (M1::EXPR! M1::VARS (M1::NTH '0 M1::TEST))
328 (M1::APP (M1::EXPR! M1::VARS (M1::NTH '2 M1::TEST))
329 '((M1::ISUB)))))
330 '((M1::ILLEGAL))))
332 (DEFUN M1::ISTORE! (M1::VARS M1::VAR)
333 (CONS (CONS 'M1::ISTORE
334 (CONS (M1::INDEX M1::VAR M1::VARS)
339 (DEFUN M1::STMT*! (M1::VARS M1::STMT-LIST)
340 (IF (ENDP M1::STMT-LIST)
342 (M1::APP (M1::STMT! M1::VARS (CAR M1::STMT-LIST))
343 (M1::STMT*! M1::VARS (CDR M1::STMT-LIST)))))
344 (DEFUN M1::STMT! (M1::VARS M1::STMT)
345 (IF (EQUAL (M1::NTH '1 M1::STMT) 'M1::=)
346 (M1::APP (M1::EXPR! M1::VARS (M1::NTH '2 M1::STMT))
347 (M1::ISTORE! M1::VARS (M1::NTH '0 M1::STMT)))
348 (IF (EQUAL (M1::NTH '0 M1::STMT) 'M1::WHILE)
349 (M1::WHILE! (M1::TEST! M1::VARS (M1::NTH '1 M1::STMT))
350 (M1::STMT*! M1::VARS (CDR (CDR M1::STMT))))
351 (IF (EQUAL (M1::NTH '0 M1::STMT)
352 'M1::RETURN)
353 (M1::APP (M1::EXPR! M1::VARS (M1::NTH '1 M1::STMT))
354 '((M1::HALT)))
355 '((M1::ILLEGAL)))))))
357 (DEFUN M1::COMPILE (M1::FORMALS M1::STMT-LIST)
358 (M1::STMT*! (M1::COLLECT-VARS-IN-STMT* M1::FORMALS M1::STMT-LIST)
359 M1::STMT-LIST))
361 (DEFTHM M1::EXAMPLE-COMPILATION-1
362 (EQUAL (M1::COMPILE '(M1::N)
363 '((M1::A M1::= 1)
364 (M1::WHILE (M1::N > 0)
365 (M1::A M1::= (M1::N * M1::A))
366 (M1::N M1::= (M1::N - 1)))
367 (M1::RETURN M1::A)))
368 '((M1::ICONST 1)
369 (M1::ISTORE 1)
370 (M1::ILOAD 0)
371 (M1::IFLE 10)
372 (M1::ILOAD 0)
373 (M1::ILOAD 1)
374 (M1::IMUL)
375 (M1::ISTORE 1)
376 (M1::ILOAD 0)
377 (M1::ICONST 1)
378 (M1::ISUB)
379 (M1::ISTORE 0)
380 (M1::GOTO -10)
381 (M1::ILOAD 1)
382 (M1::HALT))))
384 (DEFTHM M1::EXAMPLE-COMPILATION-2
385 (EQUAL (M1::COMPILE '(M1::N M1::K)
386 '((M1::A M1::= 0)
387 (M1::WHILE (M1::N > M1::K)
388 (M1::A M1::= (M1::A + 1))
389 (M1::N M1::= (M1::N - 1)))
390 (M1::RETURN M1::A)))
391 '((M1::ICONST 0)
392 (M1::ISTORE 2)
393 (M1::ILOAD 0)
394 (M1::ILOAD 1)
395 (M1::ISUB)
396 (M1::IFLE 10)
397 (M1::ILOAD 2)
398 (M1::ICONST 1)
399 (M1::IADD)
400 (M1::ISTORE 2)
401 (M1::ILOAD 0)
402 (M1::ICONST 1)
403 (M1::ISUB)
404 (M1::ISTORE 0)
405 (M1::GOTO -12)
406 (M1::ILOAD 2)
407 (M1::HALT))))
410 M1::EXAMPLE-EXECUTION-1
412 (M1::TOP
413 (M1::STACK
414 (M1::RUN
415 (M1::REPEAT '0 '1000)
416 (M1::MAKE-STATE '0
419 (M1::COMPILE '(M1::N)
420 '((M1::A M1::= 1)
421 (M1::WHILE (M1::N > 0)
422 (M1::A M1::= (M1::N * M1::A))
423 (M1::N M1::= (M1::N - 1)))
424 (M1::RETURN M1::A)))))))
428 M1::EXAMPLE-EXECUTION-2
430 (M1::TOP
431 (M1::STACK
432 (M1::RUN
433 (M1::REPEAT '0 '1000)
434 (M1::MAKE-STATE '0
437 (M1::COMPILE '(M1::N M1::K)
438 '((M1::A M1::= 0)
439 (M1::WHILE (M1::N > M1::K)
440 (M1::A M1::= (M1::A + 1))
441 (M1::N M1::= (M1::N - 1)))
442 (M1::RETURN M1::A)))))))
447 (DEFTHM M1::STACKS
448 (IF (EQUAL (M1::TOP (M1::PUSH M1::X M1::S))
449 M1::X)
450 (IF (EQUAL (M1::POP (M1::PUSH M1::X M1::S))
451 M1::S)
452 (IF (EQUAL (M1::TOP (CONS M1::X M1::S))
453 M1::X)
454 (EQUAL (M1::POP (CONS M1::X M1::S))
455 M1::S)
461 M1::STATES
463 (EQUAL (M1::PC (M1::MAKE-STATE M1::PC
464 M1::LOCALS M1::STACK M1::PROGRAM))
465 M1::PC)
467 (EQUAL (M1::LOCALS (M1::MAKE-STATE M1::PC
468 M1::LOCALS M1::STACK M1::PROGRAM))
469 M1::LOCALS)
471 (EQUAL (M1::STACK (M1::MAKE-STATE M1::PC
472 M1::LOCALS M1::STACK M1::PROGRAM))
473 M1::STACK)
475 (EQUAL (M1::PROGRAM (M1::MAKE-STATE M1::PC
476 M1::LOCALS M1::STACK M1::PROGRAM))
477 M1::PROGRAM)
479 (EQUAL (M1::PC (CONS M1::PC M1::X))
480 M1::PC)
482 (EQUAL (M1::LOCALS (CONS M1::PC (CONS M1::LOCALS M1::X)))
483 M1::LOCALS)
485 (EQUAL (M1::STACK (CONS M1::PC
486 (CONS M1::LOCALS (CONS M1::STACK M1::X))))
487 M1::STACK)
488 (EQUAL (M1::PROGRAM
489 (CONS M1::PC
490 (CONS M1::LOCALS
491 (CONS M1::STACK (CONS M1::PROGRAM M1::X)))))
492 M1::PROGRAM)
501 (DEFTHM M1::STEP-OPENER
502 (IMPLIES (CONSP (M1::NEXT-INST M1::S))
503 (EQUAL (M1::STEP M1::S)
504 (M1::DO-INST (M1::NEXT-INST M1::S)
505 M1::S))))
507 (DEFTHM M1::RUN-APP
508 (EQUAL (M1::RUN (M1::APP M1::A M1::B) M1::S)
509 (M1::RUN M1::B (M1::RUN M1::A M1::S))))
511 (DEFTHM M1::RUN-OPENER
512 (IF (EQUAL (M1::RUN 'NIL M1::S) M1::S)
513 (EQUAL (M1::RUN (CONS M1::TH M1::SCHED) M1::S)
514 (M1::RUN M1::SCHED (M1::STEP M1::S)))
517 (DEFTHM M1::NTH-ADD1!
518 (IMPLIES (NATP M1::N)
519 (EQUAL (M1::NTH (BINARY-+ '1 M1::N) LIST)
520 (M1::NTH M1::N (CDR LIST)))))
522 (DEFTHM M1::NTH-UPDATE-NTH
523 (IMPLIES (IF (NATP M1::I) (NATP M1::J) 'NIL)
524 (EQUAL (M1::NTH M1::I (M1::UPDATE-NTH M1::J M1::V LIST))
525 (IF (EQUAL M1::I M1::J)
526 M1::V (M1::NTH M1::I LIST)))))
529 M1::UPDATE-NTH-UPDATE-NTH-1
530 (IMPLIES (IF (NATP M1::I)
531 (IF (NATP M1::J)
532 (NOT (EQUAL M1::I M1::J))
535 (EQUAL (M1::UPDATE-NTH M1::I
536 M1::V (M1::UPDATE-NTH M1::J M1::W LIST))
537 (M1::UPDATE-NTH M1::J M1::W
538 (M1::UPDATE-NTH M1::I M1::V LIST)))))
540 (DEFTHM M1::UPDATE-NTH-UPDATE-NTH-2
541 (EQUAL (M1::UPDATE-NTH M1::I
542 M1::V (M1::UPDATE-NTH M1::I M1::W LIST))
543 (M1::UPDATE-NTH M1::I M1::V LIST)))
545 (DEFUN M1::! (M1::N)
546 (IF (ZP M1::N)
548 (BINARY-* M1::N (M1::! (BINARY-+ '-1 M1::N)))))
550 (DEFUN M1::IFACT (M1::N M1::A)
551 (IF (ZP M1::N)
552 M1::A
553 (M1::IFACT (BINARY-+ '-1 M1::N)
554 (BINARY-* M1::N M1::A))))
556 (DEFUN M1::IFACT-LOOP-SCHED (M1::N)
557 (IF (ZP M1::N)
558 (M1::REPEAT '0 '4)
559 (M1::APP (M1::REPEAT '0 '11)
560 (M1::IFACT-LOOP-SCHED (BINARY-+ '-1 M1::N)))))
562 (DEFUN M1::IFACT-SCHED (M1::N)
563 (M1::APP (M1::REPEAT '0 '2)
564 (M1::IFACT-LOOP-SCHED M1::N)))
567 M1::TEST-IFACT (M1::N)
568 (M1::TOP (M1::STACK (M1::RUN (M1::IFACT-SCHED M1::N)
569 (M1::MAKE-STATE '0
570 (CONS M1::N (CONS '0 'NIL))
572 '((M1::ICONST 1)
573 (M1::ISTORE 1)
574 (M1::ILOAD 0)
575 (M1::IFLE 10)
576 (M1::ILOAD 0)
577 (M1::ILOAD 1)
578 (M1::IMUL)
579 (M1::ISTORE 1)
580 (M1::ILOAD 0)
581 (M1::ICONST 1)
582 (M1::ISUB)
583 (M1::ISTORE 0)
584 (M1::GOTO -10)
585 (M1::ILOAD 1)
586 (M1::HALT)))))))
588 (DEFTHM M1::TEST-IFACT-EXAMPLES
589 (IF (EQUAL (M1::TEST-IFACT '5) (M1::! '5))
590 (IF (EQUAL (M1::TEST-IFACT '10) (M1::! '10))
591 (EQUAL (M1::TEST-IFACT '100)
592 (M1::! '100))
597 M1::IFACT-LOOP-LEMMA
598 (IMPLIES (IF (NATP M1::N) (NATP M1::A) 'NIL)
599 (EQUAL (M1::RUN (M1::IFACT-LOOP-SCHED M1::N)
600 (M1::MAKE-STATE '2
601 (CONS M1::N (CONS M1::A 'NIL))
602 M1::STACK
603 '((M1::ICONST 1)
604 (M1::ISTORE 1)
605 (M1::ILOAD 0)
606 (M1::IFLE 10)
607 (M1::ILOAD 0)
608 (M1::ILOAD 1)
609 (M1::IMUL)
610 (M1::ISTORE 1)
611 (M1::ILOAD 0)
612 (M1::ICONST 1)
613 (M1::ISUB)
614 (M1::ISTORE 0)
615 (M1::GOTO -10)
616 (M1::ILOAD 1)
617 (M1::HALT))))
618 (M1::MAKE-STATE '14
620 (CONS (M1::IFACT M1::N M1::A) 'NIL))
621 (M1::PUSH (M1::IFACT M1::N M1::A)
622 M1::STACK)
623 '((M1::ICONST 1)
624 (M1::ISTORE 1)
625 (M1::ILOAD 0)
626 (M1::IFLE 10)
627 (M1::ILOAD 0)
628 (M1::ILOAD 1)
629 (M1::IMUL)
630 (M1::ISTORE 1)
631 (M1::ILOAD 0)
632 (M1::ICONST 1)
633 (M1::ISUB)
634 (M1::ISTORE 0)
635 (M1::GOTO -10)
636 (M1::ILOAD 1)
637 (M1::HALT))))))
640 M1::IFACT-LEMMA
641 (IMPLIES (NATP M1::N)
642 (EQUAL (M1::RUN (M1::IFACT-SCHED M1::N)
643 (M1::MAKE-STATE '0
644 (CONS M1::N (CONS M1::A 'NIL))
645 M1::STACK
646 '((M1::ICONST 1)
647 (M1::ISTORE 1)
648 (M1::ILOAD 0)
649 (M1::IFLE 10)
650 (M1::ILOAD 0)
651 (M1::ILOAD 1)
652 (M1::IMUL)
653 (M1::ISTORE 1)
654 (M1::ILOAD 0)
655 (M1::ICONST 1)
656 (M1::ISUB)
657 (M1::ISTORE 0)
658 (M1::GOTO -10)
659 (M1::ILOAD 1)
660 (M1::HALT))))
661 (M1::MAKE-STATE '14
663 (CONS (M1::IFACT M1::N '1) 'NIL))
664 (M1::PUSH (M1::IFACT M1::N '1)
665 M1::STACK)
666 '((M1::ICONST 1)
667 (M1::ISTORE 1)
668 (M1::ILOAD 0)
669 (M1::IFLE 10)
670 (M1::ILOAD 0)
671 (M1::ILOAD 1)
672 (M1::IMUL)
673 (M1::ISTORE 1)
674 (M1::ILOAD 0)
675 (M1::ICONST 1)
676 (M1::ISUB)
677 (M1::ISTORE 0)
678 (M1::GOTO -10)
679 (M1::ILOAD 1)
680 (M1::HALT))))))
682 (DEFTHM M1::IFACT-IS-FACTORIAL
683 (IMPLIES (IF (NATP M1::N) (NATP M1::A) 'NIL)
684 (EQUAL (M1::IFACT M1::N M1::A)
685 (BINARY-* (M1::! M1::N) M1::A))))
688 M1::IFACT-CORRECT
689 (IMPLIES (NATP M1::N)
690 (EQUAL (M1::RUN (M1::IFACT-SCHED M1::N)
691 (M1::MAKE-STATE '0
692 (CONS M1::N (CONS M1::A 'NIL))
693 M1::STACK
694 '((M1::ICONST 1)
695 (M1::ISTORE 1)
696 (M1::ILOAD 0)
697 (M1::IFLE 10)
698 (M1::ILOAD 0)
699 (M1::ILOAD 1)
700 (M1::IMUL)
701 (M1::ISTORE 1)
702 (M1::ILOAD 0)
703 (M1::ICONST 1)
704 (M1::ISUB)
705 (M1::ISTORE 0)
706 (M1::GOTO -10)
707 (M1::ILOAD 1)
708 (M1::HALT))))
709 (M1::MAKE-STATE '14
710 (CONS '0 (CONS (M1::! M1::N) 'NIL))
711 (M1::PUSH (M1::! M1::N) M1::STACK)
712 '((M1::ICONST 1)
713 (M1::ISTORE 1)
714 (M1::ILOAD 0)
715 (M1::IFLE 10)
716 (M1::ILOAD 0)
717 (M1::ILOAD 1)
718 (M1::IMUL)
719 (M1::ISTORE 1)
720 (M1::ILOAD 0)
721 (M1::ICONST 1)
722 (M1::ISUB)
723 (M1::ISTORE 0)
724 (M1::GOTO -10)
725 (M1::ILOAD 1)
726 (M1::HALT))))))
729 M1::IFACT-CORRECT-COROLLARY-1
731 (NATP M1::N)
733 (M1::TOP
734 (M1::STACK (M1::RUN (M1::IFACT-SCHED M1::N)
735 (M1::MAKE-STATE '0
736 (CONS M1::N (CONS M1::A 'NIL))
737 M1::STACK
738 '((M1::ICONST 1)
739 (M1::ISTORE 1)
740 (M1::ILOAD 0)
741 (M1::IFLE 10)
742 (M1::ILOAD 0)
743 (M1::ILOAD 1)
744 (M1::IMUL)
745 (M1::ISTORE 1)
746 (M1::ILOAD 0)
747 (M1::ICONST 1)
748 (M1::ISUB)
749 (M1::ISTORE 0)
750 (M1::GOTO -10)
751 (M1::ILOAD 1)
752 (M1::HALT))))))
753 (M1::! M1::N))))
756 M1::IFACT-CORRECT-COROLLARY-2
758 (NATP M1::N)
760 (M1::TOP
761 (M1::STACK
762 (M1::RUN
763 (M1::IFACT-SCHED M1::N)
764 (M1::MAKE-STATE '0
765 (CONS M1::N (CONS M1::A 'NIL))
766 M1::STACK
767 (M1::COMPILE '(M1::N)
768 '((M1::A M1::= 1)
769 (M1::WHILE (M1::N > 0)
770 (M1::A M1::= (M1::N * M1::A))
771 (M1::N M1::= (M1::N - 1)))
772 (M1::RETURN M1::A)))))))
773 (M1::! M1::N))))
775 (DEFTHM M1::EXAMPLE-MODIFY-1
776 (EQUAL (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S))
777 (M1::LOCALS M1::S)
778 (M1::PUSH (M1::ARG1 M1::INST)
779 (M1::STACK M1::S))
780 (M1::PROGRAM M1::S))
781 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S))
782 (M1::LOCALS M1::S)
783 (M1::PUSH (M1::ARG1 M1::INST)
784 (M1::STACK M1::S))
785 (M1::PROGRAM M1::S))))
787 (DEFTHM M1::EXAMPLE-MODIFY-2
788 (EQUAL (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S))
789 (M1::UPDATE-NTH (M1::ARG1 M1::INST)
790 (M1::TOP (M1::STACK M1::S))
791 (M1::LOCALS M1::S))
792 (M1::POP (M1::STACK M1::S))
793 (M1::PROGRAM M1::S))
794 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S))
795 (M1::UPDATE-NTH (M1::ARG1 M1::INST)
796 (M1::TOP (M1::STACK M1::S))
797 (M1::LOCALS M1::S))
798 (M1::POP (M1::STACK M1::S))
799 (M1::PROGRAM M1::S))))
801 (DEFTHM M1::EXAMPLE-MODIFY-3
802 (EQUAL (M1::MAKE-STATE (BINARY-+ (M1::ARG1 M1::INST)
803 (M1::PC M1::S))
804 (M1::LOCALS M1::S)
805 (M1::STACK M1::S)
806 (M1::PROGRAM M1::S))
807 (M1::MAKE-STATE (BINARY-+ (M1::ARG1 M1::INST)
808 (M1::PC M1::S))
809 (M1::LOCALS M1::S)
810 (M1::STACK M1::S)
811 (M1::PROGRAM M1::S))))
813 (DEFUN M1::PATTERN-BINDINGS
814 (M1::VARS M1::ARG-EXPRESSIONS)
815 (IF (ENDP M1::VARS)
817 (CONS (CONS (CAR M1::VARS)
818 (CONS (CAR M1::ARG-EXPRESSIONS) 'NIL))
819 (M1::PATTERN-BINDINGS (CDR M1::VARS)
820 (CDR M1::ARG-EXPRESSIONS)))))
822 (DEFTHM M1::EXAMPLE-SEMANTICS-1
823 (EQUAL ((LAMBDA (M1::C M1::-PC- M1::-LOCALS-
824 M1::-STACK- M1::-PROGRAM- M1::S)
825 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S))
826 (M1::LOCALS M1::S)
827 (M1::PUSH M1::C M1::-STACK-)
828 (M1::PROGRAM M1::S)))
829 (M1::ARG1 M1::INST)
830 (M1::PC M1::S)
831 (M1::LOCALS M1::S)
832 (M1::STACK M1::S)
833 (M1::PROGRAM M1::S)
834 M1::S)
835 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S))
836 (M1::LOCALS M1::S)
837 (M1::PUSH (M1::ARG1 M1::INST)
838 (M1::STACK M1::S))
839 (M1::PROGRAM M1::S))))
841 (DEFUN M1::CONCAT-SYMBOLS (M1::PART1 M1::PART2)
843 (COERCE (M1::APP (COERCE (SYMBOL-NAME M1::PART1) 'LIST)
844 (COERCE (SYMBOL-NAME M1::PART2) 'LIST))
846 'M1::RUN))
848 (DEFUN M1::MAKE-DEFUN
849 (M1::NAME M1::ARGS M1::DCL M1::BODY)
850 (IF M1::DCL
852 (CONS M1::NAME
853 (CONS M1::ARGS
854 (CONS M1::DCL (CONS M1::BODY 'NIL)))))
856 (CONS M1::NAME
857 (CONS M1::ARGS (CONS M1::BODY 'NIL))))))