Defprod
Define a new product type, like a struct in C, following the
fty-discipline.
Defprod is a macro for introducing struct-like types. It
can be used to conveniently define a recognizer, constructor, accessors, fixing
function, and equivalence relation, and other supporting macros and
documentation for a new struct-like type. It automatically arranges so that
these new definitions follow the fty-discipline.
Defprod can be used in a standalone fashion to introduce simple (non
mutually-recursive) product types. But it is also compatible with deftypes, so it can be used to create products that are mutually-recursive
with other deftypes compatible type generators.
As with all deftypes-compatible type generators, its field types must
be types that are ``known'' to FTY. That is, they must either refer to types
that have been introduced with deffixtype or that have been produced by
other FTY type generating macros. (Fields can also be completely untyped.)
See also basetypes for some base types with fixing functions.
Basic Example
(defprod sandwich
((bread symbolp :default 'sourdough)
(coldcut meatp)
(spread condimentp)))
This example would produce:
- A recognizer sandwich-p.
- A fixing function sandwich-fix.
- An equivalence relation sandwich-equiv.
- A constructor (sandwich bread coldcut spread).
- A constructor macro (make-sandwich :bread bread ...), which simply
expands to a constructor call but uses the given defaults.
- A changer macro (change-sandwich x :bread bread ...).
- An accessor for each field, e.g., sandwich->bread.
- A b* binder sandwich, like those in std::defaggregate.
Much of this—the make/change macros, accessor names, b*
binders—is nearly identical to std::defaggregate. If you have
used defaggregate, switching to defprod should be very
comfortable.
General Syntax:
(defprod prodname
(list-of-fields)
keyword-options)
The fields are std::extended-formals, except that the guard must be
either simply a predicate or the call of a unary predicate on the field name.
Acceptable keyword arguments for each field are:
- :default: default value of the field in its constructor macro
- :rule-classes: rule-classes for the return type theorem of the
accessor.
Name/Documentation Options
- :pred
- :fix
- :equiv
- :count
- These allow you to override the default function names, which
are (respectively) name-p, name-fix, name-equiv, and
name-count.
- As a special case, :count may be nil, meaning no count function is
produced. (A count function is only produced when this is mutually-recursive
with other type generators.)
- :parents
- :short
- :long
- These let you customize the xdoc documentation produced for this
type. The documentation generated for products will automatically list the
fields and link to their types; it's often convenient to put additional notes
directly in the fields, e.g.,
(defprod monster
:parents (game)
:short "A monster to fight."
((name stringp "Name of the monster")
(health natp "How many hit points does the monster have?")
...)
:long "<p>More details about monsters could go here.</p>")
Performance/Efficiency Options
- :tag
- Defaults to nil, meaning that the product is untagged. Otherwise it
must be a keyword symbol and this symbol will be consed onto every occurrence
of the object.
- Having tags on your objects adds some execution/memory overhead, but
provides a reasonably nice way to distinguish different kinds of objects from
one another at runtime.
- :layout
- Defaults to :alist, but might instead be set to :tree,
:fulltree or :list. This determines how the fields are laid out in
the object's representation.
- The :alist format provides the best readability/debuggability but is
the worst layout for execution/memory efficiency. This layout represents
instances of your product type using an alist-like format where the name of
each field is next to its value. When printing such an object you can easily
see the fields and their values, but creating these objects requires additional
consing to put the field names on, etc.
- The :tree or :fulltree layouts provides the best efficiency and
worst readability. They pack the fields into a compact tree structure, without
their names. In :tree mode, any (nil . nil) pairs are compressed
into just nil. In :fulltree mode this compression doesn't happen,
which might marginally save time if you know your fields will never be in pairs
of nils. Tree-based structures require minimal consing, and each accessor
simply follows some minimal, fixed car/cdr path into the object. The objects
print as horrible blobs of conses that can be hard to inspect.
- The :list layout strikes a middle ground, with the fields of the
object laid out as a plain list. Accessing the fields of such a structure may
require more cdr operations than for a :tree layout, but at least
when you print them it is still pretty easy to tell what the fields are.
- Example: a tagless product with 5 fields could be laid out as follows:
`((,a . ,b) . (,c . (,d . ,e))) ;; :tree
`(,a ,b ,c ,d ,e) ;; :list
`((a . ,a) (b . ,b) (c . ,c) (d . ,d) (e . ,e)) ;; :alist
- :hons
- NIL by default. When T, the constructor is defined using hons
rather than cons, so your structures will always be structure shared.
This may improve memory efficiency in certain cases but is probably not a good
idea for most structures.
- :inline
- Default: (:acc :fix), meaning that the accessors and fixing function,
which for execution purposes is just the identity, will be defined as an inline function. This argument may also contain :xtor, which causes the
constructor to be inlined as well, but this is typically less useful as the
constructor requires some amount of consing. The option :all (not in a
list) is also possible.
Other Options
- :measure
- A measure is only necessary in the mutually-recursive case, but is probably
necessary then. The default measure is (acl2-count x), but this may not
work in the mutually-recursive case because of the possibility that x
could be (say) an atom, in which case the acl2-count of x will be no
greater than the acl2-count of a field. Often something like
(two-nats-measure (acl2-count x) 5) is a good measure for the product,
where the other mutually-recursive types have a similar measure with smaller
second component.
- :require
- :reqfix
- This adds a dependent type requirement; see the section on this feature
below.
Experimental Dependent Type Option
The top-level keyword :require can add a requirement that the fields
satisfy some relation. Using this option requires that one or more fields be
given a :reqfix option; it must be a theorem that applying the regular
fixing functions followed by the :reqfix of each field independently
yields fields that satisfy the requirement. It should also be the case that
applying the reqfixes to fields already satisfying the requirement leaves them
unchanged. For example:
(defprod sizednum
((size natp)
(bits natp :reqfix (loghead size bits)))
:require (unsigned-byte-p size bits))
If there is more than one field with a :reqfix option, these reqfixes
are applied to each field independently, after applying all of their types'
fixing functions. For example, for the following to succeed:
(defprod foo
((a atype :reqfix (afix a b c))
(b btype :reqfix (bfix a b c))
(c :reqfix (cfix a b c)))
:require (foo-req a b c))
the following must be a theorem (assuming afix and bfix are the
fixing functions for atype and btype, respectively):
(let ((a (afix a))
(b (bfix b)))
(let ((a (afix a b c))
(b (bfix a b c))
(c (cfix a b c)))
(foo-req a b c)))
Notice the LET, rather than LET*, binding the fields to their reqfixes. It
would NOT be sufficient for this to be true with a LET*.
