DEFUN-INLINE

define a potentially inlined function symbol and associated macro 
Major Section:  EVENTS

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. If doc-string is supplied, then it is associated with fn, not with fn$inline. 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.

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.

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