		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Defword

A macro to define packed integer data structures.

Example:

(DEFWORD FM9001-INSTRUCTION-WORD
  ((RN-A 4 0) (MODE-A 2 4) (IMMEDIATE 9 0) (A-IMMEDIATE 1 9)
   (RN-B 4 10) (MODE-B 2 14)
   (SET-FLAGS 4 16) (STORE-CC 4 20) (OP-CODE 4 24))
  :CONC-NAME ||
  :SET-CONC-NAME SET-)

The above example defines the instruction word layout for the FM9001. The macro defines accessing macros (RN-A i), ... ,(OP-CODE i), updating macros (SET-RN-A val i), ... ,(SET-OP-CODE val i), and a keyword updating macro (UPDATE-FM9001-INSTRUCTION-WORD val &rest args).

General form:

(DEFWORD name struct &key conc-name set-conc-name keyword-updater)

The DEFWORD macro defines a packed integer data structure, for example an instruction word for a programmable processor or a status word. DEFWORD is a simple macro that defines accessing and updating macros for the fields of the data structure. The utility of DEFWORD is mainly to simplify the specification of packed integer data structures, and to improve the readability of code manipulating these data structures without affecting performance. As long as the book "logops-lemmas" is loaded all of the important facts about the macro expansions should be available to the theorem prover.

Arguments

name:  The name of the data structure, a symbol.

struct : The field structure of the word. The form of this argument is
given by the following grammar:

<tuple>  := (<field> <size> <pos> [ <doc> ])
<struct> := () | (<tuple> . <struct>)

where:

(SYMBOLP <field>)
(AND (INTEGERP <size>) (> <size> 0))
(AND (INTEGERP <pos>) (>= <pos> 0))
(STRINGP <doc>)

In other words, a list of tuples, the first element being a symbol, the second a positive integer, the third a nonnegative integer, and the optional fourth a string.

Note that there are few other requirements on the <struct> other than the syntactic ones above. For example, the FM9001 DEFWORD shows that a word may have more than one possible structure - the first 9 bits of the FM9001 instruction word are either an immediate value, or they include the RN-A and MODE-A fields.

conc-name, set-conc-name: These are symbols whose print names will be concatenated with the field names to produce the name of the accessors and updaters respectively. The default is <name>- and SET-<name>- respectively. The access and update macro names will be interned in the package of name.

keyword-updater: This is a symbol, and specifies the name of the keyword updating macro (see below). The default is UPDATE-<name>.

Interpretation

DEFWORD creates an ACL2 DEFLABEL event named <name>.

Each tuple (<field> <size> <pos>) represents a <size>-bit field of a word at the bit position indicated. Each field tuple produces an accessor macro

(<accessor> word)

where <accessor> is computed from the :conc-name (see above). This accessor will expand into:

(RDB (BSP <size> <pos>) word).

DEFWORD also generates an updating macro

(<updater> val word)

where <updater> is computed from the :set-conc-name (see above). This macro will expand to

(WRB val (BSP <size> <pos>) word)

The keyword updater

(<keyword-updater> word &rest args)

is equivalent to multiple nested calls of the updaters on the initial word. For example,

(UPDATE-FM9001-INSTRUCTION-WORD WORD :RN-A 10 :RN-B 12)

is the same as (SET-RN-A 10 (SET-RN-B 12 WORD)).