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 the same 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 the same 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 the same lemma for

6. If your function returns dont-rw, then you also need to prove that it is syntactically correct. Otherwise skip this step.

(defthm dont-rw-syntaxp-of-meta-fnc (dont-rw-syntaxp (mv-nth 1 (<meta-fnc> term))))

7. 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> :outside-in <t-if-the-meta-rule-should-apply-from-outside-in> :valid-syntaxp <t-if-rp-termp-of-meta-fnc-is-proved>)

8. 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.

- Add-meta-rule
- A macro to add created meta rules to RP-Rewriter
- Dont-rw
- A special data structure that RP-Rewriter meta rules may return to control rewriting of returned terms.
- Attach-meta-fncs
- Creates and attaches a new meta-rule caller function to register added meta rules.
- Is-rp-clause-processor-up-to-date
- Checks if all the added meta-rules are 'registered'