|
|
|---|
|
|
|
|---|
Introduce an alias of an existing fixtype.
Sometimes a fixtype, as well as its recognizer, fixer, and equivalence,
have names that are appropriate in a general context,
but that could be made more convenient and readable
in a more restrictive context.
For instance, the ACL2::ubyte4 and ACL2::ubyte8 fixtypes
(and their recognizers, fixers, and equivalences)
are named according to
a uniform scheme in defbyte-standard-instances,
but in many contexts the names
Instead of defining new fixtypes, recognizers, fixers, and equivalences with the desired names, and inevitably having to introduce theorems about them, it is preferable to introduce and use aliases. ACL2 has built-in support to do this for functions, via add-macro-alias and add-macro-fn. For the fixtypes themselves, i.e. for the fixtype names, aliases can be actually created via deffixtype, which simply records (in the ACL2 world) the association between the fixtype name and its recognizer, fixer, and equivalence: by calling deffixtype with the aliases for recognizer, fixer, and equivalence, we effectively create an alias of the existing fixtype.
This macro automates this process. It introduces macro aliases for a fixtype's recognizer, fixer, and equivalence, along with a new fixtype associated to such aliases, which is effectively an alias of the existing fixtype.
(deffixtype-alias alias type :pred ... :fix ... :equiv ... )
A symbol to use as the new fixtype alias.
A symbol that names the existing fixtype to alias.
A symbol to use as the new recognizer alias.
If not supplied, the recognizer of the new fixtype is the same as the existing fixtype.
A symbol to use as the new fixer alias.
If not supplied, the fixer of the new fixtype is the same as the existing fixtype.
A symbol to use as the new equivalence alias.
If not supplied, the equivalence of the new fixtype is the same as the existing fixtype.
Macro definitions for the new recognizer, fixer, and equivalence (except for those whose corresponding keyword input is not supplied).
Calls of add-macro-fn to associate the new recognizer, fixer, and equivalence with the existing ones (except for those whose corresponding keyword input is not supplied).
A call of deffixtype for the new fixtype.