Defabbrev
A convenient form of macro definition for simple expansions
Examples:
(defabbrev snoc (x y) (append y (list x)))
(defabbrev sq (x) (declare (type (signed-byte 8) x)) (* x x))
General Form:
(defabbrev name (v1 ... vn) doc-string decl1 ... declk body)
where name is a new function symbol, the vi are distinct variable
symbols, and body is a term. The decli, if supplied, should be
legal declare forms; see declare. Doc-string, if
non-nil, is an optional string that can provide documentation but is
essentially ignored by ACL2.
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, defabbrev defines f to be a macro so that (f a1 ... an)
expands to body, with the ``formals,'' vi, replaced by the
``actuals,'' ai.
For example, if snoc is defined as shown in the first example above,
then (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 let to bind the ``formals'' to the
``actuals.'' Consider the second example above. Logically speaking, (sq
(ack i j)) is an abbreviation for (* (ack i j) (ack i j)). But in fact
the macro for sq introduced by defabbrev actually arranges for
(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
call of name — i.e., defabbrev should not be used in place of
defun when the function is recursive. ACL2 will not complain when the
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
name.
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
evaluated forms like cond, case, or 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 foo (see trans1):
ACL2 !>:trans1 (foo expr1 expr2)
(LET ((X EXPR1) (Y EXPR2))
(IF (TEST X) (BAR Y) NIL))
ACL2 !>
Now imagine that expr2 is a complicated expression whose evaluation is
intended only when the predicate test holds of expr1. The expansion
above suggests that expr2 will always be evaluated by the call (foo
expr1 expr2), which may be inefficient (since perhaps we only need that
value when test is true of expr1). The evaluation of expr2 may
even cause an error, for example in :program mode if the
expression expr2 has been constructed in a manner that could cause a
guard violation unless test holds of expr1.
