		Search-engine friendly clone of the ACL2 documentation.

Atc-shallow-embedding

Defstruct

Define a shallowly embedded structure type.

Introduction

Since C structure types are user-defined, we provide this macro to define a shallowly embedded ACL2 representation of a C structure type. The user must call this macro to introduce the structure types that the C code must use. The macro specifies the name and the members, where each member is specified by a name and a type. The macro records the information about the structure type in a table, and generates functions to operate on the structure type, along with some theorems.

C code shallowly embedded in ACL2 can use the generated recognizers struct-<tag>-p in guards to specify structure types for parameters; if wrapped in star, they specify pointer types to structure types.

Currently this macro only supports certain types for the members of the structure type. We plan to extend this macro to support more member types.

General Form

(defstruct name
           (name1 type1)
           (name2 type2)
           ...
  )

Inputs

name

Name of the structure type.
It must be a symbol whose symbol-name is a portable ASCII identifier that is distinct from the symbol-names of structure types introduced by previous successful calls of defstruct.
This symbol name is the tag of the structure type [C:6.7.2.3].
In the rest of this documentation page, let <tag> be the symbol-name of this input.

name1, name2, ...

Names of the members of the structure type.
Each must be a symbol whose symbol-name is a portable ASCII identifier that is distinct from the symbol-names of all the other member names in the defstruct.
There must be at least one member (name).

type1, type2, ...

Types of the members of the structure type.
Each must be one of
schar
uchar
sshort
ushort
sint
uint
slong
ulong
sllong
ullong
(schar <size?>)
(uchar <size?>)
(sshort <size?>)
(ushort <size?>)
(sint <size?>)
(uint <size?>)
(slong <size?>)
(ulong <size?>)
(sllong <size?>)
(ullong <size?>)
where <size?> is an optional positive integer which, if present, must not exceed ullong-max. The first ten specify C integer types: each is the name of an ACL2 fixtype that models a C integer type, and specifies the corresponding C integer type. The other ten specify C integer array types: each consists of the name of an ACL2 fixtype that models a C integer type, which specifies the element type of the array type, and an optional positive integer; if present, the positive integer specifies the size of the array type; if absent, the array type has unspecified size. The positive integer may be absent only if the member is the last one, in which case it represents a flexible array member [C:6.7.2.1/18]; in this case, there must be at least another member. The aforementioned upper bound on the size is so that the size of the array type is representable as a C integer constant.

Generated Events

struct-<tag>-p

Recognizer of the values of the structure type.

struct-<tag>-fix

Fixer of the values of the structure type.

struct-<tag>

Fixtype of the values of the structure type.

struct-<tag>

Constructor of the values of the structure type.
This has the same name as the fixtype (see above), but it belongs to a different name space (functions vs. fixtypes).
The constructor has the form
(define struct-<tag> ((<name1> <pred1>) (<name2> <pred2>) ...)
  :guard (and ... (equal (len <namei>) <sizei>) ...)
  :returns (struct struct-<tag>-p
                   :hyp (and ... (equal (len <namei>) <sizei>) ...))
  ...)
where there is exactly a parameter for each member, with the same and in the same order, whose type <pred1>, <pred2>, etc. is (i) the recognizer of the integer type if the member has integer type or (ii) the recognizer of lists of the element integer type if the member has array type. Furthermore, the additional guard in :guard consists of a length constraint for each array member of array type: for an array with a size, the length constraint is an equality between the len of the parameter and the positive integer length; for an array without a size (i.e. a flexible array member), the length constraint is just consp of the parameter. The return theorem of the constructor has exactly all the length equality constraints as hypotheses (it does not have the consp constraint for the flexible array member, if any.

struct-<tag>-read-<member>

Reader for a member of the structure type.
There is one such reader for every member whose name is <member>.
The reader has the form
(define struct-<tag>-read-<member> ((struct struct-<tag>-p))
  :returns (value <typei>p)
  ...)
where <typei>p is the recognizer of the type corresponding to the typei that specifies the type of the member.

struct-<tag>-write-<member>

Writer for a member of the structure type.
There is one such writer for every member whose name is <member>.
The writer has the form
(define struct-<tag>-write-<member> ((value <typei>p)
                                     (struct struct-<tag>-p))
  ;; :guard present if <typei>p is <type>-arrayp:
  :guard (equal (<type>-array-length value) ...)
  :returns (new-struct struct-<tag>-p)
  ...)
where <typei>p is the recognizer of the type corresponding to the typei that specifies the type of the member. If the member has array type, the :guard constrains the length of value to be the one of the member.

struct-<tag>-<member>-length

Length of the flexible array member.
This is generated if the last member of the structure type has an array type of unspecified size, i.e. the structure type has a flexible array member.
The function has the form
(define struct-<tag>-<member>-length ((struct struct-<tag>-p))
  :returns (len natp)
  ...)

struct-<tag>-<member>-index-okp

Index checker for an array member of the structure type.
There is one such checker for every member whose name is <member> and whose type is an array type.
If the array type of the member has a specified size, the checker has the form
(define struct-<tag>-<member>-index-okp ((index cintegerp))
  :returns (yes/no booleanp)
  ...)
If the array type of the member does not have a specified size (which may be only the case for the last member, if it is a flexible array member), the checker has the form
(define struct-<tag>-<member>-index-okp ((index cintegerp)
                                         (struct struct-<tag>-p))
  :returns (yes/no booleanp)
  ...)
In either form, this function checks if the C integer index is within the range of the array. If the length of the array is known (specified by the <size?> in the <typei> that specifies the type of the member), the checker only needs the index. For the flexible array member (if present), we also need the structure as an additional argument, from which the flexible array member size is obtained and used to check the index against it.

struct-<tag>-read-<member>-element

Reader for an element of an array member of the structure type, using a C integer as index.
There is one such reader for every member whose name is <member> and whose type is an array type.
The reader has the form
(define struct-<tag>-read-<member>-element ((index cintegerp)
                                            (struct struct-<tag>-p))
  :guard (struct-<tag>-<member>-index-okp index ...)
  :returns (value <elemtype>p)
  ...)
where <elemtype>p is the recognizer of the integer element type of the typei that specifies the type of the member, and where the ... in the :guard is either struct if the member is a flexible array member or nothing otherwise. The reader reads an element of the array member, not the whole array member.

struct-<tag>-write-<member>-element

Writer for an array member of the structure type, using a C integer as index.
There is one such writer for every member whose name is <member> and whose type is an array type.
The writer has the form
(define struct-<tag>-write-<member>-element ((index cintegerp)
                                             (value <elemtype>p)
                                             (struct struct-<tag>-p))
  :guard (struct-<tag>-<member>-index-okp index ...)
  :returns (new-struct struct-<tag>-p)
  ...)
where <elemtype>p is the recognizer of the integer element type of the typei that specifies the type of the member, and where the ... in the :guard is either struct if the member is a flexible array member or nothing otherwise. The writer writes an element of the array member, not the whole array member.

struct-<tag>-read-<member>-list

Reader for all the elements of an array member of the structure type, where the elements are returned as a list (not an array).
There is one such reader for every member whose name is <member> and whose type is an array type.
The reader has the form
(define struct-<tag>-read-<member>-list ((struct struct-<tag>-p))
  :returns (values <elemtype>-listp)
  ...)
where <elemtype>-listp is the recognizer of lists of the integer element type of the typei that specifies the type of the member.

struct-<tag>-write-<member>-list

Writer for all the elements of an array member of the structure type, where the elements are passed as a list (not an array).
There is one such writer for every member whose name is <member> and whose type is an array type.
The writer has the form
(define struct-<tag>-write-<member>-list ((value <elemtype>-listp)
                                         (struct struct-<tag>-p))
  :guard (equal (len values) ...)
  :returns (new-struct struct-<tag>-p)
  ...)
where <elemtype>-listp is the recognizer of lists of the integer element type of the typei that specifies the type of the member, and the ... in the :guard is either the positive integer size of the array if the array member has a known size, or the term (len (struct-<tag>-read-<member>-list struct)) if the array member is a flexible one.

Subtopics

Defstruct-implementation: Implementation of defstruct.