|
|
|---|
|
|
|
|---|
Functions to manage RP-Rewriter's ruleset
Users can use the functions below to register rules to RP-Rewriter's ruleset:
(rp::add-rp-rule <rule-name> ;; optional args: :disabled <t-or-nil> ;; default: nil :lambda-opt <...> ;; default: nil :hints <...> ;; default: nil :rw-direction <...> ;; default: :inside-out :ruleset <...> ;; default: rp-rules )
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 for RP-Rewriter.
:lambda-opt key checks if the rule has any lambda expressions. If that is the case, then it performs lambda-optimization 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. RP-Rewriter will know to use that rule when you refer to the original rule name, such as when enabling/disabling it.
:hints key will likely never be used but maybe necessary in some unforeseen cases when :lambda-opt is enabled.
:rw-direction key can be set to :inside-out, :both, or :outside-in. This determines the rewrite direction when applying a rule. If the key is set to :outside-in, then the rule will be tried on a term before rewriting the subterms. If it is set to :inside-out, 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 :both, then it is treated as both inside-out and outside-in.
:ruleset key select which table the rule should be saved in. By default, it is set to rp-rules. Should users choose to collect their rules in some other table to manage a different rewriting scheme and don't want the possible interference from the existing set of rules, then they may choose to use a custom table to store and read the rule names.
(rp::def-rp-rule <rule-name> <conjecture> ;;optional arguments: :rule-classes <...> ;; default: :rewrite, passed to defthm :hints <...> ;; default: nil. Passed to defthm :otf-flg <t-or-nil> ;; default: nil. Passed to defthm :instructions <t-or-nil> ;; default: nil. Passed to defthm. :disabled <t-or-nil> ;; default: nil. Disable the rule for both ACL2 and RP :disabled-for-rp <t-or-nil> ;; default: nil. Disable the rule for RP :disabled-for-ACL2 <t-or-nil> ;; default: nil. Disable the rule for ACL2 :rw-direction <...> ;; default: :inside-out. Passed to add-rp-rule :lambda-opt <...> ;; default: t. Passed to add-rp-rule. :rule-set <...> ;; default: rp-rules. Passed to add-rp-rule )
This macro simply expands to consecutive calls of defthm and add-rp-rule. It provides a compact way to add rewrite rules intended to be used by RP-Rewriter. Note that the :lambda-opt argument is set to t by default.
A given rule may be parsed differently in RP-Rewriter than how ACL2 processes rules. Therefore, using pr to understand rhs, lhs, hyp etc. of a rule may be misleading. So RP-Rewriter has its of version of pr:
(rp-pr rule-name)
This will show relevant information about a given rule.
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)
Alternatively, meta rules can be enabled/disabled without passing their trigger functions using 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 the given meta function names each of which may have multiple 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>)
Alternatively, passing the rune for executable counterpart to enable-rules/disable-rules can also work. For example:
(rp::enable-rules '((:executable-counterpart mv-nth)))
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>)
Users can 'bump' or 'bump down' rules, effectively changing their application
priority. For example,
(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)