		Search-engine friendly clone of the ACL2 documentation.

Guard-holders

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 (prog2$ term1 term2) by the term term2. But (prog2$ term1 term2) is really an abbreviation for (i.e., macroexpands to) the term (return-last 'progn term1 term2); so a more accurate explanation, at the level of proper ACL2 terms, is that the call of function return-last is replaced by its last argument. ACL2 identifies certain such transformations, from a term to a trivial simplification of it, such that the input and output are provably equal. We historically have referred to the process of making such replacements as ``removing guard holders.'' (For a discussion of the connection to guards, see the ``Essay on the Removal of Guard Holders'' in the ACL2 sources.)

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 :FN (see apply$).

(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

(from-df x)                      ==>  x

(to-df 'r)                       ==>  'r ; only when r satisfies dfp

(df0)                            ==>  0

(df1)                            ==>  1

(do$ x1 x2 x3 x4 x5 'u1)         ==> (do$ x1 x2 x3 x4 x5 'nil)
                                     ; only when u1 is non-nil

; 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 (mbe :logic l :exec e) and (ec-call (f t1 ... tk)) are effectively transformed by removing guard holders into l and (f t1 ... tk), respectively.

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)