disassemble a function
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).