Defaggregate
Introduce a record structure, like a struct in C.
Introduction
Defaggregate introduces a recognizer, constructor, and accessors for a new
record-like structure. It is similar to struct in C or defstruct in
Lisp.
Basic example:
(defaggregate employee ;; structure name
(name salary position) ;; fields
:tag :employee ;; options
)
This example would produce:
- A recognizer, (employee-p x),
- A constructor, (employee name salary position),
- An accessor for each field, e.g., (employee->name x),
- An extension of b* to easily destructure these aggregates,
- Macros for making and changing aggregates,
- (make-employee :name ... :salary ...)
- (change-employee x :salary ...)
- Basic theorems relating these new functions.
General form:
(defaggregate name
Fields
[Option]* ;; i.e., :keyword value
[/// other-events]) ;; optional, starts with the symbol ///
The name acts like a prefix; the function and theorem names we generate
will be based on this name.
The Fields describe what fields each instance of the structure will
have. The example above shows only the very simplest syntax, but fields can
also have well-formedness requirements, documentation, etc.; see below.
The Options control various settings on the structure, and many options
are described below. Options can actually come before or after the fields (or
both).
The other-events is just a place for arbitrary other events to be put,
as in define. This is mainly intended as a book structuring device, to
allow you to keep related theorems near your aggregate.
Structure Tags
The :tag of every aggregate must either be:
- A keyword symbol that typically shares its name with the name of the
aggregate, e.g., in the "employee" aggregate the tag is :employee;
or
- nil, to indicate that you want a tagless aggregate.
How are tags used? Each instance of a tagged aggregate will be a cons tree
whose car is the tag. This requires some overhead—one cons for every
instance of the aggregate—but allows us to compare tags to differentiate
between different kinds of aggregates. A tagless aggregate avoids this
overhead, but you give up the ability to easily distinguish different kinds of
tagless aggregates from one another.
To avoid introducing many theorems about car, we use an alias named
tag. Each tagged defaggregate results in three tag-related
theorems:
- Tag of constructor:
(defthm tag-of-example
(equal (tag (example field1 ... fieldN))
:example))
- Tag when recognized:
(defthm tag-when-example-p
(implies (example-p x)
(equal (tag x) :example))
:rule-classes ((:rewrite :backchain-limit-lst 0)
(:forward-chaining)))
- Not recognized when tag is wrong:
(defthm example-p-when-wrong-tag
(implies (not (equal (tag x) :example))
(equal (example-p x)
nil))
:rule-classes ((:rewrite :backchain-limit-lst 1)))
These theorems seem to perform well and settle most questions regarding the
disjointness of different kinds of aggregates. In case the latter rules become
expensive, we always add them to the tag-reasoning ruleset, so you can
disable this ruleset to turn off
almost all tag-related reasoning.
Syntax of Fields
To describe the aggregate's fields, you can make use of extended-formals syntax. This syntax means that fields can be optional and
use keyword/value options. One can also use this syntax to describe a
particular field of an aggregate -- by providing documentation or specifying a
predicate that the field must satisfy. Here is an example:
(defaggregate employee
((name "Should be in Lastname, Firstname format"
stringp :rule-classes :type-prescription)
(salary "Annual salary in dollars, nil for hourly employees"
(or (not salary) (natp salary))
:rule-classes :type-prescription)
(rank "Employee rank. Can be empty."
(implies rank (and (characterp rank)
(alpha-char-p rank))))
(position (and (position-p position)
(salary-in-range-for-position-p salary position))
:default :peon))
:tag :employee)
The "guard" for each field plays three roles:
- It is a guard on the constructor
- It is a well-formedness requirement enforced by the recognizer
- It is a theorem about the return type of the accessor.
The return-type theorem requires some special attention. By default, the
return-type theorem is an ordinary ACL2::rewrite rule. When this is not
appropriate, e.g., for name above, you may wish to use a different
:rule-classes option.
The embedded xdoc documentation gets incorporated into the
automatically-created documentation for the aggregate in a sensible way.
This is overridden by the :suppress-xdoc t option.
The :default value only affects the Make macro (see below).
Options
Layout
By default, aggregates are represented with :layout :alist, but you can
also choose other layouts.
The :alist format provides the best readability/debuggability but is
the worst layout for execution/memory efficiency. This layout represents
instances of your structure 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.
Honsed Aggregates
By default, :hons is nil and the constructor for an aggregate will
build the object using ordinary conses. However, when :hons is set to
t, we instead always use hons when building these aggregates.
Honsing is only appropriate for some structures. It is a bit slower than
consing, and should typically not be used for aggregates that will be
constructed and used in an ephemeral manner. If you are going to hons your
structures, you should probably use a :tree or :fulltree layout.
Other Options
- :pred
- Name of the recognizer for the aggregate -- must be a valid symbol for a
new function. Defaults to agg-p, where agg is the name of the
aggregate.
- :mode
- Mode for the introduced functions -- must be either :program or
:logic. Defaults to the current ACL2::defun-mode.
- :already-definedp
- Advanced option that may be useful for mutually-recursive recognizers.
This means: generate all ordinary defaggregate functions and theorems
except for the recognizer. For this to work, you have to have already
defined a "compatible" recognizer.
- :parents, :short, :long
- These options are as in xdoc. Whatever you supply for :long
will follow some automatically generated documentation that describes the
fields of the aggregate. If you don't want that xdoc, you can
turn it off with the next option.
- :suppress-xdoc
- You can use :suppress-xdoc t to prevent xdoc from being
created for this aggregate. Overrides the automatically generated
documentation as well as:parents, :short, and :long.
- :extra-field-keywords
- Advanced option for people who are writing extensions of defaggregate.
This tells defaggregate to tolerate (and ignore) certain additional keywords in
its fields. The very advanced user can then inspect these fields after
submitting the aggregate, and perhaps use them to generate additional
events.
- :verbosep
- You can use :verbosep t to turn off output hiding. This option is
generally meant for debugging failures in defaggregate.
- :rest
- This option is deprecated. Please use the new /// syntax, instead.
Dependent Requirements
The embedded "guard" in each extended formal allows you to naturally
express simple requirements, e.g., arity should be a natural and args
should be an true-listp. But what if you need something more like dependent types, e.g.,
say that arity is supposed to always match the length of args?
It's valid to refer to other fields within the guards of an embedded formal,
so one way we could write this would be, e.g.,:
(defaggregate mytype
((arity natp :rule-classes :type-prescription)
(args (and (true-listp args)
(equal (len args) arity)))))
This is perfectly valid, but you may sometimes prefer not to embed these
dependent requirements directly in the fields. For instance, in the example
above, the result-type theorem about args becomes two ACL2::rewrite
rules. It would probably be better for the true-listp part to be a ACL2::type-prescription rule. But the len requirement doesn't make sense
as a :type-prescription.
To work around this, you could use an explicit, compound :rule-classes
form with separate :corollary theorems. This gets very ugly, because you
have to write out each corollary in full, e.g.,:
(defaggregate mytype
((arity natp :rule-classes :type-prescription)
(args (and (true-listp args)
(equal (len args) arity))
:rule-classes
((:type-prescription :corollary
(implies (force (mytype-p x))
(true-listp (mytype->args x))))
(:rewrite :corollary
(implies (force (mytype-p x))
(equal (len (mytype->args x))
(mytype->arity x))))))))
So you may instead prefer to use the alternate :require syntax.
In this case, we would have:
(defaggregate mytype
((arity natp :rule-classes :type-prescription)
(args true-listp :rule-classes :type-prescription))
:require
((len-of-mytype->args (equal (len args) arity))))
This would result in an ordinary ACL2::type-prescription return-type
theorems for both arity and args, and a separate rewrite rule to deal
with the length dependency:
(defthm len-of-mytype->args
(implies (force (mytype-p x))
(equal (len (mytype->args x))
(mytype->arity x))))
The general form of each :require form is:
(theorem-name conclusion [:rule-classes ...])
Where conclusion may mention any of the fields of the aggregate. Each
requirement becomes a guard for the constructor, a well-formedness requirement
in the recognizer, and a theorem about the accessors of your structure, exactly
like the simple requirements on each field.
Make and Change Macros
Direct use of the constructor is discouraged. Instead, we introduce two
macros with every aggregate. The make macro constructs a fresh aggregate
when given values for its fields:
(make-example :field1 val1 :field2 val2 ...)
-->
(example val1 val2 ...)
The change macro is similar, but is given an existing object as a
starting point. It may be thought of as:
(change-example x :field2 val2)
-->
(make-example :field1 (example->field1 x)
:field2 val2
:field3 (example->field3 x)
...)
There are some strong advantages to using these macros instead of calling
the constructor directly.
- The person writing the code does not need to remember the order of the
fields
- The person reading the code can see what values are being given to which
fields.
- Fields whose value should be nil (or some other :default) may be
omitted from the make macro.
- Fields whose value should be left alone can be omitted from the
change macro.
These features make it easier to add new fields to the aggregate later on,
or to rearrange fields, etc.
Integration with b*
Defaggregate automatically introduces a pattern binder that integrates into
b*. This provides a concise syntax for destructuring aggregates. For
instance:
(b* ((bonus-percent 1/10)
((employee x) (find-employee name db))
(bonus (+ (* x.salary bonus-percent)
(if (equal x.position :sysadmin)
;; early christmas for me, har har...
(* x.salary 2)
0))))
bonus)
Can loosely be thought of as:
(b* ((bonus-percent 1/10)
(temp (find-employee name db))
(x.name (employee->name temp))
(x.salary (employee->salary temp))
(x.position (employee->position temp))
(bonus (+ (* x.salary bonus-percent)
(if (equal x.position :sysadmin)
;; early christmas for me, har har...
(* x.salary 2)
0))))
bonus)
For greater efficiency in the resulting code, we avoid binding components
which do not appear to be used, e.g., we will not actually bind x.name
above.
Detecting whether a variable is needed at macro-expansion time is inherently
broken because we can't truly distinguish between function names, macro names,
variable names, and so forth. It is possible to trick the binder into
including extra, unneeded variables, or into optimizing away bindings that are
necessary. In such cases, the ACL2 user will be presented with either "unused
variable" or "unbound variable" error. If you can come up with a
non-contrived example where this is really a problem, we might consider
developing some workaround, perhaps extended syntax that lets you suppress the
optimization altogether.
Extra Binder Names
You can instruct the b* binder to understand additional, "derived"
fields for certain structures.
Example. Suppose we are dealing with student structures that have
separate firstname and lastname fields. We might find that we often
want to use the student's full name. We can explain to the b* binder
that we want it to understand the syntax x.fullname by giving the
:extra-binder-names argument.
(defaggregate student
((firstname stringp)
(lastname stringp)
(grade natp))
:extra-binder-names (fullname))
When we do this, the b* binder will look for occurrences of
x.fullname and, if any are found, it will bind them to
(student->fullname x). For this to be work at all, we have to define this
function ourselves, e.g.,:
(define student->fullname ((x student-p))
:returns (fullname stringp :rule-classes :type-prescription)
(str::cat (student->firstname x)
" "
(student->lastname x)))
Once we do this, we can freely write x.fullname wherever we previously
would have had to call (student->fullname x). For instance:
(b* ((fred (make-student :firstname "Fredrick"
:lastname "Flintstone"
:grade 7))
((student fred)))
(str::cat "Fred's full name is " fred.fullname "."))
Nicely produces "Fred's full name is Fredrick Flintstone".
Subtopics
- Tag
- Get the tag from a tagged object.
- Prod-cons
- Special constructor for products that collapses (nil . nil) into nil.
- Defaggrify-defrec
- Add defaggregate-style emulation for defrec records.
