# 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.