		Search-engine friendly clone of the ACL2 documentation.

Developers-guide

Developers-guide-evaluation

How Evaluation Is Implemented in ACL2

Our focus here is primarily on evaluation in the top-level loop. Also see the section on ``Evaluators'' in the chapter, developers-guide-utilities.

ALL OF THIS TOPIC IS IMPORTANT; coverage will depend on time available at the workshop.

Introduction and further reading

This chapter is in two parts (not including this introduction). It starts with a very brief review of evaluation in the read-eval-print loop. Then it dives a bit into how *1* function definitions are generated. It may be helpful to read the following additional material either before or after reading this chapter, or perhaps, both.

The documentation topic, evaluation, explains ``*1* functions'' — we assume here that you have some basic familiarity with that notion — and ``submitted functions'', which are the functions directly produced by the defun forms in raw Lisp). That topic also explains the role of these two functions in evaluation. Below we start with a very brief illustration of that material. For other reading relevant to evaluation at the user level, see guard and consider looking at some of its subtopics, especially guard-evaluation-table. Finally, look at relevant source comments pertaining to the aspect of evaluation that you are modifying, whether that is in ev-rec, oneify, or some other function.

The implementation of evaluation in ACL2 is rather subtle. As is the case for this Developer's Guide in general, this chapter is not intended to provide complete coverage of the topic. Its purpose is to provide sufficient background so that comments and code in the ACL2 sources can fill in on demand, as necessary.

Brief overview of evaluation in the ACL2 read-eval-print loop

The section on ``Commands and events'' in the chapter, developers-guide-background, explains that evaluation of a form in the ACL2 loop is performed by a variant of the function, trans-eval. That function (as well as trans-eval itself), in turn, leads to a call of the evaluator, ev, which ultimately leads to calls of the raw Lisp function, raw-ev-fncall, to evaluate function calls (f val1 ... valk). The function raw-ev-fncall, in turn, calls the *1* function for the function symbol given as its first argument. Let's see how that works. First we define two functions and trace both of them.

(defun f1 (x)
  (declare (xargs :guard (true-listp x)))
  (car x))

(defun f2 (x)
  (f1 x))

(trace$ f1 f2)

Now let's see what can happen during evaluation.

ACL2 !>(f2 '(3 4))
1> (ACL2_*1*_ACL2::F2 (3 4))
  2> (ACL2_*1*_ACL2::F1 (3 4))
    3> (F1 (3 4))
    <3 (F1 3)
  <2 (ACL2_*1*_ACL2::F1 3)
<1 (ACL2_*1*_ACL2::F2 3)
3
ACL2 !>

Evaluation starts with a call to the *1* function for f2. Since f2 is not guard-verified, there is no call of the submitted function for f2 (see evaluation for terminology). Instead, the *1* function for f2 directly calls the *1* function for f1. Since f1 is guard-verified, this leads to a call of the submitted function for f1.

Producing 1 functions: oneify and oneify-cltl-code

The production of *1* functions is subtle, largely because many cases need to be handled in order to connect the ACL2 logic with Common Lisp; see guard-evaluation-table for a partial exploration of that connection. Stobjs must be handled properly as well.

The top-level function for creating *1* functions is oneify-cltl-code. This function, in turn, calls oneify on its guard and body. Here is annotated trace output, created by submitting the definition of f1 above after tracing as follows: (trace! (oneify-cltl-code :native t) (oneify :native t)). Note that we use ``oneify'' as a verb: to oneify is to create code for a *1* function.

; Top-level call:

1> (ONEIFY-CLTL-CODE :LOGIC
                     (F1 (X)
                         (DECLARE (XARGS :GUARD (TRUE-LISTP X)))
                         (CAR X))
                     NIL |current-acl2-world|)

; Oneify the guard:

  2> (ONEIFY (TRUE-LISTP X)
             NIL |current-acl2-world| NIL)
    3> (ONEIFY X NIL |current-acl2-world| NIL)
    <3 (ONEIFY X)
  <2 (ONEIFY (ACL2_*1*_ACL2::TRUE-LISTP X))

; Oneify the body:

  2> (ONEIFY (CAR X)
             NIL |current-acl2-world| NIL)
    3> (ONEIFY X NIL |current-acl2-world| NIL)
    <3 (ONEIFY X)
  <2 (ONEIFY (ACL2_*1*_COMMON-LISP::CAR X))

; Return the definition of the *1* function for f1 (without the leading
; ``defun''):

<1 (ONEIFY-CLTL-CODE
        (ACL2_*1*_ACL2::F1
             (X)
             (WHEN (NOT (EQ (F-GET-GLOBAL 'GUARD-CHECKING-ON
                                          *THE-LIVE-STATE*)
                            :NONE))

; Unless guard-checking is :none, we check the guard.

                   (COND ((TRUE-LISTP X)

; When the guard holds, call the submitted function to obtain the value.

                          (RETURN-FROM ACL2_*1*_ACL2::F1 (F1 X)))
                         ((F-GET-GLOBAL 'GUARD-CHECKING-ON
                                        *THE-LIVE-STATE*)

; The guard fails, and unless guard-checking is nil (or :none, but that was
; already considered above), cause an guard violation.

                          (THROW-RAW-EV-FNCALL (LIST 'EV-FNCALL-GUARD-ER
                                                     'F1
                                                     (LIST X)
                                                     '(TRUE-LISTP X)
                                                     '(NIL)
                                                     NIL)))))

; If we didn't return or get a guard violation, then call a local function
; defined to have the oneified body.  Note: LABELS is like LET but for
; local function definitions, which may be recursively defined.  See any
; Common Lisp documentation for more about LABELS.

             (LABELS ((ACL2_*1*_ACL2::F1 (X)
                                         (ACL2_*1*_COMMON-LISP::CAR X)))
                     (ACL2_*1*_ACL2::F1 X))))

Do you see an inefficiency above?

See code comments for how oneification deals with subtleties such as safe-mode, stobjs, and invariant-risk.

NEXT SECTION: developers-guide-miscellany

Developers-guide-evaluation

Introduction and further reading

Brief overview of evaluation in the ACL2 read-eval-print loop

Producing *1* functions: oneify and oneify-cltl-code

Producing 1 functions: oneify and oneify-cltl-code