|
|
|---|
|
|
|
|---|
Fixtype of translation states.
This is a product type introduced by fty::defprod.
The translation between Syntheto and ACL2 is stateful. Syntheto top-level constructs are incrementally translated to ACL2. Since new top-level constructs may depend on old ones, we keep track of the Syntheto top-level constructs translated to ACL2 so far.
These are stored as deeply embedded Syntheto ASTs, ordered as a sequence according to how they are introduced. (This suggests that we may want to use the term `Syntheto events' for what we now call `Syntheto top-level constructs', and abolish the notion of Syntheto program altogether.)
The sequence is initially empty. It grows as new Syntheto top-level constructs are translated to ACL2 (these ultimately come from the Syntheto IDE). It shrinks (as ultimately directed by the Syntheto IDE) in a similar way to ACL2's undo history commands. We represent the sequence as a list in reverse chronological order, i.e. the car is the most recent top-level construct: this makes the extension of the sequence more efficient.
For now these ASTs are the only information in the translation state. We may extend the translation state to hold additional information.
We store the curent translation state in an ACL2 table with a single key. We provide operations to initialize and extend tha translation state, and to retrieve it from the table. We also provide event macros to update it in the table. We do not provide operations to shrink the translation state: this can be achieved via ACL2's undo history commands, which also retract the ACL2 events generated from the Syntheto top-level constructs stored in the translation state.