Syntactically-clean-lambda-objects-theory
how to specify syntactic cleaning of lambda objects
The enabled status of two rewrite-lambda-modep runes are used
as flags to determine the action taken when eligible lambda objects are
encountered by the ACL2 rewriter. See rewrite-lambda-object and
rewrite-lambda-object-actions. To prevent the rewriter from diving
recursively into the body of an eligible lambda object but use a simpler
syntactic cleaning process instead, the rune (:executable-counterpart
rewrite-lambda-modep) must be enabled and the rune (:definition
rewrite-lambda-modep) must be disabled in the then-current theory. The
0-ary function syntactically-clean-lambda-objects-theory returns such a
theory.
In fact, diving into eligible quoted lambda object constants to
rewrite the body is the default action when ACL2 starts up. See rewriting-versus-cleaning-up-lambda-objects for why you might want to change
the default action when eligible lambda objects are encountered by the
rewriter.
The expression (syntactically-clean-lambda-objects-theory)
macroexpands to the theory expression
(e/d ((:executable-counterpart rewrite-lambda-modep))
((:definition rewrite-lambda-modep)))
which is a theory equal to then current theory except that the
executable-counterpart rune of rewrite-lambda-modep but the definition
rune is disabled. This expansion is suitable for use in an in-theory
event or :in-theory hint (see :hints).
Both these two runes are initally enabled, so eligible lambda object
bodies are rewritten by default until and unless some event (e.g., an in-theory or include-book) or a superior local subgoal hint changes
the status of those runes.
For example, if lambda object rewriting is active you wish to just
syntactically clean the lambda objects in Subgoal 3 of some proof,
you could use the :hints
("Subgoal 3"
:in-theory (syntactically-clean-lambda-objects-theory))
Note that if you also wish to enable or disable other runes in the same
subgoal you must construct an appropriate theory.
For example, if in Subgoal 3 of some proof you wanted to enable
LEMMA1 and disable LEMMA2 in a theory that will also specify
syntactic cleaning of lambda objects, you might write
("Subgoal 3"
:in-theory (set-difference-theories
(union-theories (syntactically-clean-lambda-objects-theory)
'(LEMMA1))
'(LEMMA2)))
Some users might prefer
("Subgoal 3"
:in-theory (e/d ((:executable-counterpart rewrite-lambda-modep)
LEMMA1)
((:definition rewrite-lambda-modep)
LEMMA2)))
See theories for general information about theories and how to
create and use them.
