← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/1999/compiler/machine.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/1999/compiler/machine.lisp
 
1
;;=========================================================================
 
2
;; Copyright (C) 1999 Institut fuer Informatik, University of Kiel, Germany
 
3
;;===========================================================================
 
4
;; File:         machine.lisp
 
5
;; Author:       Wolfgang Goerigk
 
6
;; Content:      ACL2 implementation of a simple abstract machine
 
7
;; as of:        14/04/99, University of Texas at Austin, Texas, U.S.A.
 
8
;;---------------------------------------------------------------------------
 
9
;; $Revision: 1.4 $
 
10
;; $Id: machine.lisp,v 1.4 1999/09/26 11:28:16 wg Exp wg $
 
11
;;===========================================================================
 
12
;; This book is free software; you can redistribute it and/or modify it under
 
13
;; the terms of the GNU General Public License as published by the Free
 
14
;; Software Foundation; either version 2 of the License, or (at your option)
 
15
;; any later version.
 
16
;;---------------------------------------------------------------------------
 
17
;; This book is distributed in the hope that it will be useful, but WITHOUT
 
18
;; ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
 
19
;; FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License for
 
20
;; more details.
 
21
;;---------------------------------------------------------------------------
 
22
;; You should have received a copy of the GNU General Public License along
 
23
;; with this book; if not, write to the Free Software Foundation, Inc., 675
 
24
;; Mass Ave, Cambridge, MA 02139, USA.
 
25
;;===========================================================================
 
26
;;
 
27
;; This book is part of a series of books that come with and are described in
 
28
;; the article "Wolfgang Goerigk: Compiler Verification Revisited" as part of
 
29
;; "Computer Aided Reasoning: ACL2 Case Studies" edited by Matt Kaufmann, Pete
 
30
;; Manolios and J Strother Moore.
 
31
;;
 
32
;;===========================================================================
 
33
;;
 
34
;; The Abstract Stack Machine
 
35
;; ~~~~~~~~~~~~~~~~~~~~~~~~~~
 
36
;; This book defines the executable ACL2 model of an abstract stack machine
 
37
;; and the machine code (TL) used as target code for the compilers in the book
 
38
;; "compiler".
 
39
;;
 
40
;;===========================================================================
 
41
 
 
42
(in-package "ACL2")
 
43
(include-book "../../../ordinals/e0-ordinal")
 
44
(set-well-founded-relation e0-ord-<)
 
45
 
 
46
;;===========================================================================
 
47
;; We use our own version of butlast and call it butlst.
 
48
;;---------------------------------------------------------------------------
 
49
 
 
50
(defun butlst (x)
 
51
  (declare (xargs :guard (true-listp x)))
 
52
  (if (consp x)
 
53
      (if (consp (cdr x))
 
54
          (if (consp (cddr x))
 
55
              (cons (car x) (butlst (cdr x)))
 
56
            (list (car x)))
 
57
        nil)
 
58
    nil))
 
59
 
 
60
;;===========================================================================
 
61
;; The Abstract Machine (Program Semantics)
 
62
;;===========================================================================
 
63
;;
 
64
;; Abstract Machine Programs:
 
65
;; ~~~~~~~~~~~~~~~~~~~~~~~~~~
 
66
;;   prog  == (decl_1 ... decl_n (instr_1 ... instr_k))
 
67
;;   decl  == (DEFCODE <name> (instr_1 ... instr_k))
 
68
;;
 
69
;; where in both cases n >= 0 and instructions are as defined below.
 
70
;;
 
71
;; Abstract Machine Configuration: 
 
72
;; ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
73
;;   code  == ((fn_1 . code_1) (fn_2 . code_2) ... (fn_n . code_n))
 
74
;;   stack == (top top_1 top_2 ... bottom)
 
75
;;
 
76
;; Operator calls including calls of user defined procedures consume (pop)
 
77
;; their arguments from the stack and push their result on top of the
 
78
;; stack. Instructions are
 
79
;;  
 
80
;; Abstract Machine Instructions and Evaluation
 
81
;; ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
82
;;   (PUSHC <constant>)      ; push <constant> onto the stack
 
83
;;   (PUSHV <index>)         ; push the value of the <index>'th stack cell 
 
84
;;   (CALL <name>)           ; execute the code associated with <name> in code
 
85
;;   (OPR <name>)            ; execute the Lisp operator <name> on the stack
 
86
;;   (IF <then> <else>)      ; execute <else>, if top = nil, otherwise <then>
 
87
;;   (POP <n>)               ; (top d1 ... dn . rest) -> (top . rest)
 
88
;;
 
89
;; The functions mstep executes a single instruction, applied to the stack and
 
90
;; returning the new stack.  msteps executes a sequence of instructions by
 
91
;; subsequently executing each of them.
 
92
;;
 
93
;; Since in general machine programs may not terminate, an additional
 
94
;; <number-of-steps> argument (n) forces execution to terminate. Actually, we
 
95
;; decrease n only if a user defined subroutine is called, i.e. if we start to
 
96
;; execute its body. This is sufficient to guarantee termination since it is
 
97
;; the only case, where a structural induction would fail. So the measure
 
98
;; functions we use to admit mstep and msteps are (cons (1+ (acl2-count n))
 
99
;; (acl2-count form)) and (cons (1+ (acl2-count n)) (acl2-count seq)), i.e. we
 
100
;; use the lexicographical ordering of the depth of the call-tree and the
 
101
;; complexity of the syntactical structure.  Note that the 1+ is necessary for
 
102
;; these conses to be e0-ordinalp's.
 
103
;;
 
104
;; The instruction (IF <then> <else>) assumes the condition's value on top of
 
105
;; stack.  The abstract machine language has structured code.  Operators are
 
106
;; those recognized by the function "operatorp" which is defined in
 
107
;; "compiler.lisp".
 
108
;;
 
109
;;---------------------------------------------------------------------------
 
110
 
 
111
;;---------------------------------------------------------------------------
 
112
;; The Lisp operators
 
113
;; ~~~~~~~~~~~~~~~~~~
 
114
;; for simplicity we could just use the ACL2 functions that correspond to our
 
115
;; operators (see definition of operatorp in "compiler") in order to implement
 
116
;; the operators. However, we would not be able to verify the guards because
 
117
;; we can not guarantee that the machine program uses the operators within
 
118
;; their Common Lisp domains. Therefore we define our own functions but prove
 
119
;; them to be equal to the ACL2 versions. The former makes sure that we can
 
120
;; certify this book, whereas the latter makes sure that the machine (and
 
121
;; hence the evaluator and the compiler) do something reasonable.
 
122
;;
 
123
 
 
124
(defun MCAR (x)
 
125
  (declare (xargs :guard t))
 
126
  (if (or (consp x) (equal x nil)) (car x) nil))
 
127
 
 
128
(defun MCDR (x)
 
129
  (declare (xargs :guard t))
 
130
  (if (or (consp x) (equal x nil)) (cdr x) nil))
 
131
 
 
132
(defmacro MCADR (X) (LIST 'MCAR (LIST 'MCDR X)))
 
133
(defmacro mcddr (X) (LIST 'MCDR (LIST 'MCDR X)))
 
134
(defmacro mcdar (X) (LIST 'MCDR (LIST 'MCAR X)))
 
135
(defmacro MCADDR (X) (LIST 'MCAR (LIST 'mcddr X)))
 
136
(defmacro MCADAR (X) (LIST 'MCAR (LIST 'mcdar X)))
 
137
(defmacro mcddar (X) (LIST 'MCDR (LIST 'mcdar X)))
 
138
(defmacro mcdddr (X) (LIST 'MCDR (LIST 'mcddr X)))
 
139
(defmacro MCADDAR (X) (LIST 'MCAR (LIST 'mcddar X)))
 
140
(defmacro MCADDDR (X) (LIST 'MCAR (LIST 'mcdddr X)))
 
141
 
 
142
(defun M1+ (n)
 
143
  (declare (xargs :guard t))
 
144
  (if (acl2-numberp n) (1+ n) 1))
 
145
 
 
146
(defun M1- (n)
 
147
  (declare (xargs :guard t))
 
148
  (if (acl2-numberp n) (1- n) -1))
 
149
 
 
150
(defmacro MLEN (X) (LIST 'LEN X))
 
151
(defmacro MSYMBOLP (X) (LIST 'SYMBOLP X))
 
152
(defmacro MCONSP (X) (LIST 'CONSP X))
 
153
(defmacro MATOM (X) (LIST 'ATOM X))
 
154
(defmacro MCONS (X Y) (LIST 'CONS X Y))
 
155
(defmacro MEQUAL (X Y) (LIST 'EQUAL X Y))
 
156
 
 
157
(defun MAPPEND (x y)
 
158
  (declare (xargs :guard t))
 
159
  (cond ((atom x) y)
 
160
        (t (cons (car x)
 
161
                 (MAPPEND (cdr x) y)))))
 
162
 
 
163
(defun MMEMBER (x l)
 
164
  (declare (xargs :guard t))
 
165
  (cond ((atom l) nil)
 
166
        ((equal x (car l)) l)
 
167
        (t (MMEMBER x (cdr l)))))
 
168
 
 
169
(defun MASSOC (x alist)
 
170
  (declare (xargs :guard t))
 
171
  (cond ((atom alist) nil)
 
172
        ((equal x (mcar (car alist))) (car alist))
 
173
        (t (MASSOC x (cdr alist)))))
 
174
 
 
175
(defun M+ (x y)
 
176
  (declare (xargs :guard t))
 
177
  (if (and (acl2-numberp x) (acl2-numberp y))
 
178
      (+ x y)
 
179
    (if (acl2-numberp x) x
 
180
      (if (acl2-numberp y) y
 
181
        0))))
 
182
 
 
183
(defun M- (x y)
 
184
  (declare (xargs :guard t))
 
185
  (if (and (acl2-numberp x) (acl2-numberp y))
 
186
      (- x y)
 
187
    (if (acl2-numberp x) x
 
188
      (if (acl2-numberp y) (- y)
 
189
        0))))
 
190
 
 
191
(defun M* (x y)
 
192
  (declare (xargs :guard t))
 
193
  (if (and (acl2-numberp x) (acl2-numberp y))
 
194
      (* x y)
 
195
    0))
 
196
 
 
197
;;---------------------------------------------------------------------------
 
198
;; As mentioned above, we now prove that the operators defined by functions
 
199
;; are actually as in ACL2, that is that they are equal to the corresponding
 
200
;; ACL2 functions. Then we disable them, because we don't want the prover to
 
201
;; look into our definitions but let it use what it knows about the original
 
202
;; ACL2 functions instead.
 
203
;;
 
204
 
 
205
(defthm mcar-is-like-car (equal (MCAR x) (car x)))
 
206
(defthm mcdr-is-like-cdr (equal (MCDR x) (cdr x)))
 
207
(defthm m1+-is-like-1+ (equal (M1+ n) (1+ n)))
 
208
(defthm m1--is-like-1- (equal (M1- n) (1- n)))
 
209
(defthm mappend-is-like-append (equal (MAPPEND x y) (append x y)))
 
210
(defthm mmember-is-like-member (equal (MMEMBER x l) (member x l)))
 
211
(defthm massoc-is-like-assoc (equal (MASSOC x alist) (assoc x alist)))
 
212
(defthm m+-is-like-+ (equal (M+ x y) (+ x y)))
 
213
(defthm m--is-like-- (equal (M- x y) (- x y)))
 
214
(defthm m*-is-like-* (equal (M* x y) (* x y)))
 
215
 
 
216
(in-theory (disable MCAR MCDR M1+ M1- M+ M* M- MAPPEND MMEMBER MASSOC))
 
217
 
 
218
 
 
219
;;---------------------------------------------------------------------------
 
220
;; The next is to define some data types, that is to say recognizers for
 
221
;; programs, declaration lists, instructions and instruction-lists, and
 
222
;; code. This is to be able to express the guards we want to verify. The
 
223
;; syntax of machine programs and of the code part of the machine's
 
224
;; configuration are as in the comment at the beginning of this book.
 
225
;;
 
226
 
 
227
(mutual-recursion
 
228
(defun instructionp (form)
 
229
  (declare (xargs :guard t))
 
230
  (and (consp form)
 
231
       (consp (cdr form))
 
232
       (cond ((equal (car form) 'PUSHC) t)
 
233
             ((equal (car form) 'PUSHV) (natp (cadr form)))
 
234
             ((equal (car form) 'CALL) (symbolp (cadr form)))
 
235
             ((equal (car form) 'OPR) (symbolp (cadr form)))
 
236
             ((equal (car form) 'POP) (natp (cadr form)))
 
237
             ((equal (car form) 'IF)
 
238
              (and (consp (cdr form))
 
239
                   (instruction-listp (cadr form))
 
240
                   (consp (cddr form))
 
241
                   (instruction-listp (caddr form))))
 
242
             (t nil))))
 
243
              
 
244
         
 
245
(defun instruction-listp (seq)
 
246
  (declare (xargs :guard t))
 
247
  (if (consp seq) 
 
248
    (and (instructionp (car seq))
 
249
         (instruction-listp (cdr seq)))
 
250
    (null seq)))
 
251
)
 
252
 
 
253
(defun codep (l)
 
254
  (declare (xargs :guard t))
 
255
  (cond ((atom l) (equal l nil))
 
256
        (t (and (consp (car l))
 
257
                (symbolp (caar l))
 
258
                (instruction-listp (cdar l))
 
259
                (codep (cdr l))))))       
 
260
 
 
261
(defun declsp (dcls)
 
262
  (declare (xargs :guard t))
 
263
  (if (consp dcls)
 
264
      (and (consp (car dcls))
 
265
           (equal (caar dcls) 'DEFCODE)
 
266
           (consp (cdar dcls))
 
267
           (symbolp (cadar dcls))
 
268
           (consp (cddar dcls))
 
269
           (instruction-listp (caddar dcls))
 
270
           (declsp (cdr dcls)))
 
271
    (null dcls)))
 
272
 
 
273
(defun progp (prog)
 
274
  (declare (xargs :guard t))
 
275
  (and (true-listp prog)
 
276
       (declsp (butlst prog))
 
277
       (instruction-listp (car (last prog)))))
 
278
 
 
279
;;---------------------------------------------------------------------------
 
280
;; The function get-code returns the instruction list associated with f within
 
281
;; "code".
 
282
;;
 
283
 
 
284
(defun get-code (f code) 
 
285
  (declare (xargs :guard (and (symbolp f) (alistp code))))
 
286
  (cdr (assoc f code)))
 
287
 
 
288
 
 
289
;;---------------------------------------------------------------------------
 
290
;; We need the following three theorems in order to be able to verify the
 
291
;; guards.
 
292
;;
 
293
 
 
294
(defthm codep-implies-good-code
 
295
  (implies (codep l) (instruction-listp (cdr (assoc f l)))))
 
296
(defthm codep-implies-alistp
 
297
  (implies (codep code) (alistp code)))
 
298
(defthm codep-implies-consp-assoc
 
299
  (implies (and (codep l) (assoc sym l)) (consp (assoc sym l))))
 
300
 
 
301
 
 
302
;;===========================================================================
 
303
;; Now we may start and define the machine. opr applies an operator to the
 
304
;; topmost stack cell(s), mstep executes one instruction, msteps an
 
305
;; instruction sequence (see the comment at the beginning of this script).
 
306
;;
 
307
 
 
308
(defun opr (op code stack)
 
309
  (declare (ignore code)
 
310
           (xargs :guard (true-listp stack)))
 
311
  (cond 
 
312
   ((equal op 'CAR) (cons (MCAR (car stack)) (cdr stack)))
 
313
   ((equal op 'CDR) (cons (MCDR (car stack)) (cdr stack)))
 
314
   ((equal op 'CADR) (cons (MCADR (car stack)) (cdr stack)))
 
315
   ((equal op 'CADDR) (cons (MCADDR (car stack)) (cdr stack)))
 
316
   ((equal op 'CADAR) (cons (MCADAR (car stack)) (cdr stack)))
 
317
   ((equal op 'CADDAR) (cons (MCADDAR (car stack)) (cdr stack)))
 
318
   ((equal op 'CADDDR) (cons (MCADDDR (car stack)) (cdr stack)))
 
319
   ((equal op '1-) (cons (M1- (car stack)) (cdr stack)))
 
320
   ((equal op '1+) (cons (M1+ (car stack)) (cdr stack)))
 
321
   ((equal op 'LEN) (cons (MLEN (car stack)) (cdr stack)))
 
322
   ((equal op 'SYMBOLP) (cons (MSYMBOLP (car stack)) (cdr stack)))
 
323
   ((equal op 'CONSP) (cons (MCONSP (car stack)) (cdr stack)))
 
324
   ((equal op 'ATOM) (cons (MATOM (car stack)) (cdr stack)))
 
325
   ((equal op 'CONS) (cons (MCONS (cadr stack) (car stack)) (cddr stack)))
 
326
   ((equal op 'EQUAL) (cons (MEQUAL (cadr stack) (car stack)) (cddr stack)))
 
327
   ((equal op 'APPEND) (cons (MAPPEND (cadr stack) (car stack)) (cddr stack)))
 
328
   ((equal op 'MEMBER) (cons (MMEMBER (cadr stack) (car stack)) (cddr stack)))
 
329
   ((equal op 'ASSOC) (cons (MASSOC (cadr stack) (car stack)) (cddr stack)))
 
330
   ((equal op '+) (cons (M+ (cadr stack) (car stack)) (cddr stack)))
 
331
   ((equal op '-) (cons (M- (cadr stack) (car stack)) (cddr stack)))
 
332
   ((equal op '*) (cons (M* (cadr stack) (car stack)) (cddr stack)))
 
333
   ((equal op 'LIST1) (cons (CONS (car stack) nil) (cdr stack)))
 
334
   ((equal op 'LIST2) (cons (CONS (cadr stack) (CONS (car stack) nil)) (cddr stack)))
 
335
   ))
 
336
 
 
337
 
 
338
(mutual-recursion
 
339
 
 
340
(defun mstep (form code stack n)
 
341
  (declare (xargs :measure (cons (1+ (acl2-count n)) (acl2-count form))
 
342
                  :guard (and (instructionp form) (codep code) (natp n))))
 
343
  (cond 
 
344
   ((or (zp n) (not (true-listp stack))) 'ERROR)
 
345
   ((equal (car form) 'PUSHC) (cons (cadr form) stack))
 
346
   ((equal (car form) 'PUSHV) (cons (nth (cadr form) stack) stack))
 
347
   ((equal (car form) 'CALL) 
 
348
    (msteps (cdr (assoc (cadr form) code)) code stack (1- n)))
 
349
   ((equal (car form) 'OPR) (opr (cadr form) code stack))
 
350
   ((equal (car form) 'IF)
 
351
    (if (car stack)
 
352
        (msteps (cadr form) code (cdr stack) n)
 
353
      (msteps (caddr form) code (cdr stack) n)))
 
354
   ((equal (car form) 'POP) (cons (car stack) (nthcdr (cadr form) (cdr stack))))))
 
355
 
 
356
(defun msteps (seq code stack n)
 
357
  (declare (xargs :measure (cons (1+ (acl2-count n)) (acl2-count seq))
 
358
                  :guard (and (instruction-listp seq) (codep code) (natp n))))
 
359
 
 
360
  (cond ((or (zp n) (not (true-listp stack))) 'ERROR)
 
361
        ((endp seq) stack)
 
362
        (t (msteps (cdr seq) code (mstep (car seq) code stack n) n))))
 
363
 
 
364
)
 
365
 
 
366
;;---------------------------------------------------------------------------
 
367
;; In order to download a machine program's subroutine definitions we have to
 
368
;; construct the code part of the machine configuration, which is a true
 
369
;; association list binding the procedure names to their instruction
 
370
;; sequences. That is we have get rid of the DEFCODE's and construct a true
 
371
;; association list:
 
372
;;
 
373
;;    ((DEFCODE f1 code1) (DEFCODE f2 code2) ...)  -> 
 
374
;;    ((f1 . code1) (f2 . code2) ...)
 
375
;;
 
376
 
 
377
(defun download (dcls)
 
378
  (declare (xargs :guard (declsp dcls)))
 
379
  (if (consp dcls)
 
380
      (cons (cons (cadar dcls) (caddar dcls)) 
 
381
            (download (cdr dcls)))
 
382
    nil))
 
383
 
 
384
;;---------------------------------------------------------------------------
 
385
;; Execution of an abstract machine program is executing the top level
 
386
;; instruction sequence with the code (download (butlast prog 1)) and the
 
387
;; initial stack.
 
388
;;
 
389
 
 
390
(defun execute (prog stack n)
 
391
  (declare (xargs :guard (and (progp prog) (natp n))))
 
392
  (let ((code (download (butlst prog))))
 
393
    (msteps (car (last prog)) code stack n)))
 
394
 
 
395
;;===========================================================================
 
396
;;
 
397
;; This finishes the definition of the abstract machine.
 
398
;;
 
399
;; The following two theorems install the definitional equations of "mstep"
 
400
;; and "msteps" from the above mutual recursion as :definition rules.
 
401
;;
 
402
;;---------------------------------------------------------------------------
 
403
 
 
404
(defthm msteps-eqn 
 
405
  (equal (msteps seq code stack n) 
 
406
         (cond ((or (zp n) (not (true-listp stack))) 'ERROR)
 
407
               ((endp seq) stack)
 
408
               (t (msteps 
 
409
                   (cdr seq) code (mstep (car seq) code stack n) n))))
 
410
  :rule-classes ((:definition 
 
411
                  :clique (mstep msteps) 
 
412
                  :controller-alist 
 
413
                  ((msteps t nil nil nil) (mstep t nil nil nil)))))
 
414
 
 
415
 
 
416
(defthm mstep-eqn 
 
417
  (equal (mstep form code stack n) 
 
418
         (cond 
 
419
   ((or (zp n) (not (true-listp stack))) 'ERROR)
 
420
   ((equal (car form) 'PUSHC) (cons (cadr form) stack))
 
421
   ((equal (car form) 'PUSHV) (cons (nth (cadr form) stack) stack))
 
422
   ((equal (car form) 'CALL) 
 
423
    (msteps (cdr (assoc (cadr form) code)) code stack (1- n)))
 
424
   ((equal (car form) 'OPR) (opr (cadr form) code stack))
 
425
   ((equal (car form) 'IF)
 
426
    (if (car stack)
 
427
        (msteps (cadr form) code (cdr stack) n)
 
428
      (msteps (caddr form) code (cdr stack) n)))
 
429
   ((equal (car form) 'POP) 
 
430
    (cons (car stack) (nthcdr (cadr form) (cdr stack))))))
 
431
  :rule-classes ((:definition 
 
432
                  :clique (mstep msteps) 
 
433
                  :controller-alist 
 
434
                  ((msteps t nil nil nil) (mstep t nil nil nil)))))
 
435
 
 
436
 
 
437
;;---------------------------------------------------------------------------
 
438
;; Now, we may disable mstep and msteps.
 
439
;;
 
440
 
 
441
(in-theory (disable mstep msteps))
 
442
 
 
443
;;---------------------------------------------------------------------------
 
444
;; The following function is used to suggest a combined computational and
 
445
;; structural induction on the termination argument n and the structural depth
 
446
;; of machine instructions and machine instruction sequences.
 
447
;;
 
448
 
 
449
(defun machine-induction (flag x code stack n)
 
450
  (declare (xargs :mode :logic
 
451
                  :measure (cons (1+ (acl2-count n)) (acl2-count x))))
 
452
  (if (or (atom x) (zp n))
 
453
      (list code stack n)
 
454
    (if flag
 
455
        (if (equal (car x) 'CALL)
 
456
            (machine-induction nil 
 
457
                               (cdr (assoc (cadr x) code))
 
458
                               code stack (1- n))
 
459
          (if (equal (car x) 'IF)
 
460
              (list (machine-induction nil 
 
461
                                       (cadr x) 
 
462
                                       code (cdr stack) n)
 
463
                    (machine-induction nil 
 
464
                                       (caddr x) 
 
465
                                       code (cdr stack) n))
 
466
            (list code stack n)))
 
467
      (list (machine-induction t (car x) code stack n)
 
468
            (machine-induction nil (cdr x) 
 
469
                               code 
 
470
                               (mstep (car x) code stack n)
 
471
                               n)))))
 
472
          
 
473
                    
 
474
 
 
475
 
 
476
 
 
477
 
 
478
 
 
479
 
 
480