|
|
|---|
|
|
|
|---|
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 also in the process of extending these functions to also return events consisting of generated theorems (for when proof generation is on). The theorems are generated, and designed to be proved, in a bottom-up way. This is one of a few different or slightly different approaches to proof generation, which we are exploring.