A macro to define packed integer data structures.
(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
(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.
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
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
keyword-updater: This is a symbol, and specifies the name of the keyword
updating macro (see below). The default is
DEFWORD creates an ACL2 DEFLABEL event named
DEFWORD also generates an updating macro
(<updater> val 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