		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) are handled by a separate function.

Constants and string literals undergo no transformation. No theorems are generated for them, since there is no change.

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, we parenthesize the transformed inner expression, and we return that. We generate a theorem if the two inner expressions differ (in which case the parenthesized expressions differ as well) and a theorem for the inner expressions' transformation was generated (which we can tell based on whether there is a theorem name for the inner expressions). Since c$::ldm-expr maps parenthesized expressions to the same as what the inner expressions are mapped to, the proof of the generated theorem is straightforward, but we supply the executable counterpart of c$::ldm-expr so that they can be applied to the parenthesized expressions.

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.