Getting Started with ACL2 Programming

We assume that you have read A Gentle Introduction to ACL2 Programming.

You might also want to refer to the Hyper-Card for ACL2 Programming.

Learn to Use the Documentation

Goal: Find out about the function AND

In Netscape or your favorite browser, go to the ACL2 Home Page: http://www.cs.utexas.edu/users/moore/acl2/.
Click on The User's Manual.
Click on the Index.
Click on the letter A.
Scroll down till you see the link for AND
Click on it.
Read what it says.

Goal: Using the analogous method, find out about the function REVAPPEND.

Running ACL2

ACL2 is a Common Lisp application, where the standard mode of interaction is the “read-eval-print loop” in which a Lisp expression typed by the user is read, evaluated, and its value is printed at each interactive exchange. Most ACL2 documentation, including this document, is written as though the user were typing directly to the read-eval-print loop.

But almost all users interact with ACL2 via one of two interfaces. One is Emacs, where the ACL2 image is run in Emacs' *shell* buffer, 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.

Start Emacs by typing emacs to the Unix shell.
If you don't know Emacs, a few handy commands are listed here.
Start a shell buffer by typing meta-x shell in Emacs.
You should see a new buffer, named *shell*, with the Unix prompt in it.
Start ACL2 by typing acl2 (followed by return) in the *shell* buffer.
You should see something like
```
 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.
Type :program (followed by return).
Type :redef (followed by return).

The last two commands turn off ACL2's theorem prover and allow you to use ACL2 as a Lisp execution engine.

The ACL2 Prompt

Pay special attention to the prompt!

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.

ACL2 p!> Good ACL2 read-eval-print loop type Lisp expressions to evaluate

ACL2>> Bad Common Lisp debugger exit by typing :q return

ACL2> Bad Common Lisp top-level enter ACL2 by typing (LP) return

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 package'' is ACL2. If you do not know what a symbol package is, don't worry about it. Just know that it is not the ``ACL2'' that is important about the prompt, it is the other parts!

Evaluating ACL2 Expressions

If you type an ACL2 expression to the prompt, followed by a return, ACL2 will read the expression, evaluate it, and print the result. Try typing

after the ACL2 prompt in the *shell* buffer. Then type return. It should print T. The value of the Lisp expression t is T.

Try these three:

(equal 1 2)
(if t 1 2)
(if nil 1 2)

The first should return NIL because 1 is not 2. The second and third should return 1 and 2, respectively, because

(if x y
z)

means ``if x then y, else z.''

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).

You should enter the debugger. Lisp does not expect to read a ``dot'' except in lists. You should see the debugger prompt. Get out of the debugger and back to ACL2 by typing

:q

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

:q

again. This :q is 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

(LP)

You should see the ACL2 prompt again.

More Evaluation

You can use the mouse to move an expression from Netscape to the *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)))

Remember AND? Evaluate these expressions.

(and t t nil t)
(and t t t)
(and 1 2 3)

What happens if you call a function with the wrong number of arguments?

(car 1 2)

What happens if you try to evaluate an expression that contains a variable?

(car x)

The error message is not very helpful to the new user. It ought to say: ``ACL2 cannot evaluate top-level expressions that contain variables!''

Which of these expressions evaluates to (1 . 2)?

(cons 1 2)
(1 . 2)
'(1.2)

Warning: If you evaluated the last expression, you might be in the Common Lisp debugger now! The object 1.2 is 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 (A.B).

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))

Which of these expressions evaluates to (A B)?

(CONS A (CONS B NIL))
(CONS 'A '(B))
(CONS 'A (B))

Which of these expressions evaluates to (A (B . C) D)?

(cons 'A (cons '(B . C) 'D))
'(A (B . C) . (D . NIL))
(A (B . C) D)

What is the value of the following? Recall or review the documentation first.

(revappend '(a b c) '(1 2 3))
(revappend '(a b c) nil)
(revappend '(a b c) 5)

Learning to Define Functions

Now let's define the list membership function.

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 defun above!

It is better to open another Emacs buffer. Call it script.

Type ctrl-x b script to Emacs.
Type meta-x lisp-mode to put the script buffer in Lisp syntax mode.

Now enter the above definition of mem into the script 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:

Drag the mouse over the entire defun you want to pick up.
select the *shell* buffer (as with ctrl-x b *shell* or using the menu bar).
Click middle to paste the defun into the *shell* buffer.
Type return.

This will cause an error. The trouble is that the parentheses are not balanced correctly in the definition. The error message says IF was 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-q to indent the formula consistent with its parentheses.

Go back to the script buffer and edit the defun to fix the problem. If you don't know enough about Emacs to do this, look here.

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 defun uses a variable that is not one of the formal parameters. ACL2 does not have global variables! The variable list in the defun should be 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 from the script to the *shell* buffer.

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 use.

Ok, so you've defined mem. Test it on

(mem 'a '(a b c))
(mem 'd '(a b c))

Factorial

Now put this definition into your script buffer:

(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)

What's wrong? Fix it and resubmit it. (fact 4) ought to be 24. You will be re-defining a function, which ACL2 takes somewhat seriously. You should answer y when it asks you if you want to redefine FACT.

(fact 50)
(fact 1000)

ACL2 may cause an error on the last example, depending on the Common Lisp image you are using! It is a fairly safe bet that there is a value of n for 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>>:q

You 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

:comp fact

Then try

(fact 1000)

Is that the answer you expected? Note: In some Common Lisps, even the compiled version of fact may cause a hard error and, again, if yours computes (fact 1000) it still may not compute (fact 10000), etc.

A Challenge

Now its time for you to think.

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 script buffer and prepare your definition there.)

(defun flip (p) 
  ...)

It doesn't matter what flip does if p is not a cons pair, because you should never call flip on such a p.

Test your flip

(flip '(A . B))
(flip '((A . B) . (C . D)))

(Some people are surprised at how the last answer prints out. Think about it.)

Now suppose we have a list of cons pairs, x, and we want to flip each element of x. Fill in the blank to make flip-list do that.

(defun flip-list (x)
  ...)

Test your flip-list

(flip-list '((A . 1) (B . 2) (C . 3)))

The answer should be ((1 . A) (2 . B) (3 . C)).

Follow-Up Exercises

Here are some other exercises you might want to do to learn ACL2. They are exhibited as function definitions for you to complete. After each one is an example that tests the equality of your answer with the expected answer. All the examples should evaluate to T.

(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)))

The End

Emacs

To Insert Text	just type it
To Move Around
`ctrl-f`	move forward one character
`ctrl-b`	move backward one character
`ctrl-n`	move down to next line
`ctrl-p`	move up to previous line
`ctrl-meta-f`	moves forward over balanced expression
`ctrl-meta-b`	moves backward over balanced expression
`ctrl-meta-u`	moves up one level of parens.
`meta-<`	move to the beginning of the buffer
`meta->`	move to the end of the buffer
To Delete/Yank Text
`ctrl-d`	delete one character
`ctrl-k`	kill one line -- and put it in the ``kill ring''
`ctrl-meta-k`	kill one expression - and put it in the ``kill ring''
`ctrl-y`	to yank text from the kill ring back into the buffer
Other
`ctrl-x b`	select another buffer (type buffer name)
`ctrl-x ctrl-f`	read a file into a buffer of that name
`ctrl-x ctrl-s`	write a buffer to the file it came from
`ctrl-x ctrl-w`	write a buffer to the file you name
`ctrl-meta-q`	indent the list expression immediately after the cursor in a way consistent with the parentheses

`ACL2 p!>`	Good	ACL2 read-eval-print loop	type Lisp expressions to evaluate
`ACL2>>`	Bad	Common Lisp debugger	exit by typing `:q` return
`ACL2>`	Bad	Common Lisp top-level	enter ACL2 by typing `(LP)` return