		Search-engine friendly clone of the ACL2 documentation.

History

Undo

Undoing and perhaps redefining

This topic provides a high-level view of how one can undo a definition, perhaps replacing it with a new definition. We begin with some background.

ACL2 maintains a stack of commands. For example, suppose we submit the following events in a new session.

(defun f (x) x)
(defun g (x) (* x x))
(defthm f^2-is-g
  (equal (expt (f x) 2) (g x))
  :hints (("Goal" :expand ((expt x 2)))))

Then we can see the stack of commands by using :pcb (``Print Command Block'') back to command 0, that is back to the start.

ACL2 !>:pbt 0
           0  (EXIT-BOOT-STRAP-MODE)
 L         1  (DEFUN F (X) ...)
 L         2  (DEFUN G (X) ...)
           3:x(DEFTHM F^2-IS-G ...)
ACL2 !>

Now suppose that we want to redefine g. The cleanest, safest way is to unwind the stack with :ubt (``Undo Back Through'') all the way back through (and including) g.

ACL2 !>:ubt g
 L         1:x(DEFUN F (X) ...)
ACL2 !>:pbt 0
           0  (EXIT-BOOT-STRAP-MODE)
 L         1:x(DEFUN F (X) ...)
ACL2 !>

Now we can define g again and proceed from there.

ACL2 !>(defun g (x) (expt x 2))
[[.. output omitted here ..]]
 G
ACL2 !>:pbt 0
           0  (EXIT-BOOT-STRAP-MODE)
 L         1  (DEFUN F (X) ...)
 L         2:x(DEFUN G (X) ...)
ACL2 !>(defthm f^2-is-g
         (equal (expt (f x) 2) (g x)))
[[.. output omitted here ..]]
 F^2-IS-G
ACL2 !>:pbt 0
           0  (EXIT-BOOT-STRAP-MODE)
 L         1  (DEFUN F (X) ...)
 L         2  (DEFUN G (X) ...)
           3:x(DEFTHM F^2-IS-G ...)
ACL2 !>

See ubt for more information, including variants such as :u, which undoes a single command (the most recent one). Also see oops for how to undo an undo.

It can occasionally be inconvenient to undo a large number of commands when one's goal is only to redefine a single function. In such cases one might wish to enable redefinition, even though it can be unsafe. Here is an example (admittedly contrived) for how to continue the session above. Note that there are variants of :redef — see redef — for example to avoid the query shown below and answered with `y'.

ACL2 !>:redef
 (:QUERY . :OVERWRITE)
ACL2 !>(defun f (x) (+ 10 x))

ACL2 Query (:REDEF):  The name F is in use as a function.  Its current
defun-mode is :logic. Do you want to redefine it?  (N, Y, E, O or ?):
y

Since F is non-recursive, its admission is trivial.  We observe that
the type of F is described by the theorem (ACL2-NUMBERP (F X)).  We
used primitive type reasoning.

Summary
Form:  ( DEFUN F ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 F
ACL2 !>:pbt 0
           0  (EXIT-BOOT-STRAP-MODE)
 L         1  (DEFUN F (X) ...)
 L         2  (DEFUN G (X) ...)
           3  (DEFTHM F^2-IS-G ...)
 L         4:x(DEFUN F (X) ...)
ACL2 !>

Notice that the ``theorem'' f^2-is-g is still in our session, even though it is no longer valid now that f has been redefined. This shows one reason we say that redefinition can be unsafe; it can be unsound! Other possible dangers include execution errors and ignoring, in existing definitions, redefinitions of constants and macros. Thus, undoing (and then redoing) is generally preferable to redefinition. Indeed, redefinition is disallowed in books.

You can inspect both commands that introduce a definition for f with :pcb (``Print Command Block'' in full; see pcb).

ACL2 !>:pcb! 1
 L         1  (DEFUN F (X) X)
ACL2 !>:pcb! 3
 L         3:x(DEFUN F (X) (CAR (CONS X X)))
ACL2 !>

Subtopics

Ubt: Undo the commands back through a command descriptor
Ubu: Undo the commands back up to (not including) a command descriptor
Ubt!: Undo commands, without a query or an error
U: Undo last command, without a query
Ubu!: Undo commands, without a query or an error
Ubu?: Undo commands, with queries as appropriate
Ubt?: Undo commands, with queries as appropriate
Ubt-prehistory: Undo the commands back through the last reset-prehistory event