Defobject-info
Fixtype of information about shallowly embedded external objects.
This is a product type introduced by fty::defprod.
Fields
- name-ident — ident
- name-symbol — symbolp
- type — type
- init — initer-option
- recognizer — symbolp
- initializer — symbolp
- call — pseudo-event-form
For each C external object defined via defobject, we store:
- The name, as an identifier.
While currently ident is just a wrapper of string,
it may include invariants in the future.
Thus, having the name stored as an identifier in the object information
will spare us from having to double-check the invariants
if we were to construct the identifier from the string.
- The name, as a symbol.
This is so we can ensure that ACL2 functions use the exact symbol
to access the external object.
The defobject table stores the name as key,
but the name is only the symbol-name,
and loses the symbol-package-name information.
- The type of the object.
Currently this must be either an integer type
or an integer array type with specified size,
but in the future this may become more general.
- An optional initializer of the object.
If present, it must match the type of the object:
if the object has integer type,
the initializer must consist of a single expression;
if the object has integer array type,
the initializer must consist of a list of expressions
of the same length as the array size.
However, these invariants are not captured in this fixtype currently.
- The name of the recognizer of the possible values of the object.
This recognizer is generated by defobject.
- The name of the initializer of the object,
i.e. the nullary function generated by defobject.
- The call of defobject,
used for redundancy checking.
Subtopics
- Defobject-info-fix
- Fixing function for defobject-info structures.
- Make-defobject-info
- Basic constructor macro for defobject-info structures.
- Defobject-info-equiv
- Basic equivalence relation for defobject-info structures.
- Defobject-infop
- Recognizer for defobject-info structures.
- Defobject-info->recognizer
- Get the recognizer field from a defobject-info.
- Defobject-info->name-symbol
- Get the name-symbol field from a defobject-info.
- Defobject-info->name-ident
- Get the name-ident field from a defobject-info.
- Defobject-info->initializer
- Get the initializer field from a defobject-info.
- Change-defobject-info
- Modifying constructor for defobject-info structures.
- Defobject-info->init
- Get the init field from a defobject-info.
- Defobject-info->call
- Get the call field from a defobject-info.
- Defobject-info->type
- Get the type field from a defobject-info.
