Gin
General inputs for transformation functions.
This is a product type introduced by fty::defprod.
Fields
- ienv — ienv
- The implementation environment from the code ensemble.
- const-new — symbolp
- The :const-new input of the transformation.
- vartys — c::ident-type-map
- Some variables in scope at the beginning of the construct.
The generated theorem (if any)
includes hypotheses about their presence in the computation state
before the execution of the C construct.
Currently this could be actually a subset of the variables in scope,
but it is adequate to the current proof generation,
and we are working on extending this.
- events — pseudo-event-form-list
- Theorems generated so far, in reverse order.
- thm-index — posp
- Index used to generate unique theorem names.
The transformation functions take as input the construct to transform,
which has a different type for each transformation function.
But each function also takes certain common inputs,
which we put into this data structure
for modularity and to facilitate extension.
Subtopics
- Ginp
- Recognizer for gin structures.
- Gin-fix
- Fixing function for gin structures.
- Make-gin
- Basic constructor macro for gin structures.
- Gin-equiv
- Basic equivalence relation for gin structures.
- Change-gin
- Modifying constructor for gin structures.
- Gin->vartys
- Get the vartys field from a gin.
- Gin->events
- Get the events field from a gin.
- Gin->const-new
- Get the const-new field from a gin.
- Gin->thm-index
- Get the thm-index field from a gin.
- Gin->ienv
- Get the ienv field from a gin.
