		Search-engine friendly clone of the ACL2 documentation.

Programming

Evaluation

Evaluating ACL2 expressions

This topic uses examples to expose how ACL2 uses Common Lisp to evaluate expressions. Links are provided to topics that elaborate on aspects of evaluation in ACL2.

At a high level, we can say that ACL2 evaluation takes place using the underlying host Common Lisp. But consider the form (car 3). In Common Lisp this is an error; typically you will be thrown into the Lisp debugger. In the ACL2 read-eval-print loop, however, you may see the following.

ACL2 !>(car 3)


ACL2 Error in TOP-LEVEL:  The guard for the function call (CAR X),
which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments
in the call (CAR 3).
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.

ACL2 !>

The message suggests that the function car has a guard, or precondition, that is violated by the proposed argument, 3. So clearly something more is going on here than just evaluation of the form (car 3) in Common Lisp.

In fact, every ACL2 function symbol is associated with the following two Common Lisp definitions, as explained below:

the ``executable-counterpart'' definition, sometimes called the ``*1*'' function (pronounced ``star one star''); and
the ``submitted'' definition (sometimes called the ``raw Lisp'' function).

We may also speak of the ``executable-counterpart'' and ``submitted'' functions, which are the two functions defined by the ``executable-counterpart'' and ``submitted'' definitions, respectively.

Let us explore these two functions in the case of car. When (car 3) is evaluated in the ACL2 loop, the executable-counterpart of car is applied to the argument 3. That executable-counterpart (which was hand-coded) first checks the guard of car, which fails for 3, leading to the error displayed above. If instead the form to be evaluated by ACL2 is (car '(4 5 6)), the executable-counterpart of car will first check that the guard of car holds for the list argument (4 5 6); then seeing that this is the case, it will apply the Common Lisp function car — which we consider to be the ``submitted'' function for car — to that list argument, returning 4.

The example above does not really explain why the submitted function is called ``submitted'', so let us consider the more common case of a defined function, as opposed to a primitive like car. Suppose we define the following functions f and g, each of which has an implicit guard (precondition) of t, i.e., the precondition always holds.

(defun f (x)
  (car x))
(defun g (x)
  (f x))

ACL2 defines two functions named "F": the executable-counterpart of f, sometimes called ``*1*f'', and the submitted function for f. It also defines two such functions for g. The executable-counterpart is generated by ACL2 to include not only code to check guards, but also code to invoke the executable-counterparts of its callees. (Such invocation can be avoided by a process known as verifying guards, as we explain further below.) We can see what is going on by tracing calls of f (see trace for more about tracing); some analysis follows below this display.

ACL2 !>(trace$ f g)
 ((F) (G))
ACL2 !>(g '(4 5 6))
1> (ACL2_*1*_ACL2::G (4 5 6))
  2> (ACL2_*1*_ACL2::F (4 5 6))
  <2 (ACL2_*1*_ACL2::F 4)
<1 (ACL2_*1*_ACL2::G 4)
4
ACL2 !>

It is now perhaps evident why sometimes we call the executable-counterpart functions the ``*1* functions'': the executable-counterpart is actually defined in a special ``*1*'' package that corresponds to the package of the submitted function. The trace above shows that the executable-counterpart of g calls the executable-counterpart of f, rather than calling any submitted function.

Such a trace can show us an error caused by applying car to 3.

ACL2 !>(g 3)
1> (ACL2_*1*_ACL2::G 3)
  2> (ACL2_*1*_ACL2::F 3)


ACL2 Error in TOP-LEVEL:  The guard for the function call (CAR X),
which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments
in the call (CAR 3).
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.

ACL2 !>

It is generally more efficient to invoke a submitted functions — which has as its Common Lisp definition exactly the defun form submitted to ACL2 — than it is to invoke an executable-counterpart, which is generated by ACL2 to do auxiliary calculations including guard-checking. So we next modify the example above to show that by performing a process called ``guard verification'', we can avoid *1* function calls, so that submitted functions are invoked instead. This time we supply reasonable guards for f and g, in a fresh ACL2 session.

(defun f (x)
  (declare (xargs :guard (or (consp x) (null x))))
  (car x))
(defun g (x)
  (declare (xargs :guard (consp x)))
  (f x))

This time, we see that the executable-counterpart of g directly calls the submitted function for g, because g was guard-verified when g was admitted and the value '(4 5 6) for the formal x of g satisfies the guard (consp x) of g.

ACL2 !>(trace$ f g)
 ((F) (G))
ACL2 !>(g '(4 5 6))
1> (ACL2_*1*_ACL2::G (4 5 6))
  2> (G (4 5 6))
    3> (F (4 5 6))
    <3 (F 4)
  <2 (G 4)
<1 (ACL2_*1*_ACL2::G 4)
4
ACL2 !>

We can also see that because 3 fails to satisfy the guard of g, a guard violation is signaled by the executable-counterpart of g, rather than (as before) by the executable-counterpart of car.

ACL2 !>(g 3)
1> (ACL2_*1*_ACL2::G 3)


ACL2 Error in TOP-LEVEL:  The guard for the function call (G X), which
is (CONSP X), is violated by the arguments in the call (G 3).
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.

ACL2 !>

See if you can predict the corresponding traces if instead, f has a suitable guard and is guard-verified, but g is as in the first example (with an implicit guard of t, and not guard-verified):

(defun f (x)
  (declare (xargs :guard (or (consp x) (null x))))
  (car x))
(defun g (x)
  (f x))

The corresponding trace is as follows; discussion follows.

ACL2 !>(g '(4 5 6))
1> (ACL2_*1*_ACL2::G (4 5 6))
  2> (ACL2_*1*_ACL2::F (4 5 6))
    3> (F (4 5 6))
    <3 (F 4)
  <2 (ACL2_*1*_ACL2::F 4)
<1 (ACL2_*1*_ACL2::G 4)
4
ACL2 !>(g 3)
1> (ACL2_*1*_ACL2::G 3)
  2> (ACL2_*1*_ACL2::F 3)


ACL2 Error in TOP-LEVEL:  The guard for the function call (F X), which
is (OR (CONSP X) (NULL X)), is violated by the arguments in the call
(F 3).
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.

ACL2 !>

The traces above show that first, the executable-counterpart of g calls the executable-counterpart of f. This is because g is not guard-verified, so its executable-counterpart can only invoke other executable-counterparts. However, since f is guard-verified, its executable-counterpart invokes its submitted function when the guard is satisfied, for example to generate the call (F (4 5 6)). If the guard for f fails to hold, however, the executable-counterpart for f causes a guard violation error, as shown above for the executable-counterpart call (ACL2_*1*_ACL2::F 3).

See also guard and its subtopics, especially, guards-and-evaluation, for a discussion of guards and their connection to evaluation. Advanced system hackers who want to see the executable-counterpart definition for f may invoke (trace! (oneify-cltl-code :native t)) before defining f in ACL2.

Subtopics

Guard-checking-inhibited: Avoiding certain warnings when evaluating ACL2 expressions