Introduce a typed record for use with defrstobj.
A typed record is a record-like structure: it associates
keys with values, has a
Unlike an ordinary
(foop (get a r))Meanwhile, the
(get a (set a v r)) = (foo-fix v) ; instead of just being v
You can use
(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
(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))
(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
This version of typed records is very similar in spirit to the
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
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
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