Event: Start with the library "c4".

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                     %Mapping Call Parameters                       ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: mg-to-p-local-values (locals) = if locals ≃ nil then nil

elseif simple-mg-type-refp (cadr (car (locals)))

then cons (mg-to-p-simple-literal (caddr (car (locals))), mg-to-p-local-values (cdr (locals))) else append (mg-to-p-simple-literal-list (caddr (car (locals))),

mg-to-p-local-values (cdr (locals))) endif

Theorem: mg-to-p-local-values-plistp plistp (mg-to-p-local-values (lst))

;; Given a list of formals with the call site actuals, this gives the list for the new stack
;; frame.  Each of the actuals is guaranteed to be an identifier and each of these is in
;; the previous frame with the address of the value in my-stack.  Thus, I need only copy
;; these addresses into the current frame.

Definition: map-call-formals (formals, actuals, bindings) = if formals ≃ nil then nil

else cons (cons (car (car (formals)),

cdr (assoc (car (actuals), bindings))), map-call-formals (cdr (formals), cdr (actuals), bindings)) endif

Theorem: length-map-call-formals length (map-call-formals (formals, actuals, bindings)) = length (formals)

Theorem: map-call-formals-plistp plistp (map-call-formals (x, y, z))

Theorem: listcars-map-call-formals listcars (map-call-formals (formals, actuals, bindings)) = listcars (formals)

;; Each of the local values is placed onto the temp-stk, then the indexes into
;; the stack are placed there as well.  The distance of the value from the index

;; depends on the size of the elements between.
;; The initial value of n is (length temp-stk)

Definition: map-call-locals (locals, n) = if locals ≃ nil then nil

elseif simple-mg-type-refp (cadr (car (locals))) then cons (cons (car (car (locals)), tag ('nat, n)),

map-call-locals (cdr (locals), 1 + n))

else cons (cons (car (car (locals)), tag ('nat, n)), map-call-locals (cdr (locals),

array-length (cadr (car (locals))) + n)) endif

Theorem: length-map-call-locals length (map-call-locals (locals, n)) = length (locals)

Theorem: map-call-locals-plistp plistp (map-call-locals (locals, n))

Theorem: map-call-locals-preserves-listcars listcars (map-call-locals (locals, m)) = listcars (locals)

;; The topmost frame on the ctrl-stk at the beginning of the body of the proc-call
;; contains the p-formals which represent both the formals and locals of the mg
;; subroutine.  The formals have the values of the actuals in the previous frame
;; and these are guaranteed to be addresses into the temp-stk.  The locals have been
;; placed on the temp-stk as well and the address computed for this frame are those
;; locations.  Thus, upon entry the following invariant is established: every local
;; (in the frame) contains an index into the temp-stk which contains the corresponding
;; value.

Definition: make-frame-alist (def , stmt, ctrl-stk, temp-stk) = append (map-call-locals (def-locals (def ), length (temp-stk)),

map-call-formals (def-formals (def ), call-actuals (stmt), bindings (top (ctrl-stk))))

Definition: mg-actuals-to-p-actuals (mg-actuals, bindings) = if mg-actuals ≃ nil then nil

else cons (cdr (assoc (car (mg-actuals), bindings)), mg-actuals-to-p-actuals (cdr (mg-actuals), bindings)) endif Theorem: length-mg-actuals-to-p-actuals length (mg-actuals-to-p-actuals (mg-actuals, bindings)) = length (mg-actuals)

Theorem: mg-actuals-to-p-actuals-plistp plistp (mg-actuals-to-p-actuals (actuals, bindings))

;; %mapping call parameters
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                            THE TRANSLATOR                                 ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Event: Add the shell make-cinfo, with recognizer function symbol cinfop and 3 accessors: code, with type restriction (none-of) and default value zero; labelalist, with type restriction (none-of) and default value zero; label-cnt, with type restriction (one-of numberp) and default value zero.

Definition: nullify (cinfo) = make-cinfo (nil, label-alist (cinfo), label-cnt (cinfo))

Definition: add-code (cinfo, code) = make-cinfo (append (code (cinfo), code),

label-alist (cinfo), label-cnt (cinfo))

Definition: discard-label (cinfo) = make-cinfo (code (cinfo), cdr (label-alist (cinfo)), label-cnt (cinfo))

Definition: set-label-alist (cinfo, new-label-alist) = make-cinfo (code (cinfo), new-label-alist, label-cnt (cinfo))

;; Notice that I could simply use the VALUE function directly.

Definition: fetch-label (condition, label-alist) = cdr (assoc (condition, label-alist))

;; If this definition stays unchanged, I can eliminate it entirely in favor of the
;; simpler hyp on code.

Definition: ok-cinfop (cinfo) = plistp (code (cinfo))

;; Given a list (x1 ... xn) and a label l, this generated the list
;; ((x1 . l) (x2 . l) ... (xn . l)).  Notice that this allows that use
;; of the VALUE function for accessing the label.

Definition: make-label-alist (name-list, label) = if name-list ≃ nil then nil

else cons (cons (car (name-list), label), make-label-alist (cdr (name-list), label)) endif

Definition: push-local-array-values-code (array-value) = if array-value ≃ nil then nil

else cons (list ('push-constant,

mg-to-p-simple-literal (car (array-value))), push-local-array-values-code (cdr (array-value))) endif

Theorem: length-push-local-array-values-code length (push-local-array-values-code (array-value)) = length (array-value)

Theorem: length-push-local-array-values-code2 (ok-mg-local-data-decl (local) ∧ (¬ simple-mg-type-refp (cadr (local)))) → (array-length (cadr (local)) = length (caddr (local)))

Event: Disable length-push-local-array-values-code2.

Definition: push-locals-values-code (locals) = if locals ≃ nil then nil

elseif simple-mg-type-refp (cadr (car (locals)))

then cons (list ('push-constant,

mg-to-p-simple-literal (caddr (car (locals)))), push-locals-values-code (cdr (locals))) else append (push-local-array-values-code (caddr (car (locals))),

push-locals-values-code (cdr (locals))) endif

Theorem: length-push-locals-values-code ok-mg-local-data-plistp (locals) → (length (push-locals-values-code (locals)) = data-length (locals))

Theorem: length-mg-to-p-local-values ok-mg-local-data-plistp (locals) → (length (mg-to-p-local-values (locals)) = data-length (locals))

Theorem: no-labels-in-push-local-array-values-code find-labelp (n, push-local-array-values-code (value)) = f

Theorem: no-labels-in-push-locals-values-code find-labelp (n, push-locals-values-code (actuals)) = f

Definition: push-locals-addresses-code (locals, n) = if locals ≃ nil then nil

elseif simple-mg-type-refp (cadr (car (locals)))

    then cons (list ('push-temp-stk-index, n),

push-locals-addresses-code (cdr (locals), n))

    else cons (list ('push-temp-stk-index, n),

push-locals-addresses-code (cdr (locals), 1 + (n − array-length (cadr (car (locals)))))) endif

Theorem: length-push-locals-addresses-code length (push-locals-addresses-code (locals, n)) = length (locals)

Theorem: no-labels-in-push-locals-addresses-code find-labelp (n, push-locals-addresses-code (actuals, m)) = f

Definition: push-actuals-code (actuals) = if actuals ≃ nil then nil

else cons (list ('push-local, car (actuals)), push-actuals-code (cdr (actuals))) endif

Theorem: no-labels-in-push-actuals-code find-labelp (n, push-actuals-code (actuals)) = f

Theorem: length-push-actuals-code length (push-actuals-code (actuals)) = length (actuals)

Definition: push-parameters-code (locals, actuals) = append (push-locals-values-code (locals),

append (push-locals-addresses-code (locals,

data-length (locals) − 1),

push-actuals-code (actuals)))

Theorem: length-push-parameters-code ok-mg-local-data-plistp (locals) → (length (push-parameters-code (locals, actuals))

= (data-length (locals) + length (locals) + length (actuals)))

;; COMPILING THE CONDITION MAPPING
;;
;; Generate the list '(lc lc+1 lc+2 ... lc+n-1).  These are the labels
;; necessary for the condition computation jumps.

Definition: cond-case-jump-label-list (lc, n) = if n ≃ 0 then nil

else cons (lc, cond-case-jump-label-list (1 + lc, n − 1)) endif

Theorem: length-cond-case-jump-label-list length (cond-case-jump-label-list (lc, n)) = fix (n)

Definition: index-cond-case-induction-hint (i, j , k) = if k ≃ 0 then t

else index-cond-case-induction-hint (i − 1, 1 + j , k − 1) endif

Theorem: get-cond-case-jump-label-list ((i < k) ∧ (j ∈ N)) → (get (i, cond-case-jump-label-list (j , k)) = (i + j ))

Event: Disable get-cond-case-jump-label-list.

Definition: cond-conversion (actual-conds, lc, cond-list, label-alist) = if actual-conds ≃ nil then nil

else cons (list ('dl, lc, nil,

                list ('push-constant,

mg-cond-to-p-nat (car (actual-conds),

cond-list))),

            cons ('(pop-global c-c),

cons (list ('jump,

fetch-label (car (actual-conds), label-alist)),

cond-conversion (cdr (actual-conds), 1 + lc, cond-list, label-alist)))) endif

Theorem: length-cond-conversion length (cond-conversion (call-conds, lc, cond-list, label-alist)) = (3 ∗ length (call-conds))

Definition: label-cnt-list (lc, n) = if n ≃ 0 then nil

else cons (lc, label-cnt-list (lc, n − 1)) endif

Theorem: length-label-cnt-list length (label-cnt-list (lc, n)) = fix (n)

;; I must make sure that the condition index is in-range.  I can do this by using the def-conds as
;; the list to index rather than the make-cond-list.
;; This was changed slightly to add two additional condition onto the front of the list.  This is
;; because the condition index for 'normal is not zero any longer, but is now two.  Consequently, if
;; I'm going to use the condition index as an index into the cond-case-jump-label-list, I must either
;; decrement it twice or kludge the list structure.  I simply add the label for 'routineerror twice
;; at the beginning.

Definition: condition-map-code (actual-conds, lc, cond-list, label-alist, proc-locals-lngth) = append (list (list ('push-global, 'c-c),

append (cons ('jump-case,

cons (lc,

cons (lc,

cond-case-jump-label-list (1 + lc,

1 + length (actual-conds))))),

label-cnt-list (lc, proc-locals-lngth)),

              list ('dl, lc, nil, '(push-constant (nat 1))),
              '(pop-global c-c),

list ('jump, fetch-label ('routineerror, label-alist))), append (cond-conversion (actual-conds,

1 + (1 + lc), cond-list, label-alist),

list (list ('dl, 1 + lc, nil, '(no-op)))))

Definition: proc-call-code (cinfo, stmt, cond-list, locals, cond-locals-lngth) = append (push-parameters-code (locals, call-actuals (stmt)),

cons (list ('call, call-name (stmt)),

condition-map-code (call-conds (stmt), label-cnt (cinfo), cond-list, label-alist (cinfo), cond-locals-lngth)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                   %Compiling the Predefineds                       ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; The following functions define the sequence of statements laid
;; down for a call to a predefined procedure.

Definition: mg-simple-variable-assignment-call-sequence (stmt) = list (list ('push-local, car (call-actuals (stmt))),

list ('push-local, cadr (call-actuals (stmt))),

       '(call mg-simple-variable-assignment))

Definition: mg-simple-constant-assignment-call-sequence (stmt) = list (list ('push-local, car (call-actuals (stmt))),

       list ('push-constant,

mg-to-p-simple-literal (cadr (call-actuals (stmt)))),

       '(call mg-simple-constant-assignment))

Definition: mg-simple-variable-eq-call-sequence (stmt) = list (list ('push-local, car (call-actuals (stmt))),

list ('push-local, cadr (call-actuals (stmt))), list ('push-local, caddr (call-actuals (stmt))),

       '(call mg-simple-variable-eq))

Definition: mg-simple-constant-eq-call-sequence (stmt) = list (list ('push-local, car (call-actuals (stmt))),

list ('push-local, cadr (call-actuals (stmt))),

       list ('push-constant,

mg-to-p-simple-literal (caddr (call-actuals (stmt)))),

       '(call mg-simple-constant-eq))

Definition: mg-integer-le-call-sequence (stmt) = list (list ('push-local, car (call-actuals (stmt))),

list ('push-local, cadr (call-actuals (stmt))), list ('push-local, caddr (call-actuals (stmt))),

       '(call mg-integer-le))

Definition: mg-integer-unary-minus-call-sequence (stmt, label-alist) = list (list ('push-local, car (call-actuals (stmt))),

list ('push-local, cadr (call-actuals (stmt))),

'(call mg-integer-unary-minus),
'(push-global c-c),
'(sub1-nat),
list ('test-nat-and-jump,
    'zero,

fetch-label ('routineerror, label-alist)))

Definition: mg-integer-add-call-sequence (stmt, label-alist) = list (list ('push-local, car (call-actuals (stmt))),

list ('push-local, cadr (call-actuals (stmt))), list ('push-local, caddr (call-actuals (stmt))),

'(call mg-integer-add),
'(push-global c-c),
'(sub1-nat),
list ('test-nat-and-jump,
    'zero,

fetch-label ('routineerror, label-alist)))

Definition: mg-integer-subtract-call-sequence (stmt, label-alist) = list (list ('push-local, car (call-actuals (stmt))),

list ('push-local, cadr (call-actuals (stmt))), list ('push-local, caddr (call-actuals (stmt))),

'(call mg-integer-subtract),
'(push-global c-c),
'(sub1-nat),
list ('test-nat-and-jump,
    'zero,

fetch-label ('routineerror, label-alist)))

Definition: mg-boolean-or-call-sequence (stmt) = list (list ('push-local, car (call-actuals (stmt))),

list ('push-local, cadr (call-actuals (stmt))), list ('push-local, caddr (call-actuals (stmt))),

'(call mg-boolean-or))

Definition: mg-boolean-and-call-sequence (stmt) = list (list ('push-local, car (call-actuals (stmt))), list ('push-local, cadr (call-actuals (stmt))), list ('push-local, caddr (call-actuals (stmt))),

'(call mg-boolean-and))

Definition: mg-boolean-not-call-sequence (stmt) = list (list ('push-local, car (call-actuals (stmt))),

list ('push-local, cadr (call-actuals (stmt))),

'(call mg-boolean-not))
;; The 4th argument is a numberp supplied by the pre-processor which is
;; the size of the array.  This is necessary for bounds checking.
;; >> Do I need to guarantee that it is a small-integerp?

Definition: mg-index-array-call-sequence (stmt, label-alist) = list (list ('push-local, car (call-actuals (stmt))),

list ('push-local, cadr (call-actuals (stmt))), list ('push-local, caddr (call-actuals (stmt))), list ('push-constant, tag ('int, cadddr (call-actuals (stmt)))),

'(call mg-index-array),
'(push-global c-c),
'(sub1-nat),
list ('test-nat-and-jump,
    'zero,

fetch-label ('routineerror, label-alist)))

Definition: mg-array-element-assignment-call-sequence (stmt, label-alist) = list (list ('push-local, car (call-actuals (stmt))),

list ('push-local, cadr (call-actuals (stmt))), list ('push-local, caddr (call-actuals (stmt))), list ('push-constant, tag ('int, cadddr (call-actuals (stmt)))),

'(call mg-array-element-assignment),
'(push-global c-c),
'(sub1-nat),
list ('test-nat-and-jump,
    'zero,

fetch-label ('routineerror, label-alist)))

Definition: predefined-proc-call-sequence (stmt, label-alist) = case on call-name (stmt):

case = mg-simple-variable-assignment then mg-simple-variable-assignment-call-sequence (stmt) case = mg-simple-constant-assignment then mg-simple-constant-assignment-call-sequence (stmt) case = mg-simple-variable-eq then mg-simple-variable-eq-call-sequence (stmt) case = mg-simple-constant-eq then mg-simple-constant-eq-call-sequence (stmt) case = mg-integer-le then mg-integer-le-call-sequence (stmt) case = mg-integer-unary-minus then mg-integer-unary-minus-call-sequence (stmt, label-alist) case = mg-integer-add then mg-integer-add-call-sequence (stmt, label-alist) case = mg-integer-subtract then mg-integer-subtract-call-sequence (stmt, label-alist) case = mg-boolean-or then mg-boolean-or-call-sequence (stmt) case = mg-boolean-and then mg-boolean-and-call-sequence (stmt) case = mg-boolean-not then mg-boolean-not-call-sequence (stmt) case = mg-index-array then mg-index-array-call-sequence (stmt, label-alist) case = mg-array-element-assignment then mg-array-element-assignment-call-sequence (stmt, label-alist) otherwise nil endcase

Event: Disable predefined-proc-call-sequence.

;; We now consider the bodies of the predefined routines.

Definition: mg-simple-variable-assignment-translation

= '(mg-simple-variable-assignment
  (dest source)
  nil
  (push-local source)
  (fetch-temp-stk)
  (push-local dest)
  (deposit-temp-stk)
  (ret))

Definition: mg-simple-constant-assignment-translation

= '(mg-simple-constant-assignment
(dest source)
nil
(push-local source)
(push-local dest)
(deposit-temp-stk)
(ret))
;; >>> Notice that deposit-temp-stk is different from my old deposit-temp
;;     in the order of args on the stack.  THESE WILL ALL HAVE TO CHANGE.

Definition: mg-simple-variable-eq-translation

= '(mg-simple-variable-eq
(ans x y)
nil
(push-local x)
(fetch-temp-stk)
(push-local y)
(fetch-temp-stk)
(eq)
(push-local ans)
(deposit-temp-stk)
(ret))

Definition: mg-simple-constant-eq-translation

= '(mg-simple-constant-eq
(ans x y)
nil
(push-local x)
(fetch-temp-stk)
(push-local y)
(eq)
(push-local ans)
(deposit-temp-stk)
(ret))

Definition: mg-integer-le-translation

= '(mg-integer-le
(ans x y)
nil

(push-local y)
(fetch-temp-stk)
(push-local x)
(fetch-temp-stk)
(lt-int)
(not-bool)
(push-local ans)
(deposit-temp-stk)
(ret))
;; Since the representable positives and negatives are not
;; exactly complementary, I must check that the integer in question
;; is not that exact negative which would cause a problem.

Definition: mg-integer-unary-minus-translation

= '(mg-integer-unary-minus
(ans x)
((min-int (int -2147483648)) (temp-x (int 0)))
(push-local x)
(fetch-temp-stk)
(set-local temp-x)
(push-local min-int)
(eq)
(test-bool-and-jump f 0)
(push-constant (nat 1))
(pop-global c-c)
(jump 1)
(dl 0 nil (push-local temp-x))
(neg-int)
(push-local ans)
(deposit-temp-stk)
(dl 1 nil (ret)))

Definition: mg-integer-add-translation

= '(mg-integer-add
(ans y z)
((t1 (int 0)))
(push-constant (bool f))
(push-local y)
(fetch-temp-stk)
(push-local z)
(fetch-temp-stk)

(add-int-with-carry)
(pop-local t1)
(test-bool-and-jump t 0)
(push-local t1)
(push-local ans)
(deposit-temp-stk)
(jump 1)
(dl 0 nil (push-constant (nat 1)))
(pop-global c-c)
(dl 1 nil (ret)))

Definition: mg-integer-subtract-translation

= '(mg-integer-subtract
(ans y z)
((t1 (int 0)))
(push-constant (bool f))
(push-local y)
(fetch-temp-stk)
(push-local z)
(fetch-temp-stk)
(sub-int-with-carry)
(pop-local t1)
(test-bool-and-jump t 0)
(push-local t1)
(push-local ans)
(deposit-temp-stk)
(jump 1)
(dl 0 nil (push-constant (nat 1)))
(pop-global c-c)
(dl 1 nil (ret)))

Definition: mg-boolean-or-translation

= '(mg-boolean-or
(ans b1 b2)
nil
(push-local b1)
(fetch-temp-stk)
(push-local b2)
(fetch-temp-stk)
(or-bool)
(push-local ans)
(deposit-temp-stk)
(ret))

Definition: mg-boolean-and-translation

= '(mg-boolean-and
(ans b1 b2)
nil
(push-local b1)
(fetch-temp-stk)
(push-local b2)
(fetch-temp-stk)
(and-bool)
(push-local ans)
(deposit-temp-stk)
(ret))

Definition: mg-boolean-not-translation

= '(mg-boolean-not
(ans b1)
nil
(push-local b1)
(fetch-temp-stk)
(not-bool)
(push-local ans)
(deposit-temp-stk)
(ret))
;; ans := A[i] of size
;; How do I know that the sub-nat to compute the index doesn't give an error?

Definition: mg-index-array-translation

= '(mg-index-array
(ans a i array-size)
((temp-i (nat 0)))
(push-local i)
(fetch-temp-stk)
(set-local temp-i)
(test-int-and-jump neg 0)
(push-local array-size)
(push-local temp-i)
(sub-int)
(test-int-and-jump not-pos 0)
(push-local a)
(push-local temp-i)

(int-to-nat)
(add-nat)
(fetch-temp-stk)
(push-local ans)
(deposit-temp-stk)
(jump 1)
(dl 0 nil (push-constant (nat 1)))
(pop-global c-c)
(dl 1 nil (ret)))
;; (mg-array-element-assignment A i value size)

Definition: mg-array-element-assignment-translation

= '(mg-array-element-assignment
(a i value array-size)
((temp-i (nat 0)))
(push-local i)
(fetch-temp-stk)
(set-local temp-i)
(test-int-and-jump neg 0)
(push-local array-size)
(push-local temp-i)
(sub-int)
(test-int-and-jump not-pos 0)
(push-local value)
(fetch-temp-stk)
(push-local a)
(push-local temp-i)
(int-to-nat)
(add-nat)
(deposit-temp-stk)
(jump 1)
(dl 0 nil (push-constant (nat 1)))
(pop-global c-c)
(dl 1 nil (ret)))
;; The list of translations of the predefined routines is appended
;; to the list of translations of the user-defined routines and
;; becomes the program segment of the Piton program.

Definition: predefined-procedure-translations-list = list (mg-simple-variable-assignment-translation,

mg-simple-constant-assignment-translation, mg-simple-variable-eq-translation, mg-simple-constant-eq-translation, mg-integer-le-translation, mg-integer-unary-minus-translation, mg-integer-add-translation, mg-integer-subtract-translation, mg-boolean-or-translation, mg-boolean-and-translation, mg-boolean-not-translation, mg-index-array-translation, mg-array-element-assignment-translation)

Event: Disable predefined-procedure-translations-list.

;; Insist that the condition on an IF statement is a variable.  This means that
;; it cannot be a boolean literal.  Hence the code for computing it is always.
;;   (push-local b)
;;   (fetch-temp-stk)
;; Otherwise, the number of statements would vary and I don't want to deal with that
;; now.  This is consistent with the convention for proc-calls.
;; Condition on an IF statement is either a boolean literal or the address of a
;; boolean in the my-stack array.
;; SIGNAL
;;
;;         (push-constant (nat n))            n is the index of condition in cond-list
;;         (pop-global c-c)
;;         (jump label)                       label is associated label of condition in label-alist
;;
;; PROG2
;;
;;         "code for left branch"
;;         "code for right branch"
;;
;;
;; LOOP
;;
;;          (dl l0 nil (no-op))
;;          "code for loop-body"
;;          (jump L0)
;;          (dl l1 nil (push-constant (nat 2)))

;;          (pop-global c-c)
;;
;; IF
;;
;;          (push-local b)
;;          (fetch-temp-stk)
;;          (test-bool-and-jump false L0)
;;          "code for true branch"
;;          (jump L1)
;;          (dl l0 nil (no-op))
;;          "code for false branch"
;;          (dl l1 nil (no-op))
;;
;; BEGIN-WHEN
;;
;;         "code for begin-body"
;;         (jump L1)
;;         (dl l0 nil (push-constant (nat 2)))
;;         (pop-global c-c)
;;         "code for when-arm-body"
;;         (dl l1 nil (no-op))
;;
;; PROC-CALL
;; For the statement
;;  (PROC-CALL-MG name (act1 act2 ... actj) (cond1 cond2 ... condn))
;; we make the following code.
;;    push-locals-values-code
;;    push-locals-addresses-code
;;    push actuals-code
;;    (call name)
;;    (push-global c-c)
;;    (case-jump (L0 L1 L2 ... Ln))
;;    (push-constant (nat 1))
;;    (pop-global c-c)
;;    (jump "label-for-routineerror")
;;    (dl l1 nil (push-constant "condition-number for cond1"))
;;    (pop-global c-c)
;;    (jump "label for cond1")
;;    (dl l2 nil (push-constant "condition-number for cond2"))
;;    (pop-global c-c)
;;    (jump "label for cond2")
;;        ...
;;    (dl ln nil (push-constant "condition-number for condn"))
;;    (pop-global c-c)

;;    (jump "label for condn")
;;    (dl l0 nil (no-op))
;;
;; PREDEFINED-PROC-CALL

Definition: translate (cinfo, cond-list, stmt, proc-list) = case on car (stmt):

case = no-op-mg then cinfo case = signal-mg then make-cinfo (append (code (cinfo),

                           list (list ('push-constant,

mg-cond-to-p-nat (signalled-condition (stmt), cond-list)),

                              list ('pop-global, 'c-c),

list ('jump,

fetch-label (signalled-condition (stmt),

label-alist (cinfo))))),

label-alist (cinfo), label-cnt (cinfo))

case = prog2-mg then translate (translate (cinfo,

cond-list,

prog2-left-branch (stmt), proc-list),

cond-list,

prog2-right-branch (stmt), proc-list)

case = loop-mg then discard-label (add-code (translate (make-cinfo (append (code (cinfo),

list (list ('dl, label-cnt (cinfo), nil,

                                                               '(no-op)))),

cons (cons ('leave,

1 + label-cnt (cinfo)), label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list,

loop-body (stmt), proc-list), list (list ('jump, label-cnt (cinfo)), list ('dl,

1 + label-cnt (cinfo), nil,

'(push-constant
(nat 2))),
'(pop-global c-c))))

case = if-mg then add-code (translate (add-code (translate (make-cinfo (append (code (cinfo),

                  list (list ('push-local,

if-condition (stmt)),

                      '(fetch-temp-stk),
                      list ('test-bool-and-jump,
                          'false,

label-cnt (cinfo)))),

label-alist (cinfo),

1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), list ('dl,

label-cnt (cinfo), nil,

'(no-op)))),

cond-list, if-false-branch (stmt), proc-list),

list (list ('dl, 1 + label-cnt (cinfo), nil, '(no-op))))

case = begin-mg then add-code (translate (add-code (set-label-alist (translate (make-cinfo (code (cinfo),

append (make-label-alist (when-labels (stmt),

label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list,

begin-body (stmt), proc-list),

label-alist (cinfo)),

list (list ('jump,

1 + label-cnt (cinfo)), list ('dl,

label-cnt (cinfo), nil,

   '(push-constant
     (nat 2))),
'(pop-global c-c))),

cond-list, when-handler (stmt), proc-list),

list (list ('dl, 1 + label-cnt (cinfo), nil, '(no-op))))

case = proc-call-mg then make-cinfo (append (code (cinfo),

proc-call-code (cinfo, stmt, cond-list, def-locals (fetch-called-def (stmt,

proc-list)),

length (def-cond-locals (fetch-called-def (stmt,

proc-list))))),

label-alist (cinfo), label-cnt (cinfo) + (1 + (1 + length (call-conds (stmt)))))

case = predefined-proc-call-mg then add-code (cinfo,

predefined-proc-call-sequence (stmt, label-alist (cinfo)))

otherwise cinfo endcase

Theorem: signal-translation (car (stmt) = 'signal-mg) → (translate (cinfo, cond-list, stmt, proc-list)

= make-cinfo (append (code (cinfo),

list (list ('push-constant,

mg-cond-to-p-nat (signalled-condition (stmt),

cond-list)),

list ('pop-global, 'c-c),

list ('jump,

fetch-label (signalled-condition (stmt),

label-alist (cinfo))))),

label-alist (cinfo), label-cnt (cinfo)))

Theorem: prog2-translation (car (stmt) = 'prog2-mg) → (translate (cinfo, cond-list, stmt, proc-list)

= translate (translate (cinfo, cond-list, prog2-left-branch (stmt),

proc-list),

cond-list,

prog2-right-branch (stmt), proc-list))

Theorem: loop-translation (car (stmt) = 'loop-mg) → (translate (cinfo, cond-list, stmt, proc-list)

= discard-label (add-code (translate (make-cinfo (append (code (cinfo),

list (list ('dl, label-cnt (cinfo), nil,

                                                             '(no-op)))),

cons (cons ('leave,

1 + label-cnt (cinfo)), label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list,

loop-body (stmt), proc-list), list (list ('jump, label-cnt (cinfo)),

list ('dl, 1 + label-cnt (cinfo), nil,

                                    '(push-constant
                                      (nat 2))),
                                '(pop-global c-c)))))

Theorem: if-translation (car (stmt) = 'if-mg) → (translate (cinfo, cond-list, stmt, proc-list)

= add-code (translate (add-code (translate (make-cinfo (append (code (cinfo),

                                                           list (list ('push-local,

if-condition (stmt)),

                                                               '(fetch-temp-stk),
                                                               list ('test-bool-and-jump,
                                                                   'false,

label-cnt (cinfo)))),

label-alist (cinfo),

1 + (1 + label-cnt (cinfo))),

cond-list,

if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), list ('dl,

label-cnt (cinfo), nil,

'(no-op)))),

cond-list, if-false-branch (stmt), proc-list),

list (list ('dl, 1 + label-cnt (cinfo), nil, '(no-op)))))

Theorem: begin-translation (car (stmt) = 'begin-mg) → (translate (cinfo, cond-list, stmt, proc-list)

= add-code (translate (add-code (set-label-alist (translate (make-cinfo (code (cinfo),

append (make-label-alist (when-labels (stmt),

label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list,

begin-body (stmt), proc-list),

label-alist (cinfo)),

list (list ('jump,

1 + label-cnt (cinfo)), list ('dl,

label-cnt (cinfo), nil,

'(push-constant
  (nat 2))),
'(pop-global c-c))),

cond-list, when-handler (stmt), proc-list),

list (list ('dl, 1 + label-cnt (cinfo), nil, '(no-op)))))

Theorem: call-translation

(car (stmt) = 'proc-call-mg)

→ (translate (cinfo, cond-list, stmt, proc-list)

= make-cinfo (append (code (cinfo),

proc-call-code (cinfo, stmt, cond-list, def-locals (fetch-called-def (stmt,

proc-list)), length (def-cond-locals (fetch-called-def (stmt,

proc-list))))),

label-alist (cinfo), label-cnt (cinfo) + (1 + (1 + length (call-conds (stmt))))))

Theorem: predefined-call-translation

 (car (stmt) = 'predefined-proc-call-mg)

→ (translate (cinfo, cond-list, stmt, proc-list)

= add-code (cinfo,

predefined-proc-call-sequence (stmt, label-alist (cinfo))))

Event: Disable translate.

Theorem: predefined-proc-call-code-plistp plistp (predefined-proc-call-sequence (stmt, label-alist))

Theorem: not-find-labelp-predefined-proc-call-code find-labelp (n, predefined-proc-call-sequence (stmt, label-alist)) = f

;; COMPILATION OF A PROCEDURE
;;
;; Given a procedure def of the form
;; (procedure-defn-mg name (param1 ... paramn) (cond1 ... condi) (local1 ... localj)
;;                         (local-cond1 ... local-condk) body)
;; I make the code for the body in the context of the cinfo
;;   code: nil
;;   label-alist: ((cond1 . 0) (cond2 . 0) .... (local-cond1 . 0) ...)
;;   label-cnt: 1
;; The new scheme of transforming each of the MG locals into a formal of the Piton
;; subroutine eliminates the need to convert them within the code.  I hope it also
;; eliminates the need to store the stack pointer anywhere in the data-segment.

Definition: translate-def-body (proc-def , proc-list) = add-code (translate (make-cinfo (nil,

                              cons (cons ('routineerror, 0),

make-label-alist (make-cond-list (proc-def ), 0)),

1), make-cond-list (proc-def ), def-body (proc-def ), proc-list),

            list ('(dl 0 nil (no-op)),

list ('pop*, data-length (def-locals (proc-def ))),

                '(ret)))

Event: Disable translate-def-body.

;; Both the MG formals and locals become formals in the Piton world.  This is a better
;; approach because it allows for structured locals just as for structured formals.

Definition: translate-def (def , proc-list) = append (list (def-name (def ),

append (listcars (def-locals (def )),

listcars (def-formals (def ))), nil),

code (translate-def-body (def , proc-list)))

Definition: translate-proc-list1 (proc-list1 , proc-list2 ) = if proc-list1 ≃ nil then nil

else cons (translate-def (car (proc-list1 ), proc-list2 ), translate-proc-list1 (cdr (proc-list1 ), proc-list2 )) endif

Definition: translate-proc-list (proc-list) = append (predefined-procedure-translations-list,

translate-proc-list1 (proc-list, proc-list))

Event: Disable translate-proc-list.

Theorem: translate-preserves-fields label-alist (translate (cinfo, cond-list, stmt, proc-list)) = label-alist (cinfo)

Theorem: code-always-plistp plistp (code (cinfo)) → plistp (code (translate (cinfo, cond-list, stmt, proc-list)))

Theorem: translate-preserves-ok-cinfop ok-cinfop (cinfo) → ok-cinfop (translate (cinfo, cond-list, stmt, proc-list))

Event: Disable translate-preserves-ok-cinfop.

Definition: nearly-equal-cinfos (x, y) = ((label-alist (x) = label-alist (y))

∧ (label-cnt (x) = label-cnt (y)))

Theorem: nearly-equal-cinfos-translate (cinfop (cinfo1 ) ∧ cinfop (cinfo2 ) ∧ nearly-equal-cinfos (cinfo1 , cinfo2 )) → nearly-equal-cinfos (translate (cinfo1 , cond-list, stmt, proc-list),

translate (cinfo2 , cond-list, stmt, proc-list))

Event: Disable nearly-equal-cinfos-translate.

Theorem: nullify-translate-leaves-nearly-equal cinfop (cinfo) → nearly-equal-cinfos (translate (cinfo, cond-list, stmt, proc-list),

translate (nullify (cinfo), cond-list, stmt, proc-list))

Event: Disable nullify-translate-leaves-nearly-equal.

Theorem: nullify-translate-idempotence cinfop (cinfo) → (nullify (translate (nullify (cinfo), cond-list, stmt, proc-list))

= nullify (translate (cinfo, cond-list, stmt, proc-list)))

Event: Disable nullify-translate-idempotence.

Theorem: nullify-translate-idempotence2 cinfop (cinfo) → (nullify (translate (cinfo, cond-list, stmt, proc-list))

= nullify (translate (nullify (cinfo), cond-list, stmt, proc-list)))

Event: Disable nullify-translate-idempotence2.

Theorem: code-doesnt-affect-other-fields cinfop (cinfo) → ((label-alist (translate (cinfo, cond-list, stmt, proc-list))

= label-alist (translate (nullify (cinfo), cond-list, stmt, proc-list)))

∧ (label-cnt (translate (cinfo, cond-list, stmt, proc-list))

= label-cnt (translate (nullify (cinfo), cond-list, stmt, proc-list))))

Event: Disable code-doesnt-affect-other-fields.

Theorem: add-code-doesnt-affect-other-fields (label-alist (add-code (cinfo, code)) = label-alist (cinfo)) ∧ (label-cnt (add-code (cinfo, code)) = label-cnt (cinfo))

Theorem: set-label-alist-doesnt-affect-other-fields (code (set-label-alist (cinfo, label-alist)) = code (cinfo)) ∧ (label-cnt (set-label-alist (cinfo, label-alist)) = label-cnt (cinfo))

Theorem: discard-label-doesnt-affect-other-fields (code (discard-label (cinfo)) = code (cinfo)) ∧ (label-cnt (discard-label (cinfo)) = label-cnt (cinfo))

Theorem: nullify-cancels-add-code nullify (add-code (cinfo, code)) = nullify (cinfo)

Theorem: code-add-code-commute code (add-code (cinfo, cd)) = append (code (cinfo), cd)

Theorem: label-alist-set-label-alist label-alist (set-label-alist (state, label-alist)) = label-alist

Theorem: nullify-doesnt-affect-proc-call-code proc-call-code (nullify (cinfo), stmt, cond-list, locals, k) = proc-call-code (cinfo, stmt, cond-list, locals, k)

Theorem: nullify-code-nil code (nullify (cinfo)) = nil

Definition: nullify-induction-hint (cinfo, cond-list, stmt, proc-list) = case on car (stmt):

case = no-op-mg then t case = signal-mg then t case = prog2-mg then nullify-induction-hint (cinfo,

cond-list,

prog2-left-branch (stmt), proc-list)

∧ nullify-induction-hint (translate (cinfo, cond-list, prog2-left-branch (stmt), proc-list),

cond-list, prog2-right-branch (stmt), proc-list)

∧ nullify-induction-hint (translate (nullify (cinfo), cond-list, prog2-left-branch (stmt), proc-list),

cond-list, prog2-right-branch (stmt), proc-list)

case = loop-mg then nullify-induction-hint (make-cinfo (append (code (cinfo),

list (list ('dl, label-cnt (cinfo), nil,

                     '(no-op)))),

cons (cons ('leave,

1 + label-cnt (cinfo)), label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list, loop-body (stmt), proc-list)

∧ nullify-induction-hint (make-cinfo (list (list ('dl, label-cnt (cinfo), nil,

                 '(no-op))),

cons (cons ('leave,

1 + label-cnt (cinfo)), label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list, loop-body (stmt), proc-list)

case = if-mg then nullify-induction-hint (make-cinfo (list (list ('push-local,

if-condition (stmt)),

          '(fetch-temp-stk),
          list ('test-bool-and-jump,
              'false,

label-cnt (cinfo))), label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list)

∧ nullify-induction-hint (make-cinfo (append (code (cinfo),

                 list (list ('push-local,

if-condition (stmt)),

                     '(fetch-temp-stk),
                     list ('test-bool-and-jump,
                        'false,

label-cnt (cinfo)))),

label-alist (cinfo),

1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list)

∧ nullify-induction-hint (add-code (translate (make-cinfo (append (code (cinfo),

                                  list (list ('push-local,

if-condition (stmt)),

                                      '(fetch-temp-stk),
                                      list ('test-bool-and-jump,
                                         'false,

label-cnt (cinfo)))),

label-alist (cinfo),

1 + (1 + label-cnt (cinfo))),

cond-list,

if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), list ('dl,

label-cnt (cinfo),

nil,

                '(no-op)))),

cond-list, if-false-branch (stmt), proc-list)

∧ nullify-induction-hint (add-code (translate (make-cinfo (list (list ('push-local,

if-condition (stmt)),

                              '(fetch-temp-stk),
                              list ('test-bool-and-jump,
                                  'false,

label-cnt (cinfo))), label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list,

if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), list ('dl,

label-cnt (cinfo),

nil,

                '(no-op)))),

cond-list, if-false-branch (stmt), proc-list)

case = begin-mg then nullify-induction-hint (add-code (set-label-alist (translate (make-cinfo (code (cinfo),

append (make-label-alist (when-labels (stmt),

label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list,

begin-body (stmt), proc-list),

label-alist (cinfo)),

list (list ('jump,

1 + label-cnt (cinfo)), list ('dl,

label-cnt (cinfo),

nil,

            '(push-constant
              (nat 2))),
         '(pop-global c-c))),

cond-list, when-handler (stmt), proc-list)

∧ nullify-induction-hint (make-cinfo (code (cinfo),

append (make-label-alist (when-labels (stmt),

label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list, begin-body (stmt), proc-list)

∧ nullify-induction-hint (add-code (set-label-alist (translate (nullify (make-cinfo (code (cinfo),

append (make-label-alist (when-labels (stmt),

label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo)))),

cond-list,

begin-body (stmt), proc-list),

label-alist (cinfo)),

list (list ('jump,

1 + label-cnt (cinfo)), list ('dl,

label-cnt (cinfo), nil,

'(push-constant
  (nat 2))),
'(pop-global
c-c))),

cond-list, when-handler (stmt), proc-list)

case = proc-call-mg then t case = predefined-proc-call-mg then t otherwise f endcase

Theorem: new-code-prog2-case-induction-hyps ((car (stmt) = 'prog2-mg) ∧ ok-cinfop (cinfo)) → (ok-cinfop (translate (nullify (cinfo),

cond-list, prog2-left-branch (stmt), proc-list))

∧ ok-cinfop (translate (cinfo, cond-list, prog2-left-branch (stmt), proc-list)))

Event: Disable nullify.

Theorem: new-code-prog2-case ((car (stmt) = 'prog2-mg) ∧ ok-cinfop (cinfo) ∧ (ok-cinfop (translate (nullify (cinfo), cond-list, prog2-left-branch (stmt), proc-list))

→ (append (code (translate (nullify (cinfo), cond-list, prog2-left-branch (stmt), proc-list)),

code (translate (nullify (translate (nullify (cinfo), cond-list, prog2-left-branch (stmt), proc-list)),

cond-list, prog2-right-branch (stmt), proc-list)))

= code (translate (translate (nullify (cinfo), cond-list, prog2-left-branch (stmt), proc-list),

cond-list, prog2-right-branch (stmt), proc-list))))

∧ (ok-cinfop (translate (cinfo, cond-list, prog2-left-branch (stmt), proc-list))

→ (append (code (translate (cinfo, cond-list, prog2-left-branch (stmt), proc-list)),

code (translate (nullify (translate (cinfo, cond-list, prog2-left-branch (stmt), proc-list)),

cond-list, prog2-right-branch (stmt), proc-list)))

= code (translate (translate (cinfo, cond-list, prog2-left-branch (stmt), proc-list),

cond-list, prog2-right-branch (stmt), proc-list))))

∧ (ok-cinfop (cinfo)

→ (append (code (cinfo),

code (translate (nullify (cinfo), cond-list, prog2-left-branch (stmt), proc-list)))

= code (translate (cinfo, cond-list, prog2-left-branch (stmt), proc-list)))))

→ (append (code (cinfo),

code (translate (nullify (cinfo), cond-list, stmt, proc-list))) = code (translate (cinfo, cond-list, stmt, proc-list)))

Theorem: new-code-loop-case-induction-hyps ok-cinfop (cinfo) → (ok-cinfop (make-cinfo (list (cons ('dl,

cons (label-cnt (cinfo),

                                    '(nil (no-op))))),

cons (cons ('leave, 1 + label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))))

∧ ok-cinfop (make-cinfo (append (code (cinfo),

list (cons ('dl,

cons (label-cnt (cinfo),

                                               '(nil
                                                 (no-op)))))),

cons (cons ('leave, 1 + label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo)))))

Theorem: new-code-loop-case ((car (stmt) = 'loop-mg) ∧ ok-cinfop (cinfo) ∧ (ok-cinfop (make-cinfo (list (cons ('dl,

cons (label-cnt (cinfo),

                                     '(nil (no-op))))),

cons (cons ('leave, 1 + label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))))

→ (append (code (make-cinfo (list (cons ('dl,

cons (label-cnt (cinfo),

                                             '(nil (no-op))))),

cons (cons ('leave, 1 + label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo)))),

code (translate (nullify (make-cinfo (list (cons ('dl,

cons (label-cnt (cinfo),

                            '(nil
                              (no-op))))),

cons (cons ('leave,

1 + label-cnt (cinfo)), label-alist (cinfo)), 1 + (1 + label-cnt (cinfo)))),

cond-list, loop-body (stmt), proc-list)))

= code (translate (make-cinfo (list (cons ('dl,

cons (label-cnt (cinfo),

                  '(nil
                    (no-op))))),

cons (cons ('leave,

1 + label-cnt (cinfo)), label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list, loop-body (stmt), proc-list))))

∧ (ok-cinfop (make-cinfo (append (code (cinfo),

list (cons ('dl,

cons (label-cnt (cinfo),

            '(nil (no-op)))))),

cons (cons ('leave, 1 + label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))))

→ (append (code (make-cinfo (append (code (cinfo),

list (cons ('dl,

cons (label-cnt (cinfo),

                    '(nil
                      (no-op)))))),

cons (cons ('leave,

1 + label-cnt (cinfo)), label-alist (cinfo)),

1 + (1 + label-cnt (cinfo)))),

code (translate (nullify (make-cinfo (append (code (cinfo),

list (cons ('dl,

cons (label-cnt (cinfo),

                                   '(nil

                                      (no-op)))))),

cons (cons ('leave,

1 + label-cnt (cinfo)), label-alist (cinfo)), 1 + (1 + label-cnt (cinfo)))),

cond-list, loop-body (stmt), proc-list)))

= code (translate (make-cinfo (append (code (cinfo),

list (cons ('dl,

cons (label-cnt (cinfo),

                           '(nil
                             (no-op)))))),

cons (cons ('leave,

1 + label-cnt (cinfo)), label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list, loop-body (stmt), proc-list)))))

→ (append (code (cinfo),

code (translate (nullify (cinfo), cond-list, stmt, proc-list))) = code (translate (cinfo, cond-list, stmt, proc-list)))

Theorem: new-code-if-case-induction-hyps ok-cinfop (cinfo) → (ok-cinfop (add-code (translate (make-cinfo (list (list ('push-local,

if-condition (stmt)),

              '(fetch-temp-stk),
              list ('test-bool-and-jump,
                  'false,

label-cnt (cinfo))), label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list),

list (list ('jump, 1 + label-cnt (cinfo)),

cons ('dl,

cons (label-cnt (cinfo),

     '(nil (no-op)))))))

∧ ok-cinfop (add-code (translate (make-cinfo (append (code (cinfo),

                     list (list ('push-local,

if-condition (stmt)),

                            '(fetch-temp-stk),
                            list ('test-bool-and-jump,
                               'false,

label-cnt (cinfo)))),

label-alist (cinfo),

1 + (1 + label-cnt (cinfo))),

cond-list,

if-true-branch (stmt), proc-list),

list (list ('jump, 1 + label-cnt (cinfo)),

cons ('dl,

cons (label-cnt (cinfo),

           '(nil (no-op)))))))

∧ ok-cinfop (make-cinfo (append (code (cinfo),

       list (list ('push-local,

if-condition (stmt)),

           '(fetch-temp-stk),
           list ('test-bool-and-jump,
              'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo))))

∧ ok-cinfop (make-cinfo (list (list ('push-local,

if-condition (stmt)),

    '(fetch-temp-stk),
    list ('test-bool-and-jump,
       'false,

label-cnt (cinfo))), label-alist (cinfo), 1 + (1 + label-cnt (cinfo)))))

Theorem: new-code-if-case ((car (stmt) = 'if-mg) ∧ ok-cinfop (cinfo) ∧ (ok-cinfop (add-code (translate (make-cinfo (list (list ('push-local,

if-condition (stmt)),

                 '(fetch-temp-stk),
                 list ('test-bool-and-jump,
                     'false,

label-cnt (cinfo))), label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list,

if-true-branch (stmt),

proc-list),

list (list ('jump, 1 + label-cnt (cinfo)),

cons ('dl,

cons (label-cnt (cinfo),

'(nil (no-op)))))))

→ (append (code (add-code (translate (make-cinfo (list (list ('push-local,

if-condition (stmt)),

'(fetch-temp-stk),
list ('test-bool-and-jump,
'false,

label-cnt (cinfo))), label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list),

list (list ('jump, 1 + label-cnt (cinfo)),

cons ('dl,

cons (label-cnt (cinfo),

'(nil (no-op))))))),

code (translate (nullify (add-code (translate (make-cinfo (list (list ('push-local,

if-condition (stmt)),

           '(fetch-temp-stk),
           list ('test-bool-and-jump,
               'false,

label-cnt (cinfo))), label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), cons ('dl,

cons (label-cnt (cinfo),

  '(nil
    (no-op))))))),

cond-list, if-false-branch (stmt), proc-list)))

= code (translate (add-code (translate (make-cinfo (list (list ('push-local,

if-condition (stmt)),

 '(fetch-temp-stk),
 list ('test-bool-and-jump,

                 'false,

label-cnt (cinfo))), label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), cons ('dl,

cons (label-cnt (cinfo),

     '(nil
       (no-op)))))),

cond-list, if-false-branch (stmt), proc-list))))

∧ (ok-cinfop (add-code (translate (make-cinfo (append (code (cinfo),

    list (list ('push-local,

if-condition (stmt)),

        '(fetch-temp-stk),
        list ('test-bool-and-jump,
           'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list),

list (list ('jump, 1 + label-cnt (cinfo)),

cons ('dl,

cons (label-cnt (cinfo),

'(nil (no-op)))))))

→ (append (code (add-code (translate (make-cinfo (append (code (cinfo),

            list (list ('push-local,

if-condition (stmt)),

                '(fetch-temp-stk),
                list ('test-bool-and-jump,
                    'false,

label-cnt (cinfo)))),

label-alist (cinfo),

1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list), list (list ('jump, 1 + label-cnt (cinfo)),

cons ('dl,

cons (label-cnt (cinfo),

'(nil (no-op))))))),

code (translate (nullify (add-code (translate (make-cinfo (append (code (cinfo),

list (list ('push-local,

if-condition (stmt)),

'(fetch-temp-stk),
list ('test-bool-and-jump,
'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), cons ('dl,

cons (label-cnt (cinfo),

'(nil
(no-op))))))),

cond-list, if-false-branch (stmt), proc-list)))

= code (translate (add-code (translate (make-cinfo (append (code (cinfo),

list (list ('push-local,

if-condition (stmt)),

'(fetch-temp-stk),
list ('test-bool-and-jump,
'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), cons ('dl,

cons (label-cnt (cinfo),

'(nil
(no-op)))))),

cond-list, if-false-branch (stmt), proc-list))))

∧ (ok-cinfop (make-cinfo (append (code (cinfo),

    list (list ('push-local,

if-condition (stmt)),

        '(fetch-temp-stk),
        list ('test-bool-and-jump,
           'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo))))

→ (append (code (make-cinfo (append (code (cinfo),

            list (list ('push-local,

if-condition (stmt)),

                '(fetch-temp-stk),
                list ('test-bool-and-jump,
                    'false,

label-cnt (cinfo)))),

label-alist (cinfo),

1 + (1 + label-cnt (cinfo)))),

code (translate (nullify (make-cinfo (append (code (cinfo),

                           list (list ('push-local,

if-condition (stmt)),

                               '(fetch-temp-stk),
                               list ('test-bool-and-jump,
                                  'false,

label-cnt (cinfo)))),

label-alist (cinfo),

1 + (1 + label-cnt (cinfo)))),

cond-list,

if-true-branch (stmt), proc-list)))

= code (translate (make-cinfo (append (code (cinfo),

                 list (list ('push-local,

if-condition (stmt)),

                     '(fetch-temp-stk),
                     list ('test-bool-and-jump,
                        'false,

label-cnt (cinfo)))),

label-alist (cinfo),

1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list))))

∧ (ok-cinfop (make-cinfo (list (list ('push-local, if-condition (stmt)),

'(fetch-temp-stk),
list ('test-bool-and-jump,
'false,

label-cnt (cinfo))), label-alist (cinfo), 1 + (1 + label-cnt (cinfo))))

→ (append (code (make-cinfo (list (list ('push-local,

if-condition (stmt)),

'(fetch-temp-stk),
list ('test-bool-and-jump,
'false,

label-cnt (cinfo))), label-alist (cinfo), 1 + (1 + label-cnt (cinfo)))),

code (translate (nullify (make-cinfo (list (list ('push-local,

if-condition (stmt)),

           '(fetch-temp-stk),
           list ('test-bool-and-jump,
               'false,

label-cnt (cinfo))), label-alist (cinfo), 1 + (1 + label-cnt (cinfo)))),

cond-list, if-true-branch (stmt), proc-list)))

= code (translate (make-cinfo (list (list ('push-local,

if-condition (stmt)),

 '(fetch-temp-stk),
 list ('test-bool-and-jump,
     'false,

label-cnt (cinfo))), label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list)))))

→ (append (code (cinfo),

code (translate (nullify (cinfo), cond-list, stmt, proc-list))) = code (translate (cinfo, cond-list, stmt, proc-list)))

Theorem: new-code-begin-case-induction-hyps ok-cinfop (cinfo) → (ok-cinfop (add-code (set-label-alist (translate (nullify (make-cinfo (code (cinfo), append (make-label-alist (when-labels (stmt),

label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo)))),

cond-list, begin-body (stmt), proc-list),

label-alist (cinfo)),

cons (list ('jump, 1 + label-cnt (cinfo)),

cons (cons ('dl,

cons (label-cnt (cinfo),

'(nil
(push-constant
 (nat 2))))),
'((pop-global c-c))))))

∧ ok-cinfop (make-cinfo (code (cinfo),

append (make-label-alist (when-labels (stmt),

label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))))

∧ ok-cinfop (add-code (set-label-alist (translate (make-cinfo (code (cinfo),

append (make-label-alist (when-labels (stmt),

label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list,

begin-body (stmt), proc-list),

label-alist (cinfo)),

cons (list ('jump, 1 + label-cnt (cinfo)),

cons (cons ('dl,

cons (label-cnt (cinfo),

  '(nil
    (push-constant
     (nat 2))))),
'((pop-global c-c)))))))

(prove-lemma new-code-begin-case (rewrite)
(IMPLIES
(AND
(equal (car STMT) 'BEGIN-MG)
(OK-CINFOP CINFO)

(IMPLIES
(OK-CINFOP
  (ADD-CODE
(SET-LABEL-ALIST
(TRANSLATE
(NULLIFY (MAKE-CINFO (CODE CINFO)
(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT) (LABEL-CNT CINFO))
(LABEL-ALIST CINFO))
(ADD1 (ADD1 (LABEL-CNT CINFO)))))
COND-LIST (BEGIN-BODY STMT) PROC-LIST)
(LABEL-ALIST CINFO))
(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
  (CONS (CONS 'DL (CONS (LABEL-CNT CINFO) '(NIL (PUSH-CONSTANT (NAT 2)))))
'((POP-GLOBAL C-C))))))
(EQUAL
  (APPEND
(CODE
(ADD-CODE
(SET-LABEL-ALIST
  (TRANSLATE
(NULLIFY (MAKE-CINFO (CODE CINFO)
 (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
   (LABEL-CNT CINFO))
 (LABEL-ALIST CINFO))
 (ADD1 (ADD1 (LABEL-CNT CINFO)))))
COND-LIST
(BEGIN-BODY STMT)
PROC-LIST)
  (LABEL-ALIST CINFO))
(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
(CONS (CONS 'DL
  (CONS (LABEL-CNT CINFO)
'(NIL (PUSH-CONSTANT (NAT 2)))))
'((POP-GLOBAL C-C))))))
(CODE
(TRANSLATE
(NULLIFY
  (ADD-CODE
(SET-LABEL-ALIST
(TRANSLATE
(NULLIFY (MAKE-CINFO (CODE CINFO)
(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
(LABEL-CNT CINFO))
(LABEL-ALIST CINFO))

(ADD1 (ADD1 (LABEL-CNT CINFO)))))
COND-LIST
(BEGIN-BODY STMT)
PROC-LIST)
(LABEL-ALIST CINFO))
(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
  (CONS (CONS 'DL
(CONS (LABEL-CNT CINFO)
'(NIL (PUSH-CONSTANT (NAT 2)))))
'((POP-GLOBAL C-C))))))
COND-LIST
(WHEN-HANDLER STMT)
PROC-LIST)))
  (CODE
(TRANSLATE
(ADD-CODE
(SET-LABEL-ALIST
  (TRANSLATE
(NULLIFY (MAKE-CINFO (CODE CINFO)
 (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
   (LABEL-CNT CINFO))
 (LABEL-ALIST CINFO))
 (ADD1 (ADD1 (LABEL-CNT CINFO)))))
COND-LIST
(BEGIN-BODY STMT)
PROC-LIST)
  (LABEL-ALIST CINFO))
(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
(CONS (CONS 'DL
  (CONS (LABEL-CNT CINFO)
'(NIL (PUSH-CONSTANT (NAT 2)))))
'((POP-GLOBAL C-C)))))
COND-LIST
(WHEN-HANDLER STMT)
PROC-LIST))))
(IMPLIES
(OK-CINFOP (MAKE-CINFO (CODE CINFO)
(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT) (LABEL-CNT CINFO))
(LABEL-ALIST CINFO))
(ADD1 (ADD1 (LABEL-CNT CINFO)))))
(EQUAL
  (APPEND
(CODE (MAKE-CINFO (CODE CINFO)
(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT) (LABEL-CNT CINFO))

 (LABEL-ALIST CINFO))
 (ADD1 (ADD1 (LABEL-CNT CINFO)))))
(CODE
 (TRANSLATE
   (NULLIFY (MAKE-CINFO (CODE CINFO)
(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT) (LABEL-CNT CINFO))
(LABEL-ALIST CINFO))
(ADD1 (ADD1 (LABEL-CNT CINFO)))))
   COND-LIST (BEGIN-BODY STMT) PROC-LIST)))
     (CODE (TRANSLATE (MAKE-CINFO (CODE CINFO)
  (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT) (LABEL-CNT CINFO))
  (LABEL-ALIST CINFO))
  (ADD1 (ADD1 (LABEL-CNT CINFO))))
      COND-LIST (BEGIN-BODY STMT) PROC-LIST))))
 (IMPLIES
   (OK-CINFOP
     (ADD-CODE
(SET-LABEL-ALIST
 (TRANSLATE (MAKE-CINFO (CODE CINFO)
(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT) (LABEL-CNT CINFO))
(LABEL-ALIST CINFO))
(ADD1 (ADD1 (LABEL-CNT CINFO))))
    COND-LIST (BEGIN-BODY STMT) PROC-LIST)
 (LABEL-ALIST CINFO))
(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
     (CONS (CONS 'DL (CONS (LABEL-CNT CINFO) '(NIL (PUSH-CONSTANT (NAT 2)))))
   '((POP-GLOBAL C-C))))))
   (EQUAL
     (APPEND
(CODE
 (ADD-CODE
   (SET-LABEL-ALIST
     (TRANSLATE (MAKE-CINFO (CODE CINFO)
    (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
      (LABEL-CNT CINFO))
    (LABEL-ALIST CINFO))
    (ADD1 (ADD1 (LABEL-CNT CINFO))))
COND-LIST
(BEGIN-BODY STMT)
PROC-LIST)
     (LABEL-ALIST CINFO))
   (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
 (CONS (CONS 'DL
     (CONS (LABEL-CNT CINFO)

'(NIL (PUSH-CONSTANT (NAT 2)))))
'((POP-GLOBAL C-C))))))
(CODE
(TRANSLATE
(NULLIFY
  (ADD-CODE
(SET-LABEL-ALIST
(TRANSLATE (MAKE-CINFO (CODE CINFO)
(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
(LABEL-CNT CINFO))
(LABEL-ALIST CINFO))
(ADD1 (ADD1 (LABEL-CNT CINFO))))
 COND-LIST
 (BEGIN-BODY STMT)
 PROC-LIST)
(LABEL-ALIST CINFO))
(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
  (CONS (CONS 'DL
(CONS (LABEL-CNT CINFO)
'(NIL (PUSH-CONSTANT (NAT 2)))))
'((POP-GLOBAL C-C))))))
COND-LIST
(WHEN-HANDLER STMT)
PROC-LIST)))
  (CODE
(TRANSLATE
(ADD-CODE
(SET-LABEL-ALIST
  (TRANSLATE (MAKE-CINFO (CODE CINFO)
 (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
   (LABEL-CNT CINFO))
 (LABEL-ALIST CINFO))
 (ADD1 (ADD1 (LABEL-CNT CINFO))))
COND-LIST
(BEGIN-BODY STMT)
PROC-LIST)
  (LABEL-ALIST CINFO))
(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
(CONS (CONS 'DL
  (CONS (LABEL-CNT CINFO)
'(NIL (PUSH-CONSTANT (NAT 2)))))
'((POP-GLOBAL C-C)))))
COND-LIST
(WHEN-HANDLER STMT)

PROC-LIST)))))
(EQUAL (APPEND (CODE CINFO)
(CODE (TRANSLATE (NULLIFY CINFO)
COND-LIST STMT PROC-LIST)))
(CODE (TRANSLATE CINFO COND-LIST STMT PROC-LIST))))
((INSTRUCTIONS (disable add-code set-label-alist)
PROMOTE (DEMOTE 3) (DIVE 1 1) (REWRITE NEW-CODE-BEGIN-CASE-INDUCTION-HYPS) UP S TOP PROMOTE
(DEMOTE 3) (DIVE 1 1) (REWRITE NEW-CODE-BEGIN-CASE-INDUCTION-HYPS) UP S TOP PROMOTE
(DEMOTE 3) (DIVE 1 1) (REWRITE NEW-CODE-BEGIN-CASE-INDUCTION-HYPS) UP S TOP PROMOTE
(DIVE 2 1) (REWRITE BEGIN-TRANSLATION) UP (REWRITE CODE-ADD-CODE-COMMUTE) (DIVE 1) = (DROP 5)
UP (REWRITE ASSOCIATIVITY-OF-APPEND) (DIVE 1) (REWRITE CODE-ADD-CODE-COMMUTE) (DIVE 1)
(REWRITE SET-LABEL-ALIST-DOESNT-AFFECT-OTHER-FIELDS) = (DROP 4) UP
(REWRITE ASSOCIATIVITY-OF-APPEND) UP (REWRITE ASSOCIATIVITY-OF-APPEND) TOP (REWRITE APPEND-REWRITE2)
(DIVE 1 1) (REWRITE BEGIN-TRANSLATION) UP (REWRITE CODE-ADD-CODE-COMMUTE) (DIVE 1) (S-PROP NULLIFY)
S TOP (DEMOTE 3) (DIVE 1 2) (S-PROP NULLIFY) S TOP PROMOTE (DIVE 1 1) = (DROP 3) TOP
(BASH (ENABLE NULLIFY ADD-CODE TRANSLATE-PRESERVES-FIELDS APPEND-REWRITE2 SET-LABEL-ALIST))
PROMOTE (DIVE 2 1 1) (DIVE 1 3) (REWRITE CODE-DOESNT-AFFECT-OTHER-FIELDS)
TOP (PROVE (ENABLE NULLIFY)))))

Theorem: new-code-appended-to-old ok-cinfop (cinfo) → (append (code (cinfo),

code (translate (nullify (cinfo), cond-list, stmt, proc-list))) = code (translate (cinfo, cond-list, stmt, proc-list)))

Event: Disable new-code-appended-to-old.

Theorem: new-code-appended-to-old1 ok-cinfop (cinfo) → (code (translate (cinfo, cond-list, stmt, proc-list))

= append (code (cinfo), code (translate (nullify (cinfo), cond-list, stmt, proc-list))))

Event: Disable new-code-appended-to-old1.

Definition: collect-labels (codelist) = if codelist ≃ nil then nil

elseif caar (codelist) = 'dl then cons (cadar (codelist), collect-labels (cdr (codelist))) else collect-labels (cdr (codelist)) endif

Theorem: collect-labels-plistp plistp (collect-labels (lst))

Theorem: collect-labels-distributes collect-labels (append (code1 , code2 )) = append (collect-labels (code1 ), collect-labels (code2 ))

Definition: all-labels-unique (codelist) = no-duplicates (collect-labels (codelist))

Event: Disable all-labels-unique.

Theorem: all-labels-unique-append all-labels-unique (append (x, y)) → (all-labels-unique (x) ∧ all-labels-unique (y))

Theorem: all-labels-unique-reduction (¬ all-labels-unique (y)) → (¬ all-labels-unique (append (x, y)))

Event: Disable all-labels-unique-reduction.

Theorem: all-labels-unique-reduction2 (¬ all-labels-unique (y)) → (¬ all-labels-unique (cons (x, y)))

Event: Disable all-labels-unique-reduction2.

Theorem: find-labelp-rewrites-to-member find-labelp (lab, code) = (lab ∈ collect-labels (code))

Event: Disable find-labelp-rewrites-to-member.

Theorem: all-labels-unique-reduction3 (find-labelp (lab, code1 ) ∧ find-labelp (lab, code2 )) → (¬ all-labels-unique (append (code1 , code2 )))

Event: Disable all-labels-unique-reduction3.

Theorem: no-duplicates-append-list no-duplicates (append (lst, cons (x, cons (y, lst2 )))) → no-duplicates (append (lst, list (y)))

Theorem: no-duplicates-append-list2 no-duplicates (append (lst, cons (y, lst2 ))) → no-duplicates (append (lst, list (y)))

Theorem: labels-unique-append2 all-labels-unique (append (lst1 , cons (x, cons (y, lst2 )))) → all-labels-unique (append (lst1 , list (y)))

Theorem: find-labelp-member-collect-labels find-labelp (x, code) → (x ∈ collect-labels (code))

Definition: label-hole-big-enough (cinfo, cond-list, stmt, proc-list, y) = all-labels-unique (append (code (translate (cinfo,

cond-list, stmt, proc-list)),

y))

Theorem: labels-unique-not-find-labelp (all-labels-unique (append (code1 , code2 )) ∧ find-labelp (label, code2 )) → (¬ find-labelp (label, code1 ))

Theorem: labels-unique-not-find-labelp1 all-labels-unique (append (lst, list (list ('dl, label, nil, w)))) → (find-labelp (label, lst) = f)

Definition: ok-cond-list (lst) = if lst ≃ nil then lst = nil

else (ok-mg-namep (car (lst))

         ∨ (car (lst) ∈ '(leave routineerror)))

∧ ok-cond-list (cdr (lst)) endif

Theorem: identifier-plistp-make-cond-list-ok identifier-plistp (lst) → ok-cond-list (lst)

Theorem: make-cond-list-ok

 ((car (stmt) = 'proc-call-mg)

∧ ok-mg-statement (stmt, cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list)) → ok-cond-list (make-cond-list (fetch-called-def (stmt, proc-list)))

Theorem: cond-subsetp-preserves-ok-mg-statep (cond-subsetp (r-cond-list, t-cond-list) ∧ (cc (mg-state) ≠ 'leave) ∧ ok-mg-statep (mg-state, r-cond-list)) → ok-mg-statep (mg-state, t-cond-list)

Definition: ok-translation-parameters (cinfo, cond-list, stmt, proc-list, y) = (ok-cinfop (cinfo)

∧ ok-cond-list (cond-list)

∧ label-hole-big-enough (cinfo, cond-list, stmt, proc-list, y))

Theorem: label-cnt-monotonic label-cnt (translate (cinfo, cond-list, stmt, proc-list)) ≮ label-cnt (cinfo)

Theorem: label-cnt-monotonic2 (n < label-cnt (cinfo)) → (n < label-cnt (translate (cinfo, cond-list, stmt, proc-list)))

Theorem: label-cnt-monotonic3 (n < label-cnt (cinfo)) → ((n < label-cnt (translate (cinfo, cond-list, stmt, proc-list))) = t)

Theorem: label-cnt-add1-add1-monotonic ((n < lc) ∧ (label-cnt (cinfo) = (1 + (1 + lc)))) → ((n < label-cnt (translate (cinfo, cond-list, stmt, proc-list))) = t)

Theorem: label-cnt-monotonic-cond-conversion (n < lc) → (find-labelp (n, cond-conversion (actual-conds, lc, cond-list, label-alist))

= f)

Theorem: not-find-labelp-push-parameters-code find-labelp (n, push-parameters-code (locals, actuals)) = f

Event: Disable not-find-labelp-push-parameters-code.

Theorem: find-labelp-monotonic-lessp ((n < label-cnt (cinfo)) ∧ (¬ find-labelp (n, code (cinfo)))) → (find-labelp (n, code (translate (cinfo, cond-list, stmt, proc-list))) = f)

;; The following definition is used only in the proof of procedure-calls.

Definition: label-cnt-big-enough (lc, code) = if code ≃ nil then t

elseif caar (code) = 'dl

then (cadar (code) < lc) ∧ label-cnt-big-enough (lc, cdr (code))

else label-cnt-big-enough (lc, cdr (code)) endif Definition: cond-conversion-induction-hint (lst, n) = if lst ≃ nil then t

else cond-conversion-induction-hint (cdr (lst), 1 + n) endif

Theorem: label-count-big-enough-not-find-labelp label-cnt-big-enough (lc, code) → (find-labelp (lc, code) = f)

Theorem: greater-label-count-big-enough (label-cnt-big-enough (n, code) ∧ (n ≤ m)) → label-cnt-big-enough (m, code)

Theorem: label-cnt-big-enough-distributes label-cnt-big-enough (lc, append (lst1 , lst2 )) = (label-cnt-big-enough (lc, lst1 ) ∧ label-cnt-big-enough (lc, lst2 ))

Theorem: label-cnt-lessp1 (n < label-cnt (cinfo)) → ((n < label-cnt (translate (cinfo, cond-list, stmt, proc-list))) = t)

Theorem: label-cnt-big-enough-distributes2 (label-cnt-big-enough (n, lst1 ) ∧ label-cnt-big-enough (n, lst2 )) → label-cnt-big-enough (n, append (lst1 , lst2 ))

Theorem: label-cnt-big-enough-for-push-actuals-code label-cnt-big-enough (n, push-actuals-code (actuals))

Theorem: label-cnt-big-enough-for-push-local-array-values-code label-cnt-big-enough (n, push-local-array-values-code (array-value))

Theorem: label-cnt-big-enough-for-push-locals-values-code label-cnt-big-enough (n, push-locals-values-code (actuals))

Theorem: label-cnt-big-enough-for-push-locals-addresses-code label-cnt-big-enough (n, push-locals-addresses-code (actuals, m))

Theorem: label-cnt-big-enough-for-cond-conversion label-cnt-big-enough (lc + (1 + (1 + length (lst))),

cond-conversion (lst, 1 + (1 + lc), cond-list, label-alist))

Theorem: label-cnt-big-enough-for-proc-call-code label-cnt-big-enough (label-cnt (cinfo), code (cinfo)) → label-cnt-big-enough (label-cnt (cinfo)

+ (1 + (1 + length (call-conds (stmt)))), proc-call-code (cinfo, stmt, cond-list, locals, k))

Theorem: label-cnt-big-enough-for-predefined-proc-call-code label-cnt-big-enough (n, predefined-proc-call-sequence (stmt, label-alist))

Theorem: label-cnt-stays-big-enough label-cnt-big-enough (label-cnt (cinfo), code (cinfo)) → label-cnt-big-enough (label-cnt (translate (cinfo,

cond-list, stmt, proc-list)), code (translate (cinfo, cond-list, stmt, proc-list)))

Theorem: label-cnt-big-enough-add1 label-cnt-big-enough (x, y) → label-cnt-big-enough (1 + x, y)

Theorem: lesser-label-doesnt-disturb-no-duplicates (no-duplicates (lst) ∧ (x ∉ lst)) → no-duplicates (append (lst, list (x)))

Theorem: find-labelp-reduces-to-member find-labelp (x, lst) = (x ∈ collect-labels (lst))

Theorem: member-labels-unique-not-find-labelp (all-labels-unique (append (code, code2 )) ∧ find-labelp (label, code2 )) → (¬ find-labelp (label, code))

Theorem: no-duplicates-right-cons-reduction no-duplicates (collect-labels (lst)) → (no-duplicates (append (collect-labels (lst), list (x)))

= (¬ find-labelp (x, lst)))

Theorem: label-cnt-big-enough-not-find-labelp label-cnt-big-enough (lc, code) → (find-labelp (lc, code) = f)

Theorem: not-member-cond-conversion (n < lc) → ((n ∈ collect-labels (cond-conversion (conds, lc, cond-list, label-alist)))

= f)

Theorem: no-duplicates-cond-conversion no-duplicates (collect-labels (cond-conversion (conds, lc, cond-list, label-alist)))

Theorem: no-duplicates-cond-conversion-base-case no-duplicates (append (collect-labels (cond-conversion (conds,

1 + (1 + lc), cond-list, label-alist)),

list (1 + lc)))

Theorem: no-duplicates-proc-call (no-duplicates (collect-labels (code)) ∧ label-cnt-big-enough (lc, code)) → no-duplicates (append (collect-labels (code),

cons (lc,

append (collect-labels (cond-conversion (conds, 1 + (1 + lc), cond-list, label-alist)),

list (1 + lc)))))

Theorem: collect-labels-push-actuals-code-nil collect-labels (push-actuals-code (actuals)) = nil

Theorem: collect-labels-push-local-array-values-code-nil collect-labels (push-local-array-values-code (array-value)) = nil

Theorem: collect-labels-push-locals-values-code-nil collect-labels (push-locals-values-code (actuals)) = nil

Theorem: collect-labels-push-locals-addresses-code-nil collect-labels (push-locals-addresses-code (actuals, m)) = nil

Theorem: collect-labels-predefined-proc-call-code-nil collect-labels (predefined-proc-call-sequence (stmt, label-alist)) = nil

Theorem: collect-labels-strip-label collect-labels (cons (cons ('dl, cons (label, x)), y)) = cons (label, collect-labels (y))

Theorem: labels-unique-loop-case ((car (stmt) = 'loop-mg) ∧ no-duplicates (collect-labels (code (cinfo))) ∧ label-cnt-big-enough (label-cnt (cinfo), code (cinfo)) ∧ ((no-duplicates (collect-labels (code (make-cinfo (append (code (cinfo),

list (cons ('dl,

cons (label-cnt (cinfo),

                                                                '(nil
                                                                  (no-op)))))),

cons (cons ('leave,

1 + label-cnt (cinfo)), label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))))))

∧ label-cnt-big-enough (label-cnt (make-cinfo (append (code (cinfo),

list (cons ('dl, cons (label-cnt (cinfo),

                   '(nil
                     (no-op)))))),

cons (cons ('leave,

1 + label-cnt (cinfo)), label-alist (cinfo)),

1 + (1 + label-cnt (cinfo)))),

code (make-cinfo (append (code (cinfo),

list (cons ('dl,

cons (label-cnt (cinfo),

                '(nil
                  (no-op)))))),

cons (cons ('leave,

1 + label-cnt (cinfo)), label-alist (cinfo)),

1 + (1 + label-cnt (cinfo))))))

→ no-duplicates (collect-labels (code (translate (make-cinfo (append (code (cinfo),

list (cons ('dl,

cons (label-cnt (cinfo),

                              '(nil
                                (no-op)))))),

cons (cons ('leave,

1 + label-cnt (cinfo)), label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list, loop-body (stmt), proc-list))))))

→ no-duplicates (collect-labels (code (translate (cinfo, cond-list, stmt, proc-list))))

Event: Disable labels-unique-loop-case.

Theorem: labels-unique-if-case-hyps1 ((car (stmt) = 'if-mg) ∧ no-duplicates (collect-labels (code (cinfo))) ∧ label-cnt-big-enough (label-cnt (cinfo), code (cinfo))) → (no-duplicates (collect-labels (code (make-cinfo (append (code (cinfo),

     list (list ('push-local,

if-condition (stmt)),

        '(fetch-temp-stk),
        list ('test-bool-and-jump,
            'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo))))))

∧ label-cnt-big-enough (label-cnt (make-cinfo (append (code (cinfo),

list (list ('push-local,

if-condition (stmt)),

'(fetch-temp-stk),
list ('test-bool-and-jump,
'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo)))),

code (make-cinfo (append (code (cinfo),

list (list ('push-local,

if-condition (stmt)),

'(fetch-temp-stk),
list ('test-bool-and-jump,
'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo))))))

Event: Disable labels-unique-if-case-hyps1.

Theorem: label-cnt-big-enough-not-member label-cnt-big-enough (lc, code) → (lc ∉ collect-labels (code))

Theorem: labels-unique-if-case-hyps2 ((car (stmt) = 'if-mg) ∧ no-duplicates (collect-labels (code (cinfo))) ∧ label-cnt-big-enough (label-cnt (cinfo), code (cinfo)) ∧ no-duplicates (collect-labels (code (translate (make-cinfo (append (code (cinfo),

list (list ('push-local,

if-condition (stmt)),

   '(fetch-temp-stk),
   list ('test-bool-and-jump,
       'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list)))))

→ (no-duplicates (collect-labels (code (add-code (translate (make-cinfo (append (code (cinfo),

list (list ('push-local,

if-condition (stmt)),

'(fetch-temp-stk),
list ('test-bool-and-jump,
'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), cons ('dl,

cons (label-cnt (cinfo),

'(nil
(no-op)))))))))

∧ label-cnt-big-enough (label-cnt (add-code (translate (make-cinfo (append (code (cinfo),

list (list ('push-local,

if-condition (stmt)),

'(fetch-temp-stk),
list ('test-bool-and-jump,
 'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), cons ('dl,

cons (label-cnt (cinfo),

'(nil
(no-op))))))),

code (add-code (translate (make-cinfo (append (code (cinfo),

list (list ('push-local,

if-condition (stmt)),

'(fetch-temp-stk),
list ('test-bool-and-jump,
'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo))), cond-list, if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), cons ('dl,

cons (label-cnt (cinfo),

     '(nil
       (no-op)))))))))

Event: Disable labels-unique-if-case-hyps2.

Event: Disable label-cnt-big-enough-not-member.

Theorem: labels-unique-if-case ((car (stmt) = 'if-mg) ∧ no-duplicates (collect-labels (code (cinfo))) ∧ label-cnt-big-enough (label-cnt (cinfo), code (cinfo)) ∧ ((no-duplicates (collect-labels (code (add-code (translate (make-cinfo (append (code (cinfo),

                    list (list ('push-local,

if-condition (stmt)),

                        '(fetch-temp-stk),
                        list ('test-bool-and-jump,
                            'false,

label-cnt (cinfo)))),

label-alist (cinfo),

1 + (1 + label-cnt (cinfo))),

cond-list,

if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), cons ('dl,

cons (label-cnt (cinfo),

        '(nil
          (no-op)))))))))

∧ label-cnt-big-enough (label-cnt (add-code (translate (make-cinfo (append (code (cinfo),

                     list (list ('push-local,

if-condition (stmt)),

                         '(fetch-temp-stk),
                         list ('test-bool-and-jump,
                             'false,

label-cnt (cinfo)))), label-alist (cinfo), 1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), cons ('dl,

cons (label-cnt (cinfo),

     '(nil
       (no-op))))))),

code (add-code (translate (make-cinfo (append (code (cinfo),

              list (list ('push-local,

if-condition (stmt)),

                 '(fetch-temp-stk),
                 list ('test-bool-and-jump,
                     'false,

label-cnt (cinfo)))),

label-alist (cinfo),

1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), cons ('dl,

cons (label-cnt (cinfo),

 '(nil
   (no-op)))))))))

→ no-duplicates (collect-labels (code (translate (add-code (translate (make-cinfo (append (code (cinfo),

                            list (list ('push-local,

if-condition (stmt)),

                               '(fetch-temp-stk),
                               list ('test-bool-and-jump,
                                   'false,

label-cnt (cinfo)))),

label-alist (cinfo),

1 + (1 + label-cnt (cinfo))),

cond-list,

if-true-branch (stmt), proc-list),

list (list ('jump,

1 + label-cnt (cinfo)), cons ('dl, cons (label-cnt (cinfo),

                     '(nil
                       (no-op)))))),

cond-list, if-false-branch (stmt), proc-list)))))

∧ ((no-duplicates (collect-labels (code (make-cinfo (append (code (cinfo),

      list (list ('push-local,

if-condition (stmt)),

         '(fetch-temp-stk),
         list ('test-bool-and-jump,
             'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo))))))

∧ label-cnt-big-enough (label-cnt (make-cinfo (append (code (cinfo),

       list (list ('push-local,

if-condition (stmt)),

          '(fetch-temp-stk),
          list ('test-bool-and-jump,
              'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo)))),

code (make-cinfo (append (code (cinfo),

   list (list ('push-local,

if-condition (stmt)),

       '(fetch-temp-stk),
       list ('test-bool-and-jump,
          'false,

label-cnt (cinfo)))),

label-alist (cinfo), 1 + (1 + label-cnt (cinfo))))))

→ no-duplicates (collect-labels (code (translate (make-cinfo (append (code (cinfo),

                 list (list ('push-local,

if-condition (stmt)),

                     '(fetch-temp-stk),
                     list ('test-bool-and-jump,
                        'false,

label-cnt (cinfo)))),

label-alist (cinfo),

1 + (1 + label-cnt (cinfo))),

cond-list, if-true-branch (stmt),

proc-list))))))

→ no-duplicates (collect-labels (code (translate (cinfo, cond-list, stmt, proc-list))))

Event: Disable labels-unique-if-case.

Theorem: labels-unique-begin-case-hyps ((car (stmt) = 'begin-mg) ∧ no-duplicates (collect-labels (code (cinfo))) ∧ label-cnt-big-enough (label-cnt (cinfo), code (cinfo)) ∧ no-duplicates (collect-labels (code (translate (make-cinfo (code (cinfo),

append (make-label-alist (when-labels (stmt),

label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list,

begin-body (stmt), proc-list)))))

→ (no-duplicates (collect-labels (code (add-code (set-label-alist (translate (make-cinfo (code (cinfo),

append (make-label-alist (when-labels (stmt),

label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list,

begin-body (stmt), proc-list),

label-alist (cinfo)),

cons (list ('jump,

1 + label-cnt (cinfo)), cons (cons ('dl,

cons (label-cnt (cinfo),

                                                             '(nil
                                                               (push-constant
                                                                (nat
                                                                 2))))),
                                                   '((pop-global

c-c))))))))

∧ label-cnt-big-enough (label-cnt (add-code (set-label-alist (translate (make-cinfo (code (cinfo),

append (make-label-alist (when-labels (stmt),

label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))), cond-list, begin-body (stmt), proc-list),

label-alist (cinfo)),

cons (list ('jump,

1 + label-cnt (cinfo)), cons (cons ('dl,

cons (label-cnt (cinfo),

'(nil
(push-constant
 (nat
  2))))),
'((pop-global
c-c)))))),

code (add-code (set-label-alist (translate (make-cinfo (code (cinfo),

append (make-label-alist (when-labels (stmt),

label-cnt (cinfo)),

label-alist (cinfo)), 1 + (1 + label-cnt (cinfo))),

cond-list, begin-body (stmt), proc-list),

label-alist (cinfo)),

cons (list ('jump,

1 + label-cnt (cinfo)), cons (cons ('dl,

cons (label-cnt (cinfo),

'(nil
(push-constant
(nat
2))))),
'((pop-global

c-c))))))))

Event: Disable labels-unique-begin-case-hyps.

(prove-lemma labels-unique-begin-case (rewrite)
(IMPLIES
(AND (equal (car STMT) 'BEGIN-MG)
(NO-DUPLICATES (COLLECT-LABELS (CODE CINFO)))
(LABEL-CNT-BIG-ENOUGH (LABEL-CNT CINFO) (CODE CINFO))
(IMPLIES

(AND
                (NO-DUPLICATES
  (COLLECT-LABELS
    (CODE
(ADD-CODE
(SET-LABEL-ALIST
  (TRANSLATE (MAKE-CINFO (CODE CINFO)
 (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
   (LABEL-CNT CINFO))
 (LABEL-ALIST CINFO))
 (ADD1 (ADD1 (LABEL-CNT CINFO))))
     COND-LIST
     (BEGIN-BODY STMT)
     PROC-LIST)
  (LABEL-ALIST CINFO))
(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
(CONS (CONS 'DL
  (CONS (LABEL-CNT CINFO)
'(NIL (PUSH-CONSTANT (NAT 2)))))
    '((POP-GLOBAL C-C))))))))
(LABEL-CNT-BIG-ENOUGH
  (LABEL-CNT
    (ADD-CODE
(SET-LABEL-ALIST
(TRANSLATE (MAKE-CINFO (CODE CINFO)
(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
 (LABEL-CNT CINFO))
(LABEL-ALIST CINFO))
(ADD1 (ADD1 (LABEL-CNT CINFO))))
   COND-LIST
   (BEGIN-BODY STMT)
   PROC-LIST)
(LABEL-ALIST CINFO))
(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
    (CONS (CONS 'DL
(CONS (LABEL-CNT CINFO)
'(NIL (PUSH-CONSTANT (NAT 2)))))
  '((POP-GLOBAL C-C))))))
  (CODE
    (ADD-CODE
(SET-LABEL-ALIST
(TRANSLATE (MAKE-CINFO (CODE CINFO)
(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
 (LABEL-CNT CINFO))

 (LABEL-ALIST CINFO))
 (ADD1 (ADD1 (LABEL-CNT CINFO))))
     COND-LIST
     (BEGIN-BODY STMT)
     PROC-LIST)
  (LABEL-ALIST CINFO))
(CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
      (CONS (CONS 'DL
  (CONS (LABEL-CNT CINFO)
'(NIL (PUSH-CONSTANT (NAT 2)))))
    '((POP-GLOBAL C-C))))))))
(NO-DUPLICATES
  (COLLECT-LABELS
    (CODE
      (TRANSLATE
(ADD-CODE
  (SET-LABEL-ALIST
    (TRANSLATE (MAKE-CINFO (CODE CINFO)
   (APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
     (LABEL-CNT CINFO))
   (LABEL-ALIST CINFO))
   (ADD1 (ADD1 (LABEL-CNT CINFO))))
       COND-LIST
       (BEGIN-BODY STMT)
       PROC-LIST)
    (LABEL-ALIST CINFO))
  (CONS (LIST 'JUMP (ADD1 (LABEL-CNT CINFO)))
(CONS (CONS 'DL
    (CONS (LABEL-CNT CINFO)
  '(NIL (PUSH-CONSTANT (NAT 2)))))
      '((POP-GLOBAL C-C)))))
COND-LIST
(WHEN-HANDLER STMT)
PROC-LIST)))))
      (IMPLIES
(AND
  (NO-DUPLICATES
    (COLLECT-LABELS
      (CODE (MAKE-CINFO (CODE CINFO)
(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
  (LABEL-CNT CINFO))
(LABEL-ALIST CINFO))
(ADD1 (ADD1 (LABEL-CNT CINFO)))))))
  (LABEL-CNT-BIG-ENOUGH

(LABEL-CNT (MAKE-CINFO (CODE CINFO)
(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
(LABEL-CNT CINFO))
(LABEL-ALIST CINFO))
(ADD1 (ADD1 (LABEL-CNT CINFO)))))
(CODE (MAKE-CINFO (CODE CINFO)
(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
(LABEL-CNT CINFO))
(LABEL-ALIST CINFO))
(ADD1 (ADD1 (LABEL-CNT CINFO)))))))
(NO-DUPLICATES
(COLLECT-LABELS
(CODE (TRANSLATE (MAKE-CINFO (CODE CINFO)
(APPEND (MAKE-LABEL-ALIST (WHEN-LABELS STMT)
(LABEL-CNT CINFO))
(LABEL-ALIST CINFO))
(ADD1 (ADD1 (LABEL-CNT CINFO))))
COND-LIST
(BEGIN-BODY STMT)
PROC-LIST))))))
(NO-DUPLICATES (COLLECT-LABELS (CODE (TRANSLATE CINFO COND-LIST STMT PROC-LIST)))))
((INSTRUCTIONS PROMOTE
(DEMOTE 5)
(DIVE 1 1)
S
(REWRITE LABEL-CNT-BIG-ENOUGH-ADD1)
UP S TOP PROMOTE
(DEMOTE 4)
(DIVE 1 1 1)
(REWRITE LABELS-UNIQUE-BEGIN-CASE-HYPS)
NX
(REWRITE LABELS-UNIQUE-BEGIN-CASE-HYPS)
UP UP S TOP PROMOTE
(DIVE 1 1 1)
(REWRITE BEGIN-TRANSLATION)
UP
(REWRITE CODE-ADD-CODE-COMMUTE)
UP
(REWRITE COLLECT-LABELS-DISTRIBUTES)
(DIVE 2)
(= *
   (LIST (ADD1 (LABEL-CNT CINFO)))
   ((ENABLE COLLECT-LABELS)))
UP UP

(REWRITE NO-DUPLICATES-RIGHT-CONS-REDUCTION)
(DIVE 1)
(REWRITE FIND-LABELP-MONOTONIC-LESSP)
UP S
(DIVE 2)
(REWRITE ADD-CODE-DOESNT-AFFECT-OTHER-FIELDS)
(REWRITE SET-LABEL-ALIST-DOESNT-AFFECT-OTHER-FIELDS)
UP
(REWRITE LABEL-CNT-LESSP1)
PROVE
(DIVE 1 2)
(REWRITE CODE-ADD-CODE-COMMUTE)
(DIVE 1)
(REWRITE SET-LABEL-ALIST-DOESNT-AFFECT-OTHER-FIELDS)
UP UP
(REWRITE FIND-LABELP-APPEND2)
(DIVE 3)
(= F)
TOP S
(DIVE 1)
(REWRITE FIND-LABELP-MONOTONIC-LESSP)
TOP S PROVE S
(DIVE 1)
(REWRITE LABEL-CNT-BIG-ENOUGH-NOT-FIND-LABELP)
TOP S
(REWRITE LABEL-CNT-BIG-ENOUGH-ADD1)
(DEMOTE 5)
S
(REWRITE LABEL-CNT-BIG-ENOUGH-ADD1))))

Event: Disable labels-unique-begin-case.

Event: Disable find-labelp-rewrites-to-member.

Theorem: translate-leaves-labels-unique (no-duplicates (collect-labels (code (cinfo))) ∧ label-cnt-big-enough (label-cnt (cinfo), code (cinfo))) → no-duplicates (collect-labels (code (translate (cinfo,

cond-list, stmt, proc-list))))

;; Note: many of the following lemmas may never be used, particularly the ones

;; involving assoc in the hyps.

Theorem: translate-proc-list-assoc1 (definedp (subr, proc-list) ∧ ok-mg-def-plistp1 (proc-list, proc-list2 )) → (translate-def (assoc (subr, proc-list), proc-list2 )

= assoc (subr, translate-proc-list1 (proc-list, proc-list2 )))

Event: Disable translate-proc-list-assoc1.

Theorem: translate-proc-list-assoc (user-defined-procp (subr, proc-list) ∧ ok-mg-def-plistp (proc-list)) → (translate-def (assoc (subr, proc-list), proc-list)

= assoc (subr, translate-proc-list (proc-list)))

Event: Disable translate-proc-list-assoc.

Theorem: translate-proc-list-assoc2 (user-defined-procp (subr, proc-list) ∧ ok-mg-def-plistp (proc-list)) → (assoc (subr, translate-proc-list (proc-list))

= translate-def (assoc (subr, proc-list), proc-list))

Event: Disable translate-proc-list-assoc2.

Theorem: translate-definedp1 (ok-mg-def-plistp1 (lst1 , lst2 ) ∧ definedp (x, lst1 )) → definedp (x, translate-proc-list1 (lst1 , lst2 ))

Event: Disable translate-definedp1.

Theorem: assoc-mg-simple-variable-assignment-translate-proc-list assoc ('mg-simple-variable-assignment, translate-proc-list (proc-list)) = mg-simple-variable-assignment-translation

Theorem: assoc-mg-simple-constant-assignment-translate-proc-list assoc ('mg-simple-constant-assignment, translate-proc-list (proc-list)) = mg-simple-constant-assignment-translation

Theorem: assoc-mg-simple-variable-eq-translate-proc-list assoc ('mg-simple-variable-eq, translate-proc-list (proc-list)) = mg-simple-variable-eq-translation

Theorem: assoc-mg-simple-constant-eq-translate-proc-list assoc ('mg-simple-constant-eq, translate-proc-list (proc-list)) = mg-simple-constant-eq-translation Theorem: assoc-mg-integer-le-translate-proc-list assoc ('mg-integer-le, translate-proc-list (proc-list)) = mg-integer-le-translation

Theorem: assoc-mg-integer-unary-minus-translate-proc-list assoc ('mg-integer-unary-minus, translate-proc-list (proc-list)) = mg-integer-unary-minus-translation

Theorem: assoc-mg-integer-add-translate-proc-list assoc ('mg-integer-add, translate-proc-list (proc-list)) = mg-integer-add-translation

Theorem: assoc-mg-integer-subtract-translate-proc-list assoc ('mg-integer-subtract, translate-proc-list (proc-list)) = mg-integer-subtract-translation

Theorem: assoc-mg-boolean-or-translate-proc-list assoc ('mg-boolean-or, translate-proc-list (proc-list)) = mg-boolean-or-translation

Theorem: assoc-mg-boolean-and-translate-proc-list assoc ('mg-boolean-and, translate-proc-list (proc-list)) = mg-boolean-and-translation

Theorem: assoc-mg-boolean-not-translate-proc-list assoc ('mg-boolean-not, translate-proc-list (proc-list)) = mg-boolean-not-translation

Theorem: assoc-mg-index-array-translate-proc-list assoc ('mg-index-array, translate-proc-list (proc-list)) = mg-index-array-translation

Theorem: assoc-mg-array-element-assignment-translate-proc-list assoc ('mg-array-element-assignment, translate-proc-list (proc-list)) = mg-array-element-assignment-translation

Theorem: assoc-user-defined-proc2 (¬ predefined-procp (subr)) → (assoc (subr, translate-proc-list (proc-list))

= assoc (subr, translate-proc-list1 (proc-list, proc-list)))

Theorem: translate-def-body-rewrite (ok-mg-def-plistp (proc-list) ∧ user-defined-procp (subr, proc-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 )))

→ (cdddr (assoc (subr, translate-proc-list (proc-list)))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)), code2 ))

Event: Disable translate-def-body-rewrite.

Theorem: car-definedp-defined-procp1 (user-defined-procp (subr, proc-list) ∧ ok-mg-def-plistp1 (proc-list, proc-list2 )) → definedp (subr, translate-proc-list1 (proc-list, proc-list2 ))

Event: Disable car-definedp-defined-procp1.

Theorem: car-definedp-defined-procp (user-defined-procp (subr, proc-list) ∧ ok-mg-def-plistp (proc-list)) → definedp (subr, translate-proc-list (proc-list))

Event: Disable car-definedp-defined-procp.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                                 CLOCK                                     ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; The time required for a call to a predefined procedure is the sum of
;; the time for the call sequence and that spent in the body.  The call
;; sequence is fixed but the body may have various paths.

Definition: clock-predefined-proc-call-sequence (name) = case on name:

case = mg-simple-variable-assignment then 3 case = mg-simple-constant-assignment then 3 case = mg-simple-variable-eq then 4 case = mg-simple-constant-eq then 4 case = mg-integer-le then 4 case = mg-integer-unary-minus then 6 case = mg-integer-add then 7 case = mg-integer-subtract then 7 case = mg-boolean-or then 4 case = mg-boolean-and then 4 case = mg-boolean-not then 3 case = mg-index-array then 8 case = mg-array-element-assignment then 8 otherwise 0 endcase

Event: Disable clock-predefined-proc-call-sequence.

Definition: clock-predefined-proc-call-body-translation (stmt, mg-state) = case on call-name (stmt):

case = mg-simple-variable-assignment then 5 case = mg-simple-constant-assignment then 4 case = mg-simple-variable-eq then 8 case = mg-simple-constant-eq then 7 case = mg-integer-le then 9 case = mg-integer-unary-minus then if small-integerp (inegate (untag (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))),

mg-word-size) then 11

else 10 endif case = mg-integer-add then if small-integerp (iplus (untag (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))),

untag (caddr (assoc (caddr (call-actuals (stmt)), mg-alist (mg-state))))),

mg-word-size) then 13

else 11 endif case = mg-integer-subtract then if small-integerp (idifference (untag (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))),

untag (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))),

mg-word-size) then 13

else 11 endif case = mg-boolean-or then 8 case = mg-boolean-and then 8 case = mg-boolean-not then 6 case = mg-index-array then if negativep (cadaddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))) then 7

elseif (idifference (cadddr (call-actuals (stmt)),

cadaddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state))))

= 0)

∨ negativep (idifference (cadddr (call-actuals (stmt)),

cadaddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))

then 11 else 17 endif

case = mg-array-element-assignment then if negativep (cadaddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))) then 7

elseif (idifference (cadddr (call-actuals (stmt)),

cadaddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state))))

= 0)

∨ negativep (idifference (cadddr (call-actuals (stmt)),

cadaddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))

then 11 else 17 endif

otherwise 0 endcase

Event: Disable clock-predefined-proc-call-body-translation.

Definition: predefined-proc-call-clock (stmt, mg-state) = (clock-predefined-proc-call-sequence (call-name (stmt))

+ clock-predefined-proc-call-body-translation (stmt, mg-state))

Event: Disable predefined-proc-call-clock.

;; Removed the definition of clock-r

Definition: clock (stmt, proc-list, mg-state, n) = if (n ≃ 0) ∨ (¬ normal (mg-state)) then 0

else case on car (stmt): case = no-op-mg then 0 case = signal-mg then 3 case = prog2-mg then clock (prog2-left-branch (stmt), proc-list, mg-state, n − 1)

+ clock (prog2-right-branch (stmt), proc-list, mg-meaning (prog2-left-branch (stmt), proc-list, mg-state, n − 1),

n − 1)

case = loop-mg then if ¬ normal (mg-meaning (loop-body (stmt),

proc-list, mg-state, n − 1))

then if cc (mg-meaning (loop-body (stmt), proc-list, mg-state, n − 1))

                     = 'leave

then 3 + clock (loop-body (stmt), proc-list, mg-state, n − 1)

else 1 + clock (loop-body (stmt), proc-list, mg-state, n − 1) endif

else 1 + ((1 + clock (loop-body (stmt), proc-list, mg-state, n − 1))

+ clock (stmt, proc-list, mg-meaning (loop-body (stmt), proc-list, mg-state, n − 1),

n − 1)) endif

case = if-mg then if mg-expression-falsep (if-condition (stmt), mg-state)

then if normal (mg-meaning (if-false-branch (stmt), proc-list, mg-state, n − 1))

then 5 + clock (if-false-branch (stmt), proc-list, mg-state, n − 1) else 4 + clock (if-false-branch (stmt), proc-list, mg-state, n − 1) endif

elseif normal (mg-meaning (if-true-branch (stmt), proc-list, mg-state, n − 1))

then 5 + clock (if-true-branch (stmt), proc-list, mg-state, n − 1)

else 3 + clock (if-true-branch (stmt), proc-list, mg-state, n − 1) endif

case = begin-mg then if cc (mg-meaning (begin-body (stmt),

proc-list, mg-state,

n − 1))

∈ when-labels (stmt) then if normal (mg-meaning (when-handler (stmt),

proc-list,

set-condition (mg-meaning (begin-body (stmt), proc-list, mg-state, n − 1),

                                     'normal),

n − 1))

then clock (begin-body (stmt), proc-list, mg-state, n − 1)

+ (3 + clock (when-handler (stmt), proc-list, set-condition (mg-meaning (begin-body (stmt),

proc-list, mg-state, n − 1),

                                   'normal),

n − 1))

else clock (begin-body (stmt), proc-list, mg-state, n − 1)

+ (2 + clock (when-handler (stmt), proc-list, set-condition (mg-meaning (begin-body (stmt),

proc-list, mg-state, n − 1),

                                  'normal),

n − 1)) endif

elseif normal (mg-meaning (begin-body (stmt), proc-list, mg-state, n − 1))

then 2 + clock (begin-body (stmt), proc-list, mg-state, n − 1)

else clock (begin-body (stmt), proc-list, mg-state, n − 1) endif

case = proc-call-mg then data-length (def-locals (fetch-called-def (stmt,

proc-list)))

+ length (def-locals (fetch-called-def (stmt,

proc-list)))

+ length (call-actuals (stmt))

+ 1

+ clock (def-body (fetch-called-def (stmt,

proc-list)),

proc-list,

make-call-environment (mg-state, stmt, fetch-called-def (stmt,

proc-list)),

n − 1)

+ 5

+ if normal (mg-meaning (def-body (fetch-called-def (stmt,

proc-list)),

proc-list,

make-call-environment (mg-state, stmt, fetch-called-def (stmt,

proc-list)),

n − 1)) then 1

else 3 endif

case = predefined-proc-call-mg then predefined-proc-call-clock (stmt, mg-state) otherwise 0 endcase endif

Theorem: clock-prog2 (car (stmt) = 'prog2-mg) → (clock (stmt, proc-list, mg-state, n)

= if (n ≄ 0) ∧ normal (mg-state)

then clock (prog2-left-branch (stmt), proc-list, mg-state, n − 1)

+ clock (prog2-right-branch (stmt), proc-list, mg-meaning (prog2-left-branch (stmt), proc-list, mg-state, n − 1),

n − 1)

else 0 endif)

Theorem: clock-loop (car (stmt) = 'loop-mg) → (clock (stmt, proc-list, mg-state, n)

= if (n ≄ 0) ∧ normal (mg-state)

then if ¬ normal (mg-meaning (loop-body (stmt), proc-list, mg-state, n − 1))

then if cc (mg-meaning (loop-body (stmt), proc-list, mg-state, n − 1))

                    = 'leave

then 3 + clock (loop-body (stmt), proc-list, mg-state, n − 1)

else 1 + clock (loop-body (stmt), proc-list, mg-state, n − 1) endif

else 1 + ((1 + clock (loop-body (stmt), proc-list, mg-state, n − 1))

+ clock (stmt, proc-list, mg-meaning (loop-body (stmt), proc-list, mg-state, n − 1),

n − 1)) endif

else 0 endif)

Event: Disable clock-loop.

Theorem: clock-if (car (stmt) = 'if-mg) → (clock (stmt, proc-list, mg-state, n)

= if (n ≄ 0) ∧ normal (mg-state)

then if mg-expression-falsep (if-condition (stmt), mg-state) then if normal (mg-meaning (if-false-branch (stmt),

proc-list, mg-state,

n − 1))

then 5 + clock (if-false-branch (stmt), proc-list, mg-state, n − 1)

else 4 + clock (if-false-branch (stmt), proc-list, mg-state, n − 1) endif

elseif normal (mg-meaning (if-true-branch (stmt), proc-list, mg-state, n − 1))

then 5 + clock (if-true-branch (stmt), proc-list, mg-state, n − 1)

else 3 + clock (if-true-branch (stmt), proc-list, mg-state, n − 1) endif

else 0 endif)

Theorem: clock-begin (car (stmt) = 'begin-mg) → (clock (stmt, proc-list, mg-state, n)

= if (n ≄ 0) ∧ normal (mg-state)

then if cc (mg-meaning (begin-body (stmt), proc-list, mg-state, n − 1))

∈ when-labels (stmt) then if normal (mg-meaning (when-handler (stmt),

proc-list, set-condition (mg-meaning (begin-body (stmt),

proc-list, mg-state, n − 1),

            'normal),

n − 1))

then clock (begin-body (stmt), proc-list, mg-state, n − 1)

+ (3 + clock (when-handler (stmt), proc-list, set-condition (mg-meaning (begin-body (stmt),

proc-list, mg-state, n − 1),

                                   'normal),

n − 1))

else clock (begin-body (stmt), proc-list, mg-state, n − 1)

+ (2 + clock (when-handler (stmt), proc-list, set-condition (mg-meaning (begin-body (stmt),

proc-list, mg-state, n − 1),

                                  'normal),

n − 1)) endif

elseif normal (mg-meaning (begin-body (stmt), proc-list, mg-state, n − 1))

then 2 + clock (begin-body (stmt), proc-list, mg-state, n − 1)

else clock (begin-body (stmt), proc-list, mg-state, n − 1) endif

else 0 endif)

Theorem: clock-proc-call

(car (stmt) = 'proc-call-mg)

→ (clock (stmt, proc-list, mg-state, n)

= if (n ≄ 0) ∧ normal (mg-state)

then data-length (def-locals (fetch-called-def (stmt, proc-list))) + length (def-locals (fetch-called-def (stmt, proc-list))) + length (call-actuals (stmt))

+ 1

+ clock (def-body (fetch-called-def (stmt, proc-list)), proc-list, make-call-environment (mg-state,

stmt,

fetch-called-def (stmt,

proc-list)),

n − 1)

              + 5

+ if normal (mg-meaning (def-body (fetch-called-def (stmt,

proc-list)),

proc-list,

make-call-environment (mg-state, stmt, fetch-called-def (stmt,

proc-list)),

n − 1)) then 1

else 3 endif

else 0 endif)

Theorem: clock-predefined-proc-call

 (car (stmt) = 'predefined-proc-call-mg)

→ (clock (stmt, proc-list, mg-state, n)

= if (n ≄ 0) ∧ normal (mg-state) then predefined-proc-call-clock (stmt, mg-state) else 0 endif)

Definition: map-down (mg-state, proc-list, ctrl-stk, temp-stk, addr, cond-list) = p-state (addr,

ctrl-stk,

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list),

list (list ('c-c, mg-cond-to-p-nat (cc (mg-state), cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

          'run)
;; I need the hyp that cc is not 'leave for this theorem because cond-subsetp does not
;; preserves ok-cc unless cond is not 'leave, but I can prove that meaning never
;; returns leave anyway.

Theorem: map-up-vars-inverts-map-down (all-cars-unique (mg-vars)

∧ mg-alistp (mg-vars) ∧ no-p-aliasing (bindings, mg-vars) ∧ mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk)) → (map-up-vars-list (bindings,

map-down-values (mg-vars, bindings, temp-stk), signature (mg-vars))

= mg-vars)

Theorem: cond-subset-preserves-ok-cc

((cc ≠ 'leave)

∧ cond-subsetp (r-cond-list, t-cond-list) ∧ ok-cc (cc, r-cond-list)) → ok-cc (cc, t-cond-list)

Theorem: map-up-inverts-map-down (all-cars-unique (mg-alist (mg-state)) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ cond-subsetp (r-cond-list, t-cond-list) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ (cc (mg-state) ≠ 'leave) ∧ (¬ resource-errorp (mg-state))) → (map-up (map-down (mg-state,

proc-list, ctrl-stk, temp-stk, addr, t-cond-list), signature (mg-alist (mg-state)), t-cond-list)

= mg-state)

;; These are used in the proofs which follow!

Theorem: call-exact-time-hyps1

((car (stmt) = 'proc-call-mg)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list)) → ok-mg-statement (def-body (fetch-called-def (stmt, proc-list)),

make-cond-list (fetch-called-def (stmt, proc-list)), make-name-alist (fetch-called-def (stmt, proc-list)), proc-list)

Theorem: resources-adequate-temp-stk-not-max (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk), p-ctrl-stk-size (ctrl-stk))))

→ ((length (temp-stk) < mg-max-temp-stk-size) = t)

Theorem: plus-difference-cancellation ((x − y) ≄ 0) → (((x − y) + y) = fix (x))

Theorem: lessp-difference-lemma1 ((n < (r + l)) ∧ (r < (m − l))) → ((n < m) = t)

Theorem: resources-adequate-temp-stk-not-max2 ((¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk), p-ctrl-stk-size (ctrl-stk))))

 ∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (n < (predefined-proc-call-temp-stk-requirement (call-name (stmt))

+ length (temp-stk))))

→ ((n < mg-max-temp-stk-size) = t)

Theorem: lessp-difference-lemma3 ((n ≤ p) ∧ (p < (m − c))) → ((m < (n + c)) = f)

Event: Disable lessp-difference-lemma3.

Theorem: resources-adequate-ctrl-stk-not-max ((¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk), p-ctrl-stk-size (ctrl-stk))))

 ∧ (car (stmt) = 'predefined-proc-call-mg)

∧ (n ≤ predefined-proc-call-p-frame-size (call-name (stmt)))) → ((mg-max-ctrl-stk-size < (n + p-ctrl-stk-size (ctrl-stk))) = f)

Theorem: lessp-transitive3 ((y < n) ∧ (n < (m − x))) → (((x + y) < m) = t)

Theorem: lessp-difference (y < (m − x)) → (((x + y) < m) = t)

Theorem: resources-proc-call-temp-stk-ok

((car (stmt) = 'proc-call-mg)

∧ (¬ resources-inadequatep (stmt, proc-list, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))))

→ (((length (temp-stk)

+ data-length (def-locals (fetch-called-def (stmt, proc-list))) + length (def-locals (fetch-called-def (stmt, proc-list))) + length (call-actuals (stmt))) < mg-max-temp-stk-size) = t)

Event: Disable resources-proc-call-temp-stk-ok.

Theorem: user-defined-def-locals-nil (ok-mg-def-plistp (proc-list)

 ∧ (car (stmt) = 'proc-call-mg)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list)) → (length (caddr (assoc (call-name (stmt), translate-proc-list (proc-list))))

= 0)

Event: Disable user-defined-def-locals-nil.

Theorem: user-defined-def-formals-rewrite (ok-mg-def-plistp (proc-list)

 ∧ (car (stmt) = 'proc-call-mg)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list)) → (length (cadr (assoc (call-name (stmt), translate-proc-list (proc-list))))

= (length (def-locals (assoc (call-name (stmt), proc-list))) + length (def-formals (assoc (call-name (stmt), proc-list)))))

Event: Disable user-defined-def-formals-rewrite.

Theorem: difference-preserves-lessp2 (n < m) → (((n − k) < m) = t)

Theorem: plus-lessp ((n + m + x) < (m + n)) = f

Theorem: resources-proc-call-ctrl-stk-ok

((car (stmt) = 'proc-call-mg)

∧ (¬ resources-inadequatep (stmt, proc-list, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list)

∧ user-defined-procp (subr, proc-list)) → ((mg-max-ctrl-stk-size

< (2

+ length (cadr (assoc (call-name (stmt),

translate-proc-list (proc-list))))

+ length (caddr (assoc (call-name (stmt),

translate-proc-list (proc-list))))

+ p-ctrl-stk-size (ctrl-stk))) = f)

Event: Disable resources-proc-call-ctrl-stk-ok.

Event: Make the library "c5".

Index

add-code, 3, 20–25, 27, 29–31, 35–

39, 42, 56–61 add-code-doesnt-affect-other-fie

lds, 27 all-cars-unique, 78, 79 all-labels-unique, 48, 49, 52 all-labels-unique-append, 48 all-labels-unique-reduction, 48 all-labels-unique-reduction2, 48 all-labels-unique-reduction3, 48 array-length, 2, 4, 5 assoc-mg-array-element-assignme

nt-translate-proc-list, 67 assoc-mg-boolean-and-translate-p

roc-list, 67 assoc-mg-boolean-not-translate-p

roc-list, 67 assoc-mg-boolean-or-translate-p

roc-list, 67 assoc-mg-index-array-translate-p

roc-list, 67 assoc-mg-integer-add-translate-p

roc-list, 67 assoc-mg-integer-le-translate-p

roc-list, 67 assoc-mg-integer-subtract-trans

late-proc-list, 67 assoc-mg-integer-unary-minus-tr

anslate-proc-list, 67 assoc-mg-simple-constant-assign

ment-translate-proc-list, 66 assoc-mg-simple-constant-eq-tra

nslate-proc-list, 66 assoc-mg-simple-variable-assign

ment-translate-proc-list, 66 assoc-mg-simple-variable-eq-tra

nslate-proc-list, 66 assoc-user-defined-proc2, 67

begin-body, 20, 23, 30, 31, 42, 60, 61, 72, 73, 76, 77 begin-translation, 23 bindings, 2, 78, 79

call-actuals, 2, 7–10, 69, 70, 74, 77,

81 call-conds, 7, 21, 24, 51 call-exact-time-hyps1, 79 call-name, 7, 10, 69, 71, 80–82 call-translation, 23 car-definedp-defined-procp, 68 car-definedp-defined-procp1, 68 cc, 49, 71, 73, 75, 76, 78, 79 cinfop, 26 clock, 71–78 clock-begin, 76 clock-if, 75 clock-loop, 75 clock-predefined-proc-call, 78 clock-predefined-proc-call-body

-translation, 69, 71 clock-predefined-proc-call-seque

nce, 68, 71 clock-proc-call, 77 clock-prog2, 74 code, 3, 4, 19–23, 25, 27–42, 47, 49–

61, 65, 67, 68 code-add-code-commute, 27 code-always-plistp, 25 code-doesnt-affect-other-fields, 26 collect-labels, 47–49, 52–57, 59, 60,

65 collect-labels-distributes, 48 collect-labels-plistp, 47 collect-labels-predefined-proc-

call-code-nil, 53 collect-labels-push-actuals-code

-nil, 53 collect-labels-push-local-array

-values-code-nil, 53 collect-labels-push-locals-addre

sses-code-nil, 53 collect-labels-push-locals-value

s-code-nil, 53 collect-labels-strip-label, 53 cond-case-jump-label-list, 6, 7 cond-conversion, 6, 7, 50–53 cond-conversion-induction-hint, 51 cond-subset-preserves-ok-cc, 79 cond-subsetp, 49, 79 cond-subsetp-preserves-ok-mg-st

atep, 49 condition-map-code, 7

data-length, 4, 5, 25, 74, 77, 81 def-body, 25, 74, 77–79 def-cond-locals, 21, 24 def-formals, 2, 25, 81 def-locals, 2, 21, 23, 25, 74, 77, 81 def-name, 25 definedp, 66, 68 difference-preserves-lessp2, 81 discard-label, 3, 20, 22, 27 discard-label-doesnt-affect-othe

r-fields, 27

fetch-called-def, 21, 23, 24, 49, 74,

77–79, 81 fetch-label, 3, 6, 7, 9, 10, 19, 21 find-labelp, 5, 24, 48–52 find-labelp-member-collect-labe

ls, 49 find-labelp-monotonic-lessp, 50 find-labelp-reduces-to-member, 52 find-labelp-rewrites-to-member, 48

get, 6 get-cond-case-jump-label-list, 6 greater-label-count-big-enough, 51

identifier-plistp, 49 identifier-plistp-make-cond-list

-ok, 49 idifference, 70 if-condition, 20, 22, 28, 29, 35–41,

54–59, 72, 75 if-false-branch, 20, 23, 29, 30, 37– 40, 59, 72, 75, 76

if-translation, 22

if-true-branch, 20, 22, 29, 30, 35–41, 55–59, 72, 76 index-cond-case-induction-hint, 6 inegate, 69 iplus, 69

label-alist, 3, 7, 19–31, 33–42, 53–61 label-alist-set-label-alist, 27 label-cnt, 3, 7, 19–24, 26–31, 33–42,

50–61, 65 label-cnt-add1-add1-monotonic, 50 label-cnt-big-enough, 50–55, 57–61,

65 label-cnt-big-enough-add1, 52 label-cnt-big-enough-distribute

s, 51 s2, 51

label-cnt-big-enough-for-cond-c

onversion, 51 label-cnt-big-enough-for-predefi ned-proc-call-code, 52 label-cnt-big-enough-for-proc-c

all-code, 51 label-cnt-big-enough-for-push-a

ctuals-code, 51 label-cnt-big-enough-for-push-l ocal-array-values-code, 51 ocals-addresses-code, 51 ocals-values-code, 51 label-cnt-big-enough-not-find-l

abelp, 52 label-cnt-big-enough-not-member, 55 label-cnt-lessp1, 51 label-cnt-list, 7 label-cnt-monotonic, 50 label-cnt-monotonic-cond-conver

sion, 50 label-cnt-monotonic2, 50 label-cnt-monotonic3, 50 label-cnt-stays-big-enough, 52 label-count-big-enough-not-find

-labelp, 51 label-hole-big-enough, 49, 50 labels-unique-append2, 49 labels-unique-begin-case-hyps, 60 labels-unique-if-case, 57 labels-unique-if-case-hyps1, 54 labels-unique-if-case-hyps2, 55 labels-unique-loop-case, 53 labels-unique-not-find-labelp, 49 labels-unique-not-find-labelp1, 49 length, 1–7, 21, 24, 51, 74, 77, 80–82 length-cond-case-jump-label-list, 6 length-cond-conversion, 6 length-label-cnt-list, 7 length-map-call-formals, 1 length-map-call-locals, 2 length-mg-actuals-to-p-actuals, 3 length-mg-to-p-local-values, 4 length-push-actuals-code, 5 length-push-local-array-values-

code, 4 code2, 4

length-push-locals-addresses-co

de, 5 length-push-locals-values-code, 4 length-push-parameters-code, 5 lesser-label-doesnt-disturb-no-

duplicates, 52 lessp-difference, 80 lessp-difference-lemma1, 80 lessp-difference-lemma3, 80 lessp-transitive3, 80 listcars, 1, 2, 25 listcars-map-call-formals, 1 loop-body, 19, 22, 28, 34, 35, 54, 71,

72, 75 loop-translation, 22

make-call-environment, 74, 78 make-cinfo, 3, 19–24, 28–31, 33–42,

53–61 make-cond-list, 24, 49, 79 make-cond-list-ok, 49 make-frame-alist, 2 make-label-alist, 4, 20, 23, 24, 30, 31, 42, 60, 61

make-name-alist, 79 map-call-formals, 1, 2 map-call-formals-plistp, 1 map-call-locals, 2 map-call-locals-plistp, 2 map-call-locals-preserves-listc

ars, 2 map-down, 78, 79 map-down-values, 78, 79 map-up, 79 map-up-inverts-map-down, 79 map-up-vars-inverts-map-down, 78 map-up-vars-list, 79 member-labels-unique-not-find-l

abelp, 52 mg-actuals-to-p-actuals, 2, 3 mg-actuals-to-p-actuals-plistp, 3 mg-alist, 69, 70, 78, 79 mg-alistp, 79 mg-array-element-assignment-cal

l-sequence, 10, 11 mg-array-element-assignment-tra nslation, 16, 17, 67

mg-boolean-and-call-sequence, 9, 11 mg-boolean-and-translation, 15, 17,

67 mg-boolean-not-call-sequence, 10, 11 mg-boolean-not-translation, 15, 17,

67 mg-boolean-or-call-sequence, 9, 11 mg-boolean-or-translation, 14, 17, 67 mg-cond-to-p-nat, 6, 19, 21, 78 mg-expression-falsep, 72, 75 mg-index-array-call-sequence, 10, 11 mg-index-array-translation, 15, 17,

67 mg-integer-add-call-sequence, 9, 11 mg-integer-add-translation, 13, 17,

67 mg-integer-le-call-sequence, 8, 11 mg-integer-le-translation, 12, 17, 67 mg-integer-subtract-call-sequen

ce, 9, 11 mg-integer-subtract-translation, 14,

17, 67 mg-integer-unary-minus-call-seq

uence, 9, 11 mg-integer-unary-minus-translati

on, 13, 17, 67 mg-max-ctrl-stk-size, 78, 80, 82 mg-max-temp-stk-size, 78, 80, 81 mg-meaning, 71–78 mg-simple-constant-assignment-c

all-sequence, 8, 11 mg-simple-constant-assignment-t

ranslation, 11, 12, 17, 66 mg-simple-constant-eq-call-seque

nce, 8, 11 mg-simple-constant-eq-translati

on, 12, 17, 66 mg-simple-variable-assignment-c

all-sequence, 8, 11 mg-simple-variable-assignment-t

ranslation, 11, 17, 66 mg-simple-variable-eq-call-seque

nce, 8, 11 mg-simple-variable-eq-translati

on, 12, 17, 66 mg-to-p-local-values, 1, 4 mg-to-p-local-values-plistp, 1 mg-to-p-simple-literal, 1, 4, 8 mg-to-p-simple-literal-list, 1 mg-vars-list-ok-in-p-state, 79 mg-word-size, 69, 70, 78

nearly-equal-cinfos, 26 nearly-equal-cinfos-translate, 26 new-code-appended-to-old, 47 new-code-appended-to-old1, 47 new-code-begin-case-induction-h

yps, 41 new-code-if-case, 36 new-code-if-case-induction-hyps, 35 new-code-loop-case, 33 new-code-loop-case-induction-hyp

s, 33 new-code-prog2-case, 31 new-code-prog2-case-induction-h

yps, 31 no-duplicates, 48, 52–57, 59, 60, 65 no-duplicates-append-list, 48 no-duplicates-append-list2, 48 no-duplicates-cond-conversion, 52 no-duplicates-cond-conversion-b

ase-case, 52 no-duplicates-proc-call, 53 no-duplicates-right-cons-reducti

on, 52 no-labels-in-push-actuals-code, 5 no-labels-in-push-local-array-v

alues-code, 5 no-labels-in-push-locals-addres

ses-code, 5 no-labels-in-push-locals-values

-code, 5 no-p-aliasing, 79 normal, 71–78 not-find-labelp-predefined-proc

-call-code, 24 not-find-labelp-push-parameters

-code, 50 not-member-cond-conversion, 52 nullify, 3, 26–28, 31–35, 37, 39–42,

47 nullify-cancels-add-code, 27 nullify-code-nil, 27 nullify-doesnt-affect-proc-call

-code, 27 nullify-induction-hint, 27–31 nullify-translate-idempotence, 26 nullify-translate-idempotence2, 26 nullify-translate-leaves-nearly

-equal, 26

ok-cc, 79 ok-cinfop, 4, 25, 31–38, 40–42, 47,

50 ok-cond-list, 49, 50 ok-mg-def-plistp, 49, 66–68, 79, 81 ok-mg-def-plistp1, 66, 68 ok-mg-local-data-decl, 4 ok-mg-local-data-plistp, 4, 5 ok-mg-namep, 49 ok-mg-statement, 49, 79, 81 ok-mg-statep, 49, 79 ok-translation-parameters, 50

p-ctrl-stk-size, 80–82 p-state, 78 plistp, 1–4, 24, 25, 47 plus-difference-cancellation, 80 plus-lessp, 81 predefined-call-translation, 24 predefined-proc-call-clock, 70, 71, 74,

78 predefined-proc-call-code-plistp, 24 predefined-proc-call-p-frame-si

ze, 80 predefined-proc-call-sequence, 10, 21,

24, 52, 53 predefined-proc-call-temp-stk-req

uirement, 80 predefined-procedure-translatio

ns-list, 16, 25 predefined-procp, 67 proc-call-code, 7, 21, 24, 27, 51 prog2-left-branch, 19, 21, 27, 28, 31–

33, 71, 74 prog2-right-branch, 19, 22, 28, 32,

71, 74 prog2-translation, 21 push-actuals-code, 5, 51, 53 push-local-array-values-code, 4, 5, 51,

53 push-locals-addresses-code, 5, 51, 53 push-locals-values-code, 4, 5, 51, 53 push-parameters-code, 5, 7, 50

resource-errorp, 79 resources-adequate-ctrl-stk-not

-max, 80 resources-adequate-temp-stk-not

-max, 80 -max2, 80 resources-inadequatep, 80, 81 resources-proc-call-ctrl-stk-ok, 81 resources-proc-call-temp-stk-ok, 80

set-condition, 73, 76, 77 set-label-alist, 3, 20, 23, 27, 30, 31,

42, 60, 61 set-label-alist-doesnt-affect-ot

her-fields, 27 signal-translation, 21 signalled-condition, 19, 21 signature, 79 simple-mg-type-refp, 1, 2, 4, 5 small-integerp, 69, 70

tag, 2, 10 top, 2, 78, 79 translate, 19–42, 47, 49–52, 54–61,

65, 67, 68 translate-def, 25, 66 translate-def-body, 24, 25, 67 translate-def-body-rewrite, 67 translate-definedp1, 66 translate-leaves-labels-unique, 65 translate-preserves-fields, 25 translate-preserves-ok-cinfop, 25 translate-proc-list, 25, 66–68, 78, 81,

82 translate-proc-list-assoc, 66 translate-proc-list-assoc1, 66 translate-proc-list-assoc2, 66 translate-proc-list1, 25, 66–68

untag, 69, 70 user-defined-def-formals-rewrite, 81 user-defined-def-locals-nil, 81 user-defined-procp, 66–68, 82

when-handler, 21, 23, 30, 31, 73, 76,

77 when-labels, 20, 23, 30, 31, 42, 60,

61, 73, 76