Gout
General outputs for transformation functions.
This is a product type introduced by fty::defprod.
Fields
- events — pseudo-event-form-list
- Theorems generated so far, in reverse order.
- thm-index — posp
- Index used to generate unique theorem names.
- thm-name — symbolp
- Name of the theorem generated by the transformation function.
The theorem concerns the transformation of the C construct
that the transformation function operates on.
This is nil if no theorem is generated.
- vartys — c::ident-type-map
- Some variables in scope at the end of the construct.
The generated theorem (if any)
includes conclusions about their presence in the computation state
after the execution of the construct.
This does not necessarily include all the variables in scope,
because for certain constructs (e.g. lists of block items)
we only consider variables that are also in scope
at the beginning of the construct, i.e. that occur in
the vartys component of gin.
The transformation functions return as output the transformed construct,
which has a different type for each transformation function.
But each function also returns certain common outputs,
which we put into this data structure
for modularity and to facilitate extension.
Subtopics
- Goutp
- Recognizer for gout structures.
- Gout-fix
- Fixing function for gout structures.
- Make-gout
- Basic constructor macro for gout structures.
- Gout-equiv
- Basic equivalence relation for gout structures.
- Change-gout
- Modifying constructor for gout structures.
- Gout->vartys
- Get the vartys field from a gout.
- Gout->thm-name
- Get the thm-name field from a gout.
- Gout->thm-index
- Get the thm-index field from a gout.
- Gout->events
- Get the events field from a gout.
