|
|
|---|
|
|
|
|---|
Logical contexts in which ATC generates C expressions and statements.
As ATC visits ACL2 terms that represent C expressions and statements, and generates the C expressions and statements from the terms, along with correctness theorems for them, there is a growing logical context consisting of conditional tests and of let and mv-let bindings. We call these tests and bindings `premises', which is not ideal terminology because it is essentially synonmous of `hypotheses', which in ACL2 refers specifically to terms (conditions) and not bindings. So we use `premises' because it is not used as much in ACL2; we may find a better nomenclature in the future.
We define data types for premises, and for contexts that consist of lists of premises. We carry and augment contexts as we visit terms; we use these contexts in generated theorems.