Remove trivial calls from a term
For many rule-classes, the process of converting terms to rules includes the removal of certain trivial calls from the term. Such removal is performed in some other settings as well, including hints processing, generating proof obligations for guards and termination, and the storing of induction schemes and constraints.
In all such cases, the resulting term is provably equivalent to the input
term. A common example is to replace the term
The process of removing guard-holders includes the transformations below.
That process is also applied to each argument of a function call and to the
bodies of lambda expressions (see term), usually including
quoted lambda expressions that appear in an argument position with ilk
(return-last term0 term1 term2) ==> term2 (mv-list n term) ==> term (cons-with-hint x y) ==> (cons x y) (the-check guard x y) ==> y ; For replacing a term (the type term) by term: ((lambda (y) (the-check guard x y)) val) ==> val ; For replacing equality aliases; for example, this transforms ; the macroexpansion of (member x y) to (member-equal x y): (('LAMBDA (f1 ... fk) ('RETURN-LAST ''MBE1-RAW exec logic)) a1 ... ak) ==> logic ; For other than measure theorems and induction schemes, remove lambda ; applications that are ``trivial'' in either of the following two senses. ; For replacing a term (let ((v term)) v) by term: (('LAMBDA (v) v) term) ==> term ; When each formal is equal to the corresponding actual: (('LAMBDA (f1 ... fk) body) f1 ... fk) ==> body
Because of how mbe and ec-call are defined in terms of
return-last, the expressions
The final two classes of simplification above (removal of ``trivial'' lambda applications) may be removed by executing the following form, which is local to an encapsulate form and to books.
(defattach-system remove-guard-holders-lamp constant-nil-function-arity-0)
Here is how to restore the default behavior.
(defattach-system remove-guard-holders-lamp constant-t-function-arity-0)
Note that by default, guard-holders are not removed inside calls of hide. You can however cause them to be removed inside such calls after all, as was the case through Version 8.2, as follows.
(defattach-system ; generates (local (defattach ...)) remove-guard-holders-blocked-by-hide-p constant-nil-function-arity-0)