Disassemble$
Disassemble a function
The macro disassemble$ provides a convenient interface to the
underlying disassemble utility of the host Common Lisp implementation,
which prints assembly code for a given function symbol at the terminal. If
the argument is instead a macro alias for a function symbol (see macro-aliases-table), then it prints assembly code for that function symbol
instead.
Disassemble$ works by including the community book
books/misc/disassemble.lisp, which defines the supporting function
disassemble$-fn, and then by calling that function. Note that the
arguments to disassemble$ are evaluated. Also note that
disassemble$ is intended as a top-level utility for the ACL2 loop, not to
be called in code; for such a purpose, include the above book and call
disassemble$-fn directly.
Example Forms:
(disassemble$ 'foo)
(disassemble$ 'foo :recompile t)
General Forms:
(disassemble$ form)
(disassemble$ form :recompile flg)
where form evaluates to a function symbol or a macro alias for a
function symbol and flg evaluates to any value. If flg is nil,
then the existing definition of that function symbol is disassembled. But if
flg is supplied and has a value other than nil or :default, and
if that function symbol is defined in the ACL2 loop (not merely in raw Lisp;
for example, see set-raw-mode), then the disassembly will be based on a
recompilation of that ACL2 definition. Normally this recompilation is not
necessary, but for some host Lisps, it may be useful; in particular, for CCL
the above book arranges that source code information is saved, so that the
output is annotated with such information. When recompilation takes place,
the previous definition is restored after disassembly is complete. Finally,
if flg is omitted or has the value :default — i.e., in the
default case — then recompilation may take place or not, depending on
the host Lisp. The values of (@ host-lisp) for which recompilation takes
place by default may be found by looking at the above book, or by including it
and evaluating the constant *host-lisps-that-recompile-by-default*. As
of this writing, CCL is the only such Lisp (because that is the one for which
we can obtain source annotation in the output by recompiling).
