DIVE-INTO-MACROS-TABLE

right-associated function information for the proof-checker 
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 DV and numeric diving commands (e.g., 3) in order to dive properly into subterms. See proof-checker, in particular the documentation for DV.

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: 

car-addr ; the first number in the list given to the proof-checker's
           DV command
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
The function will normally return a list of positive integers, representing the (one-based) address for diving into term that corresponds to the single-address dive into raw-term by car-address. However, it can return (cons str alist), where str is a string suitable for fmt and args is the corresponding alist for fmt.

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.