Dynamic-struct-environments
Dynamic environments for struct types in Leo.
In Leo, struct types are referenced by name.
Thus, the dynamic semantics of Leo constructs
that reference struct types by name
must be defined with respect to information for the struct type names.
We capture that via the notion of dynamic environment for struct types,
which associates dynamic information for struct types
to struct type names.
Subtopics
- Struct-dinfo-option
- Fixtype of optional dynamic information for struct types.
- Add-struct-dinfo
- Add information for a struct type to a dynamic environment.
- Struct-dinfo
- Fixtype of dynamic information about struct types.
- Struct-denv-option
- Fixtype of optional dynamic environments for struct types.
- Get-struct-dinfo
- Get the information for a struct type in a dynamic environment.
- Struct-denv
- Fixtype of dynamic environments for struct types.
- Init-struct-denv
- Initial dynamic struct environment.
