Introduce a fixer for a predicate.
Given a unary predicate, a fixer (i.e. fixing function) for the predicate can be defined in a standard way. This macro automates this.
This macro may be extended to accommodate variations in the definition of fixers.
(deffixer name :pred ... :param ... :body-fix ... :parents ... :short ... :long ... )
A symbol that specifies the name of the fixer.
A symbol that names a unary predicate. This is the predicate that the fixer is for.
The formal parameter to use for the fixer.
If not supplied, it defaults to
x, in the same package as name.
A term that defines the value of the fixer when the argument is not in the predicate. Its only free variables, if any, must be just the parameter of the fixer (see
:param). It must be the case that this term satisfies the predicate when the parameter of the fixer does not.
These, if present, are added to the XDOC topic generated for the fixer.
The fixer, with the predicate as guard and the following body:(mbe :logic (if (pred param) param body-fix) :exec param)
A rewrite rule asserting that the fixer always satisfies the predicate:(pred (name param))
A rewrite rule asserting that the fixer rewrites to the parameter when the predicate holds:(implies (pred param) (equal (name param) param))
The above items are generated in a define for the fixer.