Def-multityped-record
Introduce a multi-typed record for use with defrstobj.
A multi-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 multi-typed record has typed
elements. The type of an element is parametrized by the key. I.e., we have a
function elementp such that we know (elementp key (get key r)).
Correspondingly, there are also element-fix and element-default
functions that also take the key as input. Meanwhile, the get and set
functions for a multityped 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)) = (elem-fix a v) ; instead of just being v
The macro def-multityped-record can be used to introduce a new
multityped record structure.
Multityped records are a generalization of typed records (see ACL2::def-typed-record). A typed-record can be viewed as a multityped
record for which the elem-p, elem-fix, and elem-default
functions ignore the key.
Usage
You can use def-multityped-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: uniformly typed record for naturals
(def-multityped-record natrec
:elem-p (natp x)
:elem-default 0
:elem-fix (nfix x))
This introduces the recognizer function natrec-p, the getter function
natrec-get, the setter function natrec-set, and related theorems.
Example: multiply typed record
In this record, integer keys are associated with integer values, symbol keys have
symbol values, and any other key can contain objects of any type.
(defun foo-elem-p (key x)
(cond ((symbolp key) (symbolp x))
((integerp key) (integerp x))
(t t)))
(defun foo-elem-fix (key x)
(cond ((symbolp key) (if (symbolp x) x nil))
((integerp x) (ifix x))
(t x)))
(defun foo-elem-default (key)
(if (integerp key) 0 nil))
(def-multityped-record foorec
:elem-p (foo-elem-p k x)
:elem-default (foo-elem-default k)
:elem-fix (foo-elem-fix k x))
This produces foorec-p, foorec-get, foorec-set, and related
theorems.
General Form
(def-multityped-record name
:elem-p [element recognizer, foop -- expression involving k and x]
:elem-default [default value, e.g., 0, nil, or an expression involving k]
:elem-fix [fixing function, foo-fix -- expression involving k and x]
: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 variables acl2::k and acl2::x.
Related Work and History
This evolved from centaur/defrstobj/typed-record.lisp when we needed a
record-like stobj with a more robust set-of-get identity.
