Magic-macroexpand
A macroexpansion utility for logic-mode code
General Form:
(magic-macroexpand form ctx wrld state)
where form is a user-level term, ctx is a context (see
ctx), wrld is an ACL2 logical world, and state is the
ACL2 state. If form is a macro call then that call is expanded to
produce another form, which is recursively macroexpanded. The result is
(mv erp val), where if erp is nil then val is the desired
macroexpansion, and otherwise val is a message (see msg).
For each macro expanded in the process described above, its body must
consist of logic-mode code. Also note that the utility
magic-macroexpand is in logic mode.
Here is a simple example.
ACL2 !>(defmacro my-mac (a b) `(* ,a ,b))
Summary
Form: ( DEFMACRO MY-MAC ...)
Rules: NIL
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MY-MAC
ACL2 !>(set-guard-checking :nowarn)
Leaving guard checking on, but changing value to :NOWARN.
ACL2 !>(magic-macroexpand '(my-mac x y) 'top (w state) state)
(NIL (BINARY-* X Y))
ACL2 !>
Notice the use of (set-guard-checking :nowarn). This is optional, but
without it there may be warnings printed. Indeed, those warnings suggest
using either this method of inhibiting warnings or
(set-guard-checking :all). Such warnings may be eliminated in the
future.
