|
|
|---|
|
|
|
|---|
The steps necessary to add meta rules to RP-Rewriter
Below are the steps users need to follow, and information they may use:
1. Create your meta function.
Your meta function can return either two values:term and dont-rw; or only term. For best performance, it is recommended that you return dont-rw structure as well. If you do not want the returned term to be rewritten at all, you can return 't' for dont-rw.(define <meta-fnc> (term) :returns (mv term dont-rw) OR (term) ...)
2. Create formula-checks function.
This event submits a function with signature(def-formula-checks <formula-check-name> (<list-of-function-names>))
3. Prove that evaluation of the function returns an equivalent term under the evaluator.
This is the correctness theorem of the meta rule. Optionally, you may have (valid-sc term a), which states that the side-conditions in RP-Rewriter are correct; and (rp-termp term), which states that some of the syntactic invariances hold and the term is syntactically compatible with RP-Rewriter. See discussions for valid-sc and rp-termp.(defthm rp-evlt-of-meta-fnc (implies (and (valid-sc term a) ;;optional (rp-termp term) ;;optional (rp-evl-meta-extract-global-facts) (<formula-check-name> state)) (equal (rp-evlt (<meta-fnc> term) a) (rp-evlt term a))))
If the meta function returns dont-rw, then you need to prove this lemma for
4. Prove that meta-function retains the correctness of side-conditions.
Meta functions can introduce or change side-conditions by manipulating 'rp' instances. Therefore users need to prove that the invariance about side conditions are maintained.(defthm valid-sc-of-meta-fnc (implies (and (valid-sc term a) (rp-termp term) ;;optional (rp-evl-meta-extract-global-facts) ;;optional (<formula-check-name> state)) ;;optional (valid-sc (<meta-fnc> term) a)))
If the meta function returns dont-rw, then you need to prove this lemma for
5. Optionally, prove that the meta function returns a valid syntax.
Even though it is optional, it is recommended that you prove such a lemma for your meta function. It prevents syntactic check on every term returned from meta function.(defthm rp-termp-of-meta-fnc (implies (rp-termp term) (rp-termp (<meta-fnc> term))))
If the meta function returns dont-rw, then you need to prove this lemma for
6. Save the meta rule in the rule-set of RP-Rewriter for meta rules.
See add-meta-rule for further discussion of the options.(rp::add-meta-rule :meta-fnc <meta-fnc> :trig-fnc <trig-fnc> :returns <return-signature> :rw-direction <:inside-out, :outside-in, or :both> :valid-syntaxp <t-if-rp-termp-of-meta-fnc-is-proved>)
7. Attach these newly created meta functions.
If you are going to include this book later when other meta rules for RP-Rewriter is present, you may want to call this function when all the meta rules are included.(rp::attach-meta-fncs <a-unique-name-for-updated-clause-processor>)
You may look at examples of RP-Rewriter meta rules under /books/projects/RP-Rewriter/meta/*. implies-meta.lisp is a very simple example of an outside-in meta rule.
Some books under /books/projects/RP-Rewriter/proofs/* might be useful when proving when proving meta rules correct, especially aux-function-lemmas and eval-functions-lemmas.