Defun-inline
Define a potentially inlined function symbol and associated macro
You may be able to improve performance by replacing an event
(defun f ...) with a corresponding event (defun-inline f ...), in
order to encourage the host Lisp compiler to inline calls of f.
Example Form:
(defun-inline lng (x)
(declare (xargs :guard (true-listp x)))
(if (endp x) 0 (1+ (lng (cdr x)))))
General Form:
(defun-inline fn (var1 ... varn) doc-string dcl ... dcl body)
satisfying the same requirements as in the General Form for defun.
The effect is to define a macro fn and a function fn$inline (i.e., a
symbol in the same package as fn but whose symbol-name has the
suffix "$INLINE", such that each call of fn expands to a call of
the function symbol fn$inline on the same arguments. Moreover, table events are generated that allow the use of fn in theory expressions to represent fn$inline and that cause any
untranslated (user-level) call of fn$inline to be printed as the
corresponding call of fn. Doc-string, if non-nil, is an
optional string that can provide documentation but is essentially ignored by
ACL2.
A form (defun-inline f ...) actually defines a function named
f$inline and a corresponding macro named f whose calls expand to
calls of f$inline, while providing the illusion that there is just the
``function'' f. For example, the Example Form above macroexpands in one
step to the following form.
(progn (defmacro lng (non-stobj-var0)
(list 'lng$inline non-stobj-var0))
(add-macro-fn lng lng$inline)
(defun lng$inline (x)
(declare (xargs :guard (true-listp x)))
(if (endp x) 0 (1+ (lng (cdr x))))))
Note that the above call of add-macro-fn generates the
aforementioned two table events (see add-macro-fn), which provide the
illusion that we are just defining a function lng, as you can see in the
following log: lng appears rather than lng$inline.
ACL2 !>(set-gag-mode nil)
<state>
ACL2 !>(thm (equal (lng (append x y))
(+ (lng x) (lng y)))
:hints (("Goal" :in-theory (enable lng))))
[.. output omitted ..]
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
(EQUAL (LNG (APPEND (CDR X) Y))
(+ (LNG (CDR X)) (LNG Y))))
(EQUAL (LNG (APPEND X Y))
(+ (LNG X) (LNG Y)))).
[.. output omitted ..]
Under the hood, ACL2 arranges that every function symbol with suffix
"$INLINE" is presented to the compiler as one whose calls we would
prefer to inline. Technically: the Common Lisp form (declaim (inline
f$inline)) is generated for a function symbol f$inline before that
symbol's definition is submitted. However, the Common Lisp spec explicitly
avoids requiring that the compiler respect this declaim form.
Fortunately, Common Lisp implementations often do respect it.
Also see defund-inline, see defun-notinline, and see defund-notinline.
Remarks.
(1) None of these macros (including defun-inline) is supported for use
inside a mutual-recursion.
(2) Every function symbol defined in ACL2 whose symbol-name has the
suffix "$INLINE" is proclaimed to be inline; similarly for
"$NOTINLINE" and notinline. These restrictions are explained in a
comment in the ACL2 source definition of macro defun-inline.
(3) No special treatment for inlining (or notinlining) is given for
function symbols locally defined by flet, with two exceptions: when
explicitly declared inline or notinline by the flet form, and
for symbols discussed in (1) and (2) above that, at some point in the current
ACL2 session, were defined as function symbols in ACL2 (even if not currently
defined because of undoing or being local).
(4) The function symbol actually being defined by (defun-inline foo
...) is foo$inline. As mentioned above, one can be oblivious to this
fact when writing theory expressions or perusing prover output.
However, for other purposes (for example, verify-guards and defabsstobj :exports) you will need to supply the name of the function
symbol rather than the name of the macro; e.g., for the above form
(defun-inline foo ...), you may subsequently issue the event
(verify-guards foo$inline) but not (verify-guards foo).
(5) Obscure Remark. Suppose that you certify a book with compilation (the
default) in one host Lisp, saving the expansion file. Suppose that you then
compile in another host Lisp by using include-book with argument
:load-compiled-file :comp. Then in subsequent sessions, including that
book with the second host Lisp will not result in any inline or notinline
behavior for functions defined in the book. This may be fixed in a future
release if someone complains.
