|
|
|---|
|
|
|
|---|
Functions to manage RP-Rewriter's ruleset
Users can use the functions below to register rules to RP-Rewriter's ruleset:
ADD-RP-RULE
(rp::add-rp-rule <rule-name> &key (disabled 'nil) (beta-reduce 'nil) (hints 'nil) (outside-in 'nil))
This macro submits a table event that saves the given rule in the RP-Rewriter's ruleset to be used later. Application priority of the rule will depend on when this event is submitted rather than when the rule is originally defined.
:disabled key, when set, leaves the added rule disabled.
:beta-reduce key checks if the rule has any lambda expressions. If that is the case, then it calls defthm-lambda to create a new rule and save that instead. The name of the new rule will be printed, and it will be disabled for ACL2. You need to use that new name while enabling/disabling the added rule for RP-Rewriter.
:hints key is relevant only when :beta-reduce is set and rp::defthm-lambda.
:outside-in key can be set to :inside-out, :both, t, or nil. This determines the rewrite direction when applying a rule. If the key is set to t, then the rule will be tried on a term before rewriting the subterms. If it is set to nil, then the rule will be considered only an inside-out rule and the subterms will be rewritten first before applying the rewrite rule. If it is set to :inside-out or :both, then it is treated as both inside-out and outside-in.
DEF-RP-RULE
(rp::def-rp-rule <rule-name> <conjecture> &rest <hints>)
This macro has the same signature as defthm. It submits a defthm-lambda event in the term has a lambda expression. If it doesn't then defthm-lambda translates to defthm. It also submits a add-rp-rule event to save the rule in the rule-set.
ENABLING/DISABLING RULES
To enable rewrite, definition or meta rules:
(rp::enable-rules <rules>)
The argument should be a quoted list of rules/runes. For example: (rp::enable-rules '(implies (:rewrite append-of-nil))). To enable meta rules, their trigger function should be passed as well. For example: (rp::enable-rules '((:meta mv-nth-meta . mv-nth))).
To disable them:
(rp::disable-rules <rules>)
To disable all:
(rp::disable-all-rules)
Meta rules can be enabled/disabled without passing their trigger functions with rp::enable-meta-rules and rp::disable-meta-rules. These macros have a different signature than rp::enable-rules. For example: (rp::enable-meta-rules mv-nth-meta hons-acons-meta hons-get-meta). These macros will enable/disable the meta rules for all of their trigger functions.
(rp::enable-meta-rules meta-fnc1 meta-fnc2 ...)
and
(rp::disable-meta-rules meta-fnc1 meta-fnc2 ...)
All executable counterparts are enabled by default even if the user does not add the functions to RP-Rewriter's ruleset. They can be disabled and enabled with the macro calls below. The given function name should be unquoted.
(rp::disable-exc-counterpart <fnc-name>)
and
(rp::enable-exc-counterpart <fnc-name>)
Preprocessors and postprocessors can be enabled/disabled with the macros below.
(rp::enable-preprocessor <fnc-name>)
(rp::disable-preprocessor <fnc-name>)
(rp::enable-postprocessor <fnc-name>)
(rp::disable-postprocessor <fnc-name>)
CHANGING RULE PRIORITIES
Users can 'bump' or 'bump down' rules, effectively changing their application priority. For example, (bump-rp-rule (:definition implies)) (alternatively, (bump-rp-rule implies)) will priorities the definition rule of implies over any rewrite rule that might have been defined prior to that point. If user defines a rewrite rule about implies after this point, then that rule will be tried/applied. If it fails, then the bumped up definition rule of implies will be applied.
(rp::bump-rule <rule-name/rune>)
Reversely, bump-down-rule pushes down a rule at the end of the rule list, making it the least prioritized rule.
(rp::bump-down-rule <rule-name/rune>)
Users can bump multiple rules with a single event:
(rp::bump-rules rule-name/rune1 rule-name/rune2 ...)
Users can bump all the meta rules with the macro below:
(rp::bump-all-meta-rules)