		Search-engine friendly clone of the ACL2 documentation.

Defrstobj

Def-typed-record

Introduce a typed record for use with defrstobj.

A typed record is a record-like structure: it associates keys with values, has a get function to look up the value of some key, and has a set function to install some new value for some key.

Unlike an ordinary misc/record, a typed record is homogeneous, i.e., we unconditionally know:

(foop (get a r))

Meanwhile, the get and set functions for a typed record are almost the same as for ordinary records. The only difference is that the g-same-s theorem becomes:

(get a (set a v r)) = (foo-fix v)   ; instead of just being v

The macro def-typed-record can be used to introduce a new typed record structure for use in defrstobj array fields.

Usage

You can use def-typed-record to introduce the get- and set- functions, the ordinary get-of-set style theorems about them, and some additional definitions such as a badguy for identifying differences between typed records (which can be useful for pick-a-point style reasoning.)

Example: typed record for naturals

(def-typed-record nat
  :elem-p (natp x)
  :elem-list-p (nat-listp x)
  :elem-default 0
  :elem-fix (nfix x))

This introduces the recognizer function nat-tr-p, the getter function nat-tr-get, the setter function nat-tr-set, and related theorems.

Example: typed-record for (8-bit) bytes

(defun ubp-listp (n x)
  (declare (xargs :guard t))
  (if (atom x)
      (not x)
    (and (unsigned-byte-p n (car x))
         (ubp-listp n (cdr x)))))

(defun ubp-fix (n x)            ;; other fixing functions
  (declare (xargs :guard t))    ;; are also possible
  (if (unsigned-byte-p n x)
      x
    0))

(def-typed-record ubp8
  :elem-p       (unsigned-byte-p 8 x)
  :elem-list-p  (ubp-listp 8 x)
  :elem-default 0
  :elem-fix     (ubp-fix 8 x))

This produce ubp8-tr-p, ubp8-tr-get, ubp8-tr-set, and related theorems.

General Form

(def-typed-record name
  :elem-p        [element recognizer, foop]
  :elem-list-p   [list recognizer, foo-listp]
  :elem-default  [default value, e.g., 0, nil, ...]
  :elem-fix      [fixing function, foo-fix]
  :in-package-of [symbol to use for new names])

Note that the terms you use for elem-p and so forth need to refer to exactly the variable acl2::x.

Related Work and History

This version of typed records is very similar in spirit to the coi/records/defrecord.lisp book; see:

David Greve and Matthew Wilding. Typed ACL2 Records. ACL2 Workshop 2003.

Greve and Wilding implemented typed records by starting with an ordinary record, but instead of just storing values or fixed values into its slots, they instead store ENTRIES of the form (FOO . NON-ENTRY), where the FOO must be a foop that is not the default foop.

When developing rstobjs, I (Jared) started with Greve and Wilding's approach; see legacy-defrstobj. But when I tried to extend their work to be able to view a STOBJ array as a typed record, I ran into trouble. I didn't see a good way to prove something akin to equal-by-g, and without that it didn't seem easy to adapt the basic approach I'd developed for untyped records to also deal with typed records.

I went to Sol's office to gripe about this, and we started to try to more precisely understand what was problematic. In a short time, we had come up with a different way to implement typed records that seems to be much more suitable.

In short, instead of using a misc/record with some kind of special entries, we directly develop a new kind of typed record where the well-formed records are only allowed to have values of the proper type. This lets us nicely separate the bad part of the record (if any) from the good part, and obtain a theorem in the spirit of EQUAL-BY-G.