You might also want to refer to the Hyper-Card for ACL2 Programming.
Goal: Using the analogous method, find out about the function
But almost all users interact with ACL2 via one of two interfaces. One is
Emacs, where the ACL2 image is run in Emacs'
thereby allowing the user to cut-and-paste between a script buffer containing
an evolving file of ACL2 commands and the Lisp execution environment in which
those commands are carried out. For readers unfamiliar with Emacs we list
a few handy Emacs commands below.
The other standard interface is the ACL2 Sedan by Dillinger, Manolios, and Chamarthi, which is an Eclipse interface that protects the user from many common mistakes and provides some extensions for termination analysis and testing. Instructions for running an ACL2s demonstration session on your own may be found here. The instructions are specific to a particular course in the Department of Computer Science at the University of Texas at Austin, but should be understandable to anybody who has an installed ACL2s. Installation instructions are included.
This document is written as though Emacs were being used. But modulo the keystroke details involved in interaction (e.g., of
“pasting a command into the
*shell* buffer” versus “clicking the ‘Advance Todo Line’ button”) the discussion can be carried out in any ACL2 environment.
emacsto the Unix shell.
meta-x shellin Emacs.
*shell*, with the Unix prompt in it.
acl2(followed by return) in the
ACL2 Version 2.2 built August 23, 1998 14:52:09.and some other text, ending with
ACL2 !>The part at the bottom is the ACL2 prompt.
:program(followed by return).
:redef(followed by return).
It should be
ACL2 p!>If it is not, something is wrong! Have you followed the directions above?
By typing certain ``bad'' expressions you can get ACL2 into a state in which the prompt is different. But these ``bad states'' have prompts that look very similar to ACL2's ``normal'' prompt.
||Good||ACL2 read-eval-print loop||type Lisp expressions to evaluate|
||Bad||Common Lisp debugger||exit by typing
||Bad||Common Lisp top-level||enter ACL2 by typing
In all of these cases the ``
ACL2'' you see is not a
sign that you are in the ACL2 system. It is a sign that the ``current symbol
ACL2. If you do not know what a symbol package is,
don't worry about it. Just know that it is not the ``
that is important about the prompt, it is the other parts!
*shell*buffer. Then type return. It should print
T. The value of the Lisp expression
Try these three:
(equal 1 2)
(if t 1 2)
(if nil 1 2)
2. The second and third should return
2, respectively, because
(if x y z)means ``if
It is easy to make syntax mistakes that throw you into the debugger. Try typing the following, including the period at the end of the line, and then type return
(equal 1 1).
This is a debugger command. In this situation it causes control to be transferred back to the top-level of the ACL2 command loop. You should see the ACL2 prompt again.
If you accidentally type
:q while in the ACL2 command loop
(instead of while in the debugger), what happens? Try typing
:qis an ACL2 ``keyword command'' that causes ACL2 to transfer control back to the Common Lisp top-level. You should see the Common Lisp top-level prompt. You have exited from the ACL2 command loop.
The Common Lisp top-level is also a read-eval-print loop, but one that executes raw Common Lisp without any syntax checking. You should get back into ACL2 by typing
*shell*buffer: click and drag through the expression, then move the mouse to the
*shell*buffer and click middle. Then type return in the
*shell*buffer to evaluate the expression.
Here are some expressions to evaluate. But before you type the return after each one, think about what you believe the value will be. When you have a hypothesis, type return and see if you're right.
(cons 1 2)
(car (cons 1 2))
(cdr (cons 1 2))
(consp (cons 1 2))
(consp (car (cons 1 2)))
AND? Evaluate these expressions.
(and t t nil t)
(and t t t)
(and 1 2 3)
(car 1 2)
Which of these expressions evaluates to (1 . 2)?
(cons 1 2)
(1 . 2)
1.2is a Common Lisp floating point number and ACL2 doesn't support those.
More generally, if you want to write a dotted pair, you should put some
``whitespace'' before and after the dot! Write
'(A . B) not
Which of these expressions evaluates to
(1 2 3)?
(cons 1 2 3)
(cons 1 (cons 2 (cons 3 nil)))
(cons 1 (cons 2 3))
(CONS A (CONS B NIL))
(CONS 'A '(B))
(CONS 'A (B))
(A (B . C) D)?
(cons 'A (cons '(B . C) 'D))
'(A (B . C) . (D . NIL))
(A (B . C) D)
(revappend '(a b c) '(1 2 3))
(revappend '(a b c) nil)
(revappend '(a b c) 5)
You could just type the following to the ACL2 prompt. But don't!
(defun mem (e x) (if (consp x) (if (equal e (car list)) t (mem e (cdr x)) nil)))It is almost always a mistake to type more than one line directly to Lisp! The reason is that Lisp will not let you edit your input after you have typed a carriage return (it provides a one line buffer). And there are typos in the
It is better to open another Emacs buffer. Call it
ctrl-x b scriptto Emacs.
meta-x lisp-modeto put the
scriptbuffer in Lisp syntax mode.
Now enter the above definition of
mem into the
buffer. You can do that by moving it with the mouse. But pretend you
just typed it in as though you made it up yourself. Now you want
ACL2 to process it.
Move the definition from the
script buffer to the
*shell* buffer. There are many ways to do this in Emacs. Here is one:
defunyou want to pick up.
*shell*buffer (as with
ctrl-x b *shell*or using the menu bar).
IFwas given four arguments and expects three. Can you find the problem? Hint: Position the cursor at the top of the
defun-- on the open parenthesis -- and type
ctrl-meta-qto indent the formula consistent with its parentheses.
Go back to the
script buffer and edit the
to fix the problem. If you don't know enough about Emacs to do this,
When you have fixed the paren problem, resubmit the definition to ACL2.
Now what? The error message:
ACL2 Error in ( DEFUN MEM ...): The body of MEM contains a free occurrence of the variable symbol LIST.means that the
defunuses a variable that is not one of the formal parameters. ACL2 does not have global variables! The variable
x. Fix it and try again.
Users familiar with Emacs can set up a ``keyboard macro'' or some
other mechanism to eliminate the tedious business of moving a definition
script to the
Whenever we say something like ``define such-and-such'' in ACL2 we really
mean for you to prepare the definition in the
script buffer, so
you can correct your typos, and then submit it ACL2 by cutting and pasting as
illustrated above. If you always type new definitions at the bottom of the
script buffer, and submit them as you go, you will have
a record of your definitions and you can save it to a file for future
Ok, so you've defined mem. Test it on
(defun fact (n) (if (equal n 0) 0 (* n (fact (- n 1)))))
Once you have done that, submit it to ACL2. Now run it:
(fact 4)ought to be 24. You will be re-defining a function, which ACL2 takes somewhat seriously. You should answer
ywhen it asks you if you want to redefine
nfor which your image cannot compute
(fact n)and will exhibit a ``hard error'' like this:
Error: Invocation history stack overflow. Fast links are on: do (si::use-fast-links nil) for debugging Error signalled by IF. Broken at COND. Type :H for Help. ACL2>>:qYou will note that the prompt looks different. The prompt you see is a Lisp debugger prompt. We are not interested in talking to the debugger. To get out of it, type
:q(return), as shown above.
Now you should see the ACL2 prompt again.
The stack overflowed because
fact is being interpretted.
Compiled functions use less stack space. To compile fact, do
factmay cause a hard error and, again, if yours computes
(fact 1000)it still may not compute
(fact 10000), etc.
Suppose we have a cons pair, e.g.,
(1 . 2) and we want
to flip it around so that we have
(2 . 1). Fill in the
blank below so that the function
flip does this.
(You should move the
defun to the
and prepare your definition there.)
(defun flip (p) ...)It doesn't matter what
pis not a cons pair, because you should never call
flipon such a
(flip '(A . B))
(flip '((A . B) . (C . D)))
Now suppose we have a list of cons pairs,
x, and we
want to flip each element of
x. Fill in the blank
flip-list do that.
(defun flip-list (x) ...)
(flip-list '((A . 1) (B . 2) (C . 3)))
((1 . A) (2 . B) (3 . C)).
(defun swap (x) ; Flip every cons pair in a binary tree. ...)
(equal (swap '((a . b) . (c . d))) '((d . c) . (b . a)))
(defun size (x) ; Count the number of leaves in a binary tree. ...)
(equal (size '((a . b) . (c . d))) 4)
(defun depth (x) ; Compute the length of the longest branch in a binary tree. ...)
(equal (depth '(((a . b) . c) . (e . f))) 3)
(defun tsubst (x y z) ; Substitute x for each occurrence of y in the binary tree z. ; (We can't call this ``subst'' because such a function is ; already defined in ACL2.) ...)
(equal (tsubst 'x '(a . b) '(((a . b) a b) . ((a . b) a . b))) '((x a b) . (x . x)))
To Insert Text
|just type it|
To Move Around
||move forward one character|
||move backward one character|
||move down to next line|
||move up to previous line|
||moves forward over balanced expression|
||moves backward over balanced expression|
||moves up one level of parens.|
||move to the beginning of the buffer|
||move to the end of the buffer|
To Delete/Yank Text
||delete one character|
||kill one line -- and put it in the ``kill ring''|
||kill one expression - and put it in the ``kill ring''|
||to yank text from the kill ring back into the buffer|
||select another buffer (type buffer name)|
||read a file into a buffer of that name|
||write a buffer to the file it came from|
||write a buffer to the file you name|
||indent the list expression immediately after the cursor in a way consistent with the parentheses|