32
28
* acl2: (acl2-doc-emacs.info). Applicative Common Lisp
40
File: acl2-doc-emacs.info, Node: ACL2-COUNT, Next: ACL2-CUSTOMIZATION, Prev: ACKNOWLEDGMENTS, Up: MISCELLANEOUS
42
ACL2-COUNT a commonly used measure for justifying recursion
44
(Acl2-count x) returns a nonnegative integer that indicates the "size"
47
All characters and symbols have acl2-count 0. The acl2-count of a
48
string is the number of characters in it, i.e., its length. The
49
acl2-count of a cons is one greater than the sum of the acl2-counts of
50
the car and cdr. The acl2-count of an integer is its absolute value.
51
The acl2-count of a rational is the sum of the acl2-counts of the
52
numerator and denominator. The acl2-count of a complex rational is one
53
greater than the sum of the acl2-counts of the real and imaginary parts.
58
File: acl2-doc-emacs.info, Node: ACL2-CUSTOMIZATION, Next: APROPOS, Prev: ACL2-COUNT, Up: MISCELLANEOUS
60
ACL2-CUSTOMIZATION file of initial commands for ACL2 to run at startup
62
The file "acl2-customization.lisp" is automatically loaded, via ld, the
63
first time lp is called in an ACL2 session, provided such a file exists
64
on the current directory. Except for the fact that this ld command is
65
not typed explicitly by you, it is a standard ld command, with one
66
exception: any settings of ld specials are remembered once this call of
67
ld has completed. For example, suppose that you start your
68
customization file with (set-ld-skip-proofsp t state), so that proofs
69
are skipped as it is loaded with ld. Then the ld special
70
ld-skip-proofsp will remain t after the ld has completed, causing proofs
71
to be skipped in your ACL2 session, unless your customization file sets
72
this variable back to nil, say with (set-ld-skip-proofsp nil state).
74
The customization file "acl2-customization.lisp" actually resides on the
75
connected book directory; see *Note CBD::. Except, if that file does
76
not exist, then ACL2 looks for "acl2-customization.lisp" on your home
77
directory. If ACL2 does not find that file either, then no
78
customization occurs and lp enters the standard ACL2 read-eval-print
81
If the customization file exists, it is loaded with ld using the usual
82
default values for the ld specials (see *Note LD::). Thus, if an error
83
is encountered, no subsequent forms in the file will be evaluated.
85
To create a customization file it is recommended that you first give it
86
a name other than "acl2-customization.lisp" so that ACL2 does not try to
87
include it prematurely when you next enter lp. Then, while in the
88
uncustomized lp, explicitly invoke ld on your evolving (but renamed)
89
customization file until all forms are successfully evaluated. The same
90
procedure is recommended if for some reason ACL2 cannot successfully
91
evaluate all forms in your customization file: rename your customization
92
file so that ACL2 does not try to ld it automatically and then debug the
93
new file by explicit calls to ld.
95
When you have created a file that can be loaded with ld without error
96
and that you wish to be your customization file, name it
97
"acl2-customization.lisp" and put it on the current directory or in your
98
home directory. The first time after starting up ACL2 that you invoke
99
(lp), ACL2 will automatically load the "acl2-customization.lisp" file
100
from the cbd (see *Note CBD::) if there is one, and otherwise will load
101
it from your home directory.
103
Note that if you certify a book after the (automatic) loading of an
104
acl2-customization file, the forms in that file *will be part of the*
105
*portcullis* of the books you certify! That is, the forms in your
106
customization file at certification time will be loaded whenever anybody
107
uses the books you are certifying. Since customization files generally
108
contain idiosyncratic commands, you may not want yours to be part of the
109
books you create for others. Thus, if you have a customization file
110
then you may want to invoke :ubt 1 before certifying any books.
112
The conventions concerning ACL2 customization are liable to change as we
113
get more experience with the interaction between customization,
114
certification of books for others, and routine undoing. For example, at
115
the moment it is regarded as a *feature* of customization that it can be
116
undone but it might be regarded as a bug if you accidentally undo your
122
File: acl2-doc-emacs.info, Node: APROPOS, Next: ARRAYS, Prev: ACL2-CUSTOMIZATION, Up: MISCELLANEOUS
124
APROPOS searching :doc and :more-doc text
126
NOTE: The :docs command only makes sense at the terminal.
32
File: acl2-doc-emacs.info, Node: SET-CASE-SPLIT-LIMITATIONS, Next: SET-COMPILE-FNS, Prev: SET-BOGUS-MUTUAL-RECURSION-OK, Up: EVENTS
34
SET-CASE-SPLIT-LIMITATIONS set the case-split-limitations
38
(set-case-split-limitations '(500 100))
39
(set-case-split-limitations 'nil)
40
(set-case-split-limitations '(500 nil))
42
The first of these prevents clausify from trying the
43
subsumption/replacement (see below) loop if more than 500 clauses are
44
involved. It also discourages the clause simplifier from splitting
45
into more than 100 cases at once.
47
Note: This is an event! It does not print the usual event summary but
48
nevertheless changes the ACL2 logical world and is so recorded.
49
Moreover, its effect is to set the acl2-defaults-table, and hence its
50
effect is local to the book or encapsulate form containing it; see
51
*note ACL2-DEFAULTS-TABLE::.
54
(set-case-split-limitations lst)
56
where lst is either nil (denoting a list of two nils), or a list of
57
length two, each element of which is either nil or a natural number.
58
When nil is used as an element, it is treated as positive infinity.
59
The default setting is (500 100).
61
The first number specifies the maximum number of clauses that may
62
participate in the "subsumption/replacement" loop. Because of the
63
expensive nature of that loop (which compares every clause to every
64
other in a way that is quadratic in the number of literals in the
65
clauses), when the number of clauses exceeds about 1000, the system
66
tends to "go into a black hole," printing nothing and not even doing
67
many garbage collections (because the subsumption/replacement loop does
68
not create new clauses so much as it just tries to delete old ones).
69
The initial setting is lower than the threshold at which we see
70
noticeably bad performance, so you probably will not see this behavior
71
unless you have raised or disabled the limit.
73
Why raise the subsumption/replacement limit? The
74
subsumption/replacement loop cleans up the set of subgoals produced by
75
the simplifier. For example, if one subgoal is
77
(implies (and p q r) s) [1]
81
(implies (and p (not q) r) s) [2]
83
then the subsumption/replacement loop would produce the single subgoal
85
(implies (and p r) s) [3]
87
instead. This cleanup process is simply skipped when the number of
88
subgoals exceeds the subsumption/replacement limit. But each subgoal
89
must nonetheless be proved. The proofs of [1] and [2] are likely to
90
duplicate much work, which is only done once in proving [3]. So with a
91
low limit, you may find the system quickly produces a set of subgoals
92
but then takes a long time to prove that set. With a higher limit, you
93
may find the set of subgoals to be "cleaner" and faster to prove.
95
Why lower the subsumption/replacement limit? If you see the system go
96
into a "black hole" of the sort described above (no output, and few
97
garbage collections), it could due to the subsumption/replacement loop
98
working on a large set of large subgoals. You might temporarily lower
99
the limit so that it begins to print the uncleaned set of subgoals.
100
Perhaps by looking at the output you will realize that some function
101
can be disabled so as to prevent the case explosion. Then raise or
102
disable the limit again!
104
The second number in the case-split-limitations specifies how many case
105
splits the simplifier will allow before it begins to shut down case
106
splitting. In normal operation, when a literal rewrites to a nest of
107
IFs, the system simplifies all subsequent literals in all the contexts
108
generated by walking through the nest in all possible ways. This can
109
also cause the system to "go into a black hole" printing nothing except
110
garbage collection messages. This "black hole" behavior is different
111
from than mentioned above because space is typically being consumed at
112
a prodigious rate, since the system is rewriting the literals over and
113
over in many different contexts.
115
As the simplifier sweeps across the clause, it keeps track of the
116
number of cases that have been generated. When that number exceeds the
117
second number in case-split-limitations, the simplifier stops rewriting
118
literals. The remaining, unrewritten, literals are copied over into
119
the output clauses. IFs in those literals are split out, but the
120
literals themselves are not rewritten. Each output clause is then
121
attacked again, by subsequent simplification, and eventually the
122
unrewritten literals in the tail of the clause will be rewritten
123
because the earlier literals will stabilize and stop producing case
126
The default setting of 100 is fairly low. We have seen successful
127
proofs in which thousands of subgoals were created by a simplification.
128
By setting the second number to small values, you can force the system
129
to case split slowly. For example, a setting of 5 will cause it to
130
generate "about 5" subgoals per simplification.
132
You can read about how the simplifier works in the book Computer-Aided
133
Reasoning: An Approach (Kaufmann, Manolios, Moore). If you think about
134
it, you will see that with a low case limit, the initial literals of a
135
goal are repeatedly simplified, because each time a subgoal is
136
simplified we start at the left-most subterm. So when case splitting
137
prevents the later subterms from being fully split out, we revisit the
138
earlier terms before getting to the later ones. This can be good.
139
Perhaps it takes several rounds of rewriting before the earlier terms
140
are in normal form and then the later terms rewrite quickly. But it
141
could happen that the earlier terms are expensive to rewrite and do not
142
change, making the strategy of delayed case splits less efficient. It
145
Sometimes the simplifier produces more clauses than you might expect,
146
even with case-split-limitations in effect. As noted above, once the
147
limit has been exceeded, the simplifier does not rewrite subsequent
148
literals. But IFs in those literals are split out nonetheless.
149
Furthermore, the enforcement of the limit is - as described above - all
150
or nothing: if the limit allows us to rewrite a literal then we rewrite
151
the literal fully, without regard for limitations, and get as many
152
cases as "naturally" are produced. It quite often happens that a
153
single literal, when expanded, may grossly exceed the specified limits.
155
If the second "number" is nil and the simplifier is going to produce
156
more than 1000 clauses, a "helpful little message" to this effect is
157
printed out. This output is printed to the system's "comment window"
158
not the standard proofs output.
161
File: acl2-doc-emacs.info, Node: SET-COMPILE-FNS, Next: SET-DEFAULT-BACKCHAIN-LIMIT, Prev: SET-CASE-SPLIT-LIMITATIONS, Up: EVENTS
163
SET-COMPILE-FNS have each function compiled as you go along.
166
(set-compile-fns t) ; new functions compiled after DEFUN
167
(set-compile-fns nil) ; new functions not compiled after DEFUN
169
Note: This is an event! It does not print the usual event summary but
170
nevertheless changes the ACL2 logical world and is so recorded.
172
Also see *note COMP::, because it may be more efficient in some Common
173
Lisps to compile many functions at once rather than to compile each one
177
(set-compile-fns term)
179
where term is a variable-free term that evaluates to t or nil. This
180
macro is equivalent to
182
(table acl2-defaults-table :compile-fns term)
184
and hence is local to any books and encapsulate events in which it
185
occurs; see *note ACL2-DEFAULTS-TABLE::. However, unlike the above
186
simple call of the table event function (see *note TABLE::), no output
187
results from a set-compile-fns event.
189
Set-compile-fns may be thought of as an event that merely sets a flag
190
to t or nil. The flag's effect is felt when functions are defined, as
191
with defun. If the flag is t, functions are automatically compiled
192
after they are defined, as are their executable counterparts (see *note
193
EXECUTABLE-COUNTERPART::). Otherwise, functions are not automatically
194
compiled. Because set-compile-fns is an event, the old value of the
195
flag is restored when a set-compile-fns event is undone.
197
Even when :set-compile-fns t has been executed, functions are not
198
individually compiled when processing an include-book event. If you
199
wish to include a book of compiled functions, we suggest that you first
200
certify it with the compilation flag set (see *note CERTIFY-BOOK::) or
201
else compile the book by supplying the appropriate load-compiled-file
202
argument to include-book. More generally, compilation via
203
set-compile-fns is suppressed when the state global variable
204
ld-skip-proofsp has value 'include-book.
207
File: acl2-doc-emacs.info, Node: SET-DEFAULT-BACKCHAIN-LIMIT, Next: SET-DEFAULT-HINTS, Prev: SET-COMPILE-FNS, Up: EVENTS
209
SET-DEFAULT-BACKCHAIN-LIMIT sets the default backchain-limit used when admitting a rule
211
Note: This is an event! It does not print the usual event summary but
212
nevertheless changes the ACL2 logical world and is so recorded.
213
Moreover, its effect is to set the acl2-defaults-table, and hence its
214
effect is local to the book or encapsulate form containing it; see
215
*note ACL2-DEFAULTS-TABLE::.
217
This event sets the default backchain-limit used when a new rewrite or
218
linear rule is admitted. It must be nil or a non-negative integer.
219
(See *Note BACKCHAIN-LIMIT:: for details.)
221
:set-default-backchain-limit nil ; do not impose additional limits
222
:set-default-backchain-limit 0 ; allow only type-reasoning for
223
; relieving hypotheses
224
:set-default-backchain-limit 500 ; allow backchaining to a depth of
226
(set-default-backchain-limit 500) ; same as above
228
The initial default backchain-limit is nil.
231
File: acl2-doc-emacs.info, Node: SET-DEFAULT-HINTS, Next: SET-DEFAULT-HINTS!, Prev: SET-DEFAULT-BACKCHAIN-LIMIT, Up: EVENTS
233
SET-DEFAULT-HINTS set the default hints
237
(set-default-hints '((computed-hint-1 clause)
238
(computed-hint-2 clause
239
stable-under-simplificationp)))
240
(set-default-hints nil)
242
Note: This is an event! It does not print the usual event summary but
243
nevertheless changes the ACL2 logical world and is so recorded. It is
244
local to the book or encapsulate form in which it occurs (see *note
245
SET-DEFAULT-HINTS!:: for a corresponding non-local event).
248
(set-default-hints lst)
250
where lst is a list. Generally speaking, the elements of lst should be
251
suitable for use as computed-hints.
253
Whenever a defthm or thm command is executed, the default hints are
254
appended to the right of any explicitly provided :hints in the command.
255
The same applies to defuns as well (:hints, :guard-hints, and (for
256
ACL2(r)) :std-hints). The hints are then translated and processed just
257
as though they had been explicitly included.
259
Technically, we do not put restrictions on lst, beyond that it is a
260
true list. It would be legal to execute
262
(set-default-hints '(("Goal" :use lemma23)))
264
with the effect that the given hint is added to subsequent hints
265
supplied explicitly. An explicit "Goal" hint would, however, take
266
priority, as suggested by the mention above of "appended to the right."
268
Note that set-default-hints sets the default hints as specified. To
269
add to or remove from the current default, see *note
270
ADD-DEFAULT-HINTS:: and see *note REMOVE-DEFAULT-HINTS::.
272
Finally, note that the effects of set-default-hints, add-default-hints,
273
and remove-default-hints are local to the book in which they appear.
274
Thus, users who include a book with such forms will not have their
275
default hints affected by such forms. In order to export the effect of
276
setting the default hints, use set-default-hints!, add-default-hints!,
277
or remove-default-hints!.
280
File: acl2-doc-emacs.info, Node: SET-DEFAULT-HINTS!, Next: SET-ENFORCE-REDUNDANCY, Prev: SET-DEFAULT-HINTS, Up: EVENTS
282
SET-DEFAULT-HINTS! set the default hints non-locally
284
Please see *note SET-DEFAULT-HINTS::, which is the same as
285
set-default-hints! except that the latter is not local to the
286
encapsulate or the book in which it occurs. Probably set-default-hints
287
is to be preferred unless you have a good reason for wanting to export
288
the effect of this event outside the enclosing encapsulate or book.
291
File: acl2-doc-emacs.info, Node: SET-ENFORCE-REDUNDANCY, Next: SET-IGNORE-OK, Prev: SET-DEFAULT-HINTS!, Up: EVENTS
293
SET-ENFORCE-REDUNDANCY require most events to be redundant
296
(set-enforce-redundancy nil) ; do not require redundancy (default)
297
(set-enforce-redundancy t) ; most events (see below) must be redundant
298
(set-enforce-redundancy :warn) ; warn for most non-redundant events
300
Note: This is an event! It does not print the usual event summary but
301
nevertheless changes the ACL2 logical world and is so recorded.
304
(set-enforce-redundancy flag)
306
where flag is nil, t, or :warn, as indicated above. This macro is
307
essentially equivalent to
309
(table acl2-defaults-table :enforce-redundancy flag)
311
and hence is local to any books and encapsulate events in which it
312
occurs; see *note ACL2-DEFAULTS-TABLE::. However, unlike the above
313
simple call of the table event function (see *note TABLE::), no output
314
results from a set-enforce-redundancy event.
316
Set-enforce-redundancy may be thought of as an event that merely sets a
317
flag as indicated above, which determines whether most events, including
318
defun and defthm events, are allowed to be redundant; see *note
319
REDUNDANT-EVENTS::. The exceptions are deflabel, defpkg, encapsulate,
320
include-book, push-untouchable, remove-untouchable, set-body, and table
321
events. Any other type of non-redundant event will cause an error if
322
flag is t and a warning if flag is nil, _except_ in the course of
323
carrying out an include-book form.
325
Note that because table events that set the acl2-defaults-table are
326
implicitly local, set-enforce-redundancy events are ignored when
327
including books. However, the presence of the event
328
(set-enforce-redundancy t) in a book guarantees that its subsequent
329
definitions and theorems are redundant. This can be a useful property
330
to maintain in library development, as we now describe.
332
An example of the use of this form can be found in the distributed books
333
under directory books/rtl/rel4/. The intention in that directory has
334
been to put all the gory details in subdirectories support/ and
335
arithmetic/, so that the books in subdirectory lib/ contain only the
336
"exported" definitions and theorems. This approach is useful for human
337
readability. Moreover, suppose we want to prove new theorems in lib/.
338
Typically we wish to prove the new theorems using the existing books in
339
lib/; however, our methodology demands that the proofs go into books in
340
support/. If every theorem in lib/ is redundant, then we can _develop_
341
the proofs in lib/ but then when we are done, _move_ each book with
342
such proofs into support/ as follows. In any such book, we first
343
replace include-book forms referring to books in lib/ by include-book
344
forms referring to corresponding books in support/ and/or arithmetic/.
345
Then, we add suitable in-theory events to get us back into the original
346
lib/ proof environment.
348
The default behavior of the system is as though the :enforce-redundancy
349
value is nil. The current behavior can be ascertained by evaluating the
352
(cdr (assoc-eq :enforce-redundancy (table-alist 'acl2-defaults-table wrld)))
355
File: acl2-doc-emacs.info, Node: SET-IGNORE-OK, Next: SET-INHIBIT-WARNINGS, Prev: SET-ENFORCE-REDUNDANCY, Up: EVENTS
357
SET-IGNORE-OK allow unused formals and locals without an ignore or ignorable declaration
362
(set-ignore-ok :warn)
364
The first example above allows unused formals and locals, i.e.,
365
variables that would normally have to be declared ignored or ignorable.
366
The second example disallows unused formals and locals; this is the
367
default. The third example allows them, but prints an appropriate
370
Note: This is an event! It does not print the usual event summary but
371
nevertheless changes the ACL2 logical world and is so recorded.
372
Moreover, its effect is to set the acl2-defaults-table, and hence its
373
effect is local to the book or encapsulate form containing it; see
374
*note ACL2-DEFAULTS-TABLE::.
379
where flg is either t, nil, or :warn.
381
One might find this event useful when one is generating function
382
definitions by an automated procedure, when that procedure does not
383
take care to make sure that all formals are actually used in the
384
definitions that it generates.
386
Note: Defun will continue to report irrelevant formals even if
387
:set-ignore-ok has been set to t, unless you also use
388
set-irrelevant-formals-ok to instruct it otherwise.
391
File: acl2-doc-emacs.info, Node: SET-INHIBIT-WARNINGS, Next: SET-INVISIBLE-FNS-TABLE, Prev: SET-IGNORE-OK, Up: EVENTS
393
SET-INHIBIT-WARNINGS control warnings
396
(set-inhibit-warnings "theory" "use")
398
Note: This is an event! It does not print the usual event summary but
399
nevertheless changes the ACL2 logical world and is so recorded.
400
Moreover, its effect is to set the acl2-defaults-table, and hence its
401
effect is local to the book or encapsulate form containing it; see
402
*note ACL2-DEFAULTS-TABLE::.
405
(set-inhibit-warnings string1 string2 ...)
407
where each string is considered without regard to case. This macro is
408
equivalent to (table acl2-defaults-table :inhibit-warnings lst), where
409
lst is the list of strings supplied. This macro is an event (see *note
410
TABLE::), but no output results from a set-inhibit-warnings event.
412
The effect of this event is to suppress any warning whose label is a
413
member of this list (where again, case is ignored). For example, the
416
ACL2 Warning [Use] in ( THM ...): It is unusual to :USE ....
418
will not be printed if "use" (or "USE", etc.) is a member of the given
421
Of course, if warnings are inhibited overall -- see *note
422
SET-INHIBIT-OUTPUT-LST:: -- then the value of :inhibit-warnings is
426
File: acl2-doc-emacs.info, Node: SET-INVISIBLE-FNS-TABLE, Next: SET-IRRELEVANT-FORMALS-OK, Prev: SET-INHIBIT-WARNINGS, Up: EVENTS
428
SET-INVISIBLE-FNS-TABLE set the invisible functions table
431
(set-invisible-fns-table ((binary-+ unary--)
435
(set-invisible-fns-table t) ; restore original invisible-fns-table
437
Among other things, the setting above has the effect of making unary-
438
"invisible" for the purposes of applying permutative :rewrite rules to
439
binary-+ trees. Thus, arg and (unary- arg) will be given the same
440
weight and will be permuted so as to be adjacent. The form
441
(invisible-fns-table (w state)) returns the current value of the
442
invisible functions table.
444
Also see *note ADD-INVISIBLE-FNS:: and see *note REMOVE-INVISIBLE-FNS::
445
for events that add to and remove from the invisible functions table.
448
(set-invisible-fns-table alist)
450
where alist is either t or a true list of pairs, each element of which
451
is of the form (fn ufn1 ... ufnk), where fn is a function symbol and
452
each ufni is a unary function symbol. When alist is t, the initial
453
value of this table is used in its place. Modulo the replacement of
454
alist by the default setting when alist is t, this macro is equivalent
457
(table invisible-fns-table nil 'alist :clear)
459
which is also an event (see *note TABLE::).
461
Note that set-invisible-fns-table does not evaluate its argument.
462
However, you can call table directly for that purpose. For example,
464
(set-invisible-fns-table ((binary-+ unary--)
469
ie equivalent to the following; see *note TABLE::.
471
(table invisible-fns-table nil
472
(quote ((binary-+ unary--)
478
See *Note INVISIBLE-FNS-TABLE:: for a description of the invisible
482
File: acl2-doc-emacs.info, Node: SET-IRRELEVANT-FORMALS-OK, Next: SET-LET*-ABSTRACTIONP, Prev: SET-INVISIBLE-FNS-TABLE, Up: EVENTS
484
SET-IRRELEVANT-FORMALS-OK allow irrelevant formals in definitions
487
(set-irrelevant-formals-ok t)
488
(set-irrelevant-formals-ok nil)
489
(set-irrelevant-formals-ok :warn)
491
The first example above allows irrelevant formals in definitions; see
492
*note IRRELEVANT-FORMALS::. The second example disallows irrelevant
493
formals; this is the default. The third example allows irrelevant
494
formals, but prints an appropriate warning.
496
Note: This is an event! It does not print the usual event summary but
497
nevertheless changes the ACL2 logical world and is so recorded.
498
Moreover, its effect is to set the acl2-defaults-table, and hence its
499
effect is local to the book or encapsulate form containing it; see
500
*note ACL2-DEFAULTS-TABLE::.
503
(set-irrelevant-formals-ok flg)
505
where flg is either t, nil, or :warn.
508
File: acl2-doc-emacs.info, Node: SET-LET*-ABSTRACTIONP, Next: SET-MATCH-FREE-DEFAULT, Prev: SET-IRRELEVANT-FORMALS-OK, Up: EVENTS
510
SET-LET*-ABSTRACTIONP to shorten many prettyprinted clauses
512
Note: This is an event! It does not print the usual event summary but
513
nevertheless changes the ACL2 logical world and is so recorded.
514
Moreover, its effect is to set the acl2-defaults-table, and hence its
515
effect is local to the book or encapsulate form containing it; see
516
*note ACL2-DEFAULTS-TABLE::.
518
When this flag is set to t, subterms that occur more than once in a
519
clause are abstracted away with let*, generally shortening the
520
displayed size of the clauses. This flag only affects how clauses are
521
printed. It does not change what terms the theorem prover manipulates.
523
:set-let*-abstractionp t ;;; or, (set-let*-abstractionp t)
525
will cause the prettyprinter to do "let* abstraction" on clauses before
526
they are printed. The algorithm finds the maximal multiply-occuring
527
subterm and extracts it, binding it to some new variable and replacing
528
its occurrences by that variable. This produces a let* form. This
529
process is iterated until no subterm occurs more than once. This
530
process generally takes a little time, but less time than to print
531
large clauses. The process can greatly reduce the amount of text
532
produced by the prover.
534
THIS ONLY AFFECTS HOW THE CLAUSES ARE PRINTED! The unabstracted
535
clauses are manipulated by the theorem prover.
537
:set-let*-abstractionp nil
539
restores normal clause printing.
541
The mode is stored in the defaults table, See *Note
542
ACL2-DEFAULTS-TABLE::. Thus, the mode may be set locally in books.
545
File: acl2-doc-emacs.info, Node: SET-MATCH-FREE-DEFAULT, Next: SET-MATCH-FREE-ERROR, Prev: SET-LET*-ABSTRACTIONP, Up: EVENTS
547
SET-MATCH-FREE-DEFAULT provide default for :match-free in future rules
550
(set-match-free-default :once)
551
(set-match-free-default :all)
552
(set-match-free-default nil)
554
As described elsewhere (see *note FREE-VARIABLES::), a rewrite, linear,
555
or forward-chaining rule may have free variables in its hypotheses, and
556
ACL2 can be directed either to try all bindings (":all") or just the
557
first (":once") when relieving that hypothesis, as a basis for
558
relieving subsequent hypotheses. This direction of :all or :once is
559
generally provided by specifying either :match-free :once or
560
:match-free :all in the :rule-classes of the rule. If neither of these
561
is specified, then the most recent set-match-free-default is used by
562
ACL2 to fill in this missing :match-free field. See *Note
563
RULE-CLASSES::. Except: If the last set-match-free-default specifies
564
nil, then ACL2 reverts to the behavior it had at start-up, as described
565
in Remarks (2) and (3) below.
567
Note: This is an event! It does not print the usual event summary but
568
nevertheless changes the ACL2 logical world and is so recorded. It
569
uses the acl2-defaults-table, and hence its effect is local to the book
570
or encapsulate form in which it occurs.
574
(1) The use of set-match-free-default has no effect on existing rules.
575
In order to change the behavior of existing rules with respect to
576
free-variable matching, see *note ADD-MATCH-FREE-OVERRIDE::.
578
(2) If you submit a rewrite, linear, or forward-chaining rule with a
579
free variable in a hypothesis, and no default setting was previously
580
specified with set-match-free-default or the default setting is nil,
581
and the rule is not within a book being processed with include-book,
582
certify-book, or rebuild, then a warning or error is caused. In order
583
to make this an error instead of a warning, see *note
584
SET-MATCH-FREE-ERROR::.
586
(3) If you submit a rewrite, linear, or forward-chaining rule with a
587
free variable in a hypothesis, and no default setting has been
588
previously specified with set-match-free-default or the default setting
589
is nil, and no error is caused (see (2) above), then the default :all
593
File: acl2-doc-emacs.info, Node: SET-MATCH-FREE-ERROR, Next: SET-MEASURE-FUNCTION, Prev: SET-MATCH-FREE-DEFAULT, Up: EVENTS
595
SET-MATCH-FREE-ERROR control error vs. warning when :match-free is missing
598
(set-match-free-error nil)
599
:set-match-free-error nil
600
(set-match-free-error t)
601
:set-match-free-error t
603
As described elsewhere (see *note FREE-VARIABLES::), when a rewrite,
604
linear, or forward-chaining rule has free variables in its hypotheses,
605
the user can specify whether to try all bindings (":all") or just the
606
first (":once") when relieving its hypotheses, as a basis for relieving
607
subsequent hypotheses. This direction of :all or :once is generally
608
provided by specifying either :match-free :once or :match-free :all in
609
the :rule-classes of the rule.
611
But suppose that neither of these is specified, and that
612
set-match-free-default has not specified a default of :once or :all
613
(see *note SET-MATCH-FREE-DEFAULT::). In this case a warning will occur
614
except when in the context of include-book. If you prefer to see an
615
error in such cases, except in the context of certify-book, execute
616
(set-match-free-error t). If there is no error, then a default of :all
619
Note: This is NOT an event! Instead, set-match-free-error sets the
620
state global 'match-free-error (see *note STATE:: and see *note
621
ASSIGN::). Thus, this form cannot be put into a book. If you are
622
tempted to put it into a book, consider the fact that it really isn't
623
needed there, since the absence of :match-free does not cause an error
624
in the context of certify-book or include-book. If you still feel the
625
need for such a form, consider using set-match-free-default to provide
626
a default, at least within the scope of the current book (if any); see
627
*note SET-MATCH-FREE-DEFAULT::.
630
File: acl2-doc-emacs.info, Node: SET-MEASURE-FUNCTION, Next: SET-NON-LINEARP, Prev: SET-MATCH-FREE-ERROR, Up: EVENTS
632
SET-MEASURE-FUNCTION set the default measure function symbol
635
(set-measure-function nqthm::count)
637
Note: This is an event! It does not print the usual event summary but
638
nevertheless changes the ACL2 logical world and is so recorded.
641
(set-measure-function name)
643
where name is a function symbol of one argument. This macro is
644
equivalent to (table acl2-defaults-table :measure-function 'name), and
645
hence is local to any books and encapsulate events in which it occurs;
646
see *note ACL2-DEFAULTS-TABLE::. Although this is thus an event (see
647
*note TABLE::), nevertheless no output results from a
648
set-measure-function event.
650
This event sets the default measure function to name. Subsequently, if
651
a recursively defined function is submitted to defun with no explicitly
652
given :measure argument, defun "guesses" the measure (name var), where
653
name is the then current default measure function and var is the first
654
formal found to be tested along every branch and changed in every
657
Note that if (table acl2-defaults-table :measure-function 'name) has its
658
default value of nil, then the default measure function is acl2-count.
661
File: acl2-doc-emacs.info, Node: SET-NON-LINEARP, Next: SET-NU-REWRITER-MODE, Prev: SET-MEASURE-FUNCTION, Up: EVENTS
663
SET-NON-LINEARP to turn on or off non-linear arithmetic reasoning
667
(set-non-linearp nil)
669
See *Note NON-LINEAR-ARITHMETIC::. This event is equivalent to (table
670
acl2-defaults-table :non-linearp <t-or-nil>), and hence is local to any
671
books and encapsulate events in which it occurs; see *note
672
ACL2-DEFAULTS-TABLE::.
674
The initial value is nil.
677
File: acl2-doc-emacs.info, Node: SET-NU-REWRITER-MODE, Next: SET-REWRITE-STACK-LIMIT, Prev: SET-NON-LINEARP, Up: EVENTS
679
SET-NU-REWRITER-MODE to turn on and off the nu-rewriter
681
Note: This is an event! It does not print the usual event summary but
682
nevertheless changes the ACL2 logical world and is so recorded.
684
This event sets a flag that controls whether the ACL2 rewriter uses the
685
special-purpose nth/update-nth rewriter (nu-rewriter). The flag may
686
have one of three values: nil, t, or :literals.
688
:set-nu-rewriter-mode nil ; do not use nu-rewriter
689
:set-nu-rewriter-mode t ; use nu-rewriter in rewriting
690
:set-nu-rewriter-mode :literals ; use nu-rewriter in rewriting after
691
; a pre-pass through every literal
692
(set-nu-rewriter-mode :literals) ; same as above
694
The value nil prevents the use of the nu-rewriter. The other two
695
values allow the use of the nu-rewriter.
697
When the flag is non-nil and the rewriter encounters a term that
698
"begins with an nth", the nu-rewriter is applied. By "begins with an
699
nth" here we mean either the term is an application of nth or is an
700
application of some nonrecursive function or lambda expression whose
701
body contains an expression that begins with an nth.
703
Note that the use of the nu-rewriter here described above is driven by
704
the rewriter, i.e., the nu-rewriter is applied only to terms visited by
705
the rewriter in its inside-out sweep. When the flag is set to
706
:literals the system makes a pre-pass through every goal clause and
707
applies the nu-rewriter to every subterm. The rewriter is then used on
708
the output of that pre-pass.
710
Note: This is an event! It does not print the usual event summary but
711
nevertheless changes the ACL2 logical world and is so recorded.
712
Moreover, its effect is to set the acl2-defaults-table, and hence its
713
effect is local to the book or encapsulate form containing it; see
714
*note ACL2-DEFAULTS-TABLE::.
716
We expect to write more documentation as we gain experience with the
720
File: acl2-doc-emacs.info, Node: SET-REWRITE-STACK-LIMIT, Next: SET-STATE-OK, Prev: SET-NU-REWRITER-MODE, Up: EVENTS
722
SET-REWRITE-STACK-LIMIT Sets the rewrite stack depth used by the rewriter
724
Note: This is an event! It does not print the usual event summary but
725
nevertheless changes the ACL2 logical world and is so recorded.
728
(set-rewrite-stack-limit 30) ; set to small limit
729
:set-rewrite-stack-limit 30 ; same as above
730
(set-rewrite-stack-limit *default-rewrite-stack-limit*) ; the default
731
:set-rewrite-stack-limit (1- (expt 2 28)) ; maximum legal limit
732
:set-rewrite-stack-limit nil ; same as above -- essentially, no limit
734
This event sets the maximum stack depth for calls of certain functions
735
that implement the ACL2 rewriter; see *note REWRITE-STACK-LIMIT::. It
736
must be a non-negative integer less than 2^28. A call
737
(set-rewrite-stack-limit limit) is equivalent to:
739
(table acl2-defaults-table :rewrite-stack-limit limit).
741
The use of acl2-defaults-table ensures that this event's effect is
742
implicitly local to the book or encapsulate form in which it occurs.
744
For a different but somewhat related concept, see *note
748
File: acl2-doc-emacs.info, Node: SET-STATE-OK, Next: SET-VERIFY-GUARDS-EAGERNESS, Prev: SET-REWRITE-STACK-LIMIT, Up: EVENTS
750
SET-STATE-OK allow the use of STATE as a formal parameter
752
Note: This is an event! It does not print the usual event summary but
753
nevertheless changes the ACL2 logical world and is so recorded.
755
In brief: The variable symbol STATE has an unusual status in ACL2. In
756
order to use it, you either need to issue :set-state-ok t, as we
757
explain below, or you need to declare it to be a stobj, as explained
758
elsewhere (see *note DECLARE-STOBJS::). Now we explain in more detail.
760
Because the variable symbol STATE denotes the "current ACL2 state,"
761
ACL2 treats the symbol very restrictively when it occurs as a formal
762
parameter of a defined function. The novice user, who is unlikely to
763
be aware of the special status of that symbol, is likely to be confused
764
when error messages about STATE are printed in response to the innocent
765
choice of that symbol as a formal variable. Therefore the top-level
766
ACL2 loop can operate in a mode in which STATE is simply disallowed as
769
For a discussion of STATE, See *Note STATE:: and see *note STOBJ::.
770
Roughly speaking, at the top-level, the "current ACL2 state" is denoted
771
by the variable symbol STATE. Only the current state may be passed
772
into a function expecting a state as an argument. Furthermore, the
773
name of the formal parameter into which the current state is passed
774
must be STATE and nothing but the current state may be passed into a
775
formal of that name. Therefore, only certain access and change
776
functions can use that formal - namely with a STATE formal - and if any
777
such function produces a new state it becomes the "current state" and
778
must be passed along in the STATE position thereafter. Thus, ACL2
779
requires that the state be single-threaded. This, in turn, allows us
780
to represent only one state at a time and to produce new states from it
781
destructively in a von Neumaneque fashion. The syntactic restrictions
782
on the variable STATE are enforced by the translate mechanism (see
783
*note TRANS:: and see *note TERM::) when terms are read.
785
To prevent the novice user from seeing messages prohibiting certain
786
uses of the variable symbol STATE ACL2 has a mode in which it simply
787
disallows the use of that symbol as a formal parameter. Use of the
788
symbol causes a simple error message. The system is initially in that
791
To get out of that mode, execute:
793
:set-state-ok t ;;; or, (set-state-ok t)
795
It is not recommended that you do this until you have read the
796
documentation of STATE.
798
To enter the mode in which use of state is prohibited as a formal
803
The mode is stored in the defaults table, See *Note
804
ACL2-DEFAULTS-TABLE::. Thus, the mode may be set locally in books.
807
File: acl2-doc-emacs.info, Node: SET-VERIFY-GUARDS-EAGERNESS, Next: SET-WELL-FOUNDED-RELATION, Prev: SET-STATE-OK, Up: EVENTS
809
SET-VERIFY-GUARDS-EAGERNESS the eagerness with which guard verification is tried.
811
Example Forms: try guard verification?
812
(set-verify-guards-eagerness 0) ; no, unless :verify-guards t
813
(set-verify-guards-eagerness 1) ; yes if a :guard is supplied
814
(set-verify-guards-eagerness 2) ; yes, unless :verify-guards nil
816
Note: This is an event! It does not print the usual event summary but
817
nevertheless changes the ACL2 logical world and is so recorded.
820
(set-verify-guards-eagerness n)
822
where n is a variable-free term that evaluates to 0, 1, or 2. This
823
macro is essentially equivalent to
825
(table acl2-defaults-table :verify-guards-eagerness n)
827
and hence is local to any books and encapsulate events in which it
828
occurs; see *note ACL2-DEFAULTS-TABLE::. However, unlike the above
829
simple call of the table event function (see *note TABLE::), no output
830
results from a set-verify-guards-eagerness event.
832
Set-verify-guards-eagerness may be thought of as an event that merely
833
sets a flag to 0, 1, or 2. The flag is used by certain defun events to
834
determine whether guard verification is tried. The flag is irrelevant
835
to those defun events in :program mode and to those defun events in
836
which an explicit :verify-guards setting is provided among the xargs.
837
In the former case, guard verification is not done because it can only
838
be done when logical functions are being defined. In the latter case,
839
the explicit :verify-guards setting determines whether guard
840
verification is tried. So consider a :logic mode defun in which no
841
:verify-guards setting is provided. Is guard verification tried? The
842
answer depends on the eagerness setting as follows. If the eagerness
843
is 0, guard verification is not tried. If the eagerness is 1, it is
844
tried iff a :guard is explicitly provided in the defun. If the
845
eagerness is 2, guard verification is tried.
847
The default behavior of the system is as though the
848
:verify-guards-eagerness is 1. The current behavior can be ascertained
849
by evaluating the form (default-verify-guards-eagerness (w state)).
852
File: acl2-doc-emacs.info, Node: SET-WELL-FOUNDED-RELATION, Next: TABLE, Prev: SET-VERIFY-GUARDS-EAGERNESS, Up: EVENTS
854
SET-WELL-FOUNDED-RELATION set the default well-founded relation
857
(set-well-founded-relation lex2)
859
provided lex2 has been proved to be a well-founded relation (see *note
860
WELL-FOUNDED-RELATION::). Note: This is an event! It does not print
861
the usual event summary but nevertheless changes the ACL2 logical world
865
(set-well-founded-relation rel)
867
where rel has been proved to be a well-founded relation on objects
868
satisfying some predicate, mp; see *note WELL-FOUNDED-RELATION::. This
869
macro is equivalent to (table acl2-defaults-table
870
:well-founded-relation 'rel), and hence is local to any books and
871
encapsulate events in which it occurs; see *note ACL2-DEFAULTS-TABLE::.
873
This event sets the default well-founded relation to be that imposed on
874
mp-measures by the relation rel. Subsequently, if a recursively
875
defined function is submitted to defun with no explicitly given
876
:well-founded-relation argument, defun uses the default relation, rel,
877
and the associated domain predicate mp used in its well-foundedness
878
theorem. That is, the termination conditions generated will require
879
proving that the measure used by the defun is an mp-measure and that in
880
every recursive call the measure of the arguments decreases according
884
File: acl2-doc-emacs.info, Node: TABLE, Next: TERM-TABLE, Prev: SET-WELL-FOUNDED-RELATION, Up: EVENTS
886
TABLE user-managed tables
889
(table tests 1 '(...)) ; set contents of tests[1] to '(...)
890
(table tests 25) ; get contents of tests[25]
891
(table tests) ; return table tests as an alist
892
(table tests nil nil :clear) ; clear table tests
893
(table tests nil '((foo . 7)) :clear) ; set table tests to (foo 7)
894
(table tests nil nil :guard) ; fetch the table guard
895
(table tests nil nil :guard term) ; set the table guard
898
(table table-name key-term value-term op term)
900
where table-name is a symbol that is the name of a (possibly new)
901
table, key-term and value-term, if present, are arbitrary terms
902
involving (at most) the single variable world, op, if present, is one
903
of the table operations below, and term, if present, is a term. Table
904
returns an acl2 "error triple." The effect of table on state depends on
905
op and how many arguments are presented. Some invocations actually
906
have no effect on the ACL2 world and hence an invocation of table is
907
not always an "event". We explain below, after giving some background
910
Important Note: The table forms above are calls of a macro that expand
911
to involve the special variable state. This will prevent you from
912
accessing a table from within a hint or theory where where you do not
913
have the state variable. However, the form
915
(table-alist 'tests world)
917
returns the alist representation of the table named test in the given
918
world. Often you have access to world.
920
The ACL2 system provides "tables" by which the user can associate one
921
object with another. Tables are in essence just conventional
922
association lists -- lists of pairs -- but the ACL2 environment
923
provides a means of storing these lists in the "ACL2 world" of the
924
current state. The ACL2 user could accomplish the same ends by using
925
ACL2 "global variables;" however, limitations on global variable names
926
are imposed to ensure ACL2's soundness. By convention, no table is
927
important to ACL2's soundness, even though some features of the system
928
use tables, and the user is invited to make free use of tables.
929
Because tables are stored in the ACL2 world they are restored by
930
include-book and undone by :ubt. Many users of Nqthm requested a
931
facility by which user data could be saved in Nqthm "lib files" and
932
tables are ACL2's answer to that request.
934
Abstractly, each table is an association list mapping "keys" to
935
"values." In addition, each table has a ":guard," which is a term that
936
must be true of any key and value used. By setting the :guard on a
937
table you may enforce an invariant on the objects in the table, e.g.,
938
that all keys are positive integers and all values are symbols. Each
939
table has a "name," which must be a symbol. Given a table name, there
940
are six operations one might perform on the table.
942
:put -- associate a value with a key (possibly changing the value
943
currently associated with that key).
945
:get -- retrieve the value associated with a key (or nil if no value
946
has been associated with that key).
948
:alist -- return an alist showing all keys and non-nil values in the
951
:clear -- clear the table (so that every value is nil), or if val is
952
supplied then set table to that value (which must be an alist).
954
:guard -- fetch or set the :guard of the table.
956
When the operations above suggest that the table or its :guard are
957
modified, what is actually meant is that the current state is redefined
958
so that in it, the affected table name has the appropriate properties.
959
in such cases, the table form is an event (see *note EVENTS::). In the
960
:put case, if the key is already in the table and associated with the
961
proposed value, then the table event is redundant (see *note
964
Table forms are commonly typed by the user while interacting with the
965
system. :Put and :get forms are especially common. Therefore, we have
966
adopted a positional syntax that is intended to be convenient for most
967
applications. Essentially, some operations admit a "short form" of
970
(table name key-term value-term :put) ; long form
971
(table name key-term value-term) ; short form
973
evaluates the key- and value-terms, obtaining two objects that we call
974
key and value, checks that the key and value satisfy the :guard on the
975
named table and then "modifies" the named table so that the value
976
associated with key is value. When used like this, table is actually
977
an event in the sense that it changes the ACL2 world. In general, the
978
forms evaluated to obtain the key and value may involve the variable
979
world, which is bound to the then-current world during the evaluation
980
of the forms. However, in the special case that the table in question
981
is named acl2-defaults-table, the key and value terms may not contain
982
any variables. Essentially, the keys and values used in events setting
983
the acl2-defaults-table must be explicitly given constants. See *Note
984
ACL2-DEFAULTS-TABLE::.
986
(table name key-term nil :get) ; long form
987
(table name key-term) ; short form
989
evaluates the key-term (see note below), obtaining an object, key, and
990
returns the value associated with key in the named table (or, nil if
991
there is no value associated with key). When used like this, table is
992
not an event; the value is simply returned.
994
(table name nil nil :alist) ; long form
995
(table name) ; short form
997
returns an alist representing the named table; for every key in the
998
table with a non-nil associated value, the alist pairs the key and its
999
value. The order in which the keys are presented is unspecified. When
1000
used like this, table is not an event; the alist is simply returned.
1002
(table name nil val :clear)
1004
sets the named table to the alist val, making the checks that :put
1005
makes for each key and value of val. When used like this, table is an
1006
event because it changes the ACL2 world.
1008
(table name nil nil :guard)
1010
returns the translated form of the guard of the named table.
1012
(table name nil nil :guard term)
1014
Provided the named table is empty and has not yet been assigned a
1015
:guard and term (which is not evaluated) is a term that mentions at
1016
most the variables key, val and world, this event sets the :guard of
1017
the named table to term. Whenever a subsequent :put occurs, term will
1018
be evaluated with key bound to the key argument of the :put, val bound
1019
to the val argument of the :put, and world bound to the then current
1020
world. An error will be caused by the :put if the result of the
1023
Note that it is not allowed to change the :guard on a table once it has
1024
been explicitly set. Before the :guard is explicitly set, it is
1025
effectively just t. After it is set it can be changed only by undoing
1026
the event that set it. The purpose of this restriction is to prevent
1027
the user from changing the :guards on tables provided by other people
1030
The intuition behind the :guard mechanism on tables is to enforce
1031
invariants on the keys and values in a table, so that the values, say,
1032
can be used without run-time checking. But if the :guard of a table is
1033
sensitive to the ACL2 world, it may be possible to cause some value in
1034
the table to cease satisfying the :guard without doing any operations
1035
on the table. Consider for example the :guard "no value in this table
1036
is the name of an event." As described, that is enforced each time a
1037
value is stored. Thus, 'bang can be :put in the table provided there
1038
is no event named bang. But once it is in the table, there is nothing
1039
to prevent the user from defining bang as a function, causing the table
1040
to contain a value that could not be :put there anymore. Observe that
1041
not all state-sensitive :guards suffer this problem. The :guard "every
1042
value is an event name" remains invariant, courtesy of the fact that
1043
undoing back through an event name in the table would necessarily undo
1044
the :put of the name into the table.
1046
Table was designed primarily for convenient top-level use. Tables are
1047
not especially efficient. Each table is represented by an alist stored
1048
on the property list of the table name. :Get is just a getprop and
1049
assoc-equal. :Put does a getprop to the get the table alist, a
1050
put-assoc-equal to record the new association, and a putprop to store
1051
the new table alist -- plus the overhead associated with :guards and
1052
undoable events, and checking (for redundancy) if the key is already
1053
bound to its proposed value. Note that there are never duplicate keys
1054
in the resulting alist; in particular, when the operation :clear is
1055
used to install new alist, duplicate keys are removed from that alist.
1057
A table name may be any symbol whatsoever. Symbols already in use as
1058
function or theorem names, for example, may be used as table names.
1059
Symbols in use only as table names may be defined with defun, etc.
1060
Because there are no restrictions on the user's choice of table names,
1061
table names are not included among the logical names. Thus, :pe name
1062
will never display a table event (for a logical name other than :here).
1063
Either :pe name will display a "normal" event such as (defun name ...)
1064
or (defthm name ...) or else :pe name will cause an error indicating
1065
that name is not a logical name. This happens even if name is in use
1066
as a table name. Similarly, we do not permit table names to have
1067
documentation strings, since the same name might already have a
1068
documentation string. If you want to associate a documentation string
1069
with a table name that is being used no other way, define the name as a
1070
label and use the :doc feature of deflabel (see *note DEFLABEL::); also
1074
File: acl2-doc-emacs.info, Node: TERM-TABLE, Next: THEORY-INVARIANT, Prev: TABLE, Up: EVENTS
1076
TERM-TABLE a table used to validate meta rules
129
:Docs "compile" will find all documented topics mentioning the
133
When the :docs command is given a stringp argument it searches the text
134
produced by :doc and :more-doc and lists all the documented topics whose
135
text contains the given string. For purposes of this string matching we
136
ignore distinctions of case and the amount and kind (but not presence)
137
of white space. We also treat hyphen as whitespace.
142
File: acl2-doc-emacs.info, Node: ARRAYS, Next: BACKCHAIN-LIMIT, Prev: APROPOS, Up: MISCELLANEOUS
144
ARRAYS an introduction to ACL2 arrays.
146
Below we begin a detailed presentation of ACL2 arrays. ACL2's
147
single-threaded objects (see *Note STOBJ::) provide a similar
148
functionality that is generally more efficient but also more
156
* AREF1:: access the elements of a 1-dimensional array
158
* AREF2:: access the elements of a 2-dimensional array
160
* ARRAY1P:: recognize a 1-dimensional array
162
* ARRAY2P:: recognize a 2-dimensional array
164
* ARRAYS-EXAMPLE:: an example illustrating ACL2 arrays.
166
* ASET1:: set the elements of a 1-dimensional array
168
* ASET2:: set the elements of a 2-dimensional array
170
* COMPRESS1:: remove irrelevant pairs from a 1-dimensional array
172
* COMPRESS2:: remove irrelevant pairs from a 2-dimensional array
174
* DEFAULT:: return the :default from the header of a 1- or 2-dimensional array
176
* DIMENSIONS:: return the :dimensions from the header of a 1- or 2-dimensional array
178
* FLUSH-COMPRESS:: flush the under-the-hood array for the given name
180
* HEADER:: return the header of a 1- or 2-dimensional array
182
* MAXIMUM-LENGTH:: return the :maximum-length from the header of an array
184
* SLOW-ARRAY-WARNING:: a warning issued when arrays are used inefficiently
187
See *Note ARRAYS-EXAMPLE:: for a brief introduction illustrating the use
190
ACL2 provides relatively efficient 1- and 2-dimensional arrays. Arrays
191
are awkward to provide efficiently in an applicative language because
192
the programmer rightly expects to be able to "modify" an array object
193
with the effect of changing the behavior of the element accessing
194
function on that object. This, of course, does not make any sense in an
195
applicative setting. The element accessing function is, after all, a
196
function, and its behavior on a given object is immutable. To "modify"
197
an array object in an applicative setting we must actually produce a new
198
array object. Arranging for this to be done efficiently is a challenge
199
to the implementors of the language. In addition, the programmer
200
accustomed to the von Neumann view of arrays must learn how to use
201
immutable applicative arrays efficiently.
203
In this note we explain 1-dimensional arrays. In particular, we explain
204
briefly how to create, access, and "modify" them, how they are
205
implemented, and how to program with them. 2-dimensional arrays are
206
dealt with by analogy.
208
*The Logical Description of ACL2 Arrays*
210
An ACL2 1-dimensional array is an object that associates arbitrary
211
objects with certain integers, called "indices." Every array has a
212
dimension, dim, which is a positive integer. The indices of an array
213
are the consecutive integers from 0 through dim-1. To obtain the object
214
associated with the index i in an array a, one uses (aref1 name a i).
215
Name is a symbol that is irrelevant to the semantics of aref1 but
216
affects the speed with which it computes. We will talk more about array
217
"names" later. To produce a new array object that is like a but which
218
associates val with index i, one uses (aset1 name a i val).
220
An ACL2 1-dimensional array is actually an alist. There is no special
221
ACL2 function for creating arrays; they are generally built with the
222
standard list processing functions list and cons. However, there is a
223
special ACL2 function, called compress1, for speeding up access to the
224
elements of such an alist. We discuss compress1 later.
226
One element of the alist must be the "header" of the array. The header
227
of a 1-dimensional array with dimension dim is of the form:
229
(:HEADER :DIMENSIONS (dim)
231
:DEFAULT obj ; optional
232
:NAME name ; optional
233
:ORDER order ; optional values are < (the default), >, or :none
236
Obj may be any object and is called the "default value" of the array.
237
Max must be an integer greater than dim. Name must be a symbol. The
238
:default and :name entries are optional; if :default is omitted, the
239
default value is nil. The function header, when given a name and a 1-
240
or 2-dimensional array, returns the header of the array. The functions
241
dimensions, maximum-length, and default are similar and return the
242
corresponding fields of the header of the array. The role of the
243
:dimensions field is obvious: it specifies the legal indices into the
244
array. The roles played by the :maximum-length and :default fields are
247
Aside from the header, the other elements of the alist must each be of
248
the form (i . val), where i is an integer and 0 <= i < dim, and val is
251
The :order field of the header is ignored for 2-dimensional arrays. For
252
1-dimensional arrays, it specifies the order of keys (i, above) when the
253
array is compressed with compress1, as described below. An :order of
254
:none specifies no reordering of the alist compress1, and an order of >
255
specifies reordering by compress1 so that keys are in descending order.
256
Otherwise, the alist is reordered by compress1 so that keys are in
259
(Aref1 name a i) is guarded so that name must be a symbol, a must be an
260
array and i must be an index into a. The value of (aref1 name a i) is
261
either (cdr (assoc i a)) or else is the default value of a, depending on
262
whether there is a pair in a whose car is i. Note that name is
263
irrelevant to the value of an aref1 expression. You might :pe aref1 to
264
see how simple the definition is.
266
(Aset1 name a i val) is guarded analogously to the aref1 expression.
267
The value of the aset1 expression is essentially (cons (cons i val) a).
268
Again, name is irrelevant. Note (aset1 name a i val) is an array, a',
269
with the property that (aref1 name a' i) is val and, except for index i,
270
all other indices into a' produce the same value as in a. Note also
271
that if a is viewed as an alist (which it is) the pair "binding" i to
272
its old value is in a' but "covered up" by the new pair. Thus, the
273
length of an array grows by one when aset1 is done.
275
Because aset1 covers old values with new ones, an array produced by a
276
sequence of aset1 calls may have many irrelevant pairs in it. The
277
function compress1 can remove these irrelevant pairs. Thus, (compress1
278
name a) returns an array that is equivalent (vis-a-vis aref1) to a but
279
which may be shorter. For technical reasons, the alist returned by
280
compress1 may also list the pairs in a different order than listed in a.
282
To prevent arrays from growing excessively long due to repeated aset1
283
operations, aset1 actually calls compress1 on the new alist whenever the
284
length of the new alist exceeds the :maximum-length entry, max, in the
285
header of the array. See the definition of aset1 (for example by using
286
:pe). This is primarily just a mechanism for freeing up cons space
287
consumed while doing aset1 operations. Note however that this compress1
288
call is replaced by a hard error if the header specifies an :order of
291
This completes the logical description of 1-dimensional arrays.
292
2-dimensional arrays are analogous. The :dimensions entry of the header
293
of a 2-dimensional array should be (dim1 dim2). A pair of indices, i
294
and j, is legal iff 0 <= i < dim1 and 0 <= j < dim2. The
295
:maximum-length must be greater than dim1*dim2. Aref2, aset2, and
296
compress2 are like their counterparts but take an additional index
297
argument. Finally, the pairs in a 2-dimensional array are of the form
300
*The Implementation of ACL2 Arrays*
302
Very informally speaking, the function compress1 "creates" an ACL2 array
303
that provides fast access, while the function aref1 "maintains" fast
304
access. We now describe this informal idea more carefully.
306
Aref1 is essentially assoc. If aref1 were implemented naively the time
307
taken to access an array element would be linear in the dimension of the
308
array and the number of "assignments" to it (the number of aset1 calls
309
done to create the array from the initial alist). This is intolerable;
310
arrays are "supposed" to provide constant-time access and change.
312
The apparently irrelevant names associated with ACL2 arrays allow us to
313
provide constant-time access and change when arrays are used in
314
"conventional" ways. The implementation of arrays makes it clear what
315
we mean by "conventional."
317
Recall that array names are symbols. Behind the scenes, ACL2 associates
318
two objects with each ACL2 array name. The first object is called the
319
"semantic value" of the name and is an alist. The second object is
320
called the "raw lisp array" and is a Common Lisp array.
322
When (compress1 name alist) builds a new alist, a', it sets the semantic
323
value of name to that new alist. Furthermore, it creates a Common Lisp
324
array and writes into it all of the index/value pairs of a',
325
initializing unassigned indices with the default value. This array
326
becomes the raw lisp array of name. Compress1 then returns a', the
327
semantic value, as its result, as required by the definition of
330
When (aref1 name a i) is invoked, aref1 first determines whether the
331
semantic value of name is a (i.e., is eq to the alist a). If so, aref1
332
can determine the ith element of a by invoking Common Lisp's aref
333
function on the raw lisp array associated with name. Note that no
334
linear search of the alist a is required; the operation is done in
335
constant time and involves retrieval of two global variables, an eq test
336
and jump, and a raw lisp array access. In fact, an ACL2 array access of
337
this sort is about 5 times slower than a C array access. On the other
338
hand, if name has no semantic value or if it is different from a, then
339
aref1 determines the answer by linear search of a as suggested by the
340
assoc-like definition of aref1. Thus, aref1 always returns the
341
axiomatically specified result. It returns in constant time if the
342
array being accessed is the current semantic value of the name used.
343
The ramifications of this are discussed after we deal with aset1.
345
When (aset1 name a i val) is invoked, aset1 does two conses to create
346
the new array. Call that array a'. It will be returned as the answer.
347
(In this discussion we ignore the case in which aset1 does a compress1.)
348
However, before returning, aset1 determines if name's semantic value is
349
a. If so, it makes the new semantic value of name be a' and it smashes
350
the raw lisp array of name with val at index i, before returning a' as
351
the result. Thus, after doing an aset1 and obtaining a new semantic
352
value a', all aref1s on that new array will be fast. Any aref1s on the
353
old semantic value, a, will be slow.
355
To understand the performance implications of this design, consider the
356
chronological sequence in which ACL2 (Common Lisp) evaluates
357
expressions: basically inner-most first, left-to-right, call-by-value.
358
An array use, such as (aref1 name a i), is "fast" (constant-time) if the
359
alist supplied, a, is the value returned by the most recently executed
360
compress1 or aset1 on the name supplied. In the functional expression
361
of "conventional" array processing, all uses of an array are fast.
363
The :name field of the header of an array is completely irrelevant. Our
364
convention is to store in that field the symbol we mean to use as the
365
name of the raw lisp array. But no ACL2 function inspects :name and its
366
primary value is that it allows the user, by inspecting the semantic
367
value of the array -- the alist -- to recall the name of the raw array
368
that probably holds that value. We say "probably" since there is no
369
enforcement that the alist was compressed under the name in the header
370
or that all asets used that name. Such enforcement would be
373
*Some Programming Examples*
375
In the following examples we will use ACL2 "global variables" to hold
376
several arrays. See *Note @: atsign, and see *Note ASSIGN::.
378
Let the state global variable a be the 1-dimensional compressed array of
379
dimension 5 constructed below.
381
ACL2 !>(assign a (compress1 'demo
382
'((:header :dimensions (5)
384
:default uninitialized
388
Then (aref1 'demo (@ a) 0) is zero and (aref1 'demo (@ a) 1) is
393
ACL2 !>(assign b (aset1 'demo (@ a) 1 'one))
395
Then (aref1 'demo (@ b) 0) is zero and (aref1 'demo (@ b) 1) is one.
397
All of the aref1s done so far have been "fast."
399
Note that we now have two array objects, one in the global variable a
400
and one in the global variable b. B was obtained by assigning to a.
401
That assignment does not affect the alist a because this is an
402
applicative language. Thus, (aref1 'demo (@ a) 1) must *still* be
403
uninitialized. And if you execute that expression in ACL2 you will see
404
that indeed it is. However, a rather ugly comment is printed, namely
405
that this array access is "slow." The reason it is slow is that the raw
406
lisp array associated with the name demo is the array we are calling b.
407
To access the elements of a, aref1 must now do a linear search. Any
408
reference to a as an array is now "unconventional;" in a conventional
409
language like Ada or Common Lisp it would simply be impossible to refer
410
to the value of the array before the assignment that produced our b.
412
Now let us define a function that counts how many times a given object,
413
x, occurs in an array. For simplicity, we will pass in the name and
414
highest index of the array:
416
ACL2 !>(defun cnt (name a i x)
417
(declare (xargs :guard
418
(and (array1p name a)
421
(< i (car (dimensions name a))))
423
:measure (nfix (+ 1 i))))
424
(cond ((zp (1+ i)) 0) ; return 0 if i is at most -1
425
((equal x (aref1 name a i))
426
(1+ (cnt name a (1- i) x)))
427
(t (cnt name a (1- i) x))))
429
To determine how many times zero appears in (@ b) we can execute:
431
ACL2 !>(cnt 'demo (@ b) 4 'zero)
433
The answer is 1. How many times does uninitialized appear in (@ b)?
435
ACL2 !>(cnt 'demo (@ b) 4 'uninitialized)
437
The answer is 3, because positions 2, 3 and 4 of the array contain that
440
Now imagine that we want to assign 'two to index 2 and then count how
441
many times the 2nd element of the array occurs in the array. This
442
specification is actually ambiguous. In assigning to b we produce a new
443
array, which we might call c. Do we mean to count the occurrences in c
444
of the 2nd element of b or the 2nd element of c? That is, do we count
445
the occurrences of uninitialized or the occurrences of two? If we mean
446
the former the correct answer is 2 (positions 3 and 4 are uninitialized
447
in c); if we mean the latter, the correct answer is 1 (there is only one
448
occurrence of two in c).
450
Below are ACL2 renderings of the two meanings, which we call [former]
451
and [latter]. (Warning: Our description of these examples, and of an
452
example [fast former] that follows, assumes that only one of these three
453
examples is actually executed; for example, they are not executed in
454
sequence. See "A Word of Warning" below for more about this issue.)
456
(cnt 'demo (aset1 'demo (@ b) 2 'two) 4 (aref1 'demo (@ b) 2)) ; [former]
458
(let ((c (aset1 'demo (@ b) 2 'two))) ; [latter]
459
(cnt 'demo c 4 (aref1 'demo c 2)))
461
Note that in [former] we create c in the second argument of the call to
462
cnt (although we do not give it a name) and then refer to b in the
463
fourth argument. This is unconventional because the second reference to
464
b in [former] is no longer the semantic value of demo. While ACL2
465
computes the correct answer, namely 2, the execution of the aref1
466
expression in [former] is done slowly.
468
A conventional rendering with the same meaning is
470
(let ((x (aref1 'demo (@ b) 2))) ; [fast former]
471
(cnt 'demo (aset1 'demo (@ b) 2 'two) 4 x))
473
which fetches the 2nd element of b before creating c by assignment. It
474
is important to understand that [former] and [fast former] mean exactly
475
the same thing: both count the number of occurrences of uninitialized in
476
c. Both are legal ACL2 and both compute the same answer, 2. Indeed, we
477
can symbolically transform [fast former] into [former] merely by
478
substituting the binding of x for x in the body of the let. But [fast
479
former] can be evaluated faster than [former] because all of the
480
references to demo use the then-current semantic value of demo, which is
481
b in the first line and c throughout the execution of the cnt in the
482
second line. [Fast former] is the preferred form, both because of its
483
execution speed and its clarity. If you were writing in a conventional
484
language you would have to write something like [fast former] because
485
there is no way to refer to the 2nd element of the old value of b after
486
smashing b unless it had been saved first.
488
We turn now to [latter]. It is both clear and efficient. It creates c
489
by assignment to b and then it fetches the 2nd element of c, two, and
490
proceeds to count the number of occurrences in c. The answer is 1.
491
[Latter] is a good example of typical ACL2 array manipulation: after the
492
assignment to b that creates c, c is used throughout.
494
It takes a while to get used to this because most of us have grown
495
accustomed to the peculiar semantics of arrays in conventional
496
languages. For example, in raw lisp we might have written something
497
like the following, treating b as a "global variable":
499
(cnt 'demo (aset 'demo b 2 'two) 4 (aref 'demo b 2))
501
which sort of resembles [former] but actually has the semantics of
502
[latter] because the b from which aref fetches the 2nd element is not
503
the same b used in the aset! The array b is destroyed by the aset and b
504
henceforth refers to the array produced by the aset, as written more
507
A Word of Warning: Users must exercise care when experimenting with
508
[former], [latter] and [fast former]. Suppose you have just created b
509
with the assignment shown above,
511
ACL2 !>(assign b (aset1 'demo (@ a) 1 'one))
513
If you then evaluate [former] in ACL2 it will complain that the aref1 is
514
slow and compute the answer, as discussed. Then suppose you evaluate
515
[latter] in ACL2. From our discussion you might expect it to execute
516
fast -- i.e., issue no complaint. But in fact you will find that it
517
complains repeatedly. The problem is that the evaluation of [former]
518
changed the semantic value of demo so that it is no longer b. To try
519
the experiment correctly you must make b be the semantic value of demo
520
again before the next example is evaluated. One way to do that is to
523
ACL2 !>(assign b (compress1 'demo (@ b)))
525
before each expression. Because of issues like this it is often hard to
526
experiment with ACL2 arrays at the top-level. We find it easier to
527
write functions that use arrays correctly and efficiently than to so use
530
This last assignment also illustrates a very common use of compress1.
531
While it was introduced as a means of removing irrelevant pairs from an
532
array built up by repeated assignments, it is actually most useful as a
533
way of insuring fast access to the elements of an array.
535
Many array processing tasks can be divided into two parts. During the
536
first part the array is built. During the second part the array is used
537
extensively but not modified. If your programming task can be so
538
divided, it might be appropriate to construct the array entirely with
539
list processing, thereby saving the cost of maintaining the semantic
540
value of the name while few references are being made. Once the alist
541
has stabilized, it might be worthwhile to treat it as an array by
542
calling compress1, thereby gaining constant time access to it.
544
ACL2's theorem prover uses this technique in connection with its
545
implementation of the notion of whether a rune is disabled or not.
546
Associated with every rune is a unique integer index, called its "nume."
547
When each rule is stored, the corresponding nume is stored as a
548
component of the rule. Theories are lists of runes and membership in
549
the "current theory" indicates that the corresponding rule is enabled.
550
But these lists are very long and membership is a linear-time operation.
551
So just before a proof begins we map the list of runes in the current
552
theory into an alist that pairs the corresponding numes with t. Then we
553
compress this alist into an array. Thus, given a rule we can obtain its
554
nume (because it is a component) and then determine in constant time
555
whether it is enabled. The array is never modified during the proof,
556
i.e., aset1 is never used in this example. From the logical perspective
557
this code looks quite odd: we have replaced a linear-time membership
558
test with an apparently linear-time assoc after going to the trouble of
559
mapping from a list of runes to an alist of numes. But because the
560
alist of numes is an array, the "apparently linear-time assoc" is more
561
apparent than real; the operation is constant-time.
566
File: acl2-doc-emacs.info, Node: AREF1, Next: AREF2, Prev: ARRAYS, Up: ARRAYS
568
AREF1 access the elements of a 1-dimensional array
572
(aref1 'delta1 a (+ i k))
575
(aref1 name alist index)
577
where name is a symbol, alist is a 1-dimensional array and index is a
578
legal index into alist. This function returns the value associated with
579
index in alist, or else the default value of the array. See *Note
580
ARRAYS:: for details.
582
This function executes in virtually constant time if alist is in fact
583
the "semantic value" associated with name (see *Note ARRAYS::). When it
584
is not, aref1 must do a linear search through alist. In that case the
585
correct answer is returned but a *slow array* comment is printed to the
586
comment window. See *Note SLOW-ARRAY-WARNING::.
591
File: acl2-doc-emacs.info, Node: AREF2, Next: ARRAY1P, Prev: AREF1, Up: ARRAYS
593
AREF2 access the elements of a 2-dimensional array
597
(aref2 'delta1 a i j)
600
(aref2 name alist i j)
602
where name is a symbol, alist is a 2-dimensional array and i and j are
603
legal indices into alist. This function returns the value associated
604
with (i . j) in alist, or else the default value of the array. See
605
*Note ARRAYS:: for details.
607
This function executes in virtually constant time if alist is in fact
608
the "semantic value" associated with name (see *Note ARRAYS::). When it
609
is not, aref2 must do a linear search through alist. In that case the
610
correct answer is returned but a *slow array* comment is printed to the
611
comment window. See *Note SLOW-ARRAY-WARNING::.
616
File: acl2-doc-emacs.info, Node: ARRAY1P, Next: ARRAY2P, Prev: AREF2, Up: ARRAYS
618
ARRAY1P recognize a 1-dimensional array
627
where name and alist are arbitrary objects. This function returns t if
628
alist is a 1-dimensional ACL2 array. Otherwise it returns nil. The
629
function operates in constant time if alist is the semantic value of
630
name. See *Note ARRAYS::.
635
File: acl2-doc-emacs.info, Node: ARRAY2P, Next: ARRAYS-EXAMPLE, Prev: ARRAY1P, Up: ARRAYS
637
ARRAY2P recognize a 2-dimensional array
646
where name and alist are arbitrary objects. This function returns t if
647
alist is a 2-dimensional ACL2 array. Otherwise it returns nil. The
648
function operates in constant time if alist is the semantic value of
649
name. See *Note ARRAYS::.
654
File: acl2-doc-emacs.info, Node: ARRAYS-EXAMPLE, Next: ASET1, Prev: ARRAY2P, Up: ARRAYS
656
ARRAYS-EXAMPLE an example illustrating ACL2 arrays.
658
The example below illustrates the use of ACL2 arrays. It is not, of
659
course, a substitute for the detailed explanations provided elsewhere
660
(see *Note ARRAYS::, including subtopics).
663
ACL2 !>(defun defarray (name size initial-element)
666
:DIMENSIONS (list size)
667
:MAXIMUM-LENGTH (1+ size)
668
:DEFAULT initial-element
672
Since DEFARRAY is non-recursive, its admission is trivial. We observe
673
that the type of DEFARRAY is described by the theorem
674
(AND (CONSP (DEFARRAY NAME SIZE INITIAL-ELEMENT))
675
(TRUE-LISTP (DEFARRAY NAME SIZE INITIAL-ELEMENT))).
676
We used the :type-prescription rule COMPRESS1.
679
Form: ( DEFUN DEFARRAY ...)
680
Rules: ((:TYPE-PRESCRIPTION COMPRESS1))
682
Time: 0.02 seconds (prove: 0.00, print: 0.02, other: 0.00)
684
ACL2 !>(assign my-ar (defarray 'a1 5 17))
685
((:HEADER :DIMENSIONS (5)
686
:MAXIMUM-LENGTH 6 :DEFAULT 17 :NAME A1))
687
ACL2 !>(aref1 'a1 (@ my-ar) 3)
689
ACL2 !>(aref1 'a1 (@ my-ar) 8)
692
ACL2 Error in TOP-LEVEL: The guard for the function symbol AREF1,
694
(AND (ARRAY1P NAME L) (INTEGERP N) (>= N 0) (< N (CAR (DIMENSIONS NAME L)))),
695
is violated by the arguments in the call (AREF1 'A1 '(#) 8).
697
ACL2 !>(assign my-ar (aset1 'a1 (@ my-ar) 3 'xxx))
699
(:HEADER :DIMENSIONS (5)
700
:MAXIMUM-LENGTH 6 :DEFAULT 17 :NAME A1))
701
ACL2 !>(aref1 'a1 (@ my-ar) 3)
703
ACL2 !>(aset1 'a1 (@ my-ar) 3 'yyy) ; BAD: (@ my-ar) now points to
704
; an old copy of the array!
707
(:HEADER :DIMENSIONS (5)
708
:MAXIMUM-LENGTH 6 :DEFAULT 17 :NAME A1))
709
ACL2 !>(aref1 'a1 (@ my-ar) 3) ; Because of "BAD" above, the array
710
; access is done using assoc rather
711
; than Lisp aref, hence is slower;
712
; but the answer is still correct,
713
; reflecting the value in (@ my-ar),
714
; which was not changed above.
717
**********************************************************
718
Slow Array Access! A call of AREF1 on an array named
719
A1 is being executed slowly. See :DOC slow-array-warning
720
**********************************************************
729
File: acl2-doc-emacs.info, Node: ASET1, Next: ASET2, Prev: ARRAYS-EXAMPLE, Up: ARRAYS
731
ASET1 set the elements of a 1-dimensional array
735
(aset1 'delta1 a (+ i k) 27)
738
(aset1 name alist index val)
740
where name is a symbol, alist is a 1-dimensional array named name, index
741
is a legal index into alist, and val is an arbitrary object. See *Note
742
ARRAYS:: for details. Roughly speaking this function "modifies" alist
743
so that the value associated with index is val. More precisely, it
744
returns a new array, alist', of the same name and dimension as alist
745
that, under aref1, is everywhere equal to alist except at index where
746
the result is val. That is, (aref1 name alist' i) is (aref1 name alist
747
i) for all legal indices i except index, where (aref1 name alist' i) is
750
In order to "modify" alist, aset1 conses a new pair onto the front. If
751
the length of the resulting alist exceeds the :maximum-length entry in
752
the array header, aset1 compresses the array as with compress1.
754
It is generally expected that the "semantic value" of name will be alist
755
(see *Note ARRAYS::). This function operates in virtually constant time
756
whether this condition is true or not (unless the compress1 operation is
757
required). But the value returned by this function cannot be used
758
efficiently by subsequent aset1 operations unless alist is the semantic
759
value of name when aset1 is executed. Thus, if the condition is not
760
true, aset1 prints a *slow array* warning to the comment window. See
761
*Note SLOW-ARRAY-WARNING::.
766
File: acl2-doc-emacs.info, Node: ASET2, Next: COMPRESS1, Prev: ASET1, Up: ARRAYS
768
ASET2 set the elements of a 2-dimensional array
772
(aset2 'delta1 a i j 27)
775
(aset2 name alist i j val)
777
where name is a symbol, alist is a 2-dimensional array named name, i and
778
j are legal indices into alist, and val is an arbitrary object. See
779
*Note ARRAYS:: for details. Roughly speaking this function "modifies"
780
alist so that the value associated with (i . j) is val. More precisely,
781
it returns a new array, alist', of the same name and dimension as alist
782
that, under aref2, is everywhere equal to alist except at (i . j) where
783
the result is val. That is, (aref2 name alist' x y) is (aref2 name
784
alist x y) for all legal indices x y except i and j where (aref2 name
787
In order to "modify" alist, aset2 conses a new pair onto the front. If
788
the length of the resulting alist exceeds the :maximum-length entry in
789
the array header, aset2 compresses the array as with compress2.
791
It is generally expected that the "semantic value" of name will be alist
792
(see *Note ARRAYS::). This function operates in virtually constant time
793
whether this condition is true or not (unless the compress2 operation is
794
required). But the value returned by this function cannot be used
795
efficiently by subsequent aset2 operations unless alist is the semantic
796
value of name when aset2 is executed. Thus, if the condition is not
797
true, aset2 prints a *slow array* warning to the comment window. See
798
*Note SLOW-ARRAY-WARNING::.
803
File: acl2-doc-emacs.info, Node: COMPRESS1, Next: COMPRESS2, Prev: ASET2, Up: ARRAYS
805
COMPRESS1 remove irrelevant pairs from a 1-dimensional array
809
(compress1 'delta1 a)
812
(compress1 name alist)
814
where name is a symbol and alist is a 1-dimensional array named name.
815
See *Note ARRAYS:: for details. Logically speaking, this function
816
removes irrelevant pairs from alist, possibly shortening it. The
817
function returns a new array, alist', of the same name and dimension as
818
alist, that, under aref1, is everywhere equal to alist. That is, (aref1
819
name alist' i) is (aref1 name alist i), for all legal indices i. Alist'
820
may be shorter than alist and the non-irrelevant pairs may occur in a
821
different order than in alist.
823
Practically speaking, this function plays an important role in the
824
efficient implementation of aref1. In addition to creating the new
825
array, alist', compress1 makes that array the "semantic value" of name
826
and allocates a raw lisp array to name. For each legal index, i, that
827
raw lisp array contains (aref1 name alist' i) in slot i. Thus,
828
subsequent aref1 operations can be executed in virtually constant time
829
provided they are given name and the alist' returned by the most
830
recently executed compress1 or aset1 on name. See *Note ARRAYS::.
832
In general, compress1 returns an alist whose cdr is an association list
833
whose keys are nonnegative integers in ascending order. However, if the
834
header specifies an :order of > then the keys will occur in descending
835
order, and if the :order is :none then the keys will not be sorted,
836
i.e., compress1 is logically the identity function (though it still
837
attaches an array under the hood).
842
File: acl2-doc-emacs.info, Node: COMPRESS2, Next: DEFAULT, Prev: COMPRESS1, Up: ARRAYS
844
COMPRESS2 remove irrelevant pairs from a 2-dimensional array
848
(compress2 'delta1 a)
851
(compress2 name alist)
853
where name is a symbol and alist is a 2-dimensional array named name.
854
See *Note ARRAYS:: for details. Logically speaking, this function
855
removes irrelevant pairs from alist, possibly shortening it. The
856
function returns a new array, alist', of the same name and dimension as
857
alist, that, under aref2, is everywhere equal to alist. That is, (aref2
858
name alist' i j) is (aref2 name alist i j), for all legal indices i and
859
j. Alist' may be shorter than alist and the non-irrelevant pairs may
860
occur in a different order in alist' than in alist.
862
Practically speaking, this function plays an important role in the
863
efficient implementation of aref2. In addition to creating the new
864
array, alist', compress2 makes that array the "semantic value" of name
865
and allocates a raw lisp array to name. For all legal indices, i and j,
866
that raw lisp array contains (aref2 name alist' i j) in slot i,j. Thus,
867
subsequent aref2 operations can be executed in virtually constant time
868
provided they are given name and the alist' returned by the most
869
recently executed compress2 or aset2 on name. See *Note ARRAYS::.
874
File: acl2-doc-emacs.info, Node: DEFAULT, Next: DIMENSIONS, Prev: COMPRESS2, Up: ARRAYS
876
DEFAULT return the :default from the header of a 1- or 2-dimensional array
885
where name is an arbitrary object and alist is a 1- or 2-dimensional
886
array. This function returns the contents of the :default field of the
887
header of alist. When aref1 or aref2 is used to obtain a value for an
888
index (or index pair) not bound in alist, the default value is returned
889
instead. Thus, the array alist may be thought of as having been
890
initialized with the default value. default operates in virtually
891
constant time if alist is the semantic value of name. See *Note
897
File: acl2-doc-emacs.info, Node: DIMENSIONS, Next: FLUSH-COMPRESS, Prev: DEFAULT, Up: ARRAYS
899
DIMENSIONS return the :dimensions from the header of a 1- or 2-dimensional array
903
(dimensions 'delta1 a)
906
(dimensions name alist)
908
where name is arbitrary and alist is a 1- or 2-dimensional array. This
909
function returns the dimensions list of the array alist. That list will
910
either be of the form (dim1) or (dim1 dim2), depending on whether alist
911
is a 1- or 2-dimensional array. Dim1 and dim2 will be integers and each
912
exceed by 1 the maximum legal corresponding index. Thus, if dimensions
913
returns, say, '(100) for an array a named 'delta1, then (aref1 'delta1 a
914
99) is legal but (aref1 'delta1 a 100) violates the guards on aref1.
915
Dimensions operates in virtually constant time if alist is the semantic
916
value of name. See *Note ARRAYS::.
921
File: acl2-doc-emacs.info, Node: FLUSH-COMPRESS, Next: HEADER, Prev: DIMENSIONS, Up: ARRAYS
923
FLUSH-COMPRESS flush the under-the-hood array for the given name
927
(flush-compress 'my-array)
930
(flush-compress name)
932
where name is a symbol.
934
Recall that (compress1 nm alist) associates an under-the-hood raw Lisp
935
one-dimensional array of name nm with the given association list, alist,
936
while (compress2 nm alist) is the analogous function for two-dimensional
937
arrays; see *Note COMPRESS1:: and see *Note COMPRESS2::. The only
938
purpose of flush-compress, which always returns nil, is to remove the
939
association of any under-the-hood array with the given name, thus
940
eliminating slow array accesses (see *Note SLOW-ARRAY-WARNING::). It is
941
not necessary if the return values of compress1 and compress2 are always
942
used as the "current" copy of the named array, and thus flush-compress
943
should rarely, if ever, be needed in user applications.
945
Nevertheless, we provide the following contrived example to show how
946
flush-compress can be used to good effect. Comments have been added to
947
this log to provide explanation.
949
ACL2 !>(assign a (compress1 'demo
950
'((:header :dimensions (5)
952
:default uninitialized
956
((:HEADER :DIMENSIONS (5)
958
15 :DEFAULT UNINITIALIZED :NAME DEMO)
961
ACL2 !>(aref1 'demo (@ a) 0)
963
; As expected, the above evaluation did not cause a slow array warning. Now
964
; we associate a different under-the-hood array with the name 'demo.
965
ACL2 !>(compress1 'demo
966
'((:header :dimensions (5)
968
:default uninitialized
971
((:HEADER :DIMENSIONS (5)
973
15 :DEFAULT UNINITIALIZED :NAME DEMO)
975
; The following array access produces a slow array warning because (@ a) is
976
; no longer associated under-the-hood with the array name 'demo.
977
ACL2 !>(aref1 'demo (@ a) 0)
980
**********************************************************
981
Slow Array Access! A call of AREF1 on an array named
982
DEMO is being executed slowly. See :DOC slow-array-warning
983
**********************************************************
986
; Now we associate under-the-hood, with array name 'demo, an alist equal to
988
ACL2 !>(compress1 'demo
989
'((:header :dimensions (5)
991
:default uninitialized
995
((:HEADER :DIMENSIONS (5)
997
15 :DEFAULT UNINITIALIZED :NAME DEMO)
1000
; The following array access is still slow, because the under-the-hood array
1001
; is merely associated with a copy of (@ a), not with the actual object
1003
ACL2 !>(aref1 'demo (@ a) 0)
1006
**********************************************************
1007
Slow Array Access! A call of AREF1 on an array named
1008
DEMO is being executed slowly. See :DOC slow-array-warning
1009
**********************************************************
1012
; So we might try to fix the problem by recompressing. But this doesn't
1013
; work. It would work, by the way, if we re-assign a:
1014
; (assign a (compress1 'demo (@ a))). That is why we usually will not need
1016
ACL2 !>(compress1 'demo (@ a))
1017
((:HEADER :DIMENSIONS (5)
1019
15 :DEFAULT UNINITIALIZED :NAME DEMO)
1022
ACL2 !>(aref1 'demo (@ a) 0)
1025
**********************************************************
1026
Slow Array Access! A call of AREF1 on an array named
1027
DEMO is being executed slowly. See :DOC slow-array-warning
1028
**********************************************************
1031
; Finally, we eliminate the warning by calling flush-compress before we call
1032
; compress1. The call of flush-compress removes any under-the-hood
1033
; association of an array with the name 'demo. Then the subsequent call of
1034
; compress1 associates the object (@ a) with that name. (Technical point:
1035
; compress1 always associates the indicated name with the value that it
1036
; returns. in this case, what compress1 returns is (@ a), because (@ a) is
1037
; already, logically speaking, a compressed array1p (starts with a :header
1038
; and the natural number keys are ordered).
1039
ACL2 !>(flush-compress 'demo)
1041
ACL2 !>(compress1 'demo (@ a))
1042
((:HEADER :DIMENSIONS (5)
1044
15 :DEFAULT UNINITIALIZED :NAME DEMO)
1047
ACL2 !>(aref1 'demo (@ a) 0)
1055
File: acl2-doc-emacs.info, Node: HEADER, Next: MAXIMUM-LENGTH, Prev: FLUSH-COMPRESS, Up: ARRAYS
1057
HEADER return the header of a 1- or 2-dimensional array
1066
where name is arbitrary and alist is a 1- or 2-dimensional array. This
1067
function returns the header of the array alist. The function operates
1068
in virtually constant time if alist is the semantic value of name. See
1074
File: acl2-doc-emacs.info, Node: MAXIMUM-LENGTH, Next: SLOW-ARRAY-WARNING, Prev: HEADER, Up: ARRAYS
1076
MAXIMUM-LENGTH return the :maximum-length from the header of an array
1080
(maximum-length 'delta1 a)
1083
(maximum-length name alist)
1085
where name is an arbitrary object and alist is a 1- or 2-dimensional
1086
array. This function returns the contents of the :maximum-length field
1087
of the header of alist. Whenever an aset1 or aset2 would cause the
1088
length of the alist to exceed its maximum length, a compress1 or
1089
compress2 is done automatically to remove irrelevant pairs from the
1090
array. Maximum-length operates in virtually constant time if alist is
1091
the semantic value of name. See *Note ARRAYS::.
1096
File: acl2-doc-emacs.info, Node: SLOW-ARRAY-WARNING, Prev: MAXIMUM-LENGTH, Up: ARRAYS
1098
SLOW-ARRAY-WARNING a warning issued when arrays are used inefficiently
1100
If you use ACL2 arrays you may sometimes see a *slow array* warning. We
1101
here explain what that warning means and some likely "mistakes" it may
1104
The discussion in the documentation for arrays defines what we mean by
1105
the semantic value of a name. As noted there, behind the scenes ACL2
1106
maintains the invariant that with some names there is associated a pair
1107
consisting of an ACL2 array alist, called the semantic value of the
1108
name, and an equivalent raw lisp array. Access to ACL2 array elements,
1109
as in (aref1 name alist i), is executed in constant time when the array
1110
alist is the semantic value of the name, because we can just use the
1111
corresponding raw lisp array to obtain the answer. Aset1 and compress1
1112
modify the raw lisp array appropriately to maintain the invariant.
1114
If aref1 is called on a name and alist, and the alist is not the
1115
then-current semantic value of the name, the correct result is computed
1116
but it requires linear time because the alist must be searched. When
1117
this happens, aref1 prints a *slow array* warning message to the comment
1118
window. Aset1 behaves similarly because the array it returns will cause
1119
the *slow array* warning every time it is used.
1121
From the purely logical perspective there is nothing "wrong" about such
1122
use of arrays and it may be spurious to print a warning message. But
1123
because arrays are generally used to achieve efficiency, the *slow
1124
array* warning often means the user's intentions are not being realized.
1125
Sometimes merely performance expectations are not met; but the message
1126
may mean that the functional behavior of the program is different than
1129
Here are some "mistakes" that might cause this behavior. In the
1130
following we suppose the message was printed by aset1 about an array
1131
named name. Suppose the alist supplied aset1 is alist.
1133
(1) Compress1 was never called on name and alist. That is, perhaps you
1134
created an alist that is an array1p and then proceeded to access it with
1135
aref1 but never gave ACL2 the chance to create a raw lisp array for it.
1136
After creating an alist that is intended for use as an array, you must
1137
do (compress1 name alist) and pass the resulting alist' as the array.
1139
(2) Name is misspelled. Perhaps the array was compressed under the name
1140
'delta-1 but accessed under 'delta1?
1142
(3) An aset1 was done to modify alist, producing a new array, alist',
1143
but you subsequently used alist as an array. Inspect all (aset1 name
1144
...) occurrences and make sure that the alist modified is never used
1145
subsequently (either in that function or any other). It is good
1146
practice to adopt the following syntactic style. Suppose the alist you
1147
are manipulating is the value of the local variable alist. Suppose at
1148
some point in a function definition you wish to modify alist with aset1.
1151
(let ((alist (aset1 name alist i val))) ...)
1153
and make sure that the subsequent function body is entirely within the
1154
scope of the let. Any uses of alist subsequently will refer to the new
1155
alist and it is impossible to refer to the old alist. Note that if you
1158
(foo (let ((alist (aset1 name alist i val))) ...) ; arg 1
1159
(bar alist)) ; arg 2
1161
you have broken the rules, because in arg 1 you have modified alist but
1162
in arg 2 you refer to the old value. An appropriate rewriting is to
1165
(let ((alist (aset1 name alist alist i val)))
1167
(bar alist))) ; arg 2
1169
Of course, this may not mean the same thing.
1171
(4) A function which takes alist as an argument and modifies it with
1172
aset1 fails to return the modified version. This is really the same as
1173
(3) above, but focuses on function interfaces. If a function takes an
1174
array alist as an argument and the function uses aset1 (or a subfunction
1175
uses aset1, etc.), then the function probably "ought" to return the
1176
result produced by aset1. The reasoning is as follows. If the array is
1177
passed into the function, then the caller is holding the array. After
1178
the function modifies it, the caller's version of the array is obsolete.
1179
If the caller is going to make further use of the array, it must obtain
1180
the latest version, i.e., that produced by the function.
1079
(table term-table t '((binary-+ x y) '3 'nil (car x)))
1081
See *Note TABLE:: for a general discussion of tables and the table
1082
event used to manipulate tables.
1084
The "term-table" is used at the time a meta rule is checked for
1085
syntactic correctness. Each proposed metafunction is run on each term
1086
in this table, and the result in each case is checked to make sure that
1087
it is a termp in the current world. In each case where this test
1088
fails, a warning is printed.
1090
Whenever a metafunction is run in support of the application of a meta
1091
rule, the result must be a term in the current world. When the result
1092
is not a term, a hard error arises. The term-table is simply a means
1093
for providing feedback to the user at the time a meta rule is
1094
submitted, warning of the definite possibility that such a hard error
1095
will occur at some point in the future.
1097
The key used in term-table is arbitrary. The top-most value is always
1098
the one that is used; it is the entire list of terms to be considered.
1099
Each must be a termp in the current ACL2 world.
added
removed
doc/EMACS/acl2-doc-emacs.info-13
