Defrec
Introduce a record structure, like a struct in C.
The defrec macro is built into ACL2 and is frequently used in
the ACL2 sources to define basic kinds of structures.
Better Alternatives to Defrec
While defrec may be a reasonable choice for writing program-mode code, most users would likely be better served by using one of
the many, richer alternatives to defrec that are available in various
books. See for instance macros such as:
A major reason to favor these macros over defrec is that they
introduce the constructors and accessors for the structure as proper
functions, rather than mere macros. This is very helpful when you are trying
to use ACL2 to reason about code that works with structures. For instance, it
means that your proof goals will involve terms like (employee->position
x) instead of (cdddr x).
Another reason is that defrec does not support putting constraints on
the fields of your structure. For instance, you might want to have an
employee structure where the name field is always a string. You
can't do this with defrec, but any of the above macros support it.
Some of the above macros also have other useful features, e.g., integration
with b*, support for xdoc documentation, and so forth.
Usage
A typical use of defrec might look like this:
(defrec employee ;; name of the structure
(name salary . position) ;; fields of the structure
nil) ;; "cheap" flag
This will result in the introduction of:
- A "weak" recognizer function, weak-employee-p, which recognizes
cons structures that have the right shape. We call the recognizer weak
because it doesn't impose any constraints on the fields, e.g., there is no
requirement that the name of an employee must be a string or that the
salary must be a number.
- A make macro that can be used like this:
(make employee :name "Jimmy"
:salary 0
:position "Unpaid Intern")
- A change macro that can be used like this:
(let ((jimmy (make-employee :name "Jimmy" ...)))
(change employee jimmy :salary 300000
:position "Vice President"))
- Suitable access macros that can be used like this:
(let ((jimmy (make-employee :name "Jimmy" ...)))
(access employee jimmy :name))
Subtopics
- Change
- Mutator macro for defrec structures.
- Make
- Constructor macro for defrec structures.
- Access
- Accessor macro for defrec structures.
