#|
Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Computational Logic, Inc. PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT
IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Computational Logic, Inc. BE LIABLE TO YOU FOR ANY DAMAGES,
ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#
;; Matt Kaufmann
;; From a session with Shaun Cooper, 12/9/91.  Based on CLI Internal
;; Note 210 by Bill Young.

Event: Start with the initial nqthm theory.

Definition: length (x) = if listp (x) then 1 + length (cdr (x))

else 0 endif

Definition: plistp (x) = if listp (x) then plistp (cdr (x))

else x = nil endif

Definition: exp-p (exp)

= if exp ∈ N then t elseif ¬ plistp (exp) then f elseif length (exp) = 3 then if car (exp) = 'plus

then exp-p (cadr (exp)) ∧ exp-p (caddr (exp)) elseif car (exp) = 'times then exp-p (cadr (exp)) ∧ exp-p (caddr (exp)) elseif car (exp) = 'subtract then exp-p (cadr (exp)) ∧ exp-p (caddr (exp)) else f endif

else f endif

Theorem: exp-p-opener (exp ∉ N) → (exp-p (exp)

= if ¬ plistp (exp) then f elseif length (exp) = 3 then if car (exp) = 'plus

then exp-p (cadr (exp)) ∧ exp-p (caddr (exp)) elseif car (exp) = 'times then exp-p (cadr (exp)) ∧ exp-p (caddr (exp)) elseif car (exp) = 'subtract then exp-p (cadr (exp)) ∧ exp-p (caddr (exp)) else f endif

else f endif)

Definition: eval-s (exp) = if ¬ exp-p (exp) then 0

elseif exp ∈ N then exp elseif car (exp) = 'plus then eval-s (cadr (exp)) + eval-s (caddr (exp)) elseif car (exp) = 'times then eval-s (cadr (exp)) ∗ eval-s (caddr (exp)) elseif car (exp) = 'subtract then eval-s (cadr (exp)) − eval-s (caddr (exp)) else 0 endif

Event: Disable exp-p-opener.

Definition: target-inst-p (exp) = if exp ≃ nil then exp ∈ '(add mult sub)

else plistp (exp)

∧ (length (exp) = 2) ∧ (car (exp) = 'pushc) ∧ (cadr (exp) ∈ N) endif

Definition: target-inst-list-p (exp) = if listp (exp)

then target-inst-p (car (exp)) ∧ target-inst-list-p (cdr (exp)) else exp = nil endif

Definition: single-step (inst, s) = case on inst:

case = add then cons (cadr (s) + car (s), cddr (s)) case = mult then cons (cadr (s) ∗ car (s), cddr (s)) case = sub then cons (cadr (s) − car (s), cddr (s)) otherwise cons (cadr (inst), s) endcase

Definition: interpreter-target (inst-list, s) = if listp (inst-list)

then interpreter-target (cdr (inst-list), single-step (car (inst-list), s)) else s endif

Event: Enable exp-p-opener.

Definition: compile (exp) = if ¬ exp-p (exp) then nil

elseif exp ∈ N then list (list ('pushc, exp)) elseif car (exp) = 'plus then append (compile (cadr (exp)),

append (compile (caddr (exp)), list ('add)))

elseif car (exp) = 'times then append (compile (cadr (exp)),

append (compile (caddr (exp)), list ('mult)))

elseif car (exp) = 'subtract then append (compile (cadr (exp)),

append (compile (caddr (exp)), list ('sub)))

else nil endif

Event: Disable exp-p-opener.

Theorem: compile-preserves-legality exp-p (exp) → target-inst-list-p (compile (exp))

Theorem: interpreter-target-append interpreter-target (append (inst-list1 , inst-list2 ), s) = interpreter-target (inst-list2 , interpreter-target (inst-list1 , s))

#| first version:  provides too weak of an inductive hypothesis
(prove-lemma compiler-correctness (rewrite)
  (implies (exp-p exp)
           (equal (eval-s exp)
                  (car (interpreter-target (compile exp) s)))))
|#

Definition: compiler-correctness-induct (exp, s) = if length (exp) = 3

then compiler-correctness-induct (cadr (exp), s)

∧ compiler-correctness-induct (caddr (exp),

cons (eval-s (cadr (exp)), s))

else t endif

Theorem: compiler-correctness-plus exp-p (exp) → (interpreter-target (compile (exp), s) = cons (eval-s (exp), s))

Theorem: compiler-correctness exp-p (exp) → (eval-s (exp) = car (interpreter-target (compile (exp), s)))

Index

compile, 3, 4 compile-preserves-legality, 4 compiler-correctness, 4 compiler-correctness-induct, 4 compiler-correctness-plus, 4

eval-s, 2, 4 exp-p, 1–4 exp-p-opener, 2

interpreter-target, 3, 4 interpreter-target-append, 4

length, 1–4

plistp, 1, 2

single-step, 3

target-inst-list-p, 3, 4 target-inst-p, 2, 3