For each C structure type defined via defstruct, we store:
The tag, as an identifier.
While currently ident is just a wrapper of string,
it may include invariants in the future.
Thus, having the tag stored as an identifier in the structure information
will spare us from having to double-check the invariants
if we were to construct the identifier from the string.
A flag saying whether the structure type has a flexible array member.
The fixtype of the structures.
The recognizer of the structures.
The fixer of the structures.
The name of the theorem that rewrites away the fixer
when the recognizer holds.
The name of a theorem asserting that
if something is a structure of this type
then it is not an error.
The name of the theorem asserting that
the recognizer implies valuep.
The name of the theorem asserting that
the recognizer implies that value-kind is :struct.
The name of the theorem asserting that
the recognizer implies that type-of-value
returns the struct type, expressed as a term (type-struct ...).
The name of the theorem asserting the value of
the flexible array member flag.
The name of the theorem asserting the equality of
(type-struct <tag>)
to its quoted value,
where <tag> is the tag of this structure type.
The name of the theorem asserting the equality of
(type-pointer (type-struct <tag>))
to its quoted value,
where <tag> is the tag of this structure type.
The call of defstruct.
This supports redundancy checking.
