|
|
|---|
|
|
|
|---|
Defining ``make-self'' functions for fixtypes.
This macro automates the creation of ``make-self'' functions on fixtypes. A ``make-self'' function is one which takes a value of a particular fixtype and returns a standard constructor form which would evaluate to the input value.
The primary motivation for introducing such functions is to produce more legible forms which are consistent across different layouts.
(defmake-self type :parents ... ; no default :short ... ; no default :long ... ; no default :print ... ; default :result )
The name of the type or clique for which to create the ``make-self'' functions. ``Make-self'' functions will also be generated for all the necessary type dependencies.
These, if present, are added to the generated XDOC topic described in the Section `Generated Events' below.
Controls how much information is printed. This is a apt::print-specifier. On
nil or:error , only error messages are printed. On:result (the default) or:info , the events to be submitted are printed, in addition to error messages. Finally, all information is printed under:all .
An XDOC topic whose name is obtained by adding, at the end of the symbol
make-self- , the name of the (possibly singleton) clique to which thetype input belongs. If any of the:parents ,:short , or:long inputs are provided, they are added to this XDOC topic. This XDOC topic is generated with ACL2::defxdoc+, with:order-topics t , so that the other generated events (described below), which all have this XDOC topic as parent, are listed in order as subtopics.
For each type
<type> in the same clique specified by thetype input, as well as all type dependencies, a ``make-self'' function for that type.