|
|
|---|
|
|
|
|---|
A defthm macro that calls RP-Rewriter as a clause processor with custom arguments.
RP::Defthmrp is a macro that expands to defthm and other auxiliary events that uses RP-Rewriter as a clause-processor to attempt a proof for the given conjecture.
(rp::defthmrp <new-rule-name> <conjecture> ;; optional keys: :rule-classes <...> ;; default: :rewrite :new-synps <...> ;; an alist to attach syntaxp to some existing ;; rewrite rules. Default: nil :enable-meta-rules (meta-fnc1 meta-fnc2 ...) ;; an unquoted list of names ;; of meta functions that users ;; wants to enable. Default: nil :disable-meta-rules (meta-fnc1 meta-fnc2 ...) ;; same as above for disable :enable-rules (append '(rule1 rule2) ;; List of rule-names to enable. The *rules3* ;; macro will evaluate the expressions first ...) ;; to generate the names. Default: nil :disable-rules <...> ;; Same as above for disable :runes '(rule1 rule2 ...) ;; When nil, the macro uses the existing rule-set ;; of RP-rewriter from the table specified in the ;; ruleset argument. Otherwise, it will only use ;; the inside-out rules given in this argument. ;; Default: nil :runes-outside-in '(rule1 rule2 ...) ;; same as above but for runes to be ;; applied outside-in. Default: nil :cases (case1 case2 ...) ;; casesplit the conjecture. Default: nil :lambda-opt <...> ;; perform lambda optimization. Useful if the ;; conjecture has lambda expressions. ;; Default: t :disabled <t-or-nil> ;; Disables the resulting rule for both ACL2 and RP :disabled-for-rp <t-or-nil> ;; Disables the resulting rule only for RP :disabled-for-ACL2 <t-or-nil> ;; Disables the resulting rule only for ACL2 :rw-direction <...> ;; Rewrite direction of the resulting rule for ;; RP. Default: :inside-out :supress-warnings <t-or-nil> ;; supress some warnings. Default: nil :add-rp-rule <t-or-nil> ;; Whether or not the rule should be added as ;; a rp rule. Default: t. :ruleset <...> ;; select which table to read and save ;; the rules. Default: rp-rules )
rule-classes will be passed as is to defthm. See ACL2::rule-classes.
new-synps can be used when users want to add new syntaxp hypothesis to existing rewrite rules. This argument should be an alist. Each key is a name of the rule (not its ACL2::rune), e.g., key should be natp-implies-integerp, and not (:rewrite natp-implies-integerp). Each value should be the desired additional syntaxp expression. When parsing every added rule, the program will look up each of their names on this new-synps alist and attach a translated syntaxp term at the beginning of existing hyps of the rule. The program uses assoc-equal for look ups therefore if you have repeated keys, then the first one will override the others. The defthmrp macro will translate the given terms.
enable-meta-rules and disable-meta-rules expect a list of meta function names to enable/disable. These are passed to local events (enable-meta-rules and disable-meta-rules) before the clause processor. The program will go through all the added meta rules and enable/disable them with matching meta function names. For example, if a meta function is used in two different rules with different trigger functions, they will both be affected. enable-rules/disable-rules may be used to enable/disable specific meta rules.
enable-rules and disable-rules takes a term that will be translated and evaluated to a list of rune/rule names that will be locally disabled/enabled before the RP-Rewriter is called. See rp-ruleset for detauls about how the rules are managed.
runes and runes-outside-in can be used to tell the rewriter to use a certain set of rules instead of reading them from the table. This is by default nil and we don't expect these options to be used often.
cases is a list of terms which are used as hints in the rewriter
to casesplit. For each term in cases, the conjecture will be rewritten to
lambda-opt stands for "lambda optimization". Due to the complexity of side-condition tracking, the rewriter does not internally support lambda expressions. If you pass a lambda expression to the clause processor, it is first ACL2::beta-reduced and then the rewriting starts. In case of repeated large terms, this can cause expensive repetitive rewriting. Therefore, we implement an additional mechanism to define some local auxiliary lemmas to split each step of lambda expressions to different rewrite rules. This helps to prevent the repeated rewriting problem. Please see lambda-opt for more details. The lambda-opt argument can take :max, t, or nil. When t, it retains the original lambda expression structure. When :max, it retains the original lambda structure and tries to search for repeated terms that are not lambda wrapped in the original term. When nil, the lambda optimization feature is disabled and the term is beta-reduced before rewriting.
disabled , disabled-for-rp , and disabled-for-ACL2 controls if the rule derived from proved conjecture should be disabled for RP rewriter, ACL2 rewriter, or both.
rw-direction RP-Rewriter can rewriter both from inside-out or from outside-in directions. This argument tells the rw direction the resulting rule should have. By default, it is set to :inside-out. It can be :inside-out, :outside-in, or :both.
supress-warnings can be used to turn off printing of some warnings.
add-rp-rule tells the program whether or not to call the add-rp-rule event after proving the conjecture to register it in the rewriter's ruleset table. It is by default set to t. When set to nil, relevant arguments such as rw-direction, disabled-for-rp will be ignored. Some shared parameters between add-rp-rule and internal defthmrp functionality such as lambda-opt will be passed as is.
ruleset is passed directly to add-rp-rule as well as used by the
clause processor. It determines which
table to read and save the rewrite rule. By default, it is