|
|
|---|
|
|
|
|---|
Implementation of simpadd0.
The implementation functions have arguments and results consistently named as follows (unless otherwise stated, explicitly or implicitly, in the functions):
Implementation functions' arguments and results that are not listed above are described in, or clear from, those functions' documentation.
This transformation is implemented as a collection of ACL2 functions that operate on the abstract syntax, following the recursive structure of the abstract syntax. This is a typical pattern for C-to-C transformations, which we may want to partially automate, via things like generalized `folds' over the abstract syntax.These functions also return correctness theorems in a bottom-up fashion, for a growing subset of constructs currently supported. This is one of a few different or slightly different approaches to proof generation, which we are exploring.For a growing number of constructs, we have ACL2 functions that do most of the transformation of the construct, including theorem generation when applicable, and these ACL2 function are outside the large mutual recursion. The recursive functions recursively transform the sub-constructs, and then call the separate non-recursive functions with the results from transforming the sub-constructs. A simple example is simpadd0-expr-paren, which is called by simpadd0-expr: the caller recursively transforms the inner expression, and passes the possibly transformed expression to the callee, along with some of the simpadd0-gout components resulting from that transformation; it also passes a simpadd0-gin whose components have been updated from the aforementioned simpadd0-gout.The generated theorems involve hypotheses about variables in scope having values of appropriate types, captured as ACL2 values of type ident-type-map. Our initial approach has been to take the variables from the constructs, joining the ones for sub-constructs via simpadd0-join-vartys to obtain the ones for super-constructs. This is adequate for some of the constructs, but we need to generalize this approach for other constructs. Specifically, we are moving towards having information about the variables in scope in the AST validation annotations, and using that instead of calculating the information from the constructs. As we move towards the new approach, we may have a mix of the new and old appraoches.