Ld-redefinition-action
To allow redefinition without undoing
The present topic discusses redefining functions, macros, and
constants, using a mechanism that may be convenient but also may be unsafe or
unsound. See undo for what is often a better way to carry out
redefinition.
Ld-redefinition-action is an ld special (see ld). The
accessor is (ld-redefinition-action state) and the updater is
(set-ld-redefinition-action val state).
WARNING! If ld-redefinition-action is non-nil then ACL2 is
liable to be made unsafe or unsound, or behave in unexpected ways. For
example, redefining a macro or inlined function, f, that is called in the
body of another function, g, may not cause the new version of f to
be called by g. In addition, for some Lisps, in particular GCL Version
2.7.0 or later, the return type TP inferred for the original definition
of f might cause mishandling of the return value from f as g
still expects that value's type to be TP. Redefinition should be viewed
as a way to facilitate unsafe, but potentially useful, hacking.
The keyword command :redef will set
ld-redefinition-action to a convenient setting allowing unsound
redefinition. See below.
When ld-redefinition-action is 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 symbol in :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
existence.
Throughout the rest of this discussion we exclude from our meaning of
``redefinition'' the case in which a function in :program 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. See redefining-programs.
When 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 g. Suppose 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 database are well-formed. For example, if
ACL2 executes g by running the corresponding function in raw Common Lisp
the redefinition of 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 database contains a path
leading the theorem prover from facts about one function to facts about
another. Finally, of course, even if the database 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 fn
but may have crucially depended on the properties of the old fn. In
summary, we repeat the warning: all bets are off if you set
ld-redefinition-action to non-nil.
ACL2 provides some enforcement of the concern above, by disabling certify-book if any world-changing events exist in the
certification world that were executed with a non-nil value of
'ld-redefinition-action. (This value is checked at the end of each
top-level command, but the value does not change during evaluation of embedded
event forms; see embedded-event-form.)
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 value of 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 the
redefinition.
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:
: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 b for this redefinition. :Query
is 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 a.
: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).
In support of our own ACL2 systems programming there are two other
settings. We suggest ordinary users not use them.
: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.)
Part b of ld-redefinition-action tells the system how to
``renew'' the property list of the name being redefined. There are two
choices:
:erase — erase all properties stored under the name, or
:overwrite — preserve existing properties and let the redefining
overwrite them.
It should be stressed that neither of these b settings is guaranteed
to result in an entirely satisfactory state of affairs after the redefinition.
Roughly speaking, :erase returns 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, :overwrite might
be the correct b setting. For example if fn was a function and is
being re-defun'd with the same signature, then the properties
stored by the new defun should overwrite those stored by the old
defun but 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 BAR and you then redefine
FOO to rewrite a term beginning with the function symbol BAZ, then
the old version of FOO is still available (because the rule itself was
added to the rewrite rules for BAR, whose property list was not cleared
by redefining FOO).
The 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 :redef sets 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
database or can preserve now-invalid rules. See redundant-events, in
particular the section ``Note About Unfortunate Redundancies,'' for more
discussion of potential pitfalls of redefinition.
