		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-expr

Transform an expression.

Signature
(simpadd0-expr expr gin state) → (mv new-expr gout)
Arguments: expr — Guard (exprp expr).; gin — Guard (simpadd0-ginp gin).
Returns: new-expr — Type (exprp new-expr).; gout — Type (simpadd0-goutp gout).

Variables (i.e. identifier expressions) and constants are handled by separate functions.

String literals undergo no transformation. No theorems are generated for them, since our formal dynamic semantics does not cover them yet.

When we encounter constructs unsupported in the formal dynamic semnatics, we do not generate a theorem. Currently we also do not generate a theorem also for supported constructs for which we have not implemented theorem generation yet: we are in the process of extending the implementation.

When we encounter a parenthesized expression, we recursively transform the inner expression, and then we use a separate function to do the rest.

When we encounter an expression x + 0 that we transform into x, we also generate a theorem saying that executing the two expressions give equivalent results. This is proved by essentially just instantiating simpadd0-supporting-lemma (see its documentation, also in regard to the exact way in which we express the equivalence). This is a very preliminary theorem generation capability, which we plan to extend soon.