|
|
|---|
|
|
|
|---|
Remove the trivial lambda-bound variables.
(remove-trivial-vars term) → new-term
ACL2 lambda expressions in translated terms are always closed,
which means that they often include formal parameters
that are replaced by themselves (i.e. by the same symbols)
when the lambda expression is applied.
For instance, the untranslated term
This function removes the formal parameters of lambda expressions
that are ``trivial'' in the sense that
they are replaced by identical actual parameters.
These are ``artificial'' variables,
not let variables.
We also remove the corresponding actual parameters, of course,
so that beta reduction still makes sense,
and the number of actual parameters still matches
the number of formal parameters.
Applying this function to the example above yields
If all the formal parameters are trivial, we replace the lambda expression with its body. A lambda expression with all trivial formal parameters may not result from hand-written code, but could result from generated code.
We obtain terms whose lambda expressions may not be closed. These do not satisfy termp, but they still satisfy pseudo-termp. Furthermore, it is easy to close any open lambda expressions, by adding formal parameters, and corresponding actual parameters, for the free variables in the lambda expression.
For certain term transformations, it may be more convenient to work with the possibly open lamba expressions produced by this function. This way, every lambda expression corresponds to a let without any trivial bindings. In other languages, let expressions are normally not closed.
Theorem:
(defthm return-type-of-remove-trivial-vars.new-term (implies (pseudo-termp term) (b* ((?new-term (remove-trivial-vars term))) (pseudo-termp new-term))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-remove-trivial-vars-lst.new-terms (implies (pseudo-term-listp terms) (b* ((?new-terms (remove-trivial-vars-lst terms))) (and (pseudo-term-listp new-terms) (equal (len new-terms) (len terms))))) :rule-classes :rewrite)