This note describes my experiences at Computational Logic, Inc. learning to use the ACL2 programming and theorem proving environment [Moore].
The first few days were spent becoming familiar with the Emacs text editor. I went through the entire tutorial and memorized the most important functions. Once I felt I could use the commands reasonably well, I began learning Common LISP. This took quite a long time and I progressed from very simple functions to more complex ones. Mostly, I learned LISP through a series of exercises given to me. These were:
(defun square (x) (* x x)).
After completing all of these functions, I went back and reviewed everything I had written, beginning to form hypotheses in my head. Then I wrote down everything I could think of that could possibly be proved as a theorem about any of my functions individually, or in combination with each other. I then began testing these theorems in ACL2. I revised, and sometimes rewrote, every conjecture until ACL2 would accept it as a theorem. This consisted of going back through the computer's processes and attempting to figure out myself what aspect of the theorem needed mending. This was very difficult because it was often hard to follow the computer's "thought" process as it attempted the proof. Eventually, though often with help, ACL2 proved all of my conjectures.
After this I began working on my largest project: designing a new language. This new language was to be written inside of LISP. It was to be a postfix language, whereas LISP is a prefix language. There were only to be three types of functions in my new language: "evaluate", "store", and "declare". "Evaluate" simply evaluates a postfix expression (e.g. (2 3 +)). "Store" takes the first variable on the given stack and stores it in the alist bound with the given variable. "Declare" takes the given variable, puts it in the alist and binds it with zero. Therefore, a state that would be given the computer would have a list of functions to be performed (the program), a program counter (to keep track of which function is being performed), the variable alist which the program modifies, and the stack which is also used by the program.
I started by writing each of the three individual functions. Then I wrote recognizers for each, so that if an incorrect function or state was entered an error would not come up in ACL2. At that point, each function could be used individually with respect to a given state. I then wrote functions designed to allow the three functions to all be used at the same time to produce a desired affect on a given stack and variable alist. At this time a series of functions could be entered along with a stack and a variable alist and each function would be performed in order. If part of entry had been written incorrectly, instead of returning the new, modified state, an "error" would simply be returned.
I then wrote another new set of functions, different from the original three, but having the capability of producing the same results. These functions included "push-constant" which pushes an integer onto the stack; "push-var" which pushes the integer bound with the given variable in the alist; "add" which takes the top two values on the stack, adds them, and pushes the result back onto the stack; "sub" which does the same as "add" but subtraction instead; "mult" which multiplies; and "pop" which takes the top value from the stack and stores it in the alist bound with a given variable.
The original three functions can be translated into programs consisting of these new functions (e.g. (declare q) is the same as (push-constant 0) (pop q)). I wrote functions that would take a program in the original language and translate it into a program in the new language. These started out by translating a single function and then grew to be able to translate an entire program.
Then came the hard part. I wrote theorems about the relationship between the two languages and attempted to prove them. This was not exactly successful. The primary goal was to prove that, if a state was acceptable with the program in the original language, then that state translated into the new language was also acceptable. After that was finished, I was also supposed to prove that the translated state was not only acceptable, but that it performed the same tasks as the original would have. I never really had to worry about that though, because I never made it past the first step.
Although from the first time I attempted to prove the theorem until the last I did make some progress, it was still not really close to being accepted as a theorem. We had somewhat of a hard time finding out why this was. I knew that the translator worked because I had tested it on many cases, but to get the computer to understand that is a different story altogether. Though a specific cause was not to be found, I suspect that the problems stem from the way I designed the two languages and especially the recognizers for each. As far as I can tell, the errors were results of the syntax of these very early functions that, for some reason or another, cause the theorem prover to reject my theorem.
Overall, this has been quite an experience for a seventeen year old to partake in. Learning the ins and outs of LISP (and by no means do I know all or even most of them), although somewhat time consuming, came fairly easily and rather swiftly for me. When I look at the progress I have made, it is surprising to see the contrast between the first functions I wrote and the simple languages I designed. This had definitely been rewarding with regards to an education in Computer Science. As for the the use of the theorem prover, I don't what to say. I'm pretty sure that I could not have used it with much success at all without help from someone who was skilled in operating it. Although I could follow the computers processes fairly well as it went through a proof, I often needed help in understanding why some theorem wasn't accepted or what I needed to change about a conjecture to allow it to be proven. In that respect, the theorem prover definitely takes much more time and effort to learn, and without the instruction of someone who is skilled in using it, it would be quite difficult to understand.
;; square of a number
(defun square (x)
(* x x))
;; length of list x
(defun lgth (x)
(if (consp x)
(+ 1 (lgth (cdr x)))
0))
;; append x onto y
(defun app (x y)
(if (consp x)
(cons (car x) (app (cdr x) y))
y))
;; reverse the order of x
(defun rev (x)
(if (consp x)
(append (rev (cdr x)) (list (car x)))
nil))
;; add up all the elements of a list
(defun fadd (l)
(if (consp l)
(+ (car l) (fadd (cdr l)))
0))
;; is x a member of l
(defun my-member (x l)
(if (not (consp l))
nil
(if (equal x (car l))
t
(my-member x (cdr l)))))
;; find the last element of a list
(defun qlast (l)
(if (consp l)
(if (and (consp l) (not (consp (cdr l))))
(car l)
(qlast (cdr l)))
nil))
;; square each element of a list
(defun sqlist (l)
(if (consp l)
(append (list (* (car l) (car l))) (sqlist (cdr l)))
nil))
;; get the ith element of list l
(defun geti (i l)
(if (zp i)
(car l)
(geti (- i 1) (cdr l))))
;; replace the ith element of y with x
(defun fput (x i y)
(if (zp i)
(append (list x) (cdr y))
(cons (car y) (fput x (- i 1) (cdr y)))))
;; list all but the last element of list x
(defun mybutlast (x)
(if (atom x)
nil
(if (and (consp x) (atom (cdr x)))
nil
(cons (car x) (mybutlast (cdr x))))))
;; non-recursive form of previous example
(defun mybutlast2 (x)
(reverse (cdr (reverse x))))
;; return first n elements of list x
(defun firstn (n x)
(if (zp n)
nil
(cons (car x) (firstn (- n 1) (cdr x)))))
;; remove first occurence of x in l
(defun my-remove (x l)
(if (atom l)
l
(if (equal x (car l))
(cdr l)
(cons (car l) (my-remove x (cdr l))))))
;; Determine whether an argument is a true-listp containing
;; only integers
(defun qinteger-listp (l)
(if (consp l)
(and (integerp (car l))
(qinteger-listp (cdr l)))
(equal l nil)))
;; n factorial
(defun fact1 (n)
(if (zp n)
n
(if (equal n 1)
n
(* n (fact1 (1- n))))))
;; n factorial using an accumulator
(defun fact2 (n acc)
(If (zp n)
0
(if (equal n 1)
acc
(fact2 (1- n) (* n acc)))))
(defun fact3 (n)
(fact2 n 1))
;; fibonacci
(defun fib (k)
(if (zp k)
1
(if (equal k 1)
1
(+ (fib (- k 1)) (fib (- k 2))))))
;; fib is called 512 times when computing (fib 10). It
;; can also be thought of as being called 2 to the k-1 power.
;; fibonacci with accumulators
(defun fib1 (k acc1 acc2)
(if (zp k)
acc1
(fib1 (- k 1) acc2 (+ acc1 acc2))))
(defun fib2 (k)
(fib1 k 1 1))
;; fib1 is called 9 times when computing (fib2 10).
;; It can also be thought of as calling fib1 k-1 times.
;; adds matching elements of two lists.
(defun plus (x y)
(if (or (atom x)
(atom y))
nil
(if (not (equal (len x) (len y)))
nil
(cons (+ (car x) (car y)) (plus (cdr x) (cdr y))))))
;; a set is a true-listp with no duplicates
(defun setp (l)
(if (atom l)
(null l)
(if (member-equal (car l) (cdr l))
nil
(setp (cdr l)))))
(defthm setp-true-listp
(implies (setp l)
(true-listp l)))
(defun no-dups (l)
(if (atom l)
t
(and (not (member-equal (car l) (cdr l)))
(no-dups (cdr l)))))
(defthm setp-cdr
(implies (and (consp l)
(setp l))
(setp (cdr l))))
(defthm setp-no-dups
(implies (setp l)
(no-dups l)))
;; observation: setp implies that there are no duplicates in l
;; and that l is a true-listp and that l is a consp or nil.
;; removes duplicate elements
(defun remove-dup (l)
(if (atom l)
nil
(if (member-equal (car l) (cdr l))
(remove-dup (cdr l))
(cons (car l) (remove-dup (cdr l))))))
(defthm remove-dup-member-equal
(implies (member-equal a (remove-dup b))
(member-equal a b)))
(defthm setp-remove-dup1
(setp (remove-dup l)))
(defthm remove-dup-no-dups
(no-dups (remove-dup l)))
;; observation: remove-dup implies that there is only one of
;; every element in set l. It also implies that if there were
;; duplicates to start out with, the last one is remaining
;; and the first one(s) was/were taken out. Also, l is in
;; the same order as before only with the duplicates taken out.
;; determines whether x is in set s
(defun elementp (x s)
(member-equal x s))
;; observation: elementp implies that x is an element of set s
;; if x is a member of list s.
(defthm elementp-member-equal
(implies (elementp x s)
(member-equal x s))
:rule-classes nil)
;; determines the number of elements in a set s
(defun set-size (s)
;; assumes s is a set
(len s))
;; observation: set-size implies that the set-size of s is equal
;; to the len of s.
;; determines the number of distinct elements in set l
(defun set-size2 (l)
;; assumes s may not be a setp
(len (remove-dup l)))
(defthm setp-remove-dup
(implies (setp s)
(equal (remove-dup s) s)))
(defthm set-size-len
(implies (setp l)
(equal (set-size2 l) (len l)))
:rule-classes nil)
(defthm setp-set-size
(implies (setp s)
(equal (set-size2 s)
(set-size s))))
;;(in-theory (disable set-size2))
;; observation: set-size2 implies that the number of distinct
;; elements of set l is equal to the len of list l after
;; removing all the duplicates in l.
;; determines if all elements of x are in y, assuming x and y
;; are sets
(defun subset (x y)
(if (endp x)
t
(and (member-equal (car x) y)
(subset (cdr x) y))))
(defthm elementp-subset
(implies (and (subset x y)
(elementp z x))
(elementp z y)))
;; observation: subset implies that y is a consp and that every
;; member of x is also a member of y.
;; returns all elements that are in either x, y or both,
;; assuming x and y ar sets
(defun my-union (x y)
(if (atom x)
y
(if (member-equal (car x) y)
(my-union (cdr x) y)
(cons (car x) (my-union (cdr x) y)))))
(defthm elementp-my-union
(implies (elementp x (my-union y z))
(or (elementp x y)
(elementp x z)))
:rule-classes nil)
(defthm elementp-my-union2
(implies (and (elementp x (my-union y z))
(not (elementp x y)))
(elementp x z)))
(defthm elementp-my-union3
(implies (elementp x y)
(elementp x (my-union y z))))
(defthm elementp-my-union4
(implies (elementp x z)
(elementp x (my-union y z))))
;; observation: union implies ___?
;; returns all elements that are in both x and y,
;; assuming x and y are sets
(defun intersect (x y)
(if (consp x)
(if (not (member-equal (car x) y))
(intersect (cdr x) y)
(cons (car x) (intersect (cdr x) y)))
nil))
(defthm intersect-elementp
(implies (elementp a (intersect x y))
(and (elementp a x)
(elementp a y))))
(defthm equal-intersect-elementp
(implies (and (elementp x y)
(elementp x (intersect y z)))
(elementp x z)))
;; observation: intersect implies all elements in the new set
;; formed by intersect were contained in both set x and set y. Also,
;; elements remaining are in the same order as they were initially.
;; returns all elements of x that are not in y, assuming x and y
;; are sets
(defun set-diff (x y)
(if (consp x)
(if (member-equal (car x) y)
(set-diff (cdr x) y)
(cons (car x) (set-diff (cdr x) y)))
nil))
(defthm set-diff-not-member-equal
(implies (member-equal x (set-diff y z))
(not (member-equal x z))))
(defthm set-diff-member-equal
(implies (member-equal x (set-diff y z))
(and (member-equal x y)
(not (member-equal x z)))))
(defthm set-diff-subset
(implies (subset (set-diff x y) y)
(subset x y)))
;; observation: set-diff implies that none of the elements
;; returned were contained in set y. Also that the elements
;; returned are in the same order as originally.
;; determines if set x and set y contain the same elements
(defun set-equal (x y)
(and (subset x y)
(subset y x)))
(defthm set-equal-subset
(implies (set-equal x y)
(and (subset x y)
(subset y x))))
;; observation: set-equal implies that x is a subset of y
;; and that y is a subset of x. Does not imply that
;; the elements of x are in the same order as the elements in y.
;; counts the number of times x occurs in y, not assuming
;; y is a set.
(defun occurrences (x y)
(if (consp y)
(if (equal x (car y))
(+ 1 (occurrences x (cdr y)))
(occurrences x (cdr y)))
0))
(defthm setp-elementp-occurrences
(implies (and (setp y)
(elementp x y))
(equal (occurrences x y) 1)))
;; This section deals with bit vectors
;; (e.g. (1 0), (1 0 0 1 1 0)).
;; 1. recognizer
(defun bit-vectorp (l)
(if (atom l)
(null l)
(if (equal (car l) 1)
(bit-vectorp (cdr l))
(if (equal (car l) 0)
(bit-vectorp (cdr l))
nil))))
;; 2. all vectors of length n
(defun addbit (x l)
(if (atom l)
nil
(cons (cons x (car l)) (addbit x (cdr l)))))
(defun extendvec (l)
(append (addbit 1 l) (addbit 0 l)))
(defun kextend (k l)
(if (or (equal k 1)
(zp k))
l
(kextend (- k 1) (extendvec l))))
(defun all-vectors (x)
(kextend x '((1) (0))))
;; 3. modification
(defun addbit (x l)
(if (atom l)
nil
(cons (cons x (car l)) (addbit x (cdr l)))))
(defun extendvec2 (x l)
(if (atom x)
nil
(append (addbit (car x) l) (extendvec2 (cdr x) l))))
(defun listl (l)
(if (atom l)
l
(cons (list (car l)) (listl (cdr l)))))
(defun kextend2 (k l x)
(if (or (equal k 1)
(zp k))
l
(kextend2 (- k 1) (extendvec2 x l) x)))
(defun all-vectors2 (k l)
(kextend2 k (listl l) l))
;; a. recognizer- Checks that all members of a list have
;; some property. Can be combined with a check for true-listp.
(defun all-x (l)
(if (atom l)
(null l)
(if (x (car l))
(all-x cdr l)
nil)))
;; b. performs a function on every element of a list.
(defun xlist (l)
(if (atom l)
nil
(cons (x (car l)) (xlist (cdr l)))))
;; c. combines all the elements of a list using function x.
(defun xcombine (l)
(if (atom l)
0 or 1- depends
(x (car l) (xcombine (cdr l)))))
;; d. counts the number of X's in a list
(defun occur (x l)
(if (atom l)
0
(if (equal x (car l))
(+ 1 (occur x (cdr y)))
((occur x (cdr y))))))
;;e. combine matching elements of two lists using the function X.
(defun Xboth (x y)
(if (or (atom x)
(atom y))
nil
(if (not (equal (len x) (len y)))
nil
(cons (X (car x) (car y)) (Xboth (cdr x) (cdr y))))))
;; determines whether argument is a true-listp of cons pairs
(defun an-alistp (alist)
(if (true-listp alist)
(if (consp alist)
t
nil)
nil))
;; determines whether a name is bound in a list
(defun my-boundp (name alist)
(if (atom alist)
nil
(if (equal name (car (car alist)))
t
(my-boundp name (cdr alist)))))
;; adds pair to alist, replacing existing value of name, if any
(defun bind (val name alist)
(if (atom alist)
(cons (cons name val) alist)
(if (my-member name (car alist))
(fput (cons name val) 0 alist)
(cons (car alist) (bind val name (cdr alist))))))
;; returns the value associated with a name or nil
(defun binding (name alist)
(if (endp alist)
nil
(if (equal name (caar alist))
(car alist)
(binding name (cdr alist)))))
(defun val (name alist)
(cdr (binding name alist)))
(defun new-binding (name alist)
(if (atom alist)
nil
(if (equal name (caar alist))
(car alist)
(new-binding name (cdr alist)))))
(defun my-binding (name alist)
(if (my-boundp name alist)
(if (member-equal name (car alist))
(cdr (car alist))
(binding name (cdr alist)))
nil))
;; removes the first pair from alist if there is one
(defun unbind (name alist)
(if (endp alist)
alist
(if (equal name (caar alist))
(cdr alist)
(cons (car alist) (unbind name (cdr alist))))))
;; returns list of names bound in alist
(defun domain (alist)
(if (atom alist)
nil
(append (list (car (car alist))) (domain (cdr alist)))))
;; returns the list of values bound to names in alist
(defun range (alist)
(if (atom alist)
nil
(append (list (cdr (car alist))) (range (cdr alist)))))
;; 2. phonebook application using alists
;; is bk a legal phonebook
(defun pnump (n)
(and (integerp n)
(< 0 n)
(<= n 9999999)
(>= n 1000000)))
(defun namep (name)
(symbolp name))
(defun allpnump? (alist)
(if (atom alist)
(null alist)
(if (pnump (car (range alist)))
(allpnump? (cdr alist))
nil)))
(defun allnamep? (alist)
(if (atom alist)
(null alist)
(if (namep (car (domain alist)))
(allnamep? (cdr alist))
nil)))
(defun phonebook? (bk)
(if (and (allpnump? bk)
(allnamep? bk))
t
nil))
;; does nm have a phone number in bk
(defun in-book? (nm bk)
(if (member-equal nm (domain bk))
t
nil))
;; find nm's number in the phonebook
(defun find-phone (nm bk)
(if (in-book? nm bk)
(binding nm bk)
nil))
;; give nm the phone number pnum in bk
(defun add-phone (nm pnum bk)
(bind pnum nm bk))
;; change nm's number to pnum in bk
(defun change-phone (nm pnum bk)
(bind pnum nm bk))
;; remove nm's number from bk
(defun del-phone (nm bk)
(unbind nm bk))
;; 3. grade book
;; is n a legal gradebook
(defun pnump1 (n)
(and (integerp n)
(< 0 n)
(<= n 100)))
(defun namep (name)
(symbolp name))
(defun allpnump1? (alist)
(if (atom alist)
(null alist)
(if (pnump1 (car (range alist)))
(allpnump1? (cdr alist))
nil)))
(defun allnamep? (alist)
(if (atom alist)
(null alist)
(if (namep (car (domain alist)))
(allnamep? (cdr alist))
nil)))
(defun gradebook? (bk)
(if (and (allpnump1? bk)
(allnamep? bk))
t
nil))
;; does nm have a grade in bk
(defun in-book? (nm bk)
(if (member-equal nm (domain bk))
t
nil))
;; find nm's grade in the gradebook
(defun find-grade (nm bk)
(if (in-book? nm bk)
(binding nm bk)
nil))
;; give nm the grade pnum in bk
(defun add-grade (nm pnum bk)
(bind pnum nm bk))
;; change nm's grade to pnum in bk
(defun change-grade (nm pnum bk)
(bind pnum nm bk))
;; remove nm's grade from bk
(defun del-grade (nm bk)
(unbind nm bk))
;; insertion sort
;; insert a single element into the correct place in a list
(defun insertx (l acc)
(if (atom acc)
(cons l acc)
(if (and (equal (len acc) 1)
(> l (car acc)))
(cons (car acc) (list l))
(if (<= l (car acc))
(cons l acc)
(cons (car acc) (insertx l (cdr acc)))))))
;; sort a list of integers
(defun insersort (l)
(if (atom l)
nil
(insertx (car l) (insersort (cdr l)))))
;; bubble sort
;; checks list. if a pair is out of order, swaps them
(defun pass (l)
(if (atom l)
nil
(if (atom (cdr l))
l
(if (< (car l) (cadr l))
(cons (car l) (pass (cdr l)))
(cons (cadr l) (pass (cons (car l) (cddr l))))))))
;; calls pass k times on the list l
(defun passk (k l)
(if (zp k)
l
(passk (- k 1) (pass l))))
;; sorts list l using bubble sort
(defun bubble1 (l)
(passk (1- (len l)) l))
;; the number of comparisons made is equal to ((len l)-1) squared
;; more efficient form of bubble sorting
;; calls function only on first n elements of list
(defun pass2 (n l)
(if (zp n)
l
(if (atom l)
nil
(if (atom (cdr l))
l
(if (< (car l) (cadr l))
(cons (car l) (pass2 (1- n) (cdr l)))
(cons (cadr l) (pass2 (1- n) (cons (car l) (cddr l)))))))))
;; calls pass2 k times, looking at one less element each time
(defun pass2k (k l)
(if (zp k)
l
(pass2k (- k 1) (pass2 k l))))
;; sorts list l using pass2k
(defun bubble2 (l)
(pass2k (len l) l))
;; the number of comparisons made is equal to
;; (((len l)-1)+((len l)-2)+...+2+1)
;; 1. recognizer
(defun ok1 (l stack-depth)
(if (null l)
(equal stack-depth 1)
(let ((x (car l))
(rest (cdr l)))
(if (integerp x)
(ok1 rest (1+ stack-depth))
(if (member-equal x '(+ * -))
(if (< stack-depth 2)
nil
(ok1 rest (1- stack-depth)))
nil)))))
(defun ok (l)
(ok1 l 0))
;; 2. interpreter
;; defining stack functions
;; is the stack empty
(defun empty (stack)
(null stack))
;;returns first item on the stack
(defun top (stack)
(car stack))
;;pushes x onto the stack
(defun pushx (x stack)
(cons x stack))
;;returns the first element of the stack
(defun pop-st (stack)
(cdr stack))
;;returns the second element on the stack
(defun top2 (stack)
(cadr stack))
;; Evaluating expressions
;;differentiates between * + and -
(defun apply-op (op arg1 arg2)
(if (equal op '+)
(+ arg1 arg2)
(if (equal op '*)
(* arg1 arg2)
(- arg1 arg2))))
;; evaluates an expression
(defun eval1 (expr stack)
(if (atom expr)
stack
(if (integerp (car expr))
(eval1 (cdr expr) (pushx (car expr) stack))
(eval1 (cdr expr)
(pushx (apply-op (car expr) (top2 stack) (top stack))
(pop-st (pop-st stack)))))))
;; 3. extend evaluator to show error if called on non-legal
;; expression
(defun evaluate (expr)
(if (ok expr)
(eval1 expr nil)
'error))
;; B. adding variables to our language
;; 1. recognizer
(defun ok-expression1 (expr vars stack)
(if (atom expr)
t
(let ((x (car expr))
(rest (cdr expr)))
(if (integerp x)
(ok-expression1 rest vars (pushx 0 stack))
(if (member-equal x (domain vars))
(ok-expression1 rest vars (pushx 0 stack))
(if (member-equal x '(+ * -))
(if (< (len stack) 2)
nil
(ok-expression1 rest vars (cdr stack)))
nil))))))
;; 2. interpreter
;; creates a state from a given variable list and stack
(defun make-state (var-alist stack)
(list var-alist stack))
;; returns the variable list from the state
(defun vars (st)
(car st))
;;returns the stack from the state
(defun stack (st)
(cdr st))
;; C. extending the language 1
;; recognizer for statements
;; recognizer for eval statements
(defun ok-eval-statement (stmt vars stack)
(and (equal (car stmt) 'eval-expression)
(ok-expression (cdr stmt) vars stack)))
(defun ok-eval-statement1 (statement)
(if (atom statement)
nil
(if (equal 'eval-expression (car statement))
t
nil)))
(defun ok-eval-statement2 (statement st)
(if (ok-expression (cdr statement) (vars st))
t
nil))
(defun ok-eval-statement (statement st)
(if (and (ok-eval-statement1 statement)
(ok-eval-statement2 statement st))
t
nil))
;; recognizer for store statements
(defun ok-store-statement1 (statement)
(if (atom statement)
nil
(if (equal 'store (car statement))
t
nil)))
(defun ok-store-statement2 (statement st)
(if (atom (stack st))
nil
(if (member-equal (cadr statement) (domain (vars st)))
t
nil)))
(defun ok-store-statement (statement st)
(if (and (ok-store-statement1 statement)
(ok-store-statement2 statement st))
t
nil))
;; D. extending the language 2
;; add declare to statement types
;; recognizer for declare statements
(defun ok-declare-statement1 (stmt)
(if (atom stmt)
nil
(if (equal (car stmt) 'my-declare)
t
nil)))
(defun ok-declare-statement2 (stmt st)
(if (my-boundp (cadr stmt) (vars st))
nil
t))
(defun ok-declare-statement (stmt st)
(if (and (ok-declare-statement1 stmt)
(ok-declare-statement2 stmt st))
t
nil))
;; recognizer for all types of statements to this point
(defun ok-statement2 (stmt st)
(if (or (ok-eval-statement stmt st)
(ok-store-statement stmt st)
(ok-declare-statement stmt st))
t
nil))
;; interpreter for programs in this language
(defun int-statement (stmt st)
(if (equal (car stmt) 'store)
(store (cadr stmt) st)
(if (equal (car stmt) 'my-declare)
(my-declare (cadr stmt) st)
(if (equal (car stmt) 'eval-expression)
(eval-expression (cadr stmt) st)
'error))))
(defun all-ok1 (prog st)
(if (atom prog)
t
(if (ok-statement2 (car prog) st)
(all-ok1 (cdr prog) st)
nil)))
(defun all-ok (prog st)
(if (atom prog)
nil
(if (all-ok1 prog st)
t
nil)))
(defun int (prog st)
(if (atom prog)
st
(if (all-ok prog st)
(int (cdr prog) (int-statement (car prog) st))
'error)))
;; E. extending the language 3
;; new state; the state is a list (prog pc vars stack)
(defun new-prog (st)
(car st))
(defun new-pc (st)
(cadr st))
(defun new-vars (st)
(caddr st))
(defun new-stack (st)
(cadddr st))
;; fetches the instruction at location pc in the program
(defun fetch (st)
(geti (new-pc st) (new-prog st)))
;; executes statement in new state
(defun execute (stmt st)
(cons (new-prog st)
(cons (new-pc st)
(int-statement stmt
(cons (new-vars st)
(new-stack st))))))
;; Returns the same state, but with the pc increased by one
(defun bump-pc (st)
(cons (new-prog st)
(cons (+ 1 (new-pc st))
(cons (new-vars st) (new-stack st)))))
;; top-level interpreter function
(defun interp (st)
(declare (xargs :measure (nfix (- (len (new-prog st))
(new-pc st)))))
(let ((prog (new-prog st))
(pc (new-pc st)))
(if (and (naturalp pc)
(< pc (len prog)))
(let ((instr (fetch st)))
(interp (execute instr (bump-pc st))))
st)))
;; F. the target language
;; recognizer for target language
(defun ok-push-constant (stmt)
(if (and (equal (car stmt) 'push-constant)
(integerp (cadr stmt)))
t
nil))
(defun ok-push-var (stmt st)
(if (and (equal (car stmt) 'push-var)
(my-boundp (cadr stmt) (new-vars st)))
t
nil))
(defun ok-add (stmt st)
(if (and (equal (car stmt) 'add)
(< 1 (len (new-stack st))))
t
nil))
(defun ok-sub (stmt st)
(if (and (equal (car stmt) 'sub)
(< 1 (len (new-stack st))))
t
nil))
(defun ok-mult (stmt st)
(if (and (equal (car stmt) 'mult)
(< 1 (len (new-stack st))))
t
nil))
(defun ok-pop (stmt st)
(if (and (equal (car stmt) 'pop)
(< 0 (len (new-stack st))))
t
nil))
(defun ok-target-prog1 (stmt st)
(if (atom stmt)
st
(if (or (ok-pop stmt st)
(ok-mult stmt st)
(ok-sub stmt st)
(ok-add stmt st)
(ok-push-var stmt st)
(ok-push-constant stmt))
t
nil)))
(defun ok-target-prog (prog st)
(if (atom prog)
t
(if (ok-target-prog1 (car prog) st)
(ok-target-prog (cdr prog) st)
nil)))
;; interpreter for new statements in the target language
(defun make-target-state (prog pc vars stack)
(list* prog pc vars stack))
(defun action-push-constant (stmt st)
(cons (new-prog st)
(cons (new-pc st)
(cons (new-vars st)
(pushx (cadr stmt) (new-stack st))))))
(defun action-push-var (stmt st)
(make-target-state (new-prog st)
(new-pc st)
(new-vars st)
(pushx (val (cadr stmt) (new-vars st)) (new-stack st))))
(defun action-add (st)
(cons (new-prog st)
(cons (new-pc st)
(cons (new-vars st)
(pushx (+ (top (new-stack st)) (top2 (new-stack st)))
(cddr (new-stack st)))))))
(defun action-sub (st)
(cons (new-prog st)
(cons (new-pc st)
(cons (new-vars st)
(pushx (- (top2 (new-stack st)) (top (new-stack st)))
(cddr (new-stack st)))))))
(defun action-mult (st)
(cons (new-prog st)
(cons (new-pc st)
(cons (new-vars st)
(pushx (* (top2 (new-stack st)) (top (new-stack st)))
(cddr (new-stack st)))))))
(defun action-pop (stmt st)
(cons (new-prog st)
(cons (new-pc st)
(cons (bind (top (new-stack st)) (cadr stmt) (new-vars st))
(cdr (new-stack st))))))
;; interprets the different statements within the language
(defun interprete1 (stmt st)
(case (car stmt)
(push-constant (action-push-constant stmt st))
(push-var (action-push-var stmt st))
(add (action-add st))
(sub (action-sub st))
(mult (action-mult st))
(pop (action-pop stmt st))
(otherwise st)))
(defun t-int (st)
(let ((prog (new-prog st))
(pc (new-pc st)))
(if (< pc (len prog))
(let ((instr (fetch st)))
(t-int (interprete1 instr (bump-pc st))))
st)))
;; G. translation
;; all have the same effects on vars and stack
;; (interp '(((store b)) 0 ((a .6) (b)) 9 8 7))
;; same as
;; (t-int '(((pop b)) 0 ((a . 6) (b)) 9 8 7))
;; (interp '(((my-declare z)) 0 ((a . 6) (b)) 9 8 7))
;; same as
;; (t-int '(((push-constant 0) (pop z)) 0 ((a . 6) (b)) 9 8 7))
;; (interp '(((eval-expression (2 b *))) 0 ((a . 6) (b . 5)) 9 8 7))
;; same as
;; (t-int '(((push-constant 2) (push-var b)
;; (mult)) 0 ((a . 6) (b . 5)) 9 8 7))