Major Section: SWITCHES-PARAMETERS-AND-MODES
Examples: ACL2 !>(dive-into-macros-table (w state)) ((CAT . EXPAND-ADDRESS-CAT) (LXOR . EXPAND-ADDRESS-LXOR)This table associates macro names with functions used by the proof-checker's
DVand numeric diving commands (e.g.,
3) in order to dive properly into subterms. See proof-checker, in particular the documentation for
This table can be extended easily. See add-dive-into-macro and also see remove-dive-into-macro.
The symbol associated with a macro should be a function symbol taking four arguments, in this order:
The function will normally return a list of positive integers, representing the (one-based) address for diving into
car-addr; the first number in the list given to the proof-checker's
raw-term; the untranslated term into which we will dive
term; the translated term into which we will dive
wrld; the current ACL2 logical world
termthat corresponds to the single-address dive into
car-address. However, it can return
(cons str alist), where
stris a string suitable for
argsis the corresponding alist for
Referring to the example above,
expand-address-cat would be such a
function, which will be called on
raw-term values that are calls of
cat. See the community book
books/misc/rtl-untranslate.lisp for the
definition of such a function.
See table for a general discussion of tables.