(include-book "kestrel/fty/defomap" :dir :system)
This is analogous to deflist, defalist, and defset. Besides the fixtype itself, this macro also generates some theorems about the fixtype. Future versions of this macro may generate more theorems, as needed.
Aside from the recognizer, fixer, and equivalence for the fixtype, this macro does not generate any operations on the typed omaps. Instead, the generic omap operations can be used on typed omaps. This macro generates theorems about the use of these generic operations on typed omaps.
Future versions of this macro may be modularized to provide
a ``sub-macro'' that generates only the recognizer and theorems about it,
without the fixtype (and without the fixer and equivalence),
similarly to std::deflist and std::defalist.
That sub-macro could be called
This macro differs from defmap, which generates an alist.
(defomap type :key-type ... :val-type ... :pred ... :fix ... :equiv ... :parents ... :short ... :long ...
The name of the new fixtype.
The (existing) fixtype of the keys of the new map fixtype.
The (existing) fixtype of the values of the new map fixtype.
The name of the recognizer, fixer, and equivalence for the new fixtype.
The defaults are
typefollowed by -p, -fix, and -equiv.
These are used to generate XDOC documentation for the topic
If any of these is not supplied, the corresponding component is omitted from the generated XDOC topic.
This macro currently does not perform a thorough validation of its inputs. Erroneous inputs may result in failures of the generated events. Errors should be easy to diagnose, also since this macro has a very simple and readable implementation. Future versions of this macro should perform more thorough input validation.
The following are generated, inclusive of XDOC documentation: