32
28
* acl2: (acl2-doc-emacs.info). Applicative Common Lisp
40
File: acl2-doc-emacs.info, Node: MAKE-EVENT-DETAILS, Prev: MAKE-EVENT, Up: MAKE-EVENT
42
MAKE-EVENT-DETAILS details on make-event expansion
44
The normal user of make-event can probably ignore this section, but we
45
include it for completeness. We assume that the reader has read and
46
understood the basic documentation for make-event (see *Note
47
MAKE-EVENT::), but we begin below with a summary of expansion.
51
Here is a summary of how we handle expansion involving make-event forms.
53
(make-event form :check-expansion nil)
55
This shows the :check-expansion default of nil, and is typical user
56
input. We compute the expansion exp of form, which is the expansion of
57
the original make-event expression and is evaluated in place of that
60
(make-event form :check-expansion t)
62
The user presumably wants it checked that the expansion doesn't change
63
in the future, in particular during include-book. If the expansion of
64
form is exp, then we will evaluate exp to obtain the value as before,
65
but this time we record that the expansion of the original make-event
66
expression is (make-event form :check-expansion exp) rather than simply
69
(make-event form :check-expansion exp) ; exp a cons
71
This is generated for the case that :check-expansion is t, as explained
72
above. Evaluation is handled as described in that above case, except
73
here we check that the expansion result is the given exp. (Actually,
74
the user is also allowed supply such a form.) The original make-event
75
expression does not undergo any expansion (intuitively, it expands to
78
Now let us take a look at how we expand progn forms (encapsulate is
81
(progn ... (make-event form :check-expansion nil) ...)
83
The expansion is obtained by replacing the make-event form as follows.
84
Let exp be the expansion of form, Then replace the above make-event
85
form, which we denote as F, by (record-expansion F exp). Here,
86
record-expansion is a macro that returns its second argument.
88
(progn ... (make-event form :check-expansion t) ...)
90
The expansion is of the form (record-expansion F exp) as in the nil case
91
above, except that this time exp is (make-event form :check-expansion
92
exp'), where exp' is the expansion of form.
94
(progn ... (make-event form :check-expansion exp) ...) ; exp a cons
96
No expansion takes place unless expansion takes place for at least one
97
of the other subforms of the progn, in which case each such form F is
98
replaced by (record-expansion F exp) where exp is the expansion of F.
102
In our explanation of the semantics of make-event, we assume familiarity
103
with the notion of "embedded event form" (see *Note
104
EMBEDDED-EVENT-FORM::).
106
Let's say that the "actual embedded event form" corresponding to a given
107
form is the underlying call of an ACL2 event: that is, LOCALs are
108
dropped when ld-skip-proofsp is 'include-book, and macros are expanded
109
away, thus leaving us with a progn, a make-event, or an event form
110
(possibly encapsulate), any of which might have surrounding local,
111
skip-proofs, or with-output calls.
113
Thus, such an actual embedded event form can be viewed as having the
114
form (rebuild-expansion wrappers base-form) where base-form is a progn,
115
a make-event, or an event form (possibly encapsulate), and wrappers are
116
(as in ACL2 source function destructure-expansion) the result of
117
successively removing the event form from the result of macroexpansion,
118
leaving a sequence of (local), (skip-proofs), and (with-output ...)
119
forms. In this case we say that the form "destructures into" the
120
indicated wrappers and base-form, and that it can be "rebuilt from"
121
those wrappers and base-form.
123
Elsewhere we define the notion of the "expansion result" from an
124
evaluation (see *Note MAKE-EVENT::), and we mention that when expansion
125
concludes, the ACL2 logical world and most of the state are restored to
126
their pre-expansion values. Specifically, after evaluation of the
127
argument of make-event (even if it is aborted), the ACL2 logical world
128
is restored to its pre-evaluation value, as are all state global
129
variables in the list *protected-state-globals-for-make-event*. Thus,
130
assignments to user-defined state globals (see *Note ASSIGN::) do
131
persist after expansion, since they are not in that list.
133
We recursively define the combination of evaluation and expansion of an
134
embedded event form, as follows. We also simultaneously define the
135
notion of "expansion takes place," which is assumed to propagate upward
136
(in a sense that will be obvious), such that if no expansion takes
137
place, then the expansion of the given form is considered to be itself.
138
It is useful to keep in mind a goal that we will consider later: Every
139
make-event subterm of an expansion result has a :check-expansion field
140
that is a consp, where for this purpose make-event is viewed as a macro
141
that returns its :check-expansion field. (Implementation note: The
142
latest expansion of a make-event, progn, or encapsulate is stored in
143
state global 'last-make-event-expansion, except that if no expansion has
144
taken place for that form then 'last-make-event-expansion has value
147
If the given form is not an embedded event form, then simply cause
148
a soft error, (mv erp val state) where erp is not nil. Otherwise:
150
If the evaluation of the given form does not take place (presumably
151
because local events are being skipped), then no expansion takes
154
Let x be the actual embedded event form corresponding to the given
155
form, which destructures into wrappers W and base-form B. Then the
156
original form is evaluated by evaluating x, and its expansion is as
159
If B is (make-event form :check-expansion val), then expansion
160
takes place if and only if val is not a consp and no error occurs,
161
as now described. Let R be the expansion result from protected
162
evaluation of form, if there is no error. R must be an embedded
163
event form, or it is an error. Then evaluate/expand R, where if
164
val is not nil then state global 'ld-skip-proofsp is initialized to
165
nil. (This initialization is important so that subsequent
166
expansions are checked in a corresponding environment, i.e., where
167
proofs are turned on in both the original and subsquent
168
environments.) It is an error if this evaluation causes an error.
169
Otherwise, the evaluation yields a value, which is the result of
170
evaluation of the original make-event expression, as well as an
171
expansion, E_R. Let E be rebuilt from W and E_R. The expansion of
172
the original form is E if val is nil, and otherwise is the result
173
of replacing the original form's :check-expansion field with E,
174
with the added requirement that if val is not t (thus, a consp)
175
then E must equal val or else we cause an error.
177
If B is either (progn form1 form2 ...) or (encapsulate sigs form1
178
form2 ...), then after evaluating B, the expansion of the original
179
form is the result of rebuilding from B, with wrappers W, after
180
replacing each formi in B for which expansion takes place by
181
(record-expansion formi formi'), where formi' is the expansion of
182
formi. Note that these expansions are determined as the formi are
183
evaluated in sequence (where in the case of encapsulate, this
184
determination occurs only during the first pass). Except, if no
185
expansion takes place for any formi, then the expansion of the
186
original form is itself.
188
Otherwise, the expansion of the original form is itself.
191
Similarly to the progn and encapsulate cases above, book certification
192
causes a book to replaced by its so-called "book expansion." There,
193
each event ev for which expansion took place during the proof pass of
194
certification -- say, producing ev' -- is replaced by (record-expansion
197
Implementation Note. The book expansion is actually implemented by way
198
of the :expansion-alist field of its certificate, which associates
199
0-based positions of top-level forms in the book (not including the
200
initial in-package form) with their expansions. Thus, the book's source
201
file is not overwritten; rather, the certificate's expansion-alist is
202
applied when the book is included or compiled. End of Implementation
205
It is straightforward by computational induction to see that for any
206
expansion of an embedded event form, every make-event sub-event has a
207
consp :check-expansion field. Here, by "sub-event" we mean to expand
208
macros; and we also mean to traverse progn and encapsulate forms as well
209
as :check-expansion fields of make-event forms. Thus, we will only see
210
make-event forms with consp :check-expansion fields in the course of
211
include-book forms, the second pass of encapsulate forms, and raw Lisp.
212
This fact guarantees that an event form will always be treated as its
220
File: acl2-doc-emacs.info, Node: MUTUAL-RECURSION, Next: NTH-ALIASES-TABLE, Prev: MAKE-EVENT, Up: EVENTS
222
MUTUAL-RECURSION define some mutually recursive functions
228
(if (consp x) (oddlp (cdr x)) t))
230
(if (consp x) (evenlp (cdr x)) nil)))
233
(mutual-recursion def1 ... defn)
234
where each defi is a defun form or a defund form.
236
When mutually recursive functions are introduced it is necessary to do
237
the termination analysis on the entire clique of definitions. Each
238
defun form specifies its own measure, either with the :measure keyword
239
xarg (see *Note XARGS::) or by default to acl2-count. When a function
240
in the clique calls a function in the clique, the measure of the
241
callee's actuals must be smaller than the measure of the caller's
242
formals -- just as in the case of a simply recursive function. But with
243
mutual recursion, the callee's actuals are measured as specified by the
244
callee's defun while the caller's formals are measured as specified by
245
the caller's defun. These two measures may be different but must be
246
comparable in the sense that o< decreases through calls.
248
If you want to specify :hints or :guard-hints (see *Note XARGS::), you
249
can put them in the xargs declaration of any of the defun forms, as the
250
:hints from each form will be appended together, as will the guard-hints
253
You may find it helpful to use a lexicographic order, the idea being to
254
have a measure that returns a list of two arguments, where the first
255
takes priority over the second. Here is an example.
257
(include-book "ordinals/lexicographic-ordering" :dir :system)
261
(set-well-founded-relation l<) ; will be treated as LOCAL
265
(declare (xargs :measure (list (acl2-count x) 1)))
268
(declare (xargs :measure (list (acl2-count y) 0)))
269
(if (zp y) y (foo (1- y))))))
272
The guard analysis must also be done for all of the functions at the
273
same time. If any one of the defuns specifies the :verify-guards xarg
274
to be nil, then guard verification is omitted for all of the functions.
276
Technical Note: Each defi above must be of the form (defun ...). In
277
particular, it is not permitted for a defi to be a form that will
278
macroexpand into a defun form. This is because mutual-recursion is
279
itself a macro, and since macroexpansion occurs from the outside in, at
280
the time (mutual-recursion def1 ... defk) is expanded the defi have not
281
yet been. But mutual-recursion must decompose the defi. We therefore
282
insist that they be explicitly presented as defuns or defunds (or a
285
Suppose you have defined your own defun-like macro and wish to use it in
286
a mutual-recursion expression. Well, you can't. (!) But you can
287
define your own version of mutual-recursion that allows your defun-like
288
form. Here is an example. Suppose you define
290
(defmacro my-defun (&rest args) (my-defun-fn args))
292
where my-defun-fn takes the arguments of the my-defun form and produces
293
from them a defun form. As noted above, you are not allowed to write
294
(mutual-recursion (my-defun ...) ...). But you can define the macro
295
my-mutual-recursion so that
297
(my-mutual-recursion (my-defun ...) ... (my-defun ...))
299
expands into (mutual-recursion (defun ...) ... (defun ...)) by applying
300
my-defun-fn to each of the arguments of my-mutual-recursion.
302
(defun my-mutual-recursion-fn (lst)
303
(declare (xargs :guard (alistp lst)))
305
; Each element of lst must be a consp (whose car, we assume, is always
306
; MY-DEFUN). We apply my-defun-fn to the arguments of each element and
307
; collect the resulting list of DEFUNs.
309
(cond ((atom lst) nil)
310
(t (cons (my-defun-fn (cdr (car lst)))
311
(my-mutual-recursion-fn (cdr lst))))))
313
(defmacro my-mutual-recursion (&rest lst)
315
; Each element of lst must be a consp (whose car, we assume, is always
316
; MY-DEFUN). We obtain the DEFUN corresponding to each and list them
317
; all inside a MUTUAL-RECURSION form.
319
(declare (xargs :guard (alistp lst)))
320
(cons 'mutual-recursion (my-mutual-recursion-fn lst))).
326
File: acl2-doc-emacs.info, Node: NTH-ALIASES-TABLE, Next: PROGN, Prev: MUTUAL-RECURSION, Up: EVENTS
328
NTH-ALIASES-TABLE a table used to associate names for nth/update-nth printing
332
(table nth-aliases-table 'st0 'st)
334
This example associates the symbol st0 with the symbol st. As a result,
335
when the theorem prover prints terms of the form (nth n st0) or
336
(update-nth n val st0), where st is a stobj whose nth accessor function
337
is f-n, then it will print n as *f-n*.
341
(table nth-aliases-table 'alias-name 'name)
343
This event causes alias-name to be treated like name for purposes of the
344
printing of terms that are calls of nth and update-nth. (Note however
345
that name is not recursively looked up in this table.) Both must be
346
symbols other than state. See *Note TERM::, in particular the
347
discussion there of untranslated terms.
349
For a convenient way to add entries to this table, see *Note
350
ADD-NTH-ALIAS::. To remove entries from the table with ease, see *Note
356
File: acl2-doc-emacs.info, Node: PROGN, Next: PROGRAM, Prev: NTH-ALIASES-TABLE, Up: EVENTS
358
PROGN evaluate some events
362
(progn (defun foo (x) x)
363
(defmacro my-defun (&rest args)
365
(my-defun bar (x) (foo x)))
368
(progn event1 event2 ... eventk)
370
where k >= 0 and each eventi is a legal embedded event form (see *Note
371
EMBEDDED-EVENT-FORM::). These events are evaluated in sequence. A
372
utility is provided to assist in debugging failures of such execution;
373
see *Note REDO-FLAT::.
375
NOTE: If the eventi above are not all legal embedded event forms (see
376
*Note EMBEDDED-EVENT-FORM::), consider using er-progn instead.
378
For a related event form that does allows introduction of constraints
379
and local events, see *Note ENCAPSULATE::.
381
ACL2 does not allow the use of progn in definitions. Instead, the macro
382
er-progn can be used for sequencing state-oriented operations; see *Note
383
ER-PROGN:: and see *Note STATE::. If you are using single-threaded
384
objects (see *Note STOBJ::) you may wish to define a version of er-progn
385
that cascades the object through successive changes. ACL2's pprogn is
386
the state analogue of such a macro.
388
If your goal is simply to execute a sequence of top-level forms, for
389
example a sequence of definitions, consider using ld instead; see *Note
397
File: acl2-doc-emacs.info, Node: PROGRAM, Next: PUSH-UNTOUCHABLE, Prev: PROGN, Up: EVENTS
399
PROGRAM to set the default defun-mode to :program
406
Typing the keyword :program sets the default defun-mode to :program.
408
Functions defined in :program mode are logically undefined but can be
409
executed on constants outside of deductive contexts. See *Note
412
Note: This is an event! It does not print the usual event summary but
413
nevertheless changes the ACL2 logical world and is so recorded.
415
See *Note DEFUN-MODE:: for a discussion of the defun-modes available and
416
what their effects on the logic are. See *Note DEFAULT-DEFUN-MODE:: for
417
a discussion of how the default defun-mode is used. This event is
418
equivalent to (table acl2-defaults-table :defun-mode :program), and
419
hence is local to any books and encapsulate events in which it
420
occurs. See *Note ACL2-DEFAULTS-TABLE::.
422
Recall that the top-level form :program is equivalent to (program); see
423
*Note KEYWORD-COMMANDS::. Thus, to change the default defun-mode to
424
:program in a book, use (program), which is an embedded event form,
425
rather than :program, which is not a legal form for books. See *Note
426
EMBEDDED-EVENT-FORM::.
431
File: acl2-doc-emacs.info, Node: PUSH-UNTOUCHABLE, Next: REDO-FLAT, Prev: PROGRAM, Up: EVENTS
433
PUSH-UNTOUCHABLE add name or list of names to the list of untouchable symbols
437
(push-untouchable my-var nil)
438
(push-untouchable set-mem t)
441
(push-untouchable name fn-p :doc doc-string) or
442
(push-untouchable names fn-p :doc doc-string)
445
where name is a non-nil symbol or a true list of symbols, fn-p is any
446
value (but generally nil or t), and doc-string is an optional
447
documentation string not beginning with ":doc-section ...". If name is
448
a symbol it is treated as the singleton list containing that symbol.
449
The effect of this event is to union the given symbols into the list of
450
"untouchable variables" in the current world if fn-p is nil, else to
451
union the symbols into the list of "untouchable functions". This event
452
is redundant if every symbol listed is already a member of the
453
appropriate untouchables list (variables or functions).
455
When a symbol is on the untouchables list it is syntactically illegal
456
for any event to call a function or macro of that name, if fn-p is
457
non-nil, or to change the value of a state global variable of that name,
458
if fn-p is nil. Thus, the effect of pushing a function symbol, name,
459
onto untouchables is to prevent any future event from using that symbol
460
as a function or macro, or as a state global variable (according to
461
fn-p). This is generally done to "fence off" some primitive function
462
symbol from "users" after the developer has used the symbol freely in
463
the development of some higher level mechanism.
468
File: acl2-doc-emacs.info, Node: REDO-FLAT, Next: REMOVE-BINOP, Prev: PUSH-UNTOUCHABLE, Up: EVENTS
470
REDO-FLAT redo up through a failure in an encapsulate or progn
472
When one submits an encapsulate or progn event and one of its sub-events
473
fails, ACL2 restores its logical world as though the encapsulate or
474
progn had not been run. But sometimes one would like to debug the
475
failure by re-executing all sub-events that succeeded up to the point of
476
failure, and then re-executing the failed sub-event. Said differently,
477
imagine that the top-level encapsulate or progn form, as well as all
478
such sub-forms, were flattened into a list of events that were then
479
submitted to ACL2 up to the point of failure. This would put us in the
480
state in which the original failed event had failed, so we could now
481
submit that failed event and try modifying it, or first proving
482
additional events, in order to get it admitted.
484
Redo-flat is provided for this purpose. Consider the following (rather
485
nonsensical) example, in which the defun of f3 fails (the body is y but
486
the formal parameter list is (x)).
492
(local (defthm hack (equal (car (cons x y)) x))))
494
(local (defthm hack (equal (+ x y) (+ y x)))))
496
(make-event '(defun f2 (x) x))
497
(progn (defthm foo (equal x x) :rule-classes nil)
502
After this attempt fails, you can evaluate the following form.
506
This will first lay down a deflabel event, (deflabel r), so that you can
507
eventually remove your debugging work with (:ubt! r). Then the
508
successful sub-events that preceded the failure will be executed with
509
proofs skipped (so that this execution is fast). Then, the failed event
510
will be executed. Finally, a :pbt command is executed so that you can
511
see a summary of the events that executed successfully.
513
You can eliminate some of the steps above by supplying keyword values,
517
:succ succ ; Skip the successful sub-events if val is nil.
518
:fail fail ; Skip the failed sub-event if val is nil.
519
:label lab ; Skip deflabel if lab or succ is nil, else use (deflabel lab).
520
:pbt val ; Skip the final :pbt if val, lab, or succ is nil.
523
Also, you can avoid skipping proofs for the successful sub-events by
524
supplying keyword :succ-ld-skip-proofsp with a valid value for
525
ld-skip-proofsp; see *Note LD-SKIP-PROOFSP::.
527
If you prefer only to see the successful and failed sub-events, without
528
any events being re-executed, you may evaluate the following form
533
For the example above, this command produces the following output.
536
List of events (from encapsulate or progn) preceding the failure:
540
(LOCAL (DEFTHM HACK (EQUAL (CAR (CONS X Y)) X))))
542
(LOCAL (DEFTHM HACK (EQUAL (+ X Y) (+ Y X)))))
543
(MAKE-EVENT '(DEFUN F2 (X) X))
544
(DEFTHM FOO (EQUAL X X)
553
Redo-flat uses a scheme that should not cause spurious name conflicts
554
for local events. Above, it is mentioned that events are "flattened";
555
now we clarify this notion. Each sub-event that succeeds and is an
556
encapsulate or progn is left intact. Only such events that fail are
557
replaced by their component events. Thus, in the example above, there
558
is no conflict between the two local sub-events named "hack," because
559
these are contained in successful encapsulate sub-events, which are
560
therefore not flattened. The progn and two encapsulate events
561
surrounding the definition of f3 are, however, flattened, because that
562
definition failed to be admitted.
564
Unfortunately, an event must actually fail in order for redo-flat to
565
work. So if the system is "stuck" on an event, then you may find it
566
helpful to insert an illegal event just in front of it before submitting
567
the encapsulate or progn.
574
File: acl2-doc-emacs.info, Node: REMOVE-BINOP, Next: REMOVE-DEFAULT-HINTS, Prev: REDO-FLAT, Up: EVENTS
576
REMOVE-BINOP remove the association of a binary function name with a macro name
580
(remove-binop binary-append)
585
See *Note ADD-BINOP:: for a discussion of how to associate a macro name
586
with a binary function name for proof output purposes. This form sets
587
binop-table to the result of deleting the association of a macro name
588
with the given binary function name. If the function name has no such
589
association, then this form still generates an event, but the event has
595
File: acl2-doc-emacs.info, Node: REMOVE-DEFAULT-HINTS, Next: REMOVE-DEFAULT-HINTS!, Prev: REMOVE-BINOP, Up: EVENTS
597
REMOVE-DEFAULT-HINTS remove from the default hints
602
(remove-default-hints '((computed-hint-1 clause)
603
(computed-hint-2 clause
604
stable-under-simplificationp)))
607
Note: This is an event! It does not print the usual event summary but
608
nevertheless changes the ACL2 logical world and is so recorded. It is
609
local to the book or encapsulate form in which it occurs (see *Note
610
REMOVE-DEFAULT-HINTS!:: for a corresponding non-local event).
614
(remove-default-hints lst)
616
where lst is a list. Generally speaking, the elements of lst should be
617
suitable for use as computed-hints. Also see *Note ADD-DEFAULT-HINTS::.
619
If some elements of the given list do not belong to the existing default
620
hints, they will simply be ignored by this event.
622
Finally, note that the effects of set-default-hints, add-default-hints,
623
and remove-default-hints are local to the book in which they appear.
624
Thus, users who include a book with such forms will not have their
625
default hints affected by such forms. In order to export the effect of
626
setting the default hints, use set-default-hints!, add-default-hints!,
627
or remove-default-hints!.
632
File: acl2-doc-emacs.info, Node: REMOVE-DEFAULT-HINTS!, Next: REMOVE-DIVE-INTO-MACRO, Prev: REMOVE-DEFAULT-HINTS, Up: EVENTS
634
REMOVE-DEFAULT-HINTS! remove from the default hints non-locally
636
Please see *Note REMOVE-DEFAULT-HINTS::, which is the same as
637
remove-default-hints! except that the latter is not local to the
638
encapsulate or the book in which it occurs. Probably
639
remove-default-hints is to be preferred unless you have a good reason
640
for wanting to export the effect of this event outside the enclosing
648
File: acl2-doc-emacs.info, Node: REMOVE-DIVE-INTO-MACRO, Next: REMOVE-INVISIBLE-FNS, Prev: REMOVE-DEFAULT-HINTS!, Up: EVENTS
650
REMOVE-DIVE-INTO-MACRO removes association of proof-checker diving function with macro name
654
(remove-dive-into-macro logand)
656
This feature undoes the effect of add-dive-into-macro, which is used so
657
that the proof-checker's DV command and numeric diving commands (e.g.,
658
3) will dive properly into subterms. Please see *Note
659
ADD-DIVE-INTO-MACRO:: and especially see *Note DIVE-INTO-MACROS-TABLE::.
666
File: acl2-doc-emacs.info, Node: REMOVE-INVISIBLE-FNS, Next: REMOVE-MACRO-ALIAS, Prev: REMOVE-DIVE-INTO-MACRO, Up: EVENTS
668
REMOVE-INVISIBLE-FNS make some unary functions no longer invisible
672
(remove-invisible-fns (binary-+ unary-- foo)
674
The setting above has makes unary functions unary-- and foo no longer
675
"invisible" for the purposes of applying permutative :rewrite rules to
680
(remove-invisible-fns top-fn unary-fn1 ... unary-fnk)
682
where top-fn is a function symbol and the unary-fni are unary function
685
See *Note ADD-INVISIBLE-FNS:: and also see *Note INVISIBLE-FNS-TABLE::
686
and see *Note SET-INVISIBLE-FNS-TABLE::.
691
File: acl2-doc-emacs.info, Node: REMOVE-MACRO-ALIAS, Next: REMOVE-NTH-ALIAS, Prev: REMOVE-INVISIBLE-FNS, Up: EVENTS
693
REMOVE-MACRO-ALIAS remove the association of a function name with a macro name
697
(remove-macro-alias append)
700
(remove-macro-alias macro-name)
702
See *Note MACRO-ALIASES-TABLE:: for a discussion of macro aliases; also
703
see *Note ADD-MACRO-ALIAS::. This form sets macro-aliases-table to the
704
result of deleting the key macro-name from that table. If the name does
705
not occur in the table, then this form still generates an event, but the
706
event has no real effect.
711
File: acl2-doc-emacs.info, Node: REMOVE-NTH-ALIAS, Next: SET-BACKCHAIN-LIMIT, Prev: REMOVE-MACRO-ALIAS, Up: EVENTS
713
REMOVE-NTH-ALIAS remove the association of one symbol with another for printing of nth/update-nth terms
717
(remove-nth-alias append)
720
(remove-nth-alias alias-name)
722
See *Note NTH-ALIASES-TABLE:: for further discussion; also see *Note
723
ADD-NTH-ALIAS::. This form sets nth-aliases-table to the result of
724
deleting the key alias-name from that table. If the name does not occur
725
in the table, then this form still generates an event, but the event has
731
File: acl2-doc-emacs.info, Node: SET-BACKCHAIN-LIMIT, Next: SET-BODY, Prev: REMOVE-NTH-ALIAS, Up: EVENTS
733
SET-BACKCHAIN-LIMIT Sets the backchain-limit used by the rewriter
735
Note: This is an event! It does not print the usual event summary but
736
nevertheless changes the ACL2 logical world and is so recorded.
737
Moreover, its effect is to set the acl2-defaults-table, and hence its
738
effect is local to the book or encapsulate form containing it; see *Note
739
ACL2-DEFAULTS-TABLE::.
741
This event sets the global backchain-limit used by the ACL2 rewriter.
742
It must be nil or a non-negative integer. (See *Note BACKCHAIN-LIMIT::
746
:set-backchain-limit nil ; do not impose any additional limits
747
:set-backchain-limit 0 ; allow only type reasoning for relieving
749
:set-backchain-limit 500 ; allow backchaining to a depth of no more
751
(set-backchain-limit 500) ; same as above
753
The default limit is nil.
758
File: acl2-doc-emacs.info, Node: SET-BODY, Next: SET-BOGUS-MUTUAL-RECURSION-OK, Prev: SET-BACKCHAIN-LIMIT, Up: EVENTS
760
SET-BODY set the definition body
764
(set-body foo (:definition foo)) ; restore original definition of foo
765
(set-body foo foo) ; same as just above
766
(set-body foo my-foo-def) ; use my-foo-def for the body of foo
767
(set-body foo (:definition my-foo-def)) ; same as just above
769
Rules of class :definition can install a new definition body, used for
770
example by :expand hints. See *Note DEFINITION:: and also see *Note
771
HINTS::for a detailed discussion of the :install-body fields of
772
:definition rules and their role in :expand hints.
774
There may be several such definitions, but by default, the latest one is used
775
by :expand hints. Although the :with keyword may be used in
776
:expand hints to override this behavior locally (see *Note HINTS::), it may be
777
convenient to install a definition for expansion other than the latest one
778
--- for example, the original definition. Set-body may be used for this
783
(set-body function-symbol rule-name)
785
where rule-name is either a :definition rune or is a function symbol,
786
sym, which represents the rune (:definition sym).
788
You can view all definitions available for expansion; see *Note
796
File: acl2-doc-emacs.info, Node: SET-BOGUS-MUTUAL-RECURSION-OK, Next: SET-CASE-SPLIT-LIMITATIONS, Prev: SET-BODY, Up: EVENTS
798
SET-BOGUS-MUTUAL-RECURSION-OK allow unnecessary "mutual recursion"
802
(set-bogus-mutual-recursion-ok t)
803
(set-bogus-mutual-recursion-ok nil)
804
(set-bogus-mutual-recursion-ok :warn)
806
By default, ACL2 checks that when a "clique" of more than one function
807
is defined simultaneously (using mutual-recursion or defuns), then every
808
body calls at least one of the functions in the "clique." Below, we
809
refer to definitional events that fail this check as "bogus" mutual
810
recursions. The check is important because ACL2 does not store
811
induction schemes for functions defined with other functions in a
812
mutual-recursion or defuns event. Thus, ACL2 may have difficulty
813
proving theorems by induction that involve such functions. Moreover,
814
the check can call attention to bugs, since users generally intend that
815
their mutual recursions are not bogus.
817
Nevertheless, there are times when it is advantageous to allow bogus
818
mutual recursions, for example when they are generated mechanically,
819
even at the expense of losing stored induction schemes. The first
820
example above allows bogus mutual recursion. The second example
821
disallows bogus mutual recursion; this is the default. The third
822
example allows bogus mutual recursion, but prints an appropriate
825
Note: This is an event! It does not print the usual event summary but
826
nevertheless changes the ACL2 logical world and is so recorded.
827
Moreover, its effect is to set the acl2-defaults-table, and hence its
828
effect is local to the book or encapsulate form containing it; see *Note
829
ACL2-DEFAULTS-TABLE::.
833
(set-bogus-mutual-recursion-ok flg)
835
where flg is either t, nil, or :warn.
840
File: acl2-doc-emacs.info, Node: SET-CASE-SPLIT-LIMITATIONS, Next: SET-COMPILE-FNS, Prev: SET-BOGUS-MUTUAL-RECURSION-OK, Up: EVENTS
842
SET-CASE-SPLIT-LIMITATIONS set the case-split-limitations
847
(set-case-split-limitations '(500 100))
848
(set-case-split-limitations 'nil)
849
(set-case-split-limitations '(500 nil))
851
The first of these prevents clausify from trying the
852
subsumption/replacement (see below) loop if more than 500 clauses are
853
involved. It also discourages the clause simplifier from splitting into
854
more than 100 cases at once.
856
Note: This is an event! It does not print the usual event summary but
857
nevertheless changes the ACL2 logical world and is so recorded.
858
Moreover, its effect is to set the acl2-defaults-table, and hence its
859
effect is local to the book or encapsulate form containing it; see *Note
860
ACL2-DEFAULTS-TABLE::.
864
(set-case-split-limitations lst)
866
where lst is either nil (denoting a list of two nils), or a list of
867
length two, each element of which is either nil or a natural number.
868
When nil is used as an element, it is treated as positive infinity. The
869
default setting is (500 100).
871
The first number specifies the maximum number of clauses that may
872
participate in the "subsumption/replacement" loop. Because of the
873
expensive nature of that loop (which compares every clause to every
874
other in a way that is quadratic in the number of literals in the
875
clauses), when the number of clauses exceeds about 1000, the system
876
tends to "go into a black hole," printing nothing and not even doing
877
many garbage collections (because the subsumption/replacement loop does
878
not create new clauses so much as it just tries to delete old ones).
879
The initial setting is lower than the threshold at which we see
880
noticeably bad performance, so you probably will not see this behavior
881
unless you have raised or disabled the limit.
883
Why raise the subsumption/replacement limit? The
884
subsumption/replacement loop cleans up the set of subgoals produced by
885
the simplifier. For example, if one subgoal is
887
(implies (and p q r) s) [1]
891
(implies (and p (not q) r) s) [2]
893
then the subsumption/replacement loop would produce the single subgoal
895
(implies (and p r) s) [3]
897
instead. This cleanup process is simply skipped when the number of
898
subgoals exceeds the subsumption/replacement limit. But each subgoal
899
must nonetheless be proved. The proofs of [1] and [2] are likely to
900
duplicate much work, which is only done once in proving [3]. So with a
901
low limit, you may find the system quickly produces a set of subgoals
902
but then takes a long time to prove that set. With a higher limit, you
903
may find the set of subgoals to be "cleaner" and faster to prove.
905
Why lower the subsumption/replacement limit? If you see the system go
906
into a "black hole" of the sort described above (no output, and few
907
garbage collections), it could due to the subsumption/replacement loop
908
working on a large set of large subgoals. You might temporarily lower
909
the limit so that it begins to print the uncleaned set of subgoals.
910
Perhaps by looking at the output you will realize that some function can
911
be disabled so as to prevent the case explosion. Then raise or disable
914
The second number in the case-split-limitations specifies how many case
915
splits the simplifier will allow before it begins to shut down case
916
splitting. In normal operation, when a literal rewrites to a nest of
917
IFs, the system simplifies all subsequent literals in all the contexts
918
generated by walking through the nest in all possible ways. This can
919
also cause the system to "go into a black hole" printing nothing except
920
garbage collection messages. This "black hole" behavior is different
921
from than mentioned above because space is typically being consumed at a
922
prodigious rate, since the system is rewriting the literals over and
923
over in many different contexts.
925
As the simplifier sweeps across the clause, it keeps track of the number
926
of cases that have been generated. When that number exceeds the second
927
number in case-split-limitations, the simplifier stops rewriting
928
literals. The remaining, unrewritten, literals are copied over into the
929
output clauses. IFs in those literals are split out, but the literals
930
themselves are not rewritten. Each output clause is then attacked
931
again, by subsequent simplification, and eventually the unrewritten
932
literals in the tail of the clause will be rewritten because the earlier
933
literals will stabilize and stop producing case splits.
935
The default setting of 100 is fairly low. We have seen successful
936
proofs in which thousands of subgoals were created by a simplification.
937
By setting the second number to small values, you can force the system
938
to case split slowly. For example, a setting of 5 will cause it to
939
generate "about 5" subgoals per simplification.
941
You can read about how the simplifier works in the book Computer-Aided
942
Reasoning: An Approach (Kaufmann, Manolios, Moore). If you think about
943
it, you will see that with a low case limit, the initial literals of a
944
goal are repeatedly simplified, because each time a subgoal is
945
simplified we start at the left-most subterm. So when case splitting
946
prevents the later subterms from being fully split out, we revisit the
947
earlier terms before getting to the later ones. This can be good.
948
Perhaps it takes several rounds of rewriting before the earlier terms
949
are in normal form and then the later terms rewrite quickly. But it
950
could happen that the earlier terms are expensive to rewrite and do not
951
change, making the strategy of delayed case splits less efficient. It
954
Sometimes the simplifier produces more clauses than you might expect,
955
even with case-split-limitations in effect. As noted above, once the
956
limit has been exceeded, the simplifier does not rewrite subsequent
957
literals. But IFs in those literals are split out nonetheless.
958
Furthermore, the enforcement of the limit is -- as described above --
959
all or nothing: if the limit allows us to rewrite a literal then we
960
rewrite the literal fully, without regard for limitations, and get as
961
many cases as "naturally" are produced. It quite often happens that a
962
single literal, when expanded, may grossly exceed the specified limits.
964
If the second "number" is nil and the simplifier is going to produce
965
more than 1000 clauses, a "helpful little message" to this effect is
966
printed out. This output is printed to the system's "comment window"
967
not the standard proofs output.
972
File: acl2-doc-emacs.info, Node: SET-COMPILE-FNS, Next: SET-DEFAULT-BACKCHAIN-LIMIT, Prev: SET-CASE-SPLIT-LIMITATIONS, Up: EVENTS
974
SET-COMPILE-FNS have each function compiled as you go along.
978
(set-compile-fns t) ; new functions compiled after DEFUN
979
(set-compile-fns nil) ; new functions not compiled after DEFUN
981
Note: This is an event! It does not print the usual event summary but
982
nevertheless changes the ACL2 logical world and is so recorded.
984
Also see *Note COMP::, because it may be more efficient in some Common
985
Lisps to compile many functions at once rather than to compile each one
990
(set-compile-fns term)
992
where term is a variable-free term that evaluates to t or nil. This
993
macro is equivalent to
995
(table acl2-defaults-table :compile-fns term)
997
and hence is local to any books and encapsulate events in which it
998
occurs; see *Note ACL2-DEFAULTS-TABLE::. However, unlike the above
999
simple call of the table event function (see *Note TABLE::), no output
1000
results from a set-compile-fns event.
1002
Set-compile-fns may be thought of as an event that merely sets a flag to
1003
t or nil. The flag's effect is felt when functions are defined, as with
1004
defun. If the flag is t, functions are automatically compiled after
1005
they are defined, as are their executable counterparts (see *Note
1006
EXECUTABLE-COUNTERPART::). Otherwise, functions are not automatically
1007
compiled. Because set-compile-fns is an event, the old value of the
1008
flag is restored when a set-compile-fns event is undone.
1010
Even when :set-compile-fns t has been executed, functions are not
1011
individually compiled when processing an include-book event. If you
1012
wish to include a book of compiled functions, we suggest that you first
1013
certify it with the compilation flag set (see *Note CERTIFY-BOOK::) or
1014
else compile the book by supplying the appropriate load-compiled-file
1015
argument to include-book. More generally, compilation via
1016
set-compile-fns is suppressed when the state global variable
1017
ld-skip-proofsp has value 'include-book.
1022
File: acl2-doc-emacs.info, Node: SET-DEFAULT-BACKCHAIN-LIMIT, Next: SET-DEFAULT-HINTS, Prev: SET-COMPILE-FNS, Up: EVENTS
1024
SET-DEFAULT-BACKCHAIN-LIMIT sets the default backchain-limit used when admitting a rule
1026
Note: This is an event! It does not print the usual event summary but
1027
nevertheless changes the ACL2 logical world and is so recorded.
1028
Moreover, its effect is to set the acl2-defaults-table, and hence its
1029
effect is local to the book or encapsulate form containing it; see *Note
1030
ACL2-DEFAULTS-TABLE::.
1032
This event sets the default backchain-limit used when a new rewrite or
1033
linear rule is admitted. It must be nil or a non-negative integer.
1034
(See *Note BACKCHAIN-LIMIT:: for details.)
1037
:set-default-backchain-limit nil ; do not impose additional limits
1038
:set-default-backchain-limit 0 ; allow only type-reasoning for
1039
; relieving hypotheses
1040
:set-default-backchain-limit 500 ; allow backchaining to a depth of
1042
(set-default-backchain-limit 500) ; same as above
1045
The initial default backchain-limit is nil.
1050
File: acl2-doc-emacs.info, Node: SET-DEFAULT-HINTS, Next: SET-DEFAULT-HINTS!, Prev: SET-DEFAULT-BACKCHAIN-LIMIT, Up: EVENTS
1052
SET-DEFAULT-HINTS set the default hints
1057
(set-default-hints '((computed-hint-1 clause)
1058
(computed-hint-2 clause
1059
stable-under-simplificationp)))
1060
(set-default-hints nil)
1063
Note: This is an event! It does not print the usual event summary but
1064
nevertheless changes the ACL2 logical world and is so recorded. It is
1065
local to the book or encapsulate form in which it occurs (see *Note
1066
SET-DEFAULT-HINTS!:: for a corresponding non-local event).
1070
(set-default-hints lst)
1072
where lst is a list. Generally speaking, the elements of lst should be
1073
suitable for use as computed-hints.
1075
Whenever a defthm or thm command is executed, the default hints are
1076
appended to the right of any explicitly provided :hints in the command.
1077
The same applies to defuns as well (:hints, :guard-hints, and (for
1078
ACL2(r)) :std-hints). The hints are then translated and processed just
1079
as though they had been explicitly included.
1081
Technically, we do not put restrictions on lst, beyond that it is a true
1082
list. It would be legal to execute
1084
(set-default-hints '(("Goal" :use lemma23)))
1086
with the effect that the given hint is added to subsequent hints
1087
supplied explicitly. An explicit "Goal" hint would, however, take
1088
priority, as suggested by the mention above of "appended to the right."
1090
Note that set-default-hints sets the default hints as specified. To add
1091
to or remove from the current default, see *Note ADD-DEFAULT-HINTS:: and
1092
see *Note REMOVE-DEFAULT-HINTS::.
1094
Finally, note that the effects of set-default-hints, add-default-hints,
1095
and remove-default-hints are local to the book in which they appear.
1096
Thus, users who include a book with such forms will not have their
1097
default hints affected by such forms. In order to export the effect of
1098
setting the default hints, use set-default-hints!, add-default-hints!,
1099
or remove-default-hints!.
1104
File: acl2-doc-emacs.info, Node: SET-DEFAULT-HINTS!, Next: SET-ENFORCE-REDUNDANCY, Prev: SET-DEFAULT-HINTS, Up: EVENTS
1106
SET-DEFAULT-HINTS! set the default hints non-locally
1108
Please see *Note SET-DEFAULT-HINTS::, which is the same as
1109
set-default-hints! except that the latter is not local to the
1110
encapsulate or the book in which it occurs. Probably set-default-hints
1111
is to be preferred unless you have a good reason for wanting to export
1112
the effect of this event outside the enclosing encapsulate or book.
1119
File: acl2-doc-emacs.info, Node: SET-ENFORCE-REDUNDANCY, Next: SET-IGNORE-OK, Prev: SET-DEFAULT-HINTS!, Up: EVENTS
1121
SET-ENFORCE-REDUNDANCY require most events to be redundant
1125
(set-enforce-redundancy nil) ; do not require redundancy (default)
1126
(set-enforce-redundancy t) ; most events (see below) must be redundant
1127
(set-enforce-redundancy :warn) ; warn for most non-redundant events
1129
Note: This is an event! It does not print the usual event summary but
1130
nevertheless changes the ACL2 logical world and is so recorded.
1134
(set-enforce-redundancy flag)
1136
where flag is nil, t, or :warn, as indicated above. This macro is
1137
essentially equivalent to
1139
(table acl2-defaults-table :enforce-redundancy flag)
1141
and hence is local to any books and encapsulate events in which it
1142
occurs; see *Note ACL2-DEFAULTS-TABLE::. However, unlike the above
1143
simple call of the table event function (see *Note TABLE::), no output
1144
results from a set-enforce-redundancy event.
1146
Set-enforce-redundancy may be thought of as an event that merely sets a
1147
flag as indicated above, which determines whether most events, including
1148
defun and defthm events, are allowed to be redundant; see *Note
1149
REDUNDANT-EVENTS::. The exceptions are deflabel, defpkg, encapsulate,
1150
include-book, push-untouchable, set-body, and table events. Any other
1151
type of non-redundant event will cause an error if flag is t and a
1152
warning if flag is nil, *except* in the course of carrying out an
1155
Note that because table events that set the acl2-defaults-table are
1156
implicitly local, set-enforce-redundancy events are ignored when
1157
including books. However, the presence of the event
1158
(set-enforce-redundancy t) in a book guarantees that its subsequent
1159
definitions and theorems are redundant. This can be a useful property
1160
to maintain in library development, as we now describe.
1162
An example of the use of this form can be found in the distributed books
1163
under directory books/rtl/rel4/. The intention in that directory has
1164
been to put all the gory details in subdirectories support/ and
1165
arithmetic/, so that the books in subdirectory lib/ contain only the
1166
"exported" definitions and theorems. This approach is useful for human
1167
readability. Moreover, suppose we want to prove new theorems in lib/.
1168
Typically we wish to prove the new theorems using the existing books in
1169
lib/; however, our methodology demands that the proofs go into books in
1170
support/. If every theorem in lib/ is redundant, then we can *develop*
1171
the proofs in lib/ but then when we are done, *move* each book with such
1172
proofs into support/ as follows. In any such book, we first replace
1173
include-book forms referring to books in lib/ by include-book forms
1174
referring to corresponding books in support/ and/or arithmetic/. Then,
1175
we add suitable in-theory events to get us back into the original lib/
1178
The default behavior of the system is as though the :enforce-redundancy
1179
value is nil. The current behavior can be ascertained by evaluating the
1182
(cdr (assoc-eq :enforce-redundancy (table-alist 'acl2-defaults-table wrld)))
1188
File: acl2-doc-emacs.info, Node: SET-IGNORE-OK, Next: SET-INHIBIT-WARNINGS, Prev: SET-ENFORCE-REDUNDANCY, Up: EVENTS
1190
SET-IGNORE-OK allow unused formals and locals without an ignore declaration
1196
(set-ignore-ok :warn)
1198
The first example above allows unused formals and locals, i.e.,
1199
variables that would normally have to be declared ignored. The second
1200
example disallows unused formals and locals; this is the default. The
1201
third example allows them, but prints an appropriate warning.
1203
Note: This is an event! It does not print the usual event summary but
1204
nevertheless changes the ACL2 logical world and is so recorded.
1205
Moreover, its effect is to set the acl2-defaults-table, and hence its
1206
effect is local to the book or encapsulate form containing it; see *Note
1207
ACL2-DEFAULTS-TABLE::.
1213
where flg is either t, nil, or :warn.
1215
One might find this event useful when one is generating function
1216
definitions by an automated procedure, when that procedure does not take
1217
care to make sure that all formals are actually used in the definitions
1220
Note: Defun will continue to report irrelevant formals even if
1221
:set-ignore-ok has been set to t, unless you also use
1222
set-irrelevant-formals-ok to instruct it otherwise.
1227
File: acl2-doc-emacs.info, Node: SET-INHIBIT-WARNINGS, Next: SET-INVISIBLE-FNS-TABLE, Prev: SET-IGNORE-OK, Up: EVENTS
1229
SET-INHIBIT-WARNINGS control warnings
1233
(set-inhibit-warnings "theory" "use")
1235
Note: This is an event! It does not print the usual event summary but
1236
nevertheless changes the ACL2 logical world and is so recorded.
1237
Moreover, its effect is to set the acl2-defaults-table, and hence its
1238
effect is local to the book or encapsulate form containing it; see *Note
1239
ACL2-DEFAULTS-TABLE::.
1243
(set-inhibit-warnings string1 string2 ...)
1245
where each string is considered without regard to case. This macro is
1246
equivalent to (table acl2-defaults-table :inhibit-warnings lst), where
1247
lst is the list of strings supplied. This macro is an event (see *Note
1248
TABLE::), but no output results from a set-inhibit-warnings event.
1250
The effect of this event is to suppress any warning whose label is a
1251
member of this list (where again, case is ignored). For example, the
1254
ACL2 Warning [Use] in ( THM ...): It is unusual to :USE ....
1256
will not be printed if "use" (or "USE", etc.) is a member of the given
1259
Of course, if warnings are inhibited overall --- see *Note
1260
SET-INHIBIT-OUTPUT-LST:: -- then the value of :inhibit-warnings is
1261
entirely irrelevant.
32
File: acl2-doc-emacs.info, Node: DEFREFINEMENT, Next: DEFSTOBJ, Prev: DEFPKG, Up: EVENTS
34
DEFREFINEMENT prove that equiv1 refines equiv2
37
(defrefinement equiv1 equiv2)
39
is an abbreviation for
40
(defthm equiv1-refines-equiv2
41
(implies (equiv1 x y) (equiv2 x y))
42
:rule-classes (:refinement))
44
See *Note REFINEMENT::.
47
(defrefinement equiv1 equiv2
48
:rule-classes rule-classes
49
:instructions instructions
52
:event-name event-name
55
where equiv1 and equiv2 are known equivalence relations, event-name, if
56
supplied, is a symbol and all other arguments are as specified in the
57
documentation for defthm. The defrefinement macro expands into a call
58
of defthm. The name supplied is equiv1-refines-equiv2, unless
59
event-name is supplied, in which case it is used as the name. The term
60
supplied states that equiv1 refines equiv2. The rule-class :refinement
61
is added to the rule-classes specified, if it is not already there.
62
All other arguments to the generated defthm form are as specified by
63
the other keyword arguments above.
66
File: acl2-doc-emacs.info, Node: DEFSTOBJ, Next: DEFSTUB, Prev: DEFREFINEMENT, Up: EVENTS
68
DEFSTOBJ define a new single-threaded object
72
(reg :type (array (unsigned-byte 31) (8))
74
(p-c :type (unsigned-byte 31)
76
halt ; = (halt :type t :initially nil)
77
(mem :type (array (unsigned-byte 31) (64))
78
:initially 0 :resizable t))
82
(field1 :type type1 :initially val1 :resizable b1)
84
(fieldk :type typek :initially valk :resizable bk)
89
where name is a new symbol, each fieldi is a symbol, each typei is
90
either a type-spec or (ARRAY type-spec (max)), each vali is an object
91
satisfying typei, and each bi is t or nil. Each pair :initially vali
92
and :resizable bi may be omitted; more on this below. The alist
93
argument is optional and allows the user to override the default
94
function names introduced by this event. The doc-string is also
95
optional. The inline-flag Boolean argument is also optional and
96
declares to ACL2 that the generated access and update functions for the
97
stobj should be implemented as macros under the hood (which has the
98
effect of inlining the function calls). We describe further
99
restrictions on the fieldi, typei, vali, and on alist below. We
100
recommend that you read about single-threaded objects (stobjs) in ACL2
101
before proceeding; see *note STOBJ::.
103
The effect of this event is to introduce a new single-threaded object
104
(i.e., a "stobj"), named name, and the associated recognizers, creator,
105
accessors, updaters, constants, and, for fields of ARRAY type, length
106
and resize functions.
108
_The Single-Threaded Object Introduced_
110
The defstobj event effectively introduces a new global variable, named
111
name, which has as its initial logical value a list of k elements,
112
where k is the number of "field descriptors" provided. The elements
113
are listed in the same order in which the field descriptors appear. If
114
the :type of a field is (ARRAY type-spec (max)) then the corresponding
115
element of the stobj is initially a list of length max containing the
116
value, val, specified by :initially val. Otherwise, the :type of the
117
field is a type-spec and the corresponding element of the stobj is the
118
specified initial value val. (The actual representation of the stobj
119
in the underlying Lisp may be quite different; see *note
120
STOBJ-EXAMPLE-2::. For the moment we focus entirely on the logical
121
aspects of the object.)
123
In addition, the defstobj event introduces functions for recognizing
124
and creating the stobj and for recognizing, accessing, and updating its
125
fields. For fields of ARRAY type, length and resize functions are also
126
introduced. Constants are introduced that correspond to the accessor
129
_Restrictions on the Field Descriptions in Defstobj_
131
Each field descriptor is of the form:
133
(fieldi :TYPE typei :INITIALLY vali)
135
Note that the type and initial value are given in "keyword argument"
136
format and may be given in either order. The typei and vali
137
"arguments" are not evaluated. If omitted, the type defaults to t
138
(unrestricted) and the initial value defaults to nil.
140
Each typei must be either a type-spec or else a list of the form (ARRAY
141
type-spec (max)). The latter forms are said to be "array types."
142
Examples of legal typei are:
146
(ARRAY (SIGNED-BYTE 31) (16))
148
The typei describes the objects which are expected to occupy the given
149
field. Those objects in fieldi should satisfy typei. We are more
150
precise below about what we mean by "expected." We first present the
151
restrictions on typei and vali.
155
When typei is a type-spec it restricts the contents, x, of fieldi
156
according to the "meaning" formula given in the table for type-spec.
157
For example, the first typei above restricts the field to be an integer
158
between 0 and 31, inclusive. The second restricts the field to be an
159
integer between -2^30 and (2^30)-1, inclusive.
161
The initial value, vali, of a field description may be any ACL2 object
162
but must satisfy typei. Note that vali is not a form to be evaluated
163
but an object. A form that evaluates to vali could be written 'vali,
164
but defstobj does not expect you to write the quote mark. For example,
165
the field description
167
(days-off :initially (saturday sunday))
169
describes a field named days-off whose initial value is the list
170
consisting of the two symbols SATURDAY and SUNDAY. In particular, the
171
initial value is NOT obtained by applying the function saturday to the
172
variable sunday! Had we written
174
(days-off :initially '(saturday sunday))
176
it would be equivalent to writing
178
(days-off :initially (quote (saturday sunday)))
180
which would initialize the field to a list of length two, whose first
181
element is the symbol quote and whose second element is a list
182
containing the symbols saturday and sunday.
186
When typei is of the form (ARRAY type-spec (max)), the field is
187
supposed to be a list of items, initially of length max, each of which
188
satisfies the indicated type-spec. Max must be a non-negative integer
189
less than (2^28)-1. We discuss this limitation below. Thus,
191
(ARRAY (SIGNED-BYTE 31) (16))
193
restricts the field to be a list of integers, initially of length 16,
194
where each integer in the list is a (SIGNED-BYTE 31). We sometimes
195
call such a list an "array" (because it is represented as an array in
196
the underlying Common Lisp). The elements of an array field are
197
indexed by position, starting at 0. Thus, the maximum legal index of
198
an array field is max-1.
200
Note that the ARRAY type requires that the max be enclosed in
201
parentheses. This makes ACL2's notation consistent with the Common
202
Lisp convention of describing the (multi-)dimensionality of arrays.
203
But ACL2 currently supports only single dimensional arrays in stobjs.
205
For array fields, the initial value vali must be an object satisfying
206
the type-spec of the ARRAY description. The initial value of the field
207
is a list of max repetitions of vali.
209
Array fields can be "resized," that is, their lengths can be changed,
210
if :resizable t is supplied as shown in the example and General Form
211
above. The new length must satisfy the same restriction as does max,
212
as described above. Each array field in a defstobj event gives rise to
213
a length function, which gives the length of the field, and a resize
214
function, which modifies the length of the field if :resizable t was
215
supplied with the field when the defstobj was introduced and otherwise
218
Array resizing is relatively slow, so we recommend using it somewhat
221
_The Default Function Names_
226
(field1 :type type1 :initially val1)
228
(fieldk :type typek :initially valk)
233
name must be a new symbol, each fieldi must be a symbol, each typei
234
must be a type-spec or (ARRAY type-spec (max)), and each vali must be
235
an object satisfying typei.
237
Roughly speaking, for each fieldi, a defstobj introduces a recognizer
238
function, an accessor function, and an updater function. The accessor
239
function, for example, takes the stobj and returns the indicated
240
component; the updater takes a new component value and the stobj and
241
return a new stobj with the component replaced by the new value. But
242
that summary is inaccurate for array fields.
244
The accessor function for an array field does not take the stobj and
245
return the indicated component array, which is a list of length max.
246
Instead, it takes an additional index argument and returns the
247
indicated element of the array component. Similarly, the updater
248
function for an array field takes an index, a new value, and the stobj,
249
and returns a new stobj with the indicated element replaced by the new
252
These functions -- the recognizer, accessor, and updater, and also
253
length and resize functions in the case of array fields -- have
254
"default names." The default names depend on the field name, fieldi,
255
and on whether the field is an array field or not. For clarity,
256
suppose fieldi is named c. The default names are shown below in calls,
257
which also indicate the arities of the functions. In the expressions,
258
we use x as the object to be recognized by field recognizers, i as an
259
array index, v as the "new value" to be installed by an updater, and
260
name as the single-threaded object.
262
non-array field array field
263
recognizer (cP x) (cP x)
264
accessor (c name) (cI i name)
265
updater (UPDATE-c v name) (UPDATE-cI i v name)
266
length (c-LENGTH name)
267
resize (RESIZE-c k name)
269
Finally, a recognizer and a creator for the entire single-threaded
270
object are introduced. The creator returns the initial stobj, but may
271
only be used in limited contexts; see *note WITH-LOCAL-STOBJ::. If the
272
single-threaded object is named name, then the default names and
273
arities are as shown below.
275
top recognizer (nameP x)
276
creator (CREATE-name)
278
For example, the event
281
(X :TYPE INTEGER :INITIALLY 0)
282
(A :TYPE (ARRAY (INTEGER 0 9) (3)) :INITIALLY 9))
284
introduces a stobj named $S. The stobj has two fields, X and A. The A
285
field is an array. The X field contains an integer and is initially 0.
286
The A field contains a list of integers, each between 0 and 9,
287
inclusively. Initially, each of the three elements of the A field is 9.
289
This event introduces the following sequence of definitions:
291
(DEFUN XP (X) ...) ; recognizer for X field
292
(DEFUN AP (X) ...) ; recognizer of A field
293
(DEFUN $SP ($S) ...) ; top-level recognizer for stobj $S
294
(DEFUN CREATE-$S () ...) ; creator for stobj $S
295
(DEFUN X ($S) ...) ; accessor for X field
296
(DEFUN UPDATE-X (V $S) ...) ; updater for X field
297
(DEFUN A-LENGTH ($S) ...) ; length of A field
298
(DEFUN RESIZE-A (K $S) ...) ; resizer for A field
299
(DEFUN AI (I $S) ...) ; accessor for A field at index I
300
(DEFUN UPDATE-AI (I V $S) ...) ; updater for A field at index I
302
_Avoiding the Default Function Names_
304
If you do not like the default names listed above you may use the
305
optional :renaming alist to substitute names of your own choosing.
306
Each element of alist should be of the form (fn1 fn2), where fn1 is a
307
default name and fn2 is your choice for that name.
312
(X :TYPE INTEGER :INITIALLY 0)
313
(A :TYPE (ARRAY (INTEGER 0 9) (3)) :INITIALLY 9)
314
:renaming ((X XACCESSOR) (CREATE-$S MAKE$S)))
316
introduces the following definitions
318
(DEFUN XP (X) ...) ; recognizer for X field
319
(DEFUN AP (X) ...) ; recognizer of A field
320
(DEFUN $SP ($S) ...) ; top-level recognizer for stobj $S
321
(DEFUN MAKE$S () ...) ; creator for stobj $S
322
(DEFUN XACCESSOR ($S) ...) ; accessor for X field
323
(DEFUN UPDATE-X (V $S) ...) ; updater for X field
324
(DEFUN A-LENGTH ($S) ...) ; length of A field
325
(DEFUN RESIZE-A (K $S) ...) ; resizer for A field
326
(DEFUN AI (I $S) ...) ; accessor for A field at index I
327
(DEFUN UPDATE-AI (I V $S) ...) ; updater for A field at index I
329
Note that even though the renaming alist substitutes "XACCESSOR" for
330
"X" the updater for the X field is still called "UPDATE-X." That is
331
because the renaming is applied to the default function names, not to
332
the field descriptors in the event.
334
Use of the :renaming alist may be necessary to avoid name clashes
335
between the default names and and pre-existing function symbols.
339
Defstobj events also introduce constant definitions (see *note
340
DEFCONST::). One constant is introduced for each accessor function by
341
prefixing and suffixing a `*' character on the function name. The
342
value of that constant is the position of the field being accessed.
343
For example, if the accessor functions are a, b, and c, in that order,
344
then the following constant definitions are introduced.
350
These constants are used for certain calls of nth and update-nth that
351
are displayed to the user in proof output. For example, for stobj st
352
with accessor functions a, b, and c, in that order, the term (nth '2
353
st) would be printed during a proof as (nth *c* st). Also see *note
354
TERM::, in particular the discussion there of untranslated terms, and
355
see *note NTH-ALIASES-TABLE::.
357
_Inspecting the Effects of a Defstobj_
359
Because the stobj functions are introduced as "sub-events" of the
360
defstobj the history commands :pe and :pc will not print the
361
definitions of these functions but will print the superior defstobj
362
event. To see the definitions of these functions use the history
365
To see an s-expression containing the definitions what constitute the
366
raw Lisp implementation of the event, evaluate the form
368
(nth 4 (global-val 'cltl-command (w state)))
370
_immediately after_ the defstobj event has been processed.
372
A defstobj is considered redundant only if the name, field descriptors,
373
renaming alist, and inline flag are identical to a previously executed
374
defstobj. Note that a redundant defstobj does not reset the stobj
375
fields to their initial values.
377
_Inlining and Performance_
379
The :inline keyword argument controls whether or not accessor, updater,
380
and length functions are inlined (as macros under the hood, in raw
381
Lisp). If :inline t is provided then these are inlined; otherwise they
382
are not. The advantage of inlining is potentially better performance;
383
there have been contrived examples, doing essentially nothing except
384
accessing and updating array fields, where inlining reduced the time by
385
a factor of 10 or more; and inlining has sped up realistic examples by
386
a factor of at least 2. Inlining may get within a factor of 2 of C
387
execution times for such contrived examples, and within a few percent
388
of C execution times on realistic examples.
390
A drawback to inlining is that redefinition may not work as expected,
391
much as redefinition may not work as expected for macros: defined
392
functions that call a macro, or inlined stobj function, will not see a
393
subsequent redefinition of the macro or inlined function. Another
394
drawback to inlining is that because inlined functions are implemented
395
as macros in raw Lisp, tracing (see *note TRACE$::) will not show their
396
calls. These drawbacks are avoided by default, but the user who is not
397
concerned about them is advised to specify :inline t.
400
File: acl2-doc-emacs.info, Node: DEFSTUB, Next: DEFTHEORY, Prev: DEFSTOBJ, Up: EVENTS
402
DEFSTUB stub-out a function symbol
405
ACL2 !>(defstub subr1 (* * state) => (mv * state))
406
ACL2 !>(defstub add-hash (* * hash-table) => hash-table)
409
(defstub name args-sig => output-sig)
410
(defstub name args-sig => output-sig :doc doc-string)
412
Name is a new function symbol and (name . args-sig) => output-sig) is a
413
signature. If the optional doc-string is supplied it should be a
414
documentation string. See also the "Old Style" heading below.
416
Defstub macro expands into an encapsulate event (see *note
417
ENCAPSULATE::). Thus, no axioms are available about name but it may be
418
used wherever a function of the given signature is permitted.
422
Old Style General Form:
423
(defstub name formals output)
424
(defstub name formals output :doc doc-string)
426
where name is a new function symbol, formals is its list of formal
427
parameters, and output is either a symbol (indicating that the function
428
returns one result) or a term of the form (mv s1 ... sn), where each si
429
is a symbol (indicating that the function returns n results). Whether
430
and where the symbol state occurs in formals and output indicates how
431
the function handles state. It should be the case that (name formals
432
output) is in fact a signature (see *note SIGNATURE::).
434
Note that with the old style notation it is impossible to stub-out a
435
function that uses any single-threaded object other than state. The
436
old style is preserved for compatibility with earlier versions of ACL2.
439
File: acl2-doc-emacs.info, Node: DEFTHEORY, Next: DEFTHM, Prev: DEFSTUB, Up: EVENTS
441
DEFTHEORY define a theory (to enable or disable a set of rules)
444
(deftheory interp-theory
445
(set-difference-theories
446
(universal-theory :here)
447
(universal-theory 'interp-section)))
450
(deftheory name term :doc doc-string)
452
where name is a new symbolic name (see *note NAME::), term is a term
453
that when evaluated will produce a theory (see *note THEORIES::), and
454
doc-string is an optional documentation string (see *note
455
DOC-STRING::). Except for the variable world, term must contain no
456
free variables. Term is evaluated with world bound to the current
457
world (see *note WORLD::) and the resulting theory is then converted to
458
a _runic theory_ (see *note THEORIES::) and associated with name.
459
Henceforth, this runic theory is returned as the value of the theory
460
expression (theory name).
462
The value returned is the length of the resulting theory. For example,
463
in the following, the theory associated with 'FOO has 54 runes:
465
ACL2 !>(deftheory foo (union-theories '(binary-append)
466
(theory 'minimal-theory)))
469
Form: ( DEFTHEORY FOO ...)
472
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
477
File: acl2-doc-emacs.info, Node: DEFTHM, Next: DEFTHMD, Prev: DEFTHEORY, Up: EVENTS
479
DEFTHM prove and name a theorem
483
(equal (app (app a b) c)
486
The following nonsensical example illustrates all the optional
487
arguments but is illegal because not all combinations are permitted.
488
See *Note HINTS:: for a complete list of hints.
491
(implies (hyps x y z) (concl x y z))
492
:rule-classes (:REWRITE :GENERALIZE)
493
:instructions (induct prove promote (dive 1) x
494
(dive 2) = top (drop 2) prove)
496
:do-not '(generalize fertilize)
497
:in-theory (set-difference-theories
498
(current-theory :here)
500
:induct (and (nth n a) (nth n b))
501
:use ((:instance assoc-of-append
503
(:functional-instance
504
(:instance p-f (x a) (y b))
508
:doc "#0[one-liner/example/details]")
512
:rule-classes rule-classes
513
:instructions instructions
518
where name is a new symbolic name (see *note NAME::), term is a term
519
alleged to be a theorem, and rule-classes, instructions, hints, otf-flg
520
and doc-string are as described in their respective documentation. The
521
five keyword arguments above are all optional, however you may not
522
supply both :instructions and :hints, since one drives the proof
523
checker and the other drives the theorem prover. If :rule-classes is
524
not specified, the list (:rewrite) is used; if you wish the theorem to
525
generate no rules, specify :rule-classes nil.
527
When ACL2 processes a defthm event, it first tries to prove the term
528
using the indicated hints (see *note HINTS::) or instructions (see
529
*note PROOF-CHECKER::). If it is successful, it stores the rules
530
described by the rule-classes (see *note RULE-CLASSES::), proving the
531
necessary corollaries.
534
File: acl2-doc-emacs.info, Node: DEFTHMD, Next: DEFTTAG, Prev: DEFTHM, Up: EVENTS
536
DEFTHMD prove and name a theorem and then disable it
538
Use defthmd instead of defthm when you want to disable a theorem
539
immediately after proving it. This macro has been provided for users
540
who prefer working in a mode where theorems are only enabled when
541
explicitly directed by :in-theory. Specifically, the form
543
(defthmd NAME TERM ...)
548
(defthmd NAME TERM ...)
551
(in-theory (disable NAME)))
554
Note that defthmd commands are never redundant (see *note
555
REDUNDANT-EVENTS::). Even if the defthm event is redundant, then the
556
in-theory event will still be executed.
558
The summary for the in-theory event is suppressed. See *Note DEFTHM::
559
for documentation of defthm.
562
File: acl2-doc-emacs.info, Node: DEFTTAG, Next: DEFUN, Prev: DEFTHMD, Up: EVENTS
564
DEFTTAG introduce a trust tag (ttag)
568
(defttag tag-name :doc doc-string)
570
where tag-name is a symbol. The :doc doc-string argument is optional;
571
if supplied, then it must be a valid documentation string (see *note
572
DOC-STRING::), and the defttag call will generate a corresponding
573
defdoc event. For the rest of this discussion we ignore the :doc
576
*WARNING!* This event is intended for advanced users who, in essence,
577
want to build extensions of ACL2. Anyone who uses this event, even by
578
way of including books, is placing trust in the correctness of all
579
forms executed in the scope of that defttag event. (Thus, it may be a
580
good idea if the scope of a defttag event, which is the enclosing book
581
or encapsulate event, is kept small.) The documentation below explains
582
this issue in detail.
584
This event introduces or removes a so-called active trust tag (or
585
"ttag", pronounced "tee tag"). An active ttag is a non-nil symbol
586
(tag) that is associated with potentially unsafe acts. For example,
587
sys-call can be used in an unsafe way, for example to overwrite files,
588
or worse (see *note SYS-CALL:: for a frightening example from Bob
589
Boyer). Therefore, calls of sys-call are illegal unless a defttag
590
event has been executed. If one introduces an active ttag and then
591
writes definitions that calls sys-call, presumably in a defensibly
592
"safe" way, then responsibility for those calls is attributed to that
593
ttag. This attribution (or blame!) is at the level of books; a book's
594
certificate contains a list of ttags that are active in that book, or
595
in a book that is included (possibly locally), or in a book included in
596
a book that is included (either inclusion being potentially local), and
597
so on. We explain all this in more detail below.
599
(Defttag tag-name) is essentially equivalent to
601
(table acl2-defaults-table :ttag tag-name)
603
and hence is local to any books and encapsulate events in which it
604
occurs; see *note ACL2-DEFAULTS-TABLE::. We say more about the scope of
607
Note: This is an event! It does not print the usual event summary but
608
nevertheless executes the above table event and hence changes the ACL2
609
logical world, and is so recorded. Although no event summary is
610
printed, it is important to note that the "TTAG NOTE", discussed below,
611
is always printed for a non-nil tag-name.
613
*Active ttags.* Suppose tag-name is a non-nil symbol. Then (defttag
614
tag-name) sets tag-name to be the "active ttag." There must be an
615
active ttag in order for there to be any mention of certain function
616
and macro symbols, including sys-call; evaluate the form (strip-cars
617
*ttag-fns-and-macros*) to see the full list of such symbols. On the
618
other hand, (defttag nil) removes the active ttag, if any; there is
619
then no active ttag. The scope of a defttag form in a book being
620
certified or included is limited to subsequent forms in the same book
621
before the next defttag (if any) in that book. Similarly, if a defttag
622
form is evaluated in the top-level loop, then its effect is limited to
623
subsequent forms in the top-level loop before the next defttag in the
624
top-level loop (if any). Moreoever, certify-book is illegal when a
625
ttag is active; of course, in such a circumstance one can execute
626
(defttag nil) in order to allow book certification.
628
*Ttag notes and the "certifier."* When a defttag is executed with an
629
argument other than nil, output is printed, starting on a fresh line
630
with: TTAG NOTE. For example:
634
TTAG NOTE: Adding ttag FOO from the top level loop.
638
If the defttag occurs in an included book, the message looks like this.
640
TTAG NOTE (for included book): Adding ttag FOO from file /u/smith/acl2/my-book.lisp.
642
The "TTAG NOTE" message is always printed on a single line. The
643
intention is that one can search the standard output for all such notes
644
in order to find all defttag events. In a sense, defttag events can
645
allow you to define your own system on top of ACL2 (for example, see
646
*note PROGN!::). So in order for someone else (who we might call the
647
"certifier") to be confident that your collection of books is
648
meaningful, that certifier should certify all the user-supplied books
649
from scratch and check either that no :ttags were supplied to
650
certify-book, or else look for every TTAG NOTE in the standard output
651
in order to locate all defttag events with non-nil tag-name. In this
652
way, the certifier can in principle decide whether to be satisfied that
653
those defttag events did not allow inappropriate forms in the
656
*Allowed ttags when certifying and including books.* A defttag form
657
may not be evaluated unless its argument is a so-called "allowed" ttag.
658
All ttags are allowed in the interactive top-level loop. However,
659
during certify-book and include-book, the set of allowed ttags is
660
restricted according to the :ttags keyword argument. If this argument
661
is omitted then no ttag is allowed, so a defttag call will fail during
662
book certification or inclusion in this case. This restriction applies
663
even to defttag forms already evaluated in the so-called certification
664
world at the time certify-book is called. But note that (defttag nil)
667
A :ttags argument of certify-book and include-book can have value :all,
668
indicating that every ttag is allowed, i.e., no restriction is being
669
placed on the arguments, just as in the interactive top-level loop.
670
Otherwise, the value is a true list of ttag specifications, each having
671
one of the following forms, where sym is a non-nil symbol.
677
(3) (sym x1 x2 ... xk), where k > 0 and each xi is a string, except
678
that one xi may be nil.
680
In Case (1), (defttag sym) is allowed to occur in at most one book or
681
else in the top-level loop (i.e., the certification world for a book
682
under certification or a book being included). Case (2) allows
683
(defttag sym) to occur in an unlimited number of books. For case (3)
684
the xi specify where (defttag sym) may occur, as follows. The case
685
that xi is nil refers to the top-level loop, while all other xi are
686
filenames, where the ".lisp" extension is optional and relative
687
pathnames are considered to be relative to the connected book directory
690
An error message, as shown below, illustrates how ACL2 enforcess the
691
notion of allowed ttags. Suppose that you call certify-book with
692
argument :ttags (foo), where you have already executed (defttag foo) in
693
the certification world (i.e., before calling certify-book). Then ACL2
694
immediately associates the ttag foo with nil, where again, nil refers
695
to the top-level loop. If ACL2 then encounters (defttag foo) inside
696
that book, you will get the following error (using the full book name
697
for the book, as shown):
699
ACL2 Error in ( TABLE ACL2-DEFAULTS-TABLE ...): The ttag FOO associated
700
with file /u/smith/work/my-book.lisp is not among the set of ttags permitted
701
in the current context, namely:
705
In general the structure displayed by the error message, which is ((FOO
706
NIL)) in this case, represents the currently allowed ttags with
707
elements as discussed in (1) through (3) above. In this case, that
708
list's unique element is (FOO NIL), meaning that ttag FOO is only
709
allowed at the top level (as represented by NIL).
711
*Associating ttags with books and with the top-level loop.* When a book
712
is certified, each form (defttag tag) that is encountered for non-nil
713
tag in that book or an included book is recorded in the generated
714
certificate, which associates tag with the full-book-name of the book
715
containing that deftag. If such a defttag form is encountered outside
716
a book, hence in the portcullis of the book being certified or one of
717
its included books, then tag is associated with nil in the generated
718
certificate. Note that the notion of "included book" here applies to
719
the recursive notion of a book either included directly in the book
720
being certified or else included in such a book, where we account even
721
for locally included books.
723
For examples of ways to take advantage of ttags, see
724
books/misc/hacker.lisp and see *note TTAGS-SEEN::, see *note PROGN!::,
725
see *note REMOVE-UNTOUCHABLE::, see *note SET-RAW-MODE::, and see *note
729
File: acl2-doc-emacs.info, Node: DEFUN, Next: DEFUN-SK, Prev: DEFTTAG, Up: EVENTS
731
DEFUN define a function symbol
736
(cons (car x) (app (cdr x) y))
740
(declare (xargs :guard (and (integerp n)
744
(* n (fact (1- n)))))
747
(defun fn (var1 ... varn) doc-string dcl ... dcl body),
749
where fn is the symbol you wish to define and is a new symbolic name
750
(see *note NAME::), (var1 ... varn) is its list of formal parameters
751
(see *note NAME::), and body is its body. The definitional axiom is
752
logically admissible provided certain restrictions are met. These are
755
Note that ACL2 does not support the use of lambda-list keywords (such
756
as &optional) in the formals list of functions. We do support some
757
such keywords in macros and often you can achieve the desired syntax by
758
defining a macro in addition to the general version of your function.
759
See *Note DEFMACRO::. The documentation string, doc-string, is
760
optional; for a description of its form, see *note DOC-STRING::.
762
The _declarations_ (see *note DECLARE::), dcl, are also optional. If
763
more than one dcl form appears, they are effectively grouped together
764
as one. Perhaps the most commonly used ACL2 specific declaration is of
765
the form (declare (xargs :guard g :measure m)). This declaration in
766
the defun of some function fn has the effect of making the "guard" for
767
fn be the term g and the "measure" be the term m. The notion of
768
"measure" is crucial to ACL2's definitional principle. The notion of
769
"guard" is not, and is discussed elsewhere; see *note VERIFY-GUARDS::
770
and see *note SET-VERIFY-GUARDS-EAGERNESS::. Note that the :measure is
771
ignored in :program mode; see *note DEFUN-MODE::.
773
We now briefly discuss the ACL2 definitional principle, using the
774
following definition form which is offered as a more or less generic
778
(declare (xargs :guard (g x y)
782
(step (fn (d x) y))))
784
Note that in our generic example, fn has just two arguments, x and y,
785
the guard and measure terms involve both of them, and the body is a
786
simple case split on (test x y) leading to a "non-recursive" branch,
787
(stop x y), and a "recursive" branch. In the recursive branch, fn is
788
called after "decrementing" x to (d x) and some step function is
789
applied to the result. Of course, this generic example is quite
790
specific in form but is intended to illustrate the more general case.
792
Provided this definition is admissible under the logic, as outlined
793
below, it adds the following axiom to the logic.
802
Note that the guard of fn has no bearing on this logical axiom.
804
This defining axiom is actually implemented in the ACL2 system by a
805
:definition rule, namely
810
(step (fn (d a) b)))).
812
See *Note DEFINITION:: for a discussion of how definition rules are
813
applied. Roughly speaking, the rule causes certain instances of (fn x
814
y) to be replaced by the corresponding instances of the body above.
815
This is called "opening up" (fn x y). The instances of (fn x y) opened
816
are chosen primarily by heuristics which determine that the recursive
817
calls of fn in the opened body (after simplification) are more
818
desirable than the unopened call of fn.
820
This discussion has assumed that the definition of fn was admissible.
821
Exactly what does that mean? First, fn must be a previously
822
unaxiomatized function symbol (however, see *note
823
LD-REDEFINITION-ACTION::). Second, the formal parameters must be
824
distinct variable names. Third, the guard, measure, and body should
825
all be terms and should mention no free variables except the formal
826
parameters. Thus, for example, body may not contain references to
827
"global" or "special" variables; ACL2 constants or additional formals
828
should be used instead.
830
The final conditions on admissibility concern the termination of the
831
recursion. Roughly put, all applications of fn must terminate. In
832
particular, there must exist a binary relation, rel, and some unary
833
predicate mp such that rel is well-founded on objects satisfying mp,
834
the measure term m must always produce something satisfying mp, and the
835
measure term must decrease according to rel in each recursive call,
836
under the hypothesis that all the tests governing the call are
837
satisfied. By the meaning of well-foundedness, we know there are no
838
infinitely descending chains of successively rel-smaller mp-objects.
839
Thus, the recursion must terminate.
841
The only primitive well-founded relation in ACL2 is o< (see *note
842
O<::), which is known to be well-founded on the o-ps (see *note O-P::).
843
For the proof of well-foundedness, see *note
844
PROOF-OF-WELL-FOUNDEDNESS::. However it is possible to add new
845
well-founded relations. For details, see *note
846
WELL-FOUNDED-RELATION::. We discuss later how to specify which
847
well-founded relation is selected by defun and in the present
848
discussion we assume, without loss of generality, that it is o< on the
851
For example, for our generic definition of fn above, with measure term
852
(m x y), two theorems must be proved. The first establishes that m
857
The second shows that m decreases in the (only) recursive call of fn:
859
(implies (not (test x y))
860
(o< (m (d x) y) (m x y))).
862
Observe that in the latter formula we must show that the "m-size" of (d
863
x) and y is "smaller than" the m-size of x and y, provided the test,
864
(test x y), in the body fails, thus leading to the recursive call (fn
867
See *Note O<:: for a discussion of this notion of "smaller than." It
868
should be noted that the most commonly used ordinals are the natural
869
numbers and that on natural numbers, o< is just the familiar "less
870
than" relation (<). Thus, it is very common to use a measure m that
871
returns a nonnegative integer, for then (o-p (m x y)) becomes a simple
872
conjecture about the type of m and the second formula above becomes a
873
conjecture about the less-than relationship of nonnegative integer
876
The most commonly used measure function is acl2-count, which computes a
877
nonnegative integer size for all ACL2 objects. See *Note ACL2-COUNT::.
879
Probably the most common recursive scheme in Lisp programming is when
880
some formal is supposed to be a list and in the recursive call it is
881
replaced by its cdr. For example, (test x y) might be simply (atom x)
882
and (d x) might be (cdr x). In that case, (acl2-count x) is a suitable
883
measure because the acl2-count of a cons is strictly larger than the
884
acl2-counts of its car and cdr. Thus, "recursion by car" and
885
"recursion by cdr" are trivially admitted if acl2-count is used as the
886
measure and the definition protects every recursive call by a test
887
insuring that the decremented argument is a consp. Similarly,
888
"recursion by 1-" in which a positive integer formal is decremented by
889
one in recursion, is also trivially admissible. See *Note
890
BUILT-IN-CLAUSES:: to extend the class of trivially admissible
893
We now turn to the question of which well-founded relation defun uses.
894
It should first be observed that defun must actually select both a
895
relation (e.g., o<) and a domain predicate (e.g., o-p) on which that
896
relation is known to be well-founded. But, as noted elsewhere (see
897
*note WELL-FOUNDED-RELATION::), every known well-founded relation has a
898
unique domain predicate associated with it and so it suffices to
899
identify simply the relation here.
901
The xargs field of a declare permits the explicit specification of any
902
known well-founded relation with the keyword :well-founded-relation.
903
An example is given below. If the xargs for a defun specifies a
904
well-founded relation, that relation and its associated domain
905
predicate are used in generating the termination conditions for the
908
If no :well-founded-relation is specified, defun uses the
909
:well-founded-relation specified in the acl2-defaults-table. See *Note
910
SET-WELL-FOUNDED-RELATION:: to see how to set the default well-founded
911
relation (and, implicitly, its domain predicate). The initial default
912
well-founded relation is o< (with domain predicate o-p).
914
This completes the brief sketch of the ACL2 definitional principle.
916
On very rare occasions ACL2 will seem to "hang" when processing a
917
definition, especially if there are many subexpressions of the body
918
whose function symbol is if (or which macroexpand to such an
919
expression). In those cases you may wish to supply the following to
920
xargs: :normalize nil. This is an advanced feature that turns off
921
ACL2's usual propagation upward of if tests.
923
The following example illustrates all of the available declarations,
924
but is completely nonsensical. For documentation, see *note XARGS:: and
927
(defun example (x y z a b c i j)
928
(declare (ignore a b c)
930
(xargs :guard (symbolp x)
932
:well-founded-relation my-wfr
935
:do-not '(generalize fertilize)
936
:expand ((assoc x a) (member y z))
937
:restrict ((<-trans ((x x) (y (foo x)))))
938
:hands-off (length binary-append)
939
:in-theory (set-difference-theories
940
(current-theory :here)
942
:induct (and (nth n a) (nth n b))
944
:use ((:instance assoc-of-append
946
(:functional-instance
947
(:instance p-f (x a) (y b))
950
:guard-hints (("Subgoal *1/3'"
951
:use ((:instance assoc-of-append
952
(x a) (y b) (z c)))))
956
(example-body x y z i j))
added
removed
doc/EMACS/acl2-doc-emacs.info-10
