		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Stmt-gin

Inputs for C statement generation.

This is a product type introduced by fty::defprod.

Fields

context — atc-context: Described in atc-implementation. It is the context just before this statement, i.e. the context in which this statement is generated.
var-term-alist — symbol-pseudoterm-alist: Described in atc-implementation.
typed-formals — atc-symbol-varinfo-alist: Described in atc-implementation.
inscope — atc-symbol-varinfo-alist-list: Described in atc-implementation. It contains the variables in scope just before this statement, i.e. the ones in scope for this statement.
loop-flag — booleanp: The L flag described in the user documentation.
affect — symbol-list: Described in atc-implementation.
fn — symbolp: Described in atc-implementation. It is the target function for which the statement is generated.
fn-guard — symbolp: Described in atc-implementation.
compst-var — symbolp: Described in atc-implementation.
fenv-var — symbolp: Described in atc-implementation.
limit-var — symbolp: Described in atc-implementation.
prec-fns — atc-symbol-fninfo-alist: Described in atc-implementation.
prec-tags — atc-string-taginfo-alist: Described in atc-implementation.
prec-objs — atc-string-objinfo-alist: Described in atc-implementation.
thm-index — posp: Described in atc-implementation.
names-to-avoid — symbol-list: Described in atc-implementation.
proofs — booleanp: A flag indicating whether modular proof generation should continue or not. This will be eliminated when modular proof generation will cover all of the ATC-generated code.

This does not include the term, which is passed as a separate input.

Subtopics

Stmt-ginp: Recognizer for stmt-gin structures.
Make-stmt-gin: Basic constructor macro for stmt-gin structures.
Stmt-gin-fix: Fixing function for stmt-gin structures.
Stmt-gin-equiv: Basic equivalence relation for stmt-gin structures.
Change-stmt-gin: Modifying constructor for stmt-gin structures.
Stmt-gin->var-term-alist: Get the var-term-alist field from a stmt-gin.
Stmt-gin->typed-formals: Get the typed-formals field from a stmt-gin.
Stmt-gin->names-to-avoid: Get the names-to-avoid field from a stmt-gin.
Stmt-gin->prec-tags: Get the prec-tags field from a stmt-gin.
Stmt-gin->prec-objs: Get the prec-objs field from a stmt-gin.
Stmt-gin->prec-fns: Get the prec-fns field from a stmt-gin.
Stmt-gin->inscope: Get the inscope field from a stmt-gin.
Stmt-gin->thm-index: Get the thm-index field from a stmt-gin.
Stmt-gin->loop-flag: Get the loop-flag field from a stmt-gin.
Stmt-gin->limit-var: Get the limit-var field from a stmt-gin.
Stmt-gin->fn-guard: Get the fn-guard field from a stmt-gin.
Stmt-gin->fenv-var: Get the fenv-var field from a stmt-gin.
Stmt-gin->context: Get the context field from a stmt-gin.
Stmt-gin->compst-var: Get the compst-var field from a stmt-gin.
Stmt-gin->affect: Get the affect field from a stmt-gin.
Stmt-gin->proofs: Get the proofs field from a stmt-gin.
Stmt-gin->fn: Get the fn field from a stmt-gin.