Major Section: OTHER
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. It 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 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).
