		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]. 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 an integer member of the structure type.
There is one such reader for every member whose name is <member> and whose type is an integer type.
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 integer type corresponding to the typei that specifies the type of the member.

struct-<tag>-write-<member>

Writer for an integer member of the structure type.
There is one such writer for every member whose name is <member> and whose type is an integer type.
The writer has the form
(define struct-<tag>-write-<member> ((value <typei>p)
                                     (struct struct-<tag>-p))
  :returns (new-struct struct-<tag>-p)
  ...)
where <typei>p is the recognizer of the integer type corresponding to the typei that specifies the type 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

ACL2 integer index checker for an array member of the structure type.
There is one such checker for every member whose name is <member> ans 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 integerp))
  :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 integerp)
                                         (struct struct-<tag>-p))
  :returns (yes/no booleanp)
  ...)
In either form, this function checks if the 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.
This checker is used by the ones that operate on indices of C integer types below.

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

C integer 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, and for every choice of an integer type <type> for the index.
If the array type of the member has a specified size, the checker has the form
(define struct-<tag>-<member>-<type>-index-okp ((index <type>p))
  :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 <type>p)
                                         (struct struct-<tag>-p))
  :returns (yes/no booleanp)
  ...)
This function checks if the 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.
This checker converts the C integer index to an ACL2 integer index and calls the checker struct-<tag>-<member>-index-okp above.

struct-<tag>-read-<member>

Reader for an array member of the structure type, using an ACL2 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> ((index integerp)
                                    (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.
This reader is used by the ones that operate on indices of C integer types below.

struct-<tag>-read-<member>-<type>

Reader for an array member of the structure type, using a C integer as an index.
There is one such reader for every member whose name is <member> and whose type is an array type, and for every choice of an integer type <type> for the index.
The reader has the form
(define struct-<tag>-read-<member>-<type> ((index <type>p)
                                           (struct struct-<tag>-p))
  :guard (struct-<tag>-<member>-<type>-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.
This reader converts the C integer index to an ACL2 integer index and calls the reader struct-<tag>-read-<member> above.

struct-<tag>-write-<member>

Writer for an array member of the structure type, using an ACL2 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> ((index integerp)
                                     (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.
This writer is used by the ones that operate on indices of C integer types below.

struct-<tag>-write-<member>-<type>

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, and for every choice of an integer type <type> for the index.
The writer has the form
(define struct-<tag>-write-<member>-<type> ((index <type>p)
                                            (value <elemtype>p)
                                            (struct struct-<tag>-p))
  :guard (struct-<tag>-<member>-<type>-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.
This writer converts the C integer index to an ACL2 integer index and calls the writer struct-<tag>-write-<member> above.

struct-<tag>-read-<member>-all

Reader for all the elements of an array member of the structure type.
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>-all ((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>-all

Writer for all the elements of an array member of the structure type.
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>-all ((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>-all struct)) if the array member is a flexible one.

Subtopics

Defstruct-implementation: Implementation of defstruct.