|
|
|---|
|
|
|
|---|
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.We are extending these functions to also return correctness theorems in a bottom-up fashion. We will eventually replace the top-level theorems, which are currently very specific and brittle, with robust ones that emerge from the bottom-up generation. 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. An example is simpadd0-expr-paren, which is called by simpadd0-expr: the caller recursively transforms the inner expression, and passes to the callee the possibly transformed expression, 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.