Atc-implementation
Implementation of atc.
The implementation functions have arguments and results
consistently named as follows
(unless otherwise stated, explicitly or implicitly,
in the functions):
- state is the ACL2 state.
- wrld is the ACL2 world.
- ctx is the context used for errors.
- targets is the list (t1 ... tp) of inputs to atc,
or a suffix of it.
- target is an element in targets.
- target-fns is the sublist of targets
consisting of all the functions, in the same order;
or it is a suffix of this list of target functions.
- fn is one of the function symbols in targets.
- inscope is a list of alists from ACL2 variable symbols to C types.
These are the variables in scope
for the ACL2 term whose code is being generated,
organized in nested scopes from innermost to outermost.
This is like a symbol table for ACL2's representation of the C code.
- prec-fns is an alist from ACL2 function symbols to function information.
The function symbols are the ones in targets that precede,
in the latter list,
the target in targets for which C code is being generated.
- prec-tags is an alist
from ACL2 defstruct names to their associated information.
The defstructs are the ones in targets that precede,
in the latter list,
the target in targets for which C code is being generated.
The prec-tags alist is always a subset of the defstruct table
that is constructed by defstruct calls
and that is part of the ACL2 world prior to calling ATC:
the prec-tags is initially empty,
gets extended as targets that are defstruct names are processed,
and eventually contains all the defstruct table information
for the defstruct targets passed to ATC.
The reason for using the prec-tags alist this way,
instead of using the defstruct table directly,
is so that we can ensure that all the targets are supplied to ATC,
and in the right order;
furthermore, it makes it easier and more efficient
to retrieve information about all the target defstructs of interest.
- prec-objs is an alist
from ACL2 defobject names to their associated information.
The defobjects are the ones in targets that precede,
in the latter list,
the target in targets for which C code is being generated.
The prec-objs alist is always a subset of the defobject table
that is constructed by defobject calls
and that is part of the ACL2 world prior to calling ATC:
the prec-objs is initially empty,
gets extended as targets that are defobject names are processed,
and eventually contains all the defobject table information
for the defobject targets passed to ATC.
The reason for using the prec-objs alist this way,
instead of using the defobject table directly,
is so that we can ensure that all the targets are supplied to ATC,
and in the right order;
furthermore, it makes it easier and more efficient
to retrieve information about all the target defobjects of interest.
- output-dir is the homonymous input to the event macro.
- file-name is the homonymous input to the event macro.
- path-wo-ext is the path of the generated file(s),
without the .c or .h extension.
This path-wo-ext is obtained from output-dir and file-name.
- header is the homonymous input to the event macro.
- proofs is the homonymous input to the event macro.
- const-name is the homonymous input to the event macro.
- print is the homonymous input to the event macro.
- call is the call of the event macro.
- fn-appconds is an alist
from the recursive functions among t, ..., tp
to the names (keywords) of the corresponding applicability conditions.
- prog-const is the symbol specified by const-name.
This is nil if proofs is nil.
- wf-thm is the name of the generated program well-formedness theorem.
This is nil if proofs is nil.
- fn-thms is an alist from t1, ..., tp
to the names of the generated respective correctness theorems.
This is nil if proofs is nil.
- fn-guard is the name of a locally generated function
for the guard of fn.
- typed-formals is an alist
from the formal parameters of one of the functions in t1, ..., tp
to their C types.
The keys are unique and in the same order as the formal parameters.
- var-term-alist is an alist from variables to terms
that keeps track of the current substitution context
as terms are recursively processed.
This alist collects the let and mv-let bindings
encountered along the way.
These are used to properly instantiate terms
limits associated to function calls,
because those limits apply to the functions' formals,
which must therefore be replaced not just with the actuals of the call,
but with those actuals with variables replaced with terms
according to the bindings that lead to the call.
- affect is a list of symbols consisting of
the variables of array or structure type affected by
one of the functions in t1, ..., tp.
This affect is denoted as vars in the user documentation.
- context is the context in which theorems are generated
for each generated piece of C code.
- thm-index is a positive integer
that is threaded through the code generation functions
to generate unique and readable local theorem names.
- compst-var is a symbol used as a variable for
the computation state in generated theorems.
- fenv-var is a symbol used as a variable for
the function environment in generated theorems.
- limit-var is a symbol used as a variable for
the execution recursion limit in generated theorems.
- names-to-avoid is a cumulative list of names of generated events,
used to ensure the absence of name clashes in the generated events.
Implementation functions' arguments and results
that are not listed above
are described in, or clear from,
those functions' documentation.
Subtopics
- Atc-abstract-syntax
- Abstract syntax of C for ATC.
- Atc-pretty-printer
- A pretty-printer of C abstract syntax for ATC.
- Atc-event-and-code-generation
- Event generation and code generation performed by atc.
- Fty-pseudo-term-utilities
- FTY utilities for pseudo-terms.
- Atc-term-recognizers
- Recognizers of ACL2 terms for ATC.
- Atc-input-processing
- Input processing performed by atc.
- Atc-shallow-embedding
- Shallow embedding of C in ACL2 for ATC.
- Atc-process-inputs-and-gen-everything
- Process the inputs and generate the events and code.
- Atc-table
- Table of atc calls.
- Atc-fn
- Event expansion of atc.
- Atc-pretty-printing-options
- Options for the ATC pretty-printer.
- Atc-types
- C types for ATC.
- Atc-macro-definition
- Definition of the atc macro.
