Defretgen-rules
Syntax and meaning of rules and abbreviations for defretgen
and defret-mutual-generate
The defretgen and defret-mutual-generate macros produce defret forms by applying a series of rules to functions. Each rule is a pair
(condition actions) where if the condition is satisfied by the function,
the actions modify that function's defret form. The rules may be written
directly by the user or generated using some abbreviations, discussed
below.
Condition language
The condition under which a rule applies may be a Boolean formula using
AND/OR/NOT, T and NIL, and the following checks:
- (:has-formal <io-var-test>) checks that the function has a formal
satisfying the specified input/output variable test; see the section on
input/output conditions below.
- (:has-return <io-var-test>) checks that the
function has a return value satisfying the given criteria, simple to
has-formal.
- (:fnname name) only applies to the given function.
- :recursive, :nonrec, :mutrec, :constrained check
whether the function is of that type, where :recursive means singly
recursive.
See the function dmgen-eval-condition for implementation.
Input/output variable conditions
Several conditions and actions have tests on input/output variables. These
are constructed as Boolean (and/or/not) combinations of the following base
tests:
- (:type type-name) tests the type of the formal or return value
- (:prop property) tests whether the given property is present
- (:name name) tests whether the name of the formal or return value matches.
As a special case, a single base test can be written with the keyword and
value spliced into the condition or action form; that is, the following two
conditions are equivalent:
(:has-formal (:type foo))
(:has-formal :type foo)
Actions
An action may be any of the following:
- (:add-hyp term) adds term as a top-level hypothesis.
- (:add-concl term) adds term as a conclusion, conjoined with any others.
- (:add-bindings . bindings) adds the given B* bindings, after
binding the return values but outside of both the hyps and conclusions.
- (:each-formal <io-var-test> :var var :action action), where each
action is an :add-hyp, :push-hyp or :add-concl form, adds the
given hyp or conclusion for each formal matching the io-var-test criteria, with
var in these actions replaced by the name of the formal.
- (:each-return <io-var-test> :var var :action action),
similar to each-formal but acts on return values instead of formals.
- (:push-hyp term) pushes term as a hypothesis for any conclusions
added subsequently until it is popped off the stack with (:pop-hyp).
- (:pop-hyp) removes the most recently pushed hypothesis so it won't
affect subsequent conclusions added.
- (:add-keyword key val ...) adds the keyword/value pairs as arguments
to the resulting defret form; typical keys to use are :hints and
:rule-classes.
- (:set-thmname template) sets the theorem name template for the
defret to the given symbol, which may include the substring <FN>
which is replaced by the name of the function.
Common Abbreviations
The defretgen and defret-mutual-generate macros support some other keywords
besides :rules, each of which generates rules according to some common usage
patterns. Note that the ordering of rules is significant for the behavior of
:push-hyp/:pop-hyp and :add-concl. The rules generated by these
abbreviations are considered before the explicit :rules; this means that
any conclusions generated by :return-concls will not be affected by any
:push-hyp forms from the :rules.
:formal-hyps
This keyword generates hypotheses based on the names/types/properties of formals. Its
argument is a list of elements of one of the following forms:
- (formalname hyp-term [ <io-var-test> ]) adds the given hyp to the
theorem of any function with a formal of the given name. If an io-var-test is
given, it will only be added if that formal satisfies it.
- ((type-pred name) hyp-term) adds the given hyp term for every formal
of the given type, binding that formal to name.
- (<io-var-test> name hyp-term) adds the given hyp for every formal
satisfying the given io-var-test, binding that formal to name.
:return-concls
This keyword generates hypotheses based on the names/types of return values.
Its argument is a list of elements similar to those of :formal-hyps.
:function-keys
This keyword adds hints or other keywords to the theorems corresponding to
function names. For example:
:function-keys
((rewrite-term-list
:hints ('(:expand ((termlist-vars x)))))
