Major Section: MISCELLANEOUS
Ld-redefinition-action is an
ld special (see ld). The accessor
(ld-redefinition-action state) and the updater is
(set-ld-redefinition-action val state). If
non-nil then ACL2 is liable to be made unsafe or unsound by
ill-considered definitions. The keyword command
redef will set
ld-redefinition-action to a convenient setting allowing unsound
redefinition. See below.
nil, redefinition is
prohibited. In that case, an error message is printed upon any
attempt to introduce a name that is already in use. There is one
exception to this rule. It is permitted to redefine a function
program mode to be a function symbol in
logic mode provided the formals and body remain the same.
This is the standard way a function ``comes into'' logical
Throughout the rest of this discussion we exclude from our meaning
of ``redefinition'' the case in which a function in
mode is identically redefined in
logic mode. At one time,
ACL2 freely permitted the signature-preserving redefinition of
program mode functions but it no longer does.
ld-redefinition-action is non-
nil, you are allowed to redefine
a name that is already in use. The system may be rendered unsound
by such an act. It is important to understand how dangerous
redefinition is. Suppose
fn is a function symbol that is called
from within some other function, say
fn is redefined so
that its arity changes. Then the definition of
g is rendered
syntactically ill-formed by the redefinition. This can be
devastating since the entire ACL2 system assumes that terms in its
data base are well-formed. For example, if ACL2 executes
running the corresponding function in raw Common Lisp the
fn may cause raw lisp to break in irreparable ways.
As Lisp programmers we live with this all the time by following the
simple rule: after changing the syntax of a function don't run any
function that calls it via its old syntax. This rule also works in
the context of the evaluation of ACL2 functions, but it is harder to
follow in the context of ACL2 deductions, since it is hard to know
whether the data base contains a path leading the theorem prover
from facts about one function to facts about another. Finally, of
course, even if the data base is still syntactically well-formed
there is no assurance that all the rules stored in it are valid.
For example, theorems proved about
g survive the redefinition of
but may have crucially depended on the properties of the old
summary, we repeat the warning: all bets are off if you set
ld-redefinition-action to non-
If at any point in a session you wish to see the list of all names that have been redefined, see redefined-names.
That said, we'll give you enough rope to hang yourself. When
ld-redefinition-action is non-
nil, it must be a pair,
(a . b). The
a determines how the system interacts with you when a
redefinition is submitted. The value of
b allows you to specify how
the property list of the redefined name is to be ``renewed'' before
There are several dimensions to the space of possibilities controlled by part a: Do you want to be queried each time you redefine a name, so you can confirm your intention? (We sometimes make typing mistakes or simply forget we have used that name already.) Do you want to see a warning stating that the name has been redefined? Do you want ACL2 system functions given special protection from possible redefinition? Below are the choices for part a:
In support of our own ACL2 systems programming there are two other settings. We suggest ordinary users not use them.
:query-- every attempt to redefine a name will produce a query. The query will allow you to abort the redefinition or proceed. It will will also allow you to specify the part
bfor this redefinition.
:Queryis the recommended setting for users who wish to dabble in redefinition.
:warn-- any user-defined function may be redefined but a post-redefinition warning is printed. The attempt to redefine a system name produces a query. If you are prototyping and testing a big system in ACL2 this is probably the desired setting for part
:doit-- any user-defined function may be redefined silently (without query or warning) but when an attempt is made to redefine a system function, a query is made. This setting is recommended when you start making massive changes to your prototyped system (and tire of even the warning messages issued by
:warn!-- every attempt to redefine a name produces a warning but no query. Since ACL2 system functions can be redefined this way, this setting should be used by the only-slightly-less-than supremely confident ACL2 system hacker.
:doit!-- this setting allows any name to be redefined silently (without query or warnings). ACL2 system functions are fair game. This setting is reserved for the supremely confident ACL2 system hacker. (Actually, this setting is used when we are loading massively modified versions of the ACL2 source files.)
ld-redefinition-actiontells the system how to ``renew'' the property list of the name being redefined. There are two choices:
It should be stressed that neither of these
:erase-- erase all properties stored under the name, or
:overwrite-- preserve existing properties and let the redefining overwrite them.
bsettings is guaranteed to result in an entirely satisfactory state of affairs after the redefinition. Roughly speaking,
:erasereturns the property list of the name to the state it was in when the name was first introduced. Lemmas, type information, etc., stored under that name are lost. Is that what you wanted? Sometimes it is, as when the old definition is ``completely wrong.'' But other times the old definition was ``almost right'' in the sense that some of the work done with it is still (intended to be) valid. In that case,
:overwritemight be the correct
bsetting. For example if
fnwas a function and is being re-
defun'd with the same signature, then the properties stored by the new
defunshould overwrite those stored by the old
defunbut the properties stored by
defthms will be preserved.
In addition, neither setting will cause ACL2 to erase properties
stored under other symbols! Thus, if
FOO names a rewrite rule
which rewrites a term beginning with the function symbol
you then redefine
FOO to rewrite a term beginning with the
BAZ, then the old version of
FOO is still
available (because the rule itself was added to the rewrite rules
BAR, whose property list was not cleared by redefining
b setting is only used as the default action when no query is
made. If you choose a setting for part a that produces a query then
you will have the opportunity, for each redefinition, to specify
whether the property list is to be erased or overwritten.
The keyword command
ld-redefinition-action to the pair
(:query . :overwrite). Since the resulting query will give you the
chance to specify
:erase instead of
:overwrite, this setting is
quite convenient. But when you are engaged in heavy-duty
prototyping, you may wish to use a setting such as
:warn or even
:doit. For that you will have to invoke a form such as:
(set-ld-redefinition-action '(:doit . :overwrite) state) .
Encapsulate causes somewhat odd interaction with the user if
redefinition occurs within the encapsulation because the
encapsulated event list is processed several times. For example, if
the redefinition action causes a query and a non-local definition is
actually a redefinition, then the query will be posed twice, once
during each pass. C'est la vie.
Finally, it should be stressed again that redefinition is dangerous
because not all of the rules about a name are stored on the property
list of the name. Thus, redefinition can render ill-formed terms
stored elsewhere in the data base or can preserve now-invalid