Major Section: EVENTS
Examples: (defabbrev snoc (x y) (append y (list x))) (defabbrev sq (x) (declare (type (signed-byte 8) x)) (* x x))where
General Form: (defabbrev name (v1 ... vn) doc-string decl1 ... declk body)
nameis a new function symbol, the
viare distinct variable symbols, and
bodyis a term. The
decli, if supplied, should be legal
declareforms; see declare.
Doc-stringis an optional documentation string; see doc-string.
Roughly speaking, the
defabbrev event is akin to defining
f so that
(f v1 ... vn) = body. But rather than do this
by adding a new axiom,
f to be a macro
(f a1 ... an) expands to
body, with the ``formals,''
vi, replaced by the ``actuals,''
For example, if
snoc is defined as shown in the first example
(snoc (+ i j) temp) is just an abbreviation for
(append temp (list (+ i j))).
In order to generate efficiently executable Lisp code,
the macro that
defabbrev introduces uses a
bind the ``formals'' to the ``actuals.'' Consider the second
example above. Logically speaking,
(sq (ack i j)) is an
(* (ack i j) (ack i j)). But in fact
the macro for
sq introduced by
(sq (ack i j)) to expand to:
(let ((x (ack i j))) (* x x))which executes more efficiently than
(* (ack i j) (ack i j)).
In the theorem prover, the
let above expands to
((lambda (x) (* x x)) (ack i j))and thence to
(* (ack i j) (ack i j)).
It is important to note that the term in
body should not contain a
name -- i.e.,
defabbrev should not be used to in place
defun when the function is recursive. ACL2 will not complain when
defabbrev form is processed, but instead ACL2 will more than
likely go into an infinite loop during macroexpansion of any form that
has a call of
It is also important to note that the parameters of any call of a
macro defined by defabbrev will, as is the case for the parameters
of a function call, be evaluated before the body is evaluated, since
this is the evaluation order of
let. This may lead to some
errors or unexpected inefficiencies during evaluation if the body
contains any conditionally evaluted forms like
if. Consider the following example.
(defabbrev foo (x y) (if (test x) (bar y) nil))Notice a typical one-step expansion of a call of
ACL2 !>:trans1 (foo expr1 expr2) (LET ((X EXPR1) (Y EXPR2)) (IF (TEST X) (BAR Y) NIL)) ACL2 !>Now imagine that
expr2is a complicated expression whose evaluation is intended only when the predicate
expr1. The expansion above suggests that
expr2will always be evaluated by the call
(foo expr1 expr2), which may be inefficient (since perhaps we only need that value when
testis true of
expr1). The evaluation of
expr2may even cause an error, for example in
programmode if the expression
expr2has been constructed in a manner that could cause a guard violation unless