		Search-engine friendly clone of the ACL2 documentation.

Simplify

ACL2::return-last-blockers

Functions and rules for prog2$ and other macros implemented with return-last.

Summary. The theory named return-last-blockers, in the "ACL2" package, contains ACL2::runes that can be disabled to preserve calls of certain special operators — including prog2$, mbe, time$, and others — when invoking the simplify transformation. Included are the definition runes for corresponding functions acl2::prog2$-fn, acl2::mbe-fn, acl2::time$-fn. This is all explained further below.

The ACL2 system makes use of many special macros that are implemented using an operator, return-last, that provides special behavior in the underlying Lisp implementation. These include prog2$, time$, mbe, and several others. Evaluate the form (table return-last-table) to get an idea of what they are, for example as follows (comments added).

ACL2 !>(table return-last-table)
 ((TIME$1-RAW . TIME$1) ; time$
  (WITH-PROVER-TIME-LIMIT1-RAW . WITH-PROVER-TIME-LIMIT1) ; with-prover-time-limit
  (WITH-FAST-ALIST-RAW . WITH-FAST-ALIST) ; with-fast-alist
  (WITH-STOLEN-ALIST-RAW . WITH-STOLEN-ALIST) ; with-stolen-alist
  (FAST-ALIST-FREE-ON-EXIT-RAW . FAST-ALIST-FREE-ON-EXIT) ; fast-alist-free-on-exit
  (PROGN . PROG2$) ; prog2$
  (MBE1-RAW . MBE1) ; mbe
  (EC-CALL1-RAW . EC-CALL1) ; ec-call
  (WITH-GUARD-CHECKING1-RAW . WITH-GUARD-CHECKING1)) ; with-guard-checking
ACL2 !>

For each such operator op (those in the comments just above), the "simplify" book defines a ``return-last blocker'' function, op-fn, that is obtained by adding the suffix "-FN" to its name. For example, corresponding to prog2$ is a function, prog2$-fn. Each such function is defined logically to return the second of its two arguments, and thus it agrees logically with the corresponding macro; for example, (prog2$-fn x y) is provably equal to y and hence also to (prog2$ x y).

The theory named return-last-blockers, in the "ACL2" package, contains three rules for each return-last blocker: its ACL2::definition rule, its ACL2::executable-counterpart rule, and its ACL2::type-prescription rule. These rules are all enabled by default.

Return-last is in a class of operators, ACL2::guard-holders, whose calls are typically expanded before a rule or a ``ACL2::normalized'' definition body is stored. This can be unfortunate for simplification if one intends to preserve the special behavior afforded by the operator, such as prog2$ or time$, that generated that use of return-last. The following edited log shows that by disabling blockers one can get the desired result in such cases.

ACL2 !>(defun foo (n) (time$ (reverse (make-list n))))
[[.. output elided ..]]
 FOO
ACL2 !>(simplify foo)
; Notice that the time$ call has been eliminated!
(DEFUN FOO$1 (N)
       (DECLARE (XARGS :GUARD T :VERIFY-GUARDS NIL))
       (REPEAT N NIL))
(DEFTHM FOO-BECOMES-FOO$1 (EQUAL (FOO N) (FOO$1 N)))
ACL2 !>:u ; Undo and try again, this time to preserve the time$ call.
 L         3:x(DEFUN FOO (N) ...)
ACL2 !>(simplify foo

; Disable time$-fn to preserve the time$ call.  It might be good to disabled
; associated runes (:e time$-fn) and (:t time$-fn) as well, but in this case,
; at least, that wasn't necessary.

                 :disable (time$-fn))
(DEFUN FOO$1 (N)
       (DECLARE (XARGS :GUARD T :VERIFY-GUARDS NIL))
       (TIME$ (REPEAT N NIL)))
(DEFTHM FOO-BECOMES-FOO$1 (EQUAL (FOO N) (FOO$1 N)))
ACL2 !>