Add-meta-rule
A macro to add created meta rules to RP-Rewriter
(add-meta-rule :meta-fnc <meta-fnc-name> ;; mandatory
:trig-fnc <trig-fnc-name> ;; mandatory
:formula-checks <formula-check-fnc-name> ;; nil by default, necessary in most cases.
:returns <return-signature> ;; optional
:rw-directuon <:inside-out, :outside-in, or :both> ;; optional, :inside-out by default
:valid-syntaxp <t-or-nil> ;; optional, t by default
:disabled <t-or-nil> ;; optional, t by default
:hints <regular-ACL2-hints> ;; optional
:cl-name-prefix <nil-or-a-unqiue-prefix> ;; optional, nil by default
)
registers a verified meta-rule for RP-Rewriter.
Mandatory arguments:
- :meta-fnc must be the name of the meta function.
- :trig-fnc the function to trigger this meta function
Optional Arguments:
- :formula-checks the name of the formula-checks function created
with def-formula-checks if the meta rule needed one. This will likely be
necessary for most cases.
- :returns return signature of the meta function. By default, it is 'term',
which means that it only returns the rewritten term. Other acceptable forms are
(mv term dont-rw), (mv term dont-rw rp-state), (mv term rp-state) etc. in any
order.
- :rw-direction whether the meta rule be applied from outside-in or
inside-out. You can pass :inside-out, nil (same as :inside-out), :outside-in or
:both. If you choose to make it an outside-in rule,
then it is recommended that you input the current dont-rw structure to the meta
function and update
it accordingly.
- :valid-syntaxp if you proved that your meta function returns rp-termp,
then set this to t. Otherwise, RP-Rewriter will have to call rp-termp everytime
the meta runction changes the term.
- :disabled will cause the registered meta rule to be disabled by default,
but it can be later enabled by the user.
- :hints regular ACL2 hints passed to the internal defthm event that checks
the correctness of necessary lemmas mentioned in Rp-rewriter/meta-rules.
- :cl-name-prefix Meta functions are attached to RP-Rewriter using a
defattach mechanism. By default, add-meta-rule will not trigger this mechanism,
and the user needs to call attach-meta-fncs once all the necessary meta
rules are created and included in the same book. If you wish to call attach-meta-fncs automatically with rp::add-meta-rule, then pass a unique
name for :cl-name-prefix. It is nil by default, which will prevent attach-meta-fncs from being executed.
