		Search-engine friendly clone of the ACL2 documentation.

Defbitstruct

Define a bitvector type with accessors for its fields.

This macto defines a bitstruct type. A bitstruct can either be a base type, which is a single fixed-width integer, or a product type containing fields that are bits, Booleans, or other bitstructs. Such a product is represented as a single integer produced by concatenating all the fields together, where the first field is least significant.

Examples:

A bitstruct can be made up of single bits and Booleans. (The difference is only in the return type of the accessors and the input type of the updaters; the representation is the same.) The fields are ordered LSB first, so a is bit 0 of the representation and c is bit 2. This defines a predicate, fixing function, accessors, and a constructor similar to defprod, but also updaters such as !foo->a.

(defbitstruct foo
  ((a bitp)
   (b booleanp)
   (c bitp)))

A bitstruct can also contain fields that are other bitstructs. Here, the first field is a foo, which is three bits wide, so the b and c fields are bits 3 and 4, respectively. Also, since :signedp t was specified, the representation is signed: the product is represented as a 5-bit signed integer rather than a 5-bit natural.

(defbitstruct bar
  ((myfoo foo-p)
   (b booleanp)
   (c bitp))
  :signedp t)

A bitstruct can also be defined without any fields, giving only a width. These are mainly useful as fields of other bitstructs. This makes sense when the individual bits aren't meaningful, and their combined value is what's important. This defines a rounding-control as a 2-bit unsigned value.

(defbitstruct rounding-control 2)

Sometimes we may want to nest one bitstruct inside another, but also directly access the fields of the internal struct. Providing the :subfields keyword causes defbitstruct to produce direct accessors and updaters for the subfields of the nested struct. The following definition of mxcsr produces the usual accesors and updaters including mxcsr->flags and mxcsr->masks, but also mxcsr->ie and mxcsr->im, etc.

(defbitstruct fp-flags
  ((ie bitp)
   (de bitp)
   (ze bitp)
   (oe bitp)
   (ue bitp)
   (pe bitp)))

(defbitstruct mxcsr
  ((flags fp-flags :subfields (ie de ze oe ue pe))
   (daz bitp)
   (masks fp-flags :subfields (im dm zm om um pm))
   (rc  rounding-control)
   (ftz bitp)))

Syntax

A defbitstruct form is one of:

(defbitstruct typename fields [ options ] )

(defbitstruct typename width [ options ] ).

The syntax of fields is described below.

Top-level options

:pred, :fix, :equiv -- override the default names (foo-p, foo-fix, and foo-equiv) for the predicate, fixing function, and equivalence relation.
:parents, :short, :long -- provide xdoc for the bitstruct
:signedp -- when true, represents the structure as a signed integer rather than an unsigned one. (Signed and unsigned fields can be used inside unsigned and signed bitstructs -- they are simply sign- or zero-extended as necessary when accessed.)
:msb-first -- when non-NIL, reverses the order of the top-level fields, it does not reverse :subfield accessors/updaters.

Field Syntax

A field has the following form:

(fieldname type [ docstring ] [ options ... ] )

The type can be either a predicate or type name, i.e., bit or bitp, and must refer to either a single-bit type (bit or boolean) or a previously-defined bitstruct type. The docstring is a string which may contain xdoc syntax.

Field Options

:accessor, :updater -- override the default names struct->field, !struct->field for the accessor and updater functions.
:default -- change the default value for the field in the make-foo macro. The default default is NIL for Boolean fields and 0 for everything else.
:rule-classes -- override the rule classes of the accessor function's return type theorem. The default is :rewrite; it may be appealing to use :type-prescription, but typically the type prescription for the accessor should be determined automatically anyway.
:subfields -- Indicates that accessors and updaters should be created for subfields of this field, and gives their subfield names. See the section on subfields below.

Subfields

The :subfields field option may only be used on a field whose type is itself a bitstruct type containing fields. The value of the :subfields argument should be a list of subfield_entries, according to the following syntax:

subfield_entry ::= name | ( name ( subfield_entry ... ) )

Each top-level entry corresponds to a subfield of the field type. If the entry uses the second syntax, which itself has a list of entries, those entries correspond to sub-subfields of the subfield type. For example:

(defbitstruct innermost
  ((aa bitp)
   (bb bitp)))

(defbitstruct midlevel
  ((ii innermost :subfields (iaa ibb))
   (qq bitp)
   (jj innermost :subfields (jaa jbb))))

(defbitstruct toplevel
  ((ss innermost :subfields (saa sbb))
   (tt midlevel  :subfields ((tii (tiaa tibb))
                             tqq
                             tjj))))

For the toplevel bitstruct, this generates the following subfield accessors, in addition to the direct accessors toplevel->ss and toplevel->tt:

(toplevel->saa x)    == (innermost->aa (toplevel->ss x))
(toplevel->sbb x)    == (innermost->bb (toplevel->ss x))
(toplevel->tii x)    == (midlevel->ii (toplevel->ss x))
(toplevel->tiaa x)   == (innermost->aa (midlevel->ii (toplevel->tt x)))
(toplevel->tibb x)   == (innermost->bb (midlevel->ii (toplevel->tt x)))
(toplevel->tqq x)    == (midlevel->qq (toplevel->tt x))
(toplevel->tjj x)    == (midlevel->jj (toplevel->tt x))