← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to doc/HTML/LD-REDEFINITION-ACTION.html

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/HTML/LD-REDEFINITION-ACTION.html
1
1
<html>
2
 
<head><title>LD-REDEFINITION-ACTION.html  --  ACL2 Version 3.0.1</title></head>
 
2
<head><title>LD-REDEFINITION-ACTION.html  --  ACL2 Version 3.1</title></head>
3
3
<body text=#000000 bgcolor="#FFFFFF">
4
4
<h2>LD-REDEFINITION-ACTION</h2>to allow redefinition without undoing
5
5
<pre>Major Section:  <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
6
6
</pre><p>
7
7
 
8
 
<code>Ld-redefinition-action</code> is an <code><a href="LD.html">ld</a></code> special (see <a href="LD.html">ld</a>).  The accessor
9
 
is <code>(ld-redefinition-action state)</code> and the updater is
10
 
<code>(set-ld-redefinition-action val state)</code>.  <strong>If</strong> <code>ld-redefinition-action</code>
11
 
<strong>is</strong> <code>non-nil</code> <strong>then ACL2 is liable to be made unsafe or unsound by</strong>
12
 
<strong>ill-considered definitions</strong>.  The keyword command <code>:</code><code><a href="REDEF.html">redef</a></code> will set
13
 
<code>ld-redefinition-action</code> to a convenient setting allowing unsound
14
 
redefinition.  See below.
 
8
<code>Ld-redefinition-action</code> is an <code><a href="LD.html">ld</a></code> special (see <a href="LD.html">ld</a>).  The accessor is
 
9
<code>(ld-redefinition-action state)</code> and the updater is
 
10
<code>(set-ld-redefinition-action val state)</code>.<p>
 
11
 
 
12
<strong>WARNING!</strong>  If <code>ld-redefinition-action</code> is non-<code>nil</code> then ACL2 is
 
13
liable to be made unsafe or unsound by ill-considered definitions.  The
 
14
keyword command <code>:</code><code><a href="REDEF.html">redef</a></code> will set <code>ld-redefinition-action</code> to a
 
15
convenient setting allowing unsound redefinition.  See below.
15
16
<p>
16
 
When <code>ld-redefinition-action</code> is <code>nil</code>, redefinition is
17
 
prohibited.  In that case, an error message is printed upon any
18
 
attempt to introduce a name that is already in use.  There is one
19
 
exception to this rule.  It is permitted to redefine a function
20
 
symbol in <code>:</code><code><a href="PROGRAM.html">program</a></code> mode to be a function symbol in
21
 
<code>:</code><code><a href="LOGIC.html">logic</a></code> mode provided the formals and body remain the same.
22
 
This is the standard way a function ``comes into'' logical
 
17
When <code>ld-redefinition-action</code> is <code>nil</code>, redefinition is prohibited.  In
 
18
that case, an error message is printed upon any attempt to introduce a name
 
19
that is already in use.  There is one exception to this rule.  It is
 
20
permitted to redefine a function symbol in <code>:</code><code><a href="PROGRAM.html">program</a></code> mode to be a
 
21
function symbol in <code>:</code><code><a href="LOGIC.html">logic</a></code> mode provided the formals and body remain
 
22
the same.  This is the standard way a function ``comes into'' logical
23
23
existence.<p>
24
24
 
25
 
Throughout the rest of this discussion we exclude from our meaning
26
 
of ``redefinition'' the case in which a function in <code>:</code><code><a href="PROGRAM.html">program</a></code>
27
 
mode is identically redefined in <code>:</code><code><a href="LOGIC.html">logic</a></code> mode.  At one time,
28
 
ACL2 freely permitted the <a href="SIGNATURE.html">signature</a>-preserving redefinition of
29
 
<code>:</code><code><a href="PROGRAM.html">program</a></code> mode functions but it no longer does.
30
 
See <a href="REDEFINING-PROGRAMS.html">redefining-programs</a>.<p>
 
25
Throughout the rest of this discussion we exclude from our meaning of
 
26
``redefinition'' the case in which a function in <code>:</code><code><a href="PROGRAM.html">program</a></code> mode is
 
27
identically redefined in <code>:</code><code><a href="LOGIC.html">logic</a></code> mode.  At one time, ACL2 freely
 
28
permitted the <a href="SIGNATURE.html">signature</a>-preserving redefinition of <code>:</code><code><a href="PROGRAM.html">program</a></code>
 
29
mode functions but it no longer does.  See <a href="REDEFINING-PROGRAMS.html">redefining-programs</a>.<p>
31
30
 
32
 
When <code>ld-redefinition-action</code> is non-<code>nil</code>, you are allowed to redefine
33
 
a name that is already in use.  <strong>The system may be rendered unsound</strong>
34
 
by such an act.  It is important to understand how dangerous
35
 
redefinition is.  Suppose <code>fn</code> is a function symbol that is called
36
 
from within some other function, say <code>g</code>.  Suppose <code>fn</code> is redefined so
37
 
that its arity changes.  Then the definition of <code>g</code> is rendered
38
 
syntactically ill-formed by the redefinition.  This can be
39
 
devastating since the entire ACL2 system assumes that terms in its
40
 
data base are well-formed.  For example, if ACL2 executes <code>g</code> by
41
 
running the corresponding function in raw Common Lisp the
42
 
redefinition of <code>fn</code> may cause raw lisp to break in irreparable ways.
43
 
As Lisp programmers we live with this all the time by following the
44
 
simple rule: after changing the syntax of a function don't run any
45
 
function that calls it via its old syntax.  This rule also works in
46
 
the context of the evaluation of ACL2 functions, but it is harder to
47
 
follow in the context of ACL2 deductions, since it is hard to know
48
 
whether the data base contains a path leading the theorem prover
49
 
from facts about one function to facts about another.  Finally, of
50
 
course, even if the data base is still syntactically well-formed
51
 
there is no assurance that all the rules stored in it are valid.
52
 
For example, theorems proved about <code>g</code> survive the redefinition of <code>fn</code>
53
 
but may have crucially depended on the properties of the old <code>fn</code>.  In
54
 
summary, we repeat the warning: <strong>all bets are off if you set</strong>
 
31
When <code>ld-redefinition-action</code> is non-<code>nil</code>, you are allowed to redefine a
 
32
name that is already in use.  <strong>The system may be rendered unsound</strong> by such
 
33
an act.  It is important to understand how dangerous redefinition is.
 
34
Suppose <code>fn</code> is a function symbol that is called from within some other
 
35
function, say <code>g</code>.  Suppose <code>fn</code> is redefined so that its arity changes.
 
36
Then the definition of <code>g</code> is rendered syntactically ill-formed by the
 
37
redefinition.  This can be devastating since the entire ACL2 system assumes
 
38
that terms in its data base are well-formed.  For example, if ACL2 executes
 
39
<code>g</code> by running the corresponding function in raw Common Lisp the
 
40
redefinition of <code>fn</code> may cause raw lisp to break in irreparable ways.  As
 
41
Lisp programmers we live with this all the time by following the simple rule:
 
42
after changing the syntax of a function don't run any function that calls it
 
43
via its old syntax.  This rule also works in the context of the evaluation of
 
44
ACL2 functions, but it is harder to follow in the context of ACL2 deductions,
 
45
since it is hard to know whether the data base contains a path leading the
 
46
theorem prover from facts about one function to facts about another.
 
47
Finally, of course, even if the data base is still syntactically well-formed
 
48
there is no assurance that all the rules stored in it are valid.  For
 
49
example, theorems proved about <code>g</code> survive the redefinition of <code>fn</code> but
 
50
may have crucially depended on the properties of the old <code>fn</code>.  In summary,
 
51
we repeat the warning: <strong>all bets are off if you set</strong>
55
52
<code>ld-redefinition-action</code> to <strong>non</strong>-<code>nil</code>.<p>
56
53
 
57
 
If at any point in a session you wish to see the list of all names
58
 
that have been redefined, see <a href="REDEFINED-NAMES.html">redefined-names</a>.<p>
 
54
ACL2 provides some enforcement of the concern above, by disabling
 
55
<code><a href="CERTIFY-BOOK.html">certify-book</a></code> if any <a href="WORLD.html">world</a>-changing <a href="EVENTS.html">events</a> exist in the
 
56
certification <a href="WORLD.html">world</a> that were executed with a non-<code>nil</code> value of
 
57
<code>'ld-redefinition-action</code>.  (This value is checked at the end of each
 
58
top-level command, but the value does not change during evaluation of
 
59
embedded event forms; see <a href="EMBEDDED-EVENT-FORM.html">embedded-event-form</a>.)<p>
 
60
 
 
61
If at any point in a session you wish to see the list of all names that have
 
62
been redefined, see <a href="REDEFINED-NAMES.html">redefined-names</a>.<p>
59
63
 
60
64
That said, we'll give you enough rope to hang yourself.  When
61
 
<code>ld-redefinition-action</code> is non-<code>nil</code>, it must be a pair, <code>(a .  b)</code>.  The
62
 
value of <code>a</code> determines how the system interacts with you when a
63
 
redefinition is submitted.  The value of <code>b</code> allows you to specify how
64
 
the property list of the redefined name is to be ``renewed'' before
65
 
the redefinition.<p>
66
 
 
67
 
There are several dimensions to the space of possibilities controlled by
68
 
part a: Do you want to be queried each time you redefine a name, so you
69
 
can confirm your intention?  (We sometimes make typing mistakes or simply
70
 
forget we have used that name already.)  Do you want to see a warning
71
 
stating that the name has been redefined?  Do you want ACL2 system
72
 
functions given special protection from possible redefinition?  Below are
73
 
the choices for part a:
74
 
<blockquote><p>
75
 
 
76
 
<code>:query</code> -- every attempt to redefine a name will produce a query.
77
 
The query will allow you to abort the redefinition or proceed.  It will
78
 
will also allow you to specify the part <code>b</code> for this redefinition.
79
 
<code>:Query</code> is the recommended setting for users who wish to dabble in
 
65
<code>ld-redefinition-action</code> is non-<code>nil</code>, it must be a pair, <code>(a .  b)</code>.
 
66
The value of <code>a</code> determines how the system interacts with you when a
 
67
redefinition is submitted.  The value of <code>b</code> allows you to specify how the
 
68
property list of the redefined name is to be ``renewed'' before the
80
69
redefinition.<p>
81
70
 
 
71
There are several dimensions to the space of possibilities controlled by part
 
72
a: Do you want to be queried each time you redefine a name, so you can
 
73
confirm your intention?  (We sometimes make typing mistakes or simply forget
 
74
we have used that name already.)  Do you want to see a warning stating that
 
75
the name has been redefined?  Do you want ACL2 system functions given special
 
76
protection from possible redefinition?  Below are the choices for part
 
77
a:
 
78
<blockquote><p>
 
79
 
 
80
<code>:query</code> -- every attempt to redefine a name will produce a query.  The
 
81
query will allow you to abort the redefinition or proceed.  It will will also
 
82
allow you to specify the part <code>b</code> for this redefinition.  <code>:Query</code> is the
 
83
recommended setting for users who wish to dabble in redefinition.<p>
 
84
 
82
85
<code>:warn</code> -- any user-defined function may be redefined but a
83
 
post-redefinition warning is printed.  The attempt to redefine a
84
 
system name produces a query.  If you are prototyping and testing a
85
 
big system in ACL2 this is probably the desired setting for part <code>a</code>.<p>
 
86
post-redefinition warning is printed.  The attempt to redefine a system name
 
87
produces a query.  If you are prototyping and testing a big system in ACL2
 
88
this is probably the desired setting for part <code>a</code>.<p>
86
89
 
87
90
<code>:doit</code> -- any user-defined function may be redefined silently
88
 
(without query or warning) but when an attempt is made to redefine a
89
 
system function, a query is made.  This setting is recommended when
90
 
you start making massive changes to your prototyped system (and tire
91
 
of even the warning messages issued by <code>:warn</code>).<p>
 
91
(without query or warning) but when an attempt is made to redefine a system
 
92
function, a query is made.  This setting is recommended when you start making
 
93
massive changes to your prototyped system (and tire of even the warning
 
94
messages issued by <code>:warn</code>).<p>
92
95
 
93
96
</blockquote>
94
97
In support of our own ACL2 systems <a href="PROGRAMMING.html">programming</a> there are two other
96
99
<blockquote><p>
97
100
 
98
101
<code>:warn!</code> -- every attempt to redefine a name produces a warning but no
99
 
query.  Since ACL2 system functions can be redefined this way, this
100
 
setting should be used by the only-slightly-less-than supremely
101
 
confident ACL2 system hacker.<p>
 
102
query.  Since ACL2 system functions can be redefined this way, this setting
 
103
should be used by the only-slightly-less-than supremely confident ACL2 system
 
104
hacker.<p>
102
105
 
103
106
<code>:doit!</code> -- this setting allows any name to be redefined silently
104
 
(without query or warnings).  ACL2 system functions are fair game.
105
 
This setting is reserved for the supremely confident ACL2 system
106
 
hacker.  (Actually, this setting is used when we are loading
107
 
massively modified versions of the ACL2 source files.)<p>
 
107
(without query or warnings).  ACL2 system functions are fair game.  This
 
108
setting is reserved for the supremely confident ACL2 system hacker.
 
109
(Actually, this setting is used when we are loading massively modified
 
110
versions of the ACL2 source files.)<p>
108
111
 
109
112
</blockquote>
110
 
Part <code>b</code> of <code>ld-redefinition-action</code> tells the system how to ``renew''
111
 
the property list of the name being redefined.  There are two
 
113
Part <code>b</code> of <code>ld-redefinition-action</code> tells the system how to
 
114
``renew'' the property list of the name being redefined.  There are two
112
115
choices:
113
116
<blockquote><p>
114
117
 
118
121
overwrite them.<p>
119
122
 
120
123
</blockquote>
121
 
It should be stressed that neither of these <code>b</code> settings is
122
 
guaranteed to result in an entirely satisfactory state of affairs
123
 
after the redefinition.  Roughly speaking, <code>:erase</code> returns the
124
 
property list of the name to the state it was in when the name was
125
 
first introduced.  Lemmas, type information, etc., stored under that
126
 
name are lost.  Is that what you wanted?  Sometimes it is, as when
127
 
the old definition is ``completely wrong.'' But other times the old
128
 
definition was ``almost right'' in the sense that some of the work
129
 
done with it is still (intended to be) valid.  In that case,
130
 
<code>:overwrite</code> might be the correct <code>b</code> setting.  For example if
131
 
<code>fn</code> was a function and is being re-<code><a href="DEFUN.html">defun</a></code>'d with the same
132
 
<a href="SIGNATURE.html">signature</a>, then the properties stored by the new <code><a href="DEFUN.html">defun</a></code>
133
 
should overwrite those stored by the old <code><a href="DEFUN.html">defun</a></code> but the
134
 
properties stored by <code><a href="DEFTHM.html">defthm</a></code>s will be preserved.<p>
135
 
 
136
 
In addition, neither setting will cause ACL2 to erase properties
137
 
stored under other symbols!  Thus, if <code>FOO</code> names a rewrite rule
138
 
which rewrites a term beginning with the function symbol <code>BAR</code> and
139
 
you then redefine <code>FOO</code> to rewrite a term beginning with the
140
 
function symbol <code>BAZ</code>, then the old version of <code>FOO</code> is still
141
 
available (because the rule itself was added to the rewrite rules
142
 
for <code>BAR</code>, whose property list was not cleared by redefining
143
 
<code>FOO</code>).<p>
144
 
 
145
 
The <code>b</code> setting is only used as the default action when no query is
146
 
made.  If you choose a setting for part a that produces a query then
147
 
you will have the opportunity, for each redefinition, to specify
148
 
whether the property list is to be erased or overwritten.<p>
149
 
 
150
 
The keyword command <code>:</code><code><a href="REDEF.html">redef</a></code> sets <code>ld-redefinition-action</code> to the pair
151
 
<code>(:query . :overwrite)</code>.  Since the resulting query will give you the
152
 
chance to specify <code>:erase</code> instead of <code>:overwrite</code>, this setting is
153
 
quite convenient.  But when you are engaged in heavy-duty
154
 
prototyping, you may wish to use a setting such as <code>:warn</code> or even
155
 
<code>:doit</code>.  For that you will have to invoke a form such as:
 
124
It should be stressed that neither of these <code>b</code> settings is guaranteed
 
125
to result in an entirely satisfactory state of affairs after the
 
126
redefinition.  Roughly speaking, <code>:erase</code> returns the property list of the
 
127
name to the state it was in when the name was first introduced.  Lemmas, type
 
128
information, etc., stored under that name are lost.  Is that what you wanted?
 
129
Sometimes it is, as when the old definition is ``completely wrong.'' But
 
130
other times the old definition was ``almost right'' in the sense that some of
 
131
the work done with it is still (intended to be) valid.  In that case,
 
132
<code>:overwrite</code> might be the correct <code>b</code> setting.  For example if <code>fn</code> was
 
133
a function and is being re-<code><a href="DEFUN.html">defun</a></code>'d with the same <a href="SIGNATURE.html">signature</a>, then
 
134
the properties stored by the new <code><a href="DEFUN.html">defun</a></code> should overwrite those stored by
 
135
the old <code><a href="DEFUN.html">defun</a></code> but the properties stored by <code><a href="DEFTHM.html">defthm</a></code>s will be
 
136
preserved.<p>
 
137
 
 
138
In addition, neither setting will cause ACL2 to erase properties stored under
 
139
other symbols!  Thus, if <code>FOO</code> names a rewrite rule which rewrites a term
 
140
beginning with the function symbol <code>BAR</code> and you then redefine <code>FOO</code> to
 
141
rewrite a term beginning with the function symbol <code>BAZ</code>, then the old
 
142
version of <code>FOO</code> is still available (because the rule itself was added to
 
143
the rewrite rules for <code>BAR</code>, whose property list was not cleared by
 
144
redefining <code>FOO</code>).<p>
 
145
 
 
146
The <code>b</code> setting is only used as the default action when no query is made.
 
147
If you choose a setting for part a that produces a query then you will have
 
148
the opportunity, for each redefinition, to specify whether the property list
 
149
is to be erased or overwritten.<p>
 
150
 
 
151
The keyword command <code>:</code><code><a href="REDEF.html">redef</a></code> sets <code>ld-redefinition-action</code> to the
 
152
pair <code>(:query . :overwrite)</code>.  Since the resulting query will give you the
 
153
chance to specify <code>:erase</code> instead of <code>:overwrite</code>, this setting is quite
 
154
convenient.  But when you are engaged in heavy-duty prototyping, you may wish
 
155
to use a setting such as <code>:warn</code> or even <code>:doit</code>.  For that you will have
 
156
to invoke a form such as:
156
157
 
157
158
<pre>
158
159
(set-ld-redefinition-action '(:doit . :overwrite) state) .
160
161
<p>
161
162
 
162
163
<code><a href="ENCAPSULATE.html">Encapsulate</a></code> causes somewhat odd interaction with the user if
163
 
redefinition occurs within the encapsulation because the
164
 
<a href="ENCAPSULATE.html">encapsulate</a>d event list is processed several times.  For example, if
165
 
the redefinition action causes a query and a non-local definition is
166
 
actually a redefinition, then the query will be posed twice, once
167
 
during each pass.  C'est la vie.<p>
 
164
redefinition occurs within the encapsulation because the <a href="ENCAPSULATE.html">encapsulate</a>d
 
165
event list is processed several times.  For example, if the redefinition
 
166
action causes a query and a non-local definition is actually a redefinition,
 
167
then the query will be posed twice, once during each pass.  C'est la vie.<p>
168
168
 
169
 
Finally, it should be stressed again that redefinition is dangerous
170
 
because not all of the rules about a name are stored on the property
171
 
list of the name.  Thus, redefinition can render ill-formed terms
172
 
stored elsewhere in the data base or can preserve now-invalid
173
 
rules.  See <a href="REDUNDANT-EVENTS.html">redundant-events</a>, in particular the section ``Note About
174
 
Unfortunate Redundancies,'' for more discussion of potential pitfalls of
175
 
redefinition.
 
169
Finally, it should be stressed again that redefinition is dangerous because
 
170
not all of the rules about a name are stored on the property list of the
 
171
name.  Thus, redefinition can render ill-formed terms stored elsewhere in the
 
172
data base or can preserve now-invalid rules.  See <a href="REDUNDANT-EVENTS.html">redundant-events</a>, in
 
173
particular the section ``Note About Unfortunate Redundancies,'' for more
 
174
discussion of potential pitfalls of redefinition.
176
175
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
177
176
</body>
178
177
</html>