Event generation and code generation performed by `atc`.

We generate C abstract syntax, which we pretty-print to a file and also assign to a named constant.

Given the restrictions on the target functions, the translation is relatively straightforward, by design.

Some events are generated in two slightly different variants:
one that is local to the generated `encapsulate`,
and one that is exported from the `encapsulate`.
Proof hints are in the former but not in the latter,
thus keeping the ACL2 history ``clean'';
some proof hints may refer to events
that are generated only locally to the `encapsulate`.

Some code and event generation functions
group some of their inputs and some of their outputs
into `fty::defprod` values,
to make the code more readable and more easily extensible,
at a performance cost that should be unimportant.
These product fixtypes have names

proofs is a flag that is threaded through and that is used to determine and to indicate whether modular proofs are generated or not. We are incrementally developing a new approch to proof generation that generates compositional and more efficient theorems as each ACL2 construct is translated to the corresponding C construct. Not all constructs are currently covered: as soon as a non-covered construct is encountered, we stop generating modular theorems and we set the flag; prior to attempting to generate a modular theorem, the flag is checked, and modular theorem generation is skipped, even if the current construct is covered, but the reason is that previous constructs were not covered, and thus we cannot reliably generate a modular proof for a construct when we don't have modular proofs for the sub-constructs. Eventually we will eliminate this flag, once modular proof generation covers all the constructs.

Other components are described where the types are defined.

- Atc-symbolic-computation-states
- Canonical representation of the computation states for the symbolic execution.
- Atc-symbolic-execution-rules
- Symbolic execution rules for ATC.
- Atc-gen-ext-declon-lists
- Generate two lists of C external declarations from the targets, including generating C loops from recursive ACL2 functions.
- Atc-function-and-loop-generation
- Generation of C functions and loops.
- Atc-statement-generation
- Generation of C statements.
- Atc-gen-fileset
- Generate a file set from the ATC targets, and accompanying events.
- Atc-gen-everything
- Generate the file and the events.
- Atc-gen-obj-declon
- Generate a C external object declaration.
- Atc-gen-fileset-event
- Event to pretty-print the generated C code to the file system.
- Atc-tag-tables
- Tables of
`defstruct`s, and operations on these tables. - Atc-expression-generation
- Generation of C expressions.
- Atc-generation-contexts
- Logical contexts in which ATC generates C expressions and statements.
- Atc-gen-wf-thm
- Generate the theorem asserting the static well-formedness of the generated C code (referenced as the named constant).
- Term-checkers-atc
- Checkers of ACL2 terms that represent C constructs, used by ATC.
- Atc-variable-tables
- Tables of ACL2 variables, and operations on these tables.
- Term-checkers-common
- Checkers of ACL2 terms that represent C constructs,
common to ATC and
`defobject`. - Atc-gen-init-fun-env-thm
- Generate the theorem asserting that
applying
`init-fun-env`to the translation unit gives the corresponding function environment. - Atc-gen-appconds
- Generate the applicability conditions.
- Read-write-variables
- Functions to read and write variables.
- Atc-gen-thm-assert-events
- Generate assertion events to double-check that all the correctness theorems were generated.
- Test*
- Wrapper for contextual tests.
- Atc-gen-prog-const
- Generate the named constant for the abstract syntax tree of the generated C code (i.e. C file set).
- Atc-gen-expr-bool
- Generate a C expression from an ACL2 term that must be an expression term returning a boolean.
- Atc-theorem-generation
- Facilities for generating theorems in ATC.
- Atc-tag-generation
- Generation of C tag declarations (currently just structures).
- Atc-gen-expr-pure
- Generate a C expression from an ACL2 term that must be a pure expression term.
- Atc-function-tables
- Tables of ACL2 functions, and operations on these tables.
- Atc-object-tables
- Tables of
`defobject`s, and operations on these tables.