Types+vartab
Fixtype of pairs consisting of
a non-empty set of types and a variable table.
This is a product type introduced by fty::defprod.
Fields
- return-types — type-set
- variables — var-table
Additional Requirements
The following invariant is enforced on the fields:
(not (emptyp return-types))
This captures the information inferred by the static semantics
about a statement (or block item or block).
The information consists of:
- A non-empty set of types that describes
the possible values returned by the statement.
These are determined by the return statements;
in the presence of conditionals,
the possible types in the two branches are merged (i.e. unioned).
The type void is used to describe statements
that do not return a value,
but instead transfer control to the next statement (if any).
- A possibly updated variable table.
This is updated by block items that are declarations.
We actually only need to return possibly updated variable tables
from the ACL2 function check-block-item;
the ACL2 functions check-stmt and check-block-item-list
could just return a set of types (see above).
However, for uniformity we have all three functions
return also a possibly updated variable table.
Subtopics
- Types+vartab-fix
- Fixing function for types+vartab structures.
- Types+vartab-equiv
- Basic equivalence relation for types+vartab structures.
- Make-types+vartab
- Basic constructor macro for types+vartab structures.
- Types+vartab->return-types
- Get the return-types field from a types+vartab.
- Types+vartab->variables
- Get the variables field from a types+vartab.
- Change-types+vartab
- Modifying constructor for types+vartab structures.
- Types+vartab-p
- Recognizer for types+vartab structures.
