DEFABBREV

a convenient form of macro definition for simple expansions 
Major Section:  EVENTS


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 is 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, 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 to 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 evaluted 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.