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.
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
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.
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
(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
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
; 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