32
28
* acl2: (acl2-doc-emacs.info). Applicative Common Lisp
40
File: acl2-doc-emacs.info, Node: WRITE-BYTE$, Next: XARGS, Prev: WORMHOLE, Up: MISCELLANEOUS
42
WRITE-BYTE$ See *Note IO::.
49
File: acl2-doc-emacs.info, Node: XARGS, Prev: WRITE-BYTE$, Up: MISCELLANEOUS
51
XARGS giving hints to defun
53
Common Lisp's defun function does not easily allow one to pass extra
54
arguments such as "hints". ACL2 therefore supports a peculiar new
55
declaration (see *Note DECLARE::) designed explicitly for passing
56
additional arguments to defun via a keyword-like syntax.
58
The following declaration is nonsensical but does illustrate all of the
61
(declare (xargs :guard (symbolp x)
62
:guard-hints (("Goal" :in-theory (theory batch1)))
63
:hints (("Goal" :in-theory (theory batch1)))
71
:well-founded-relation my-wfr))
74
(xargs :key1 val1 ... :keyn valn)
76
where the keywords and their respective values are as shown below. Note
77
that once "inside" the xargs form, the "extra arguments" to defun are
78
passed exactly as though they were keyword arguments.
82
Value is a term involving only the formals of the function being
83
defined. The actual guard used for the definition is the conjunction of
84
all the guards and types (see *Note DECLARE::) declared.
88
Value: hints (see *Note HINTS::), to be used during the guard
89
verification proofs as opposed to the termination proofs of the defun.
93
Value: hints (see *Note HINTS::), to be used during the termination
94
proofs as opposed to the guard verification proofs of the defun.
98
Value is a term involving only the formals of the function being
99
defined. This term is indicates what is getting smaller in the
100
recursion. The well-founded relation with which successive measures are
105
Value is :program or :logic, indicating the defun mode of the function
106
introduced. See *Note DEFUN-MODE::. If unspecified, the defun mode
107
defaults to the default defun mode of the current world. To convert a
108
function from :program mode to :logic mode, see *Note
109
VERIFY-TERMINATION::.
113
Value is t or nil (the default). If t, the function has no executable
114
counterpart and is permitted to use single-threaded object names and
115
functions arbitrarily, as in theorems rather than as in executable
116
definitions. Such functions are not permitted to declare any names to
117
be :stobjs but accessors, etc., may be used, just as in theorems. Since
118
the default is nil, the value supplied is only of interest when it is t.
122
Value is a flag telling defun whether to propagate if tests upward.
123
Since the default is to do so, the value supplied is only of interest
124
when it is nil. (See *Note DEFUN::).
128
Value is a flag indicating "onward through the fog" (see *Note
133
Value is either a single stobj name or a true list of stobj names.
134
Every stobj name among the formals of the function must be listed, if
135
the corresponding actual is to be treated as a stobj. That is, if a
136
function uses a stobj name as a formal parameter but the name is not
137
declared among the :stobjs then the corresponding argument is treated as
138
ordinary. The only exception to this rule is state: whether you include
139
it or not, state is always treated as a single-threaded object. This
140
declaration has two effects. One is to enforce the syntactic
141
restrictions on single-threaded objects. The other is to strengthen the
142
guard of the function being defined so that it includes conjuncts
143
specifying that each declared single-threaded object argument satisfies
144
the recognizer for the corresponding single-threaded object.
148
Value is t or nil, indicating whether or not guards are to be verified
149
upon completion of the termination proof. This flag should only be t if
150
the :mode is unspecified but the default defun mode is :logic, or else
153
:WELL-FOUNDED-RELATION
155
Value is a function symbol that is known to be a well-founded relation
156
in the sense that a rule of class :well-founded-relation has been proved
157
about it. See *Note WELL-FOUNDED-RELATION::.
162
File: acl2-doc-emacs.info, Node: OTHER, Next: PROGRAMMING, Prev: MISCELLANEOUS, Up: Top
164
OTHER other commonly used top-level functions
169
* atsign:: (@) get the value of a global variable in state
171
* ACL2-DEFAULTS-TABLE:: a table specifying certain defaults, e.g., the default defun-mode
173
* ACL2-HELP:: the acl2-help mailing list
175
* ASSIGN:: assign to a global variable in state
177
* CERTIFY-BOOK!:: a variant of certify-book
179
* CW-GSTACK:: debug a rewriting loop or stack overflow
181
* EXIT:: quit entirely out of Lisp
183
* GOOD-BYE:: quit entirely out of Lisp
185
* LD:: the ACL2 read-eval-print loop, file loader, and command processor
187
* PROPS:: print the ACL2 properties on a symbol
189
* PSO:: show the most recently saved output
191
* PSO!:: show the most recently saved output, including proof-tree output
193
* PSTACK:: seeing what is the prover up to
195
* Q:: quit ACL2 (type :q) -- reenter with (lp)
197
* QUIT:: quit entirely out of Lisp
199
* REBUILD:: a convenient way to reconstruct your old state
201
* RESET-LD-SPECIALS:: restores initial settings of the ld specials
203
* SAVE-EXEC:: save an executable image and (for most Common Lisps) a wrapper script
205
* SET-GUARD-CHECKING:: control checking guards during execution of top-level forms
207
* SET-INHIBIT-OUTPUT-LST:: control output
209
* SET-PRINT-CLAUSE-IDS:: cause subgoal numbers to be printed when 'prove output is inhibited
211
* SET-RAW-MODE:: enter or exit "raw mode," a raw Lisp environment
213
* SET-SAVED-OUTPUT:: save proof output for later display with :pso or :pso!
215
* SET-TAINTED-OKP:: control output
217
* SKIP-PROOFS:: skip proofs for a given form -- a quick way to introduce unsoundness
219
* THM:: prove a theorem
221
* TIME$:: time a form
223
* TRANS:: print the macroexpansion of a form
225
* TRANS!:: print the macroexpansion of a form without single-threadedness concerns
227
* TRANS1:: print the one-step macroexpansion of a form
229
* WITH-PROVER-TIME-LIMIT:: limit the time for proofs
232
Related topics other than immediate subtopics:
233
* CERTIFY-BOOK:: how to produce a certificate for a book
236
This section contains an assortment of functions that fit into none of
237
the other categories and yet are suffiently useful as to merit
238
"advertisement" in the :help command.
243
File: acl2-doc-emacs.info, Node: atsign, Next: ACL2-DEFAULTS-TABLE, Prev: OTHER, Up: OTHER
245
@ get the value of a global variable in state
250
(assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))
255
where symbol is any symbol to which you have assigned a global value.
256
This macro expands into (f-get-global 'symbol state), which retrieves
257
the stored value of the symbol.
259
The macro assign makes it convenient to set the value of a symbol. The
260
:ubt operation has no effect on the global-table of state. Thus, you
261
may use these globals to hang onto useful data structures even though
262
you may undo back past where you computed and saved them.
267
File: acl2-doc-emacs.info, Node: ACL2-DEFAULTS-TABLE, Next: ACL2-HELP, Prev: atsign, Up: OTHER
269
ACL2-DEFAULTS-TABLE a table specifying certain defaults, e.g., the default defun-mode
273
(table acl2-defaults-table :defun-mode) ; current default defun-mode
274
(table acl2-defaults-table :defun-mode :program)
275
; set default defun-mode to :program
278
See *Note TABLE:: for a discussion of tables in general. The legal keys
279
for this table are shown below. They may be accessed and changed via
280
the general mechanisms provided by tables. However, there are often
281
more convenient ways to access and/or change the defaults. (See also
286
the default defun-mode, which must be :program or :logic. See *Note
287
DEFUN-MODE:: for a general discussion of defun-modes. The :defun-mode
288
key may be conveniently set by keyword commands naming the new
289
defun-mode, :program and :logic. See *Note PROGRAM:: and see *Note
294
if t, cause ACL2 to insist that most events are redundant (see *Note
295
REDUNDANT-EVENTS::); if :warn, cause a warning instead of an error for
296
such non-redundant events; else, nil. See *Note
297
SET-ENFORCE-REDUNDANCY::.
299
:verify-guards-eagerness
301
an integer between 0 and 2 indicating how eager the system is to verify
302
the guards of a defun event. See *Note SET-VERIFY-GUARDS-EAGERNESS::.
306
When this key's value is t, functions are compiled when they are
307
defun'd; otherwise, the value is nil. To set the flag, see *Note
312
the default measure function used by defun when no :measure is supplied
313
in xargs. The default measure function must be a function symbol of one
314
argument. Let mfn be the default measure function and suppose no
315
:measure is supplied with some recursive function definition. Then
316
defun finds the first formal, var, that is tested along every branch and
317
changed in each recursive call. The system then "guesses" that (mfn
318
var) is the :measure for that defun.
320
:well-founded-relation
322
the default well-founded relation used by defun when no
323
:well-founded-relation is supplied in xargs. The default well-founded
324
relation must be a function symbol, rel, of two arguments about which a
325
:well-founded-relation rule has been proved. See *Note
326
WELL-FOUNDED-RELATION::.
328
:bogus-mutual-recursion-ok
330
When this key's value is t, ACL2 skips the check that every function in
331
a mutual-recursion (or defuns) "clique" calls at least one other
332
function in that "clique." Otherwise, the value is the keyword nil (the
333
default) or :warn (which makes the check but merely warns when the check
334
fails). See *Note SET-BOGUS-MUTUAL-RECURSION-OK::.
336
:irrelevant-formals-ok
338
When this key's value is t, the check for irrelevant formals is
339
bypassed; otherwise, the value is the keyword nil (the default) or :warn
340
(which makes the check but merely warns when the check fails). See
341
*Note IRRELEVANT-FORMALS:: and see *Note SET-IRRELEVANT-FORMALS-OK::.
345
When this key's value is t, the check for ignored variables is bypassed;
346
otherwise, the value is the keyword nil (the default) or :warn (which
347
makes the check but merely warns when the check fails. See *Note
352
ACL2 prints warnings that may, from time to time, seem excessive to
353
experienced users. Each warning is "labeled" with a string identifying
354
the type of warning. Consider for example
356
ACL2 Warning [Use] in ( THM ...): It is unusual to :USE ....
358
Here, the label is "Use". The value of the key :inhibit-warnings is a
359
list of such labels, where case is ignored. Any warning whose label is
360
a member of this list (where again, case is ignored) is suppressed. See
361
*Note SET-INHIBIT-WARNINGS:: and also see *Note
362
SET-INHIBIT-OUTPUT-LST::.
366
This key's value is a list of function symbols used to define the notion
367
of "BDD normal form." See *Note BDD-ALGORITHM:: and see *Note HINTS::.
371
This key's value is either t or nil and indicates whether the user is
372
aware of the syntactic restrictions on the variable symbol STATE. See
373
*Note SET-STATE-OK::.
377
This key's value is either nil or a non-negative integer. It is used to
378
set the backchain limit upon starting rewriting. See *Note
381
:default-backchain-limit
383
This key's value is either nil or a non-negative integer. It is used to
384
set the backchain limit of a rule if one has not been specified. See
385
*Note BACKCHAIN-LIMIT::.
389
This key's value is a nonnegative integer less than (expt 2 28). It is
390
used to limit the depth of calls of ACL2 rewriter functions. See *Note
391
REWRITE-STACK-LIMIT::.
395
This key affects how the system displays subgoals. The value is either
396
t or nil. When t, let* expressions are introduced before printing to
397
eliminate common subexpressions. The actual goal being worked on is
402
This key's value is nil, t, or :literals. When the value is non-nil,
403
the rewriter gives special treatment to expressions and functions
404
defined in terms of nth and update-nth. See set-nu-rewriter-mode.
406
:case-split-limitations
408
This key's value is a list of two "numbers." Either "number" may
409
optionally be nil, which is treated like positive infinity. The numbers
410
control how the system handles case splits in the simplifier. See *Note
411
SET-CASE-SPLIT-LIMITATIONS::.
413
:include-book-dir-alist
415
This key's value is used by include-book's :DIR argument to associate a
416
directory with a keyword. An exception is the keyword :SYSTEM for the
417
distributed ACL2 books/ directory; see *Note INCLUDE-BOOK::, in
418
particular the section on "Books Directory."
422
This key's value is either :all, :once, or nil. See *Note
423
SET-MATCH-FREE-DEFAULT::.
427
This key's value is a list of runes. See *Note
428
ADD-MATCH-FREE-OVERRIDE::.
430
:match-free-override-nume
432
This key's value is an integer used in the implementation of
433
add-match-free-override, so that only existing runes are affected by
438
This key's value is either t or nil and indicates whether the user
439
wishes ACL2 to extend the linear arithmetic decision procedure to
440
include non-linear reasoning. See *Note NON-LINEAR-ARITHMETIC::.
442
Note: Unlike all other tables, acl2-defaults-table can affect the
443
soundness of the system. The table mechanism therefore enforces on it a
444
restriction not imposed on other tables: when table is used to update
445
the acl2-defaults-table, the key and value must be variable-free forms.
448
(table acl2-defaults-table :defun-mode :program),
450
(table acl2-defaults-table :defun-mode ':program), and
452
(table acl2-defaults-table :defun-mode (compute-mode *my-data*))
454
are all examples of legal events (assuming compute-mode is a function of
455
one non-state argument that produces a defun-mode as its single value),
457
(table acl2-defaults-table :defun-mode (compute-mode (w state)))
459
is not legal because the value form is state-sensitive.
461
Consider for example the following three events which one might make
462
into the text of a book.
466
(table acl2-defaults-table
468
(if (ld-skip-proofsp state) :logic :program))
470
(defun crash-and-burn (x) (car x))
472
The second event is illegal because its value form is state-sensitive.
473
If it were not illegal, then it would set the :defun-mode to :program
474
when the book was being certified but would set the defun-mode to :logic
475
when the book was being loaded by include-book. That is because during
476
certification, ld-skip-proofsp is nil (proof obligations are generated
477
and proved), but during book inclusion ld-skip-proofsp is non-nil (those
478
obligations are assumed to have been satisfied.) Thus, the above book,
479
when loaded, would create a function in :logic mode that does not
480
actually meet the conditions for such status.
482
For similar reasons, table events affecting acl2-defaults-table are
483
illegal within the scope of local forms. That is, the text
487
(local (table acl2-defaults-table :defun-mode :program))
489
(defun crash-and-burn (x) (car x))
491
is illegal because acl2-defaults-table is changed locally. If this text
492
were acceptable as a book, then when the book was certified,
493
crash-and-burn would be processed in :program mode, but when the
494
certified book was included later, crash-and-burn would have :logic mode
495
because the local event would be skipped.
501
(program) ;which is (table acl2-defaults-table :defun-mode :program)
503
(defun crash-and-burn (x) (car x))
505
is acceptable and defines crash-and-burn in :program mode, both during
506
certification and subsequent inclusion.
508
We conclude with an important observation about the relation between
509
acl2-defaults-table and include-book, certify-book, and encapsulate.
510
Including or certifying a book never has an effect on the
511
acl2-defaults-table, nor does executing an encapsulate event; we always
512
restore the value of this table as a final act. (Also see *Note
513
INCLUDE-BOOK::, see *Note ENCAPSULATE::, and see *Note CERTIFY-BOOK::.)
514
That is, no matter how a book fiddles with the acl2-defaults-table, its
515
value immediately after including that book is the same as immediately
516
before including that book. If you want to set the acl2-defaults-table
517
in a way that persists, you need to do so using commands that are not
518
inside books. It may be useful to set your favorite defaults in your
519
acl2-customization file; see *Note ACL2-CUSTOMIZATION::.
524
File: acl2-doc-emacs.info, Node: ACL2-HELP, Next: ASSIGN, Prev: ACL2-DEFAULTS-TABLE, Up: OTHER
526
ACL2-HELP the acl2-help mailing list
528
You can email questions about ACL2 usage to the acl2-help mailing list:
529
acl2-help@lists.cc.utexas.edu. If you have more general questions about
530
ACL2, for example, about projects completed using ACL2, you may prefer
531
the acl2 mailing list, acl2@lists.cc.utexas.edu, which tends to have
539
File: acl2-doc-emacs.info, Node: ASSIGN, Next: CERTIFY-BOOK!, Prev: ACL2-HELP, Up: OTHER
541
ASSIGN assign to a global variable in state
545
(assign x (expt 2 10))
546
(assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))
551
where symbol is any symbol (with certain enforced exclusions to avoid
552
overwriting ACL2 system "globals") and term is any ACL2 term that could
553
be evaluated at the top-level. Assign evaluates the term, stores the
554
result as the value of the given symbol in the global-table of state,
555
and returns the result. (Note: the actual implementation of the storage
556
of this value is much more efficient than this discussion of the logic
557
might suggest.) Assign is a macro that effectively expands to the more
558
complicated but understandable:
560
(pprogn (f-put-global 'symbol term state)
561
(mv nil (f-get-global 'symbol term state) state)).
563
The macro @ gives convenient access to the value of such globals. The
564
:ubt operation has no effect on the global-table of state. Thus, you
565
may use these globals to hang onto useful data structures even though
566
you may undo back past where you computed and saved them.
571
File: acl2-doc-emacs.info, Node: CERTIFY-BOOK!, Next: CW-GSTACK, Prev: ASSIGN, Up: OTHER
573
CERTIFY-BOOK! a variant of certify-book
577
(certify-book! "my-arith" 3) ;Certify in a world with 3
578
; commands, starting in a world
579
; with at least 3 commands.
580
(certify-book! "my-arith") ;Certify in the initial world.
581
(certify-book! "my-arith" 0 nil) ;As above, but do not compile.
584
(certify-book! book-name k compile-flg)
586
where book-name is a book name (see *Note BOOK-NAME::), k is a
587
nonnegative integer used to indicate the "certification world," and
588
compile-flg indicates whether you wish to compile the (functions in the)
591
This command is identical to certify-book, except that the second
592
argument k may not be t in certify-book! and if k exceeds the current
593
command number, then an appropriate ubt! will be executed first. See
594
*Note CERTIFY-BOOK:: and see *Note UBT!::.
599
File: acl2-doc-emacs.info, Node: CW-GSTACK, Next: EXIT, Prev: CERTIFY-BOOK!, Up: OTHER
601
CW-GSTACK debug a rewriting loop or stack overflow
606
(cw-gstack :frames 10) ; show only the top 10 frames
607
(cw-gstack :frames (1 10)) ; same as above: show only frames 1 through 10
608
(cw-gstack :frames (10 20)) ; show only frames 10 through 20
609
(cw-gstack :evisc-tuple nil) ; print using default "evisceration"
610
(cw-gstack :evisc-tuple x) ; print with evisceration tuple x
612
For the last case above, see *Note LD-EVISC-TUPLE::.
614
Stack overflows may occur, perhaps caused by looping rewrite rules. In
615
some Lisps, especially GCL, stack overflows often manifest themselves as
616
segmentation faults, causing the entire ACL2 image to crash. Finding
617
looping rewrite rules can be tricky, especially if you are using books
618
supplied by other people. (However, see *Note SET-REWRITE-STACK-LIMIT::
619
for a way to avoid stack overflows caused by rewriter loops.)
621
A wonderful trick is the following. When there is a stack overflow
622
during a proof, abort and then try it again after turning on rewrite
623
stack monitoring with :brr t. When the stack overflows again, exit to
624
raw Lisp. How you exit to raw Lisp depends on which Lisp you are using.
625
In Allegro Common Lisp, for example, the stack overflow will leave you
626
in an interactive break. It is often a good idea to exit the break
627
immediately (e.g., using :pop if you use Allegro Common Lisp, or :q
628
using GCL), which will leave you in the top-level ACL2 command loop,
629
after which it is recommended to leave that loop using :q. That will
630
leave you in raw Lisp. Then, execute
634
If the loop is in the rewriter, it will probably be evident! You can
635
re-enter the ACL2 loop now with (lp).
637
Note: By default, cw-gstack "eviscerates" terms, printing abbreviated
638
representations of large terms. The user can control this behavior by
639
using (cw-gstack :evisc-tuple x), where x is nil or an evisceration
640
tuple; see *Note LD-EVISC-TUPLE::. For example, (cw-gstack :evisc-tuple
641
nil) will avoid all evisceration, while the default behavior can be
642
obtained by using (cw-gstack :evisc-tuple '(nil 3 4 (hide))), meaning
643
that substructures deeper than 3 are replaced by "#" and those longer
644
than 4 are replaced by "...", and terms of the form (hide ...) are
647
If you are in GCL the stack overflow may cause a segmentation fault and
648
abort the Lisp job. This makes it harder to debug but here is what you
649
do. First, re-create the situation just prior to submitting the form
650
that will cause the stack overflow. You can do this without suffering
651
through all the proofs by using the :ld-skip-proofsp option of ld to
652
reload your scripts. Before you submit the form that causes the stack
653
overflow, exit the ACL2 command loop with :q. In raw GCL type:
655
(si::use-fast-links nil)
657
This will slow GCL down but make it detect and signal stack overflows
658
rather than overwrite the system memory. Now reenter the ACL2 command
661
Now carry on as described above, turning on rewrite stack monitoring
662
with :brr t and provoking the stack overflow. When it occurs, you will
663
be in an interactive break. Exit to raw Lisp with two successive :q's,
664
one to get out of the error break and the next to get out of the
665
top-level ACL2 command loop. Then in raw GCL execute (cw-gstack).
667
Suggestion: Once you have found the loop and fixed it, you should
668
execute the ACL2 command :brr nil, so that you don't slow down
669
subsequent proof attempts. If you are in GCL, you should also get into
670
raw Lisp and execute (si::use-fast-links t).
677
File: acl2-doc-emacs.info, Node: EXIT, Next: GOOD-BYE, Prev: CW-GSTACK, Up: OTHER
679
EXIT quit entirely out of Lisp
688
File: acl2-doc-emacs.info, Node: GOOD-BYE, Next: LD, Prev: EXIT, Up: OTHER
690
GOOD-BYE quit entirely out of Lisp
696
*Note: Your entire session will disappear forever when you type*
699
The command :good-bye quits not only out of the ACL2 command loop, but
700
in fact quits entirely out of the underlying Lisp. Thus, there is no
701
going back! You will *not* be able to re-enter the command loop after
702
typing :good-bye! All your work will be lost!!!
704
This command may not work in some underlying Common Lisp
705
implementations. But we don't expect there to be any harm in trying.
706
It *does* work in GCL and Allegro CL, at least as of this writing.
708
In some systems, typing control-d at the top-level ACL2 prompt
709
(control-c control-d if inside emacs) will call this function.
711
If you merely want to exit the ACL2 command loop, use :q instead (see
717
File: acl2-doc-emacs.info, Node: LD, Next: PROPS, Prev: GOOD-BYE, Up: OTHER
719
LD the ACL2 read-eval-print loop, file loader, and command processor
723
(LD standard-oi ; open obj in channel, stringp file name
724
; to open and close, or list of forms
726
; Optional keyword arguments:
727
:dir ... ; use this add-include-book-dir directory
728
:standard-co ... ; open char out or file to open and close
729
:proofs-co ... ; open char out or file to open and close
730
:current-package ... ; known package name
731
:ld-skip-proofsp ... ; nil, 'include-book, or t
732
; (see *Note LD-SKIP-PROOFSP::)
733
:ld-redefinition-action ; nil or '(:a . :b)
734
:ld-prompt ... ; nil, t, or some prompt printer fn
735
:ld-keyword-aliases ... ; an alist pairing keywords to parse info
736
:ld-pre-eval-filter ... ; :all, :query, or some new name
737
:ld-pre-eval-print ... ; nil, t, or :never
738
:ld-post-eval-print ... ; nil, t, or :command-conventions
739
:ld-evisc-tuple ... ; nil or '(alist nil nil level length)
740
:ld-error-triples ... ; nil or t
741
:ld-error-action ... ; :return (default), :continue or :error
742
:ld-query-control-alist ; alist supplying default responses
743
:ld-verbose ...) ; nil or t
746
Ld is the top-level ACL2 read-eval-print loop. (When you call lp, a
747
little initialization is done in raw Common Lisp and then ld is called.)
748
ld is also a general-purpose ACL2 file loader and a command interpreter.
749
Ld is actually a macro that expands to a function call involving state.
750
Ld returns an "error/value/state" triple as explained below.
752
The arguments to ld, except for :dir, all happen to be global variables
753
in state. For example, 'current-package and 'ld-verbose are global
754
variables, which may be accessed via (@ current-package) and (@
755
ld-verbose). When ld is called, it "binds" these variables. By "binds"
756
we actually mean the variables are globally set but restored to their
757
old values on exit. Because ld provides the illusion of state global
758
variables being bound, they are called "ld specials" (after the Lisp
759
convention of calling a variable "special" if it is referenced freely
760
after having been bound).
762
Note that all arguments but the first are passed via keyword. Any
763
variable not explicitly given a value in a call retains its pre-call
764
value, with the exception of :ld-error-action, which defaults to :return
765
if not explicitly specified.
767
Just as an example to drive the point home: If current-package is "ACL2"
770
(ld *standard-oi* :current-package "MY-PKG")
772
you would find yourself in (an inner) read-eval-print loop in which the
773
current-package was "MY-PKG". You could operate there as long as you
774
wished, changing the current package at will. But when you typed :q you
775
would return to the outer read-eval-print loop where the current package
776
would still be "ACL2".
778
Roughly speaking, ld repeatedly reads a form from standard-oi, evaluates
779
it, and prints its result to standard-co. It does this until the form
780
evaluates to an error triple whose value component is :q or until the
781
input channel or list is emptied. However, ld has many bells and
782
whistles controlled by the ld specials. Each such special is documented
783
individually. For example, see the documentation for standard-oi,
784
current-package, ld-pre-eval-print, etc.
786
A more precise description of ld is as follows. In the description
787
below we use the ld specials as variables, e.g., we say "a form is read
788
from standard-oi." By this usage we refer to the current value of the
789
named state global variable, e.g., we mean "a form is read from the
790
current value of 'standard-oi." This technicality has an important
791
implication: If while interacting with ld you change the value of one of
792
the ld specials, e.g., 'standard-oi, you will change the behavior of ld,
793
e.g., subsequent input will be taken from the new value.
795
Three ld specials are treated as channels: standard-oi is treated as an
796
object input channel and is the source of forms evaluated by ld;
797
standard-co and proofs-co are treated as character output channels and
798
various flavors of output are printed to them. However, the supplied
799
values of these specials need not actually be channels; several special
800
cases are recognized.
802
If the supplied value of one of these is in fact an open channel of the
803
appropriate type, that channel is used and is not closed by ld. If the
804
supplied value of one of these specials is a string, the string is
805
treated as a file name in (essentially) Unix syntax (see *Note
806
PATHNAME::) and a channel of the appropriate type is opened to/from that
807
file. Any channel opened by ld during the binding of the ld specials is
808
automatically closed by ld upon termination. If standard-co and
809
proofs-co are equal strings, only one channel to that file is opened and
812
As a special convenience, when standard-oi is a string and the :dir
813
argument is also provided, we look up :dir in the table of directories
814
maintained by add-include-book-dir, and prepend this directory to
815
standard-oi to create the filename. (In this case, however, we require
816
that standard-oi is a relative pathname, not an absolute pathname.) For
817
example, one can write (ld "arithmetic/top-with-meta.lisp" :dir :system)
818
to ld that particular system library. (Of course, you should almost
819
always load books like arithmetic/top-with-meta using include-book
820
instead of ld.) If :dir is not specified, then a relative pathname is
821
resolved using the connected book directory; see *Note CBD::.
823
Several other alternatives are allowed for standard-oi. If standard-oi
824
is a true list then it is taken as the list of forms to be processed.
825
If standard-oi is a list ending in an open channel, then ld processes
826
the forms in the list and then reads and processes the forms from the
827
channel. Analogously, if standard-oi is a list ending a string, an
828
object channel from the named file is opened and ld processes the forms
829
in the list followed by the forms in the file. That channel is closed
830
upon termination of ld.
832
The remaining ld specials are handled more simply and generally have to
833
be bound to one of a finite number of tokens described in the :doc
834
entries for each ld special. Should any ld special be supplied an
835
inappropriate value, an error message is printed.
837
Next, if ld-verbose is t, ld prints the message "ACL2 loading name"
838
where name names the file or channel from which forms are being read.
839
At the conclusion of ld, it will print "Finished loading name" if
842
Finally, ld repeatedly executes the ACL2 read-eval-print step, which may
843
be described as follows. A prompt is printed to standard-co if
844
ld-prompt is non-nil. The format of the prompt is determined by
845
ld-prompt. If it is t, the default ACL2 prompt is used. If it is any
846
other non-nil value then it is treated as an ACL2 function that will
847
print the desired prompt. See *Note LD-PROMPT::. In the exceptional
848
case where ld's input is coming from the terminal (*standard-oi*) but
849
its output is going to a different sink (i.e., standard-co is not
850
*standard-co*), we also print the prompt to the terminal.
852
Ld then reads a form from standard-oi. If the object read is a keyword,
853
ld constructs a "keyword command form" by possibly reading several more
854
objects. See *Note KEYWORD-COMMANDS::. This construction process is
855
sensitive to the value of ld-keyword-aliases. See *Note
856
LD-KEYWORD-ALIASES::. Otherwise, the object read is treated as the
859
Ld next decides whether to evaluate or skip this form, depending on
860
ld-pre-eval-filter. Initially, the filter must be either :all, :query,
861
or a new name. If it is :all, it means all forms are evaluated. If it
862
is :query, it means each form that is read is displayed and the user is
863
queried. Otherwise, the filter is a name and each form that is read is
864
evaluated as long as the name remains new, but if the name is ever
865
introduced then no more forms are read and ld terminates. See *Note
866
LD-PRE-EVAL-FILTER::.
868
If the form is to be evaluated, first prints the form to standard-co, if
869
ld-pre-eval-print is t. With this feature, ld can process an input file
870
or form list and construct a script of the session that appears as
871
though each form was typed in. See *Note LD-PRE-EVAL-PRINT::.
873
Ld then evaluates the form, with state bound to the current state. The
874
result is some list of (multiple) values. If a state is among the
875
values, then ld uses that state as the subsequent current state.
877
Depending on ld-error-triples, ld may interpret the result as an
878
"error." See *Note LD-ERROR-TRIPLES::. We first discuss ld's behavior
879
if no error signal is detected (either because none was sent or because
880
ld is ignoring them as per ld-error-triples).
882
In the case of a non-erroneous result, ld does two things: First, if the
883
logical world in the now current state is different than the world
884
before execution of the form, ld adds to the world a "command landmark"
885
containing the form evaluated. See *Note COMMAND-DESCRIPTOR::. Second,
886
ld prints the result to standard-co, according to ld-post-eval-print.
887
If ld-post-eval-print is nil, no result is printed. If it is t, all of
888
the results are printed as a list of (multiple) values. Otherwise, it
889
is :command-conventions and only the non-erroneous "value" component of
890
the result is printed. See *Note LD-POST-EVAL-PRINT::.
892
Whenever ld prints anything (whether the input form, a query, or some
893
results) it "eviscerates" it if ld-evisc-tuple is non-nil. Essentially,
894
evisceration is a generalization of Common Lisp's use of *print-level*
895
and *print-length* to hide large substructures. See *Note
898
We now return to the case of a form whose evaluation signals an error.
899
In this case, ld first restores the ACL2 logical world to what it was
900
just before the erroneous form was evaluated. Thus, a form that
901
partially changes the world (i.e., begins to store properties) and then
902
signals an error, has no effect on the world. You may see this happen
903
on commands that execute several events (e.g., an encapsulate or a progn
904
of several defuns): even though the output makes it appear that the
905
initial events were executed, if an error is signalled by a later event
906
the entire block of events is discarded.
908
After rolling back, ld takes an action determined by ld-error-action.
909
If the action is :continue, ld merely iterates the read-eval-print step.
910
Note that nothing suggestive of the value of the "erroneous" form is
911
printed. If the action is :return, ld terminates normally. If the
912
action is :error, ld terminates signalling an error to its caller. If
913
its caller is in fact another instance of ld and that instance is
914
watching out for error signals, the entire world created by the
915
erroneous inner ld will be discarded by the outer ld.
917
Ld returns an error triple, (mv erp val state). Erp is t or nil
918
indicating whether an error is being signalled. If no error is
919
signalled, val is the "reason" ld terminated and is one of :exit
920
(meaning :q was read), :eof (meaning the input source was exhausted),
921
:error (meaning an error occurred but has been supressed) or :filter
922
(meaning the ld-pre-eval-filter terminated ld).
927
File: acl2-doc-emacs.info, Node: PROPS, Next: PSO, Prev: LD, Up: OTHER
929
PROPS print the ACL2 properties on a symbol
936
Props takes one argument, a symbol, and prints all of the properties
937
that are on that symbol in the ACL2 world.
942
File: acl2-doc-emacs.info, Node: PSO, Next: PSO!, Prev: PROPS, Up: OTHER
944
PSO show the most recently saved output
946
Evaluate :pso in order to print output that was generated in an
947
environment where output was being saved; see *Note SET-SAVED-OUTPUT::
948
for details. However, proof-tree output will be suppressed; use :pso!
949
if you want that output to be printed as well.
956
File: acl2-doc-emacs.info, Node: PSO!, Next: PSTACK, Prev: PSO, Up: OTHER
958
PSO! show the most recently saved output, including proof-tree output
960
Evaluate :pso in order to print output that was generated in an
961
environment where output was being saved; see *Note SET-SAVED-OUTPUT::
962
for details. Note that proof-tree will be included; use :pso if you
963
want that output to be suppressed.
970
File: acl2-doc-emacs.info, Node: PSTACK, Next: Q, Prev: PSO!, Up: OTHER
972
PSTACK seeing what is the prover up to
976
(pstack) ; inspect break
977
(pstack t) ; inspect break, printing all calls in abbreviated form
978
(pstack :all) ; as above, but only abbreviating the ACL2 world
981
When the form (pstack) is executed during a break from a proof, or at
982
the end of a proof that the user has aborted, a "process stack" (or
983
"prover stack") will be printed that gives some idea of what the theorem
984
prover has been doing. Moreover, by evaluating (verbose-pstack t)
985
before starting a proof (see *Note VERBOSE-PSTACK::) one can get
986
trace-like information about prover functions, including time summaries,
987
printed to the screen during a proof. This feature is currently quite
988
raw and may be refined considerably as time goes on, based on user
989
suggestions. For example, the usual control of printing given by
990
set-inhibit-output-lst is irrelevant for printing the pstack.
992
The use of (pstack t) or (pstack :all) should only be used by those who
993
are comfortable looking at functions in the ACL2 source code.
994
Otherwise, simply use (pstack).
999
* VERBOSE-PSTACK:: seeing what is the prover up to (for advanced users)
1002
Entries in the pstack include the following (listed here alphabetically,
1003
except for the first).
1005
preprocess-clause, simplify-clause, etc. (in general,xxx-clause):
1006
top-level processes in the prover "waterfall"
1008
clausify: splitting a goal into subgoals
1010
ev-fncall: evaluating a function on explicit arguments
1012
ev-fncall-meta: evaluating a metafunction
1014
forward-chain: building a context for the current goal using
1015
forward-chaining rules
1017
induct: finding an induction scheme
1019
pop-clause: getting the next goal to prove by induction
1021
process-assumptions: creating forcing rounds
1023
remove-built-in-clauses: removing built-in clauses (see *Note
1026
process-equational-polys: deducing interesting equations
1028
remove-trivial-equivalences: removing trivial equalities (and
1029
equivalences) from the current goal
1031
rewrite-atm: rewriting a top-level term in the current goal
1033
setup-simplify-clause-pot-lst: building the linear arithmetic database
1034
for the current goal
1036
strip-branches, subsumption-replacement-loop: subroutines of clausify
1038
waterfall: top-level proof control
1045
File: acl2-doc-emacs.info, Node: VERBOSE-PSTACK, Prev: PSTACK, Up: PSTACK
1047
VERBOSE-PSTACK seeing what is the prover up to (for advanced users)
1051
(verbose-pstack t) ; get trace-like information on prover during proofs
1052
(verbose-pstack '(fn1 fn2 ...))
1053
; as above, but omit calls of the indicated functions
1054
(verbose-pstack nil) ; turn off trace-like information on prover
1056
For example, (verbose-pstack '(ev-fncall)) will provide a trace of
1057
various prover functions during proofs, except for the function
1060
By evaluating (verbose-pstack t) one can get trace-like information
1061
during subsequent proofs about prover functions, including time
1062
summaries, printed to the screen during a proof. To turn off this
1063
feature, evaluate (verbose-pstack nil). Also See *Note PSTACK::.
1070
File: acl2-doc-emacs.info, Node: Q, Next: QUIT, Prev: PSTACK, Up: OTHER
1072
Q quit ACL2 (type :q) -- reenter with (lp)
1079
The keyword command :q typed at the top-level of the ACL2 loop will
1080
terminate the loop and return control to the Common Lisp top-level (or,
1081
more precisely, to whatever program invoked lp). To reenter the ACL2
1082
loop, execute (acl2::lp) in Common Lisp. You will be in the same state
1083
as you were when you exited with :q, unless during your stay in Common
1084
Lisp you messed the data structures representating the ACL2 state
1085
(including files, property lists, and single-threaded objects).
1087
Unlike all other keyword commands, typing :q is not equivalent to
1088
invoking the function q. There is no function q.
1093
File: acl2-doc-emacs.info, Node: QUIT, Next: REBUILD, Prev: Q, Up: OTHER
1095
QUIT quit entirely out of Lisp
1104
File: acl2-doc-emacs.info, Node: REBUILD, Next: RESET-LD-SPECIALS, Prev: QUIT, Up: OTHER
1106
REBUILD a convenient way to reconstruct your old state
1110
ACL2 !>(rebuild "project.lisp")
1111
ACL2 !>(rebuild "project.lisp" t)
1112
ACL2 !>(rebuild "project.lisp" :all)
1113
ACL2 !>(rebuild "project.lisp" :query)
1114
ACL2 !>(rebuild "project.lisp" 'lemma-22)
1117
Rebuild allows you to assume all the commands in a given file or list,
1118
supplied in the first argument. Because rebuild processes an arbitrary
1119
sequence of commands with ld-skip-proofsp t, it is unsound! However, if
1120
each of these commands is in fact admissible, then processing them with
1121
rebuild will construct the same logical state that you would be in if
1122
you typed each command and waited through the proofs again. Thus,
1123
rebuild is a way to reconstruct a state previously obtained by proving
1124
your way through the commands.
1126
The second, optional argument to rebuild is a "filter" (see *Note
1127
LD-PRE-EVAL-FILTER::) that lets you specify which commands to process.
1128
You may specify t, :all, :query, or a new logical name. t and :all both
1129
mean that you expect the entire file or list to be processed. :query
1130
means that you will be asked about each command in turn. A new name
1131
means that all commands will be processed as long as the name is new,
1132
i.e., rebuild will stop processing commands immediately after executing
1133
a command that introduces name. Rebuild will also stop if any command
1134
causes an error. You may therefore wish to plant an erroneous form in
1135
the file, e.g., (mv t nil state), (see *Note LD-ERROR-TRIPLES::), to
1136
cause rebuild to stop there. The form (i-am-here) is such a pre-defined
1137
form. If you do not specify a filter, rebuild will query you for one.
1139
Inspection of the definition of rebuild, e.g., via :pc rebuild-fn, will
1140
reveal that it is just a glorified call to the function ld. See *Note
1141
LD:: if you find yourself wishing that rebuild had additional
1147
File: acl2-doc-emacs.info, Node: RESET-LD-SPECIALS, Next: SAVE-EXEC, Prev: REBUILD, Up: OTHER
1149
RESET-LD-SPECIALS restores initial settings of the ld specials
1153
(reset-ld-specials t)
1154
(reset-ld-specials nil)
1157
Roughly speaking, the ld specials are certain state global variables,
1158
such as current-package, ld-prompt, and ld-pre-eval-filter, which are
1159
managed by ld as though they were local variables. These variables
1160
determine the channels on which ld reads and prints and control many
1161
options of ld. See *Note LD:: for the details on what the ld specials
1164
This function, reset-ld-specials, takes one Boolean argument, flg. The
1165
function resets all of the ld specials to their initial, top-level
1166
values, except for the three channel variables, standard-oi,
1167
standard-co, and proofs-co, which are reset to their initial values only
1168
if flg is non-nil. Of course, if you are in a recursive call of ld,
1169
then when you exit that call, the ld specials will be restored to the
1170
values they had at the time ld was called recursively. To see what the
1171
initial values are, inspect the value of the constant
1172
*initial-ld-special-bindings*.
1177
File: acl2-doc-emacs.info, Node: SAVE-EXEC, Next: SET-GUARD-CHECKING, Prev: RESET-LD-SPECIALS, Up: OTHER
1179
SAVE-EXEC save an executable image and (for most Common Lisps) a wrapper script
1181
See *Note SAVING-AND-RESTORING:: for an explanation of why one might
1182
want to use this function.
1185
; Save an executable named my-saved_acl2:
1186
(save-exec "my-saved_acl2"
1187
"This saved image includes Version 7 of Project Foo.")
1189
; Same as above, but with a generic comment instead:
1190
(save-exec "my-saved_acl2" nil)
1193
(save-exec exec-filename extra-startup-string)
1195
where exec-filename is the filename of the proposed executable and
1196
extra-startup-string is a non-empty string to be printed after the
1197
normal ACL2 startup message when you start up the saved image. However,
1198
extra-startup-string is allowed to be nil, in which case a generic
1199
string will be printed instead.
1201
*Note*: For technical reasons, we require that you first execute :q, to
1202
exit the ACL2 read-eval-print loop, before evaluating a save-exec call.
1204
For most Common Lisps, the specified file (e.g., "my-saved_acl2" in the
1205
examples above) will be written as a small script, which in turn invokes
1206
a saved image to which an extension has been appended (e.g.,
1207
my-saved_acl2.gcl for the examples above, when the underlying Common
1208
Lisp is GCL on a non-Windows system).
1213
File: acl2-doc-emacs.info, Node: SET-GUARD-CHECKING, Next: SET-INHIBIT-OUTPUT-LST, Prev: SAVE-EXEC, Up: OTHER
1215
SET-GUARD-CHECKING control checking guards during execution of top-level forms
1217
Detailed comments about the arguments of this function may be found
1218
elsewhere: see *Note GUARD-EVALUATION-TABLE::. Here we provide an
1219
introduction to the use of set-guard-checking.
1221
New users are encouraged to execute one of the following forms in order
1222
to avoid evaluation errors due to guards:
1224
(set-guard-checking :none)
1225
(set-guard-checking nil)
1227
The former avoids all guard-checking on user-defined functions and
1228
should generally work fine for new users, the only drawback being
1229
efficiency loss on compute-intensive problems. All settings other than
1230
:none check guards, but a value of nil allows evaluation to continue in
1231
the logic when guards fail (avoiding the raw Lisp definition in that
1234
You may put one of the above forms in the "acl2-customization.lisp" file
1235
in your current directory (see *Note CBD::) or your home directory; see
1236
*Note ACL2-CUSTOMIZATION::.
1238
Note that guards are not part of the ACL2 logic, and hence new users can
1239
completely ignore the notion of guard (and the rest of this
1240
documentation section after this paragraph!). For example, (car 3) and
1241
nil can be proved equal in the ACL2 logic, as follows, even though the
1242
guard on car requires its first argument to be a cons pair or nil.
1244
(thm (equal (car 3) nil))
1246
Moreover, unless your functions or top-level forms call built-in ACL2
1247
functions that are defined in :program mode, the following property will
1250
Evaluation of (set-guard-checking :none) will allow evaluation of
1251
forms such as (car 3) to take place without error in the top level
1252
loop, not only when proving theorems.
1256
If you feel bold, then you may wish to read the rest of this
1257
documentation topic; also see *Note GUARD::.
1259
See *Note GUARD-EVALUATION-TABLE:: for a succinct table, with associated
1260
discussion, that covers in detail the material presented in the rest of
1263
The top-level ACL2 loop has a variable which controls which sense of
1264
execution is provided. To turn "guard checking on," by which we mean
1265
that guards are checked at runtime, execute the top-level form
1266
:set-guard-checking t. To allow guard violations, do
1267
:set-guard-checking nil, or do :set-guard-checking :none to turn off all
1268
guard-checking, so that raw Lisp definitions of user-defined functions
1269
are avoided unless their guard is t. The status of guard-checking is
1270
reflected in the prompt.
1274
means guard checking is on and
1278
means guard checking is off. The exclamation mark can be thought of as
1279
"barring" certain computations. The absence of the mark suggests the
1280
absence of error messages or unbarred access to the logical axioms.
1285
will signal an error, while
1291
We will return at the end of this documentation topic to discuss two
1292
other values, :all and :nowarn, for :set-guard-checking. We also note
1293
that evaluation of built-in :program mode functions always takes place
1296
Whether guards are checked during evaluation is independent of the
1297
default-defun-mode. We note this simply because it is easy to confuse
1298
":program mode" with "evaluation in Common Lisp" and thus with "guard
1299
checking on;" and it is easy to confuse ":logic mode" with "evaluation
1300
in the logic" and with "guard checking off." But the default-defun-mode
1301
determines whether newly submitted definitions introduce programs or add
1302
logical axioms. That mode is independent of whether evaluation checks
1303
guards or not. You can operate in :logic mode with runtime guard
1304
checking on or off. Analogously, you can operate in :program mode with
1305
runtime guard checking on or off.
1307
For further discussion on evaluation and guards see *Note
1308
GUARDS-AND-EVALUATION::, in particular the exception for safe-mode in
1309
the "Aside" there. See *Note GUARD::for a general discussion of guards.
1311
Now we fulfill our promise above to discuss two other values for
1312
:set-guard-checking:
1314
:set-guard-checking :nowarn
1315
:set-guard-checking :all
1317
The meaning of these values is perhaps best described by the following
1318
example provided by David Rager.
1320
ACL2 !>(defun my-test (expr)
1321
(declare (xargs :guard (true-listp expr)
1322
:verify-guards nil))
1325
(cons (my-test (car expr))
1326
(my-test (cdr expr)))))
1328
The admission of MY-TEST is trivial, using the relation O< (which is
1329
known to be well-founded on the domain recognized by O-P) and the measure
1330
(ACL2-COUNT EXPR). We could deduce no constraints on the type of MY-
1331
TEST. However, in normalizing the definition we used primitive type
1335
Form: ( DEFUN MY-TEST ...)
1336
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
1338
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
1340
ACL2 !>(my-test '(a b c))
1342
ACL2 Warning [Guards] in TOP-LEVEL: Guard-checking will be inhibited
1343
on recursive calls of the executable counterpart (i.e., in the ACL2
1344
logic) of MY-TEST. To check guards on all recursive calls:
1345
(set-guard-checking :all)
1346
To leave behavior unchanged except for inhibiting this message:
1347
(set-guard-checking :nowarn)
1352
If you think about evaluation of (my-test '(a b c)), you will see that
1353
it leads to the recursive call (my-test 'a), which one might expect to
1354
cause a guard violation since the symbol a is not a true-listp.
1355
However, as the warning above explains, we do not by default check
1356
guards on recursive calls. The reason is efficiency -- imagine a simple
1357
definition with a guard that is slow to evaluate. The values :nowarn
1358
and :all for :set-guard-checking have been introduced as ways of dealing
1359
with the above warning. The value :nowarn simply turns off the warning
1360
above. The value :all causes all guards to be checked, even on
1361
recursive calls and even on all calls of non-built-in :program mode
1362
functions --- unless, of course, a call is made of a function whose
1363
guard has been verified (see *Note VERIFY-GUARDS::), where the arguments
1364
satisfy the guard, in which case the corresponding call is made in raw
1365
Lisp without subsidiary guard-checking. We still say that
1366
"guard-checking is on" after :set-guard-checking is invoked with values
1367
t, :nowarn, and :all, otherwise (after value nil) we say "guard-checking
1370
For technical reasons, :all does not have its advertised effect in the
1371
case of built-in :program-mode functions. If you are interested in this
1372
technical detail, see the comment "In the boot-strap world..." in source
1373
function oneify-cltl-code.
1375
We conclude with a remark about the use of :set-guard-checking for
1376
experimenting with ACL2 as a logic or as a programming language. If one
1377
views ACL2 as a logic, one may wish to use :set-guard-checking :none,
1378
while if instead one views ACL2 as a functional programming language,
1379
one may wish to use :set-guard-checking :all. The following transcript
1380
illustrates this distinction by way of example. Specifically, (car 3)
1381
is equal to nil in the ACL2 logic, but may be viewed as a programming
1382
error. The default of :set-guard-checking t is problematic for learning
1383
ACL2 using :program mode functions, since one can get raw Lisp errors.
1384
In the example below, the raw Lisp error occurs because foo implicitly
1385
has a guard of t, hence (foo 3) is evaluated in raw Lisp, which leads to
1386
a raw Lisp call of c[(car 3)].
1388
ACL2 !>(defun foo (x)
1389
(declare (xargs :mode :program))
1393
Form: ( DEFUN FOO ...)
32
File: acl2-doc-emacs.info, Node: LD-SKIP-PROOFSP, Next: LD-VERBOSE, Prev: LD-REDEFINITION-ACTION, Up: MISCELLANEOUS
34
LD-SKIP-PROOFSP how carefully ACL2 processes your commands
37
ACL2 !>(set-ld-skip-proofsp t state)
39
ACL2 !s>(set-ld-skip-proofsp nil state)
41
ACL2 !>(set-ld-skip-proofsp 'include-book state)
45
A global variable in the ACL2 state, called 'ld-skip-proofsp,
46
determines the thoroughness with which ACL2 processes your commands.
47
This variable may take on one of three values: t, nil or 'include-book.
48
When ld-skip-proofsp is non-nil, the system assumes that which ought
49
to be proved and is thus unsound. The form (set-ld-skip-proofsp flg
50
state) is the general-purpose way of setting ld-skip-proofsp. This
51
global variable is an "ld special," which is to say, you may call ld in
52
such a way as to "bind" this variable for the dynamic extent of the ld.
54
When ld-skip-proofsp is non-nil, the default prompt displays the
55
character s. Thus, the prompt
59
means that the default defun-mode is :logic (otherwise the character p,
60
for :program, would also be printed; see *note DEFAULT-PRINT-PROMPT::)
61
but "proofs are being skipped."
63
Observe that there are two legal non-nil values, t and 'include-book.
64
When ld-skip-proofsp is t, ACL2 skips all proof obligations but
65
otherwise performs all other required analysis of input events. When
66
ld-skip-proofsp is 'include-book, ACL2 skips not only proof obligations
67
but all analysis except that required to compute the effect of
68
successfully executed events. To explain the distinction, let us
69
consider one particular event, say a defun. Very roughly speaking, a
70
defun event normally involves a check of the syntactic well-formedness
71
of the submitted definition, the generation and proof of the
72
termination conditions, and the computation and storage of various
73
rules such as a :definition rule and some :type-prescription rules. By
74
"normally" above we mean when ld-skip-proofsp is nil. How does a defun
75
behave when ld-skip-proofsp is non-nil?
77
If ld-skip-proofsp is t, then defun performs the syntactic
78
well-formedness checks and computes and stores the various rules, but
79
it does not actually carry out the termination proofs. If
80
ld-skip-proofsp is 'include-book, defun does not do the syntactic
81
well-formedness check nor does it carry out the termination proof.
82
Instead, it merely computes and stores the rules under the assumption
83
that the checks and proofs would all succeed. Observe that a setting
84
of 'include-book is "stronger" than a setting of t in the sense that
85
'include-book causes defun to assume even more about the admissibility
86
of the event than t does.
88
As one might infer from the choice of name, the include-book event sets
89
ld-skip-proofsp to 'include-book when processing the events in a book
90
being loaded. Thus, include-book does the miminal work necessary to
91
carry out the effects of every event in the book. The syntactic checks
92
and proof obligations were, presumably, successfully carried out when
93
the book was certified.
95
A non-nil value for ld-skip-proofsp also affects the system's output
96
messages. Event summaries (the paragraphs that begin "Summary" and
97
display the event forms, rules used, etc.) are not printed when
98
ld-skip-proofsp is non-nil. Warnings and observations are printed when
99
ld-skip-proofsp is t but are not printed when it is 'include-book.
101
Intuitively, ld-skip-proofsp t means skip just the proofs and otherwise
102
do all the work normally required for an event; while ld-skip-proofsp
103
'include-book is "stronger" and means do as little as possible to
104
process events. In accordance with this intuition, local events are
105
processed when ld-skip-proofsp is t but are skipped when
106
ld-skip-proofsp is 'include-book.
108
The ACL2 system itself uses only two settings, nil and 'include-book,
109
the latter being used only when executing the events inside of a book
110
being included. The ld-skip-proofsp setting of t is provided as a
111
convenience to the user. For example, suppose one has a file of
112
events. By loading it with ld with ld-skip-proofsp set to t, the
113
events can all be checked for syntactic correctness and assumed without
114
proof. This is a convenient way to recover a state lost by a system
115
crash or to experiment with a modification of an events file.
117
The foregoing discussion is actually based on a lie. ld-skip-proofsp
118
is allowed two other values, 'initialize-acl2 and
119
'include-book-with-locals. The first causes behavior similar to t but
120
skips local events and avoids some error checks that would otherwise
121
prevent ACL2 from properly booting. The second is identical to
122
'include-book but also executes local events. These additional values
123
are not intended for use by the user, but no barriers to their use have
126
We close by reminding the user that ACL2 is potentially unsound if
127
ld-skip-proofsp is ever set by the user. We provide access to it
128
simply to allow experimentation and rapid reconstruction of lost or
129
modified logical worlds.
132
File: acl2-doc-emacs.info, Node: LD-VERBOSE, Next: LEMMA-INSTANCE, Prev: LD-SKIP-PROOFSP, Up: MISCELLANEOUS
134
LD-VERBOSE determines whether ld prints ``ACL2 Loading ...''
136
Ld-verbose is an ld special (see *note LD::). The accessor is
137
(ld-verbose state) and the updater is (set-ld-verbose val state).
138
Ld-verbose must be t, nil or a string or consp suitable for fmt
139
printing via the ~@ command. The initial value of ld-verbose is a fmt
140
message that prints the ACL2 version number, ld level and connected
143
Before processing the forms in standard-oi, ld may print a header. The
144
printing of this header is controlled by ld-verbose. If ld-verbose is
145
nil, no header is printed. If it is t, ld prints the message
149
where <file> is the input channel supplied to ld. A similar message is
150
printed when ld completes. If ld-verbose is neither t nor nil then it
151
is presumably a header and is printed with the ~@ fmt directive before
152
ld begins to read and process forms. In this case the ~@ fmt directive
153
is interpreted in an environment in which #\v is the ACL2 version
154
string, #\l is the level of the current recursion in ld and/or
155
wormhole, and #\c is the connected book directory (cbd).
158
File: acl2-doc-emacs.info, Node: LEMMA-INSTANCE, Next: LINEAR-ARITHMETIC, Prev: LD-VERBOSE, Up: MISCELLANEOUS
160
LEMMA-INSTANCE an object denoting an instance of a theorem
162
Lemma instances are the objects one provides via :use and :by hints
163
(see *note HINTS::) to bring to the theorem prover's attention some
164
previously proved or easily provable fact. A typical use of the :use
165
hint is given below. The value specified is a list of five lemma
168
:use (reverse-reverse
169
(:type-prescription app)
170
(:instance assoc-of-app
172
(:functional-instance p-f
173
(p consp) (f flatten))
174
(:instance (:theorem (equal x x))
177
Observe that an event name can be a lemma instance. The :use hint
178
allows a single lemma instance to be provided in lieu of a list, as in:
184
:use (:instance assoc-of-app (x a) (y b) (z c))
186
A lemma instance denotes a formula which is either known to be a
187
theorem or which must be proved to be a theorem before it can be used.
188
To use a lemma instance in a particular subgoal, the theorem prover
189
adds the formula as a hypothesis to the subgoal before the normal
190
theorem proving heuristics are applied.
192
A lemma instance, or lmi, is of one of the following five forms:
194
(1) name, where name names a previously proved theorem, axiom, or
195
definition and denotes the formula (theorem) of that name.
197
(2) rune, where rune is a rune (see *note RUNE::) denoting the
198
:corollary justifying the rule named by the rune.
200
(3) (:theorem term), where term is any term alleged to be a theorem.
201
Such a lemma instance denotes the formula term. But before using such a
202
lemma instance the system will undertake to prove term.
204
(4) (:instance lmi (v1 t1) ... (vn tn)), where lmi is recursively a
205
lemma instance, the vi's are distinct variables and the ti's are terms.
206
Such a lemma instance denotes the formula obtained by instantiating
207
the formula denoted by lmi, replacing each vi by ti.
209
(5) (:functional-instance lmi (f1 g1) ... (fn gn)), where lmi is
210
recursively a lemma instance and each fi is an "instantiable" function
211
symbol of arity ni and gi is a function symbol or a pseudo-lambda
212
expression of arity ni. An instantiable function symbol is any defined
213
or constrained function symbol except the primitives not, member,
214
implies, and o<, and a few others, as listed by the constant
215
*non-instantiable-primitives*. These are built-in in such a way that we
216
cannot recover the constraints on them. A pseudo-lambda expression is
217
an expression of the form (lambda (v1 ... vn) body) where the vi are
218
distinct variable symbols and body is any term. No a priori relation
219
is imposed between the vi and the variables of body, i.e., body may
220
ignore some vi's and may contain "free" variables. However, we do not
221
permit v to occur freely in body if the functional substitution is to
222
be applied to any formula (lmi or the constraints to be satisfied) in a
223
way that inserts v into the scope of a binding of v by let or mv-let
224
(or, lambda). If you happen to violate this restriction, an
225
informative error message will be printed. That message will list for
226
you the potentially illegal choices for v in the context in which the
227
functional substitution is offered. A :functional-instance lemma
228
instance denotes the formula obtained by functionally instantiating the
229
formula denoted by lmi, replacing fi by gi. However, before such a
230
lemma instance can be used, the system will generate proof obligations
231
arising from the replacement of the fi's by the gi's in constraints
232
that "support" the lemma to be functionally instantiated; see *note
233
CONSTRAINT::. One might expect that if the same instantiated
234
constraint were generated on behalf of several events, then each of
235
those instances would have to be proved. However, for the sake of
236
efficiency, ACL2 stores the fact that such an instantiated constraint
237
has been proved and avoids it in future events.
239
Obscure case for definitions. If the lemma instance refers to a
240
:definition rune, then it refers to the corollary formula of that rune,
241
which can be a simplified ("normalized") form of the original formula.
242
However, if the hint is a :by hint and the lemma instance is based on a
243
name (i.e., a symbol), rather than a rune, then the formula is the
244
original formula of the event, as shown by :pe, rather than the
245
normalized version, as shown by :pf. This is as one would expect: If
246
you supply the name of an event, you expect it to refer to the original
247
event. For :use hints we use the simplified (normalized) form instead,
248
which is reasonable since one would expect simplification during the
249
proof that re-traces the normalization done at the time the rule was
252
See *Note FUNCTIONAL-INSTANTIATION-EXAMPLE:: for an example of the use
253
of :functional-instance (so-called "functional instantiation)."
256
File: acl2-doc-emacs.info, Node: LINEAR-ARITHMETIC, Next: LOCAL-INCOMPATIBILITY, Prev: LEMMA-INSTANCE, Up: MISCELLANEOUS
258
LINEAR-ARITHMETIC A description of the linear arithmetic decision procedure
260
We describe the procedure very roughly here. Fundamental to the
261
procedure is the notion of a linear polynomial inequality. A "linear
262
polynomial" is a sum of terms, each of which is the product of a
263
rational constant and an "unknown." The "unknown" is permitted to be 1
264
simply to allow a term in the sum to be constant. Thus, an example
265
linear polynomial is 3*x + 7*a + 2; here x and a are the (interesting)
266
unknowns. However, the unknowns need not be variable symbols. For
267
example, (length x) might be used as an unknown in a linear polynomial.
268
Thus, another linear polynomial is 3*(length x) + 7*a. A "linear
269
polynomial inequality" is an inequality (either < or <=) relation
270
between two linear polynomials. Note that an equality may be
271
considered as a pair of inequalities; e.q., 3*x + 7*a + 2 = 0 is the
272
same as the conjunction of 3*x + 7*a + 2 <= 0 and 0 <= 3*x + 7*a + 2.
274
Certain linear polynomial inequalities can be combined by
275
cross-multiplication and addition to permit the deduction of a third
276
inequality with fewer unknowns. If this deduced inequality is
277
manifestly false, a contradiction has been deduced from the assumed
280
For example, suppose we have two assumptions
285
and we wish to prove that, given p1 and p2, a < 0. As suggested above,
286
we proceed by assuming the negation of our goal
290
and looking for a contradiction.
292
By cross-multiplying and adding the first two inequalities, (that is,
293
multiplying p1 by 2, p2 by 3 and adding the respective sides), we
294
deduce the intermediate result
296
p4: 6*x + 14*a + 9 < 8 + 6*x
298
which, after cancellation, is:
302
If we then cross-multiply and add p3 to p4, we get
306
a contradiction. Thus, we have proved that p1 and p2 imply the
309
All of the unknowns of an inequality must be eliminated by cancellation
310
in order to produce a constant inequality. We can choose to eliminate
311
the unknowns in any order, but we eliminate them in term-order, largest
312
unknowns first. (See *Note TERM-ORDER::.) That is, two polys are
313
cancelled against each other only when they have the same largest
314
unknown. For instance, in the above example we see that x is the
315
largest unknown in each of p1 and p2, and a in p3 and p4.
317
Now suppose that this procedure does not produce a contradiction but
318
instead yields a set of nontrivial inequalities. A contradiction might
319
still be deduced if we could add to the set some additional
320
inequalities allowing further cancellations. That is where :linear
321
lemmas come in. When the set of inequalities has stabilized under
322
cross-multiplication and addition and no contradiction is produced, we
323
search the data base of :linear rules for rules about the unknowns that
324
are candidates for cancellation (i.e., are the largest unknowns in
325
their respective inequalities). See *Note LINEAR:: for a description
326
of how :linear rules are used.
328
See also non-linear-arithmetic for a description of an extension to the
329
linear-arithmetic procedure described here.
332
File: acl2-doc-emacs.info, Node: LOCAL-INCOMPATIBILITY, Next: LOGICAL-NAME, Prev: LINEAR-ARITHMETIC, Up: MISCELLANEOUS
334
LOCAL-INCOMPATIBILITY when non-local events won't replay in isolation
336
Sometimes a "local incompatibility" is reported while attempting to
337
embed some events, as in an encapsulate or include-book. This is
338
generally due to the use of a locally defined name in a non-local event
339
or the failure to make a witnessing definition local.
341
local incompatibilities may be detected while trying to execute the
342
strictly non-local events of an embedding. For example, encapsulate
343
operates by first executing all the events (local and non-local) with
344
ld-skip-proofsp nil, to confirm that they are all admissible. Then it
345
attempts merely to assume the non-local ones to create the desired
346
theory, by executing the events with ld-skip-proofsp set to
347
'include-book. Similarly, include-book assumes the non-local ones,
348
with the understanding that a previously successful certify-book has
349
performed the admissiblity check.
351
How can a sequence of events admitted with ld-skip-proofsp nil fail
352
when ld-skip-proofsp is 'include-book? The key observation is that in
353
the latter case only the non-local events are processed. The local
354
ones are skipped and so the non-local ones must not depend upon them.
356
Two typical mistakes are suggested by the detection of a local
357
incompatibility: (1) a locally defined function or macro was used in a
358
non-local event (and, in the case of encapsulate, was not included
359
among the signatures) and (2) the witnessing definition of a function
360
that was included among the signatures of an encapsulate was not made
363
An example of mistake (1) would be to include among your encapsulated
364
events both (local (defun fn ...)) and (defthm lemma (implies (fn ...)
365
...)). Observe that fn is defined locally but a formula involving fn
366
is defined non-locally. In this case, either the defthm should be made
367
local or the defun should be made non-local.
369
An example of mistake (2) would be to include (fn (x) t) among your
370
signatures and then to write (defun fn (x) ...) in your events, instead
371
of (local (defun fn ...)).
373
One subtle aspect of encapsulate is that if you constrain any member of
374
a mutually recursive clique you must define the entire clique locally
375
and then you must constrain those members of it you want axiomatized
378
Errors due to local incompatibility should never occur in the
379
assumption of a fully certified book. Certification ensures against
380
it. Therefore, if include-book reports an incompatibility, we assert
381
that earlier in the processing of the include-book a warning was
382
printed advising you that some book was uncertified. If this is not
383
the case -- if include-book reports an incompatibility and there has
384
been no prior warning about lack of certification -- please report it
387
When a local incompatibility is detected, we roll-back to the world in
388
which we started the encapsulate or include-book. That is, we discard
389
the intermediate world created by trying to process the events skipping
390
proofs. This is clean, but we realize it is very frustrating because
391
the entire sequence of events must be processed from scratch. Assuming
392
that the embedded events were, once upon a time, processed as top-level
393
commands (after all, at some point you managed to create this sequence
394
of commands so that the local and non-local ones together could survive
395
a pass in which proofs were done), it stands to reason that we could
396
define a predicate that would determine then, before you attempted to
397
embed them, if local incompatibilities exist. We hope to do that,
400
We conclude with a subtle example of local incompatibility. The problem
401
is that in order for foo-type-prescription to be admitted using the
402
specified :typed-term (foo x), the conclusion (my-natp (foo x)) depends
403
on my-natp being a compound-recognizer. This is fine on the first pass
404
of the encapsulate, during which lemma my-natp-cr is admitted. But
405
my-natp-cr is skipped on the second pass because it is marked local,
406
and this causes foo-type-prescription to fail on the second pass.
409
(declare (xargs :guard t))
418
(local (defthm my-natp-cr
422
:rule-classes :compound-recognizer))
423
(defthm foo-type-prescription
425
:hints (("Goal" :in-theory (enable foo)))
426
:rule-classes ((:type-prescription :typed-term (foo x)))))
429
File: acl2-doc-emacs.info, Node: LOGICAL-NAME, Next: LOOP-STOPPER, Prev: LOCAL-INCOMPATIBILITY, Up: MISCELLANEOUS
431
LOGICAL-NAME a name created by a logical event
439
"project/task-1/arith.lisp"
442
A logical name is either a name introduced by some event, such as
443
defun, defthm, or include-book, or else is the keyword :here, which
444
refers to the most recent such event. See *Note EVENTS::. Every
445
logical name is either a symbol or a string. For the syntactic rules
446
on names, see *note NAME::. The symbols name functions, macros,
447
constants, axioms, theorems, labels, and theories. The strings name
448
packages or books. We permit the keyword symbol :here to be used as a
449
logical name denoting the most recently completed event.
451
The logical name introduced by an include-book is the full book name
452
string for the book (see *note FULL-BOOK-NAME::). Thus, under the
453
appropriate setting for the current book directory (see *note CBD::)
454
the event (include-book "arith") may introduce the logical name
456
"/usr/home/smith/project/task-1/arith.lisp" .
458
Under a different cbd setting, it may introduce a different logical
461
"/local/src/acl2/library/arith.lisp" .
463
It is possible that identical include-book events forms in a session
464
introduce two different logical names because of the current book
467
A logical name that is a string is either a package name or a book
468
name. If it is not a package name, we support various conventions to
469
interpret it as a book name. If it does not end with the string
470
".lisp" we extend it appropriately. Then, we search for any book name
471
that has the given logical name as a terminal substring. Suppose
472
(include-book "arith") is the only include-book so far and that
473
"/usr/home/smith/project/task-1/arith.lisp" is the source file it
474
processed. Then "arith", "arith.lisp" and "task-1/arith.lisp" are all
475
logical names identifying that include-book event (unless they are
476
package names). Now suppose a second (include-book "arith") is
477
executed and processes "/local/src/acl2/library/arith.lisp". Then
478
"arith" is no longer a logical name, because it is ambiguous. However,
479
"task-1/arith" is a logical name for the first include-book and
480
"library/arith" is a logical name for the second. Indeed, the first
481
can be named by "1/arith" and the second by "y/arith".
483
Logical names are used primarily in the theory manipulation functions,
484
e.g., universal-theory and current-theory with which you may obtain
485
some standard theories as of some point in the historical past. The
486
reference points are the introductions of logical names, i.e., the past
487
is determined by the events it contains. One might ask, "Why not
488
discuss the past with the much more flexible language of command
489
descriptors?" (See *Note COMMAND-DESCRIPTOR::.) The reason is that
490
inside of such events as encapsulate or macro commands that expand to
491
progns of events, command descriptors provide too coarse a grain.
493
When logical names are used as referents in theory expressions used in
494
books, one must consider the possibility that the defining event within
495
the book in question becomes redundant by the definition of the name
496
prior to the assumption of the book. See *Note REDUNDANT-EVENTS::.
499
File: acl2-doc-emacs.info, Node: LOOP-STOPPER, Next: LP, Prev: LOGICAL-NAME, Up: MISCELLANEOUS
501
LOOP-STOPPER limit application of permutative rewrite rules
503
See *Note RULE-CLASSES:: for a discussion of the syntax of the
504
:loop-stopper field of :rewrite rule-classes. Here we describe how
505
that field is used, and also how that field is created when the user
506
does not explicitly supply it.
508
For example, the built-in :rewrite rule commutativity-of-+,
510
(implies (and (acl2-numberp x)
512
(equal (+ x y) (+ y x))),
514
creates a rewrite rule with a loop-stopper of ((x y binary-+)). This
515
means, very roughly, that the term corresponding to y must be "smaller"
516
than the term corresponding to x in order for this rule to apply.
517
However, the presence of binary-+ in the list means that certain
518
functions that are "invisible" with respect to binary-+ (by default,
519
unary- is the only such function) are more or less ignored when making
520
this "smaller" test. We are much more precise below.
522
Our explanation of loop-stopping is in four parts. First we discuss
523
ACL2's notion of "term order." Next, we bring in the notion of
524
"invisibility", and use it together with term order to define orderings
525
on terms that are used in the loop-stopping algorithm. Third, we
526
describe that algorithm. These topics all assume that we have in hand
527
the :loop-stopper field of a given rewrite rule; the fourth and final
528
topic describes how that field is calculated when it is not supplied by
531
ACL2 must sometimes decide which of two terms is syntactically simpler.
532
It uses a total ordering on terms, called the "term order." Under
533
this ordering constants such as '(a b c) are simpler than terms
534
containing variables such as x and (+ 1 x). Terms containing variables
535
are ordered according to how many occurrences of variables there are.
536
Thus x and (+ 1 x) are both simpler than (cons x x) and (+ x y). If
537
variable counts do not decide the order, then the number of function
538
applications are tried. Thus (cons x x) is simpler than (+ x (+ 1 y))
539
because the latter has one more function application. Finally, if the
540
number of function applications do not decide the order, a
541
lexicographic ordering on Lisp objects is used. See *Note TERM-ORDER::
544
When the loop-stopping algorithm is controlling the use of permutative
545
:rewrite rules it allows term1 to be moved leftward over term2 only if
546
term1 is smaller, in a suitable sense. Note: The sense used in
547
loop-stopping is *not* the above explained term order but a more
548
complicated ordering described below. The use of a total ordering
549
stops rules like commutativity from looping indefinitely because it
550
allows (+ b a) to be permuted to (+ a b) but not vice versa, assuming a
551
is smaller than b in the ordering. Given a set of permutative rules
552
that allows arbitrary permutations of the tips of a tree of function
553
calls, this will normalize the tree so that the smallest argument is
554
leftmost and the arguments ascend in the order toward the right. Thus,
555
for example, if the same argument appears twice in the tree, as x does
556
in the binary-+ tree denoted by the term (+ a x b x), then when the
557
allowed permutations are done, all occurrences of the duplicated
558
argument in the tree will be adjacent, e.g., the tree above will be
559
normalized to (+ a b x x).
561
Suppose the loop-stopping algorithm used term order, as noted above,
562
and consider the binary-+ tree denoted by (+ x y (- x)). The arguments
563
here are in ascending term order already. Thus, no permutative rules
564
are applied. But because we are inside a +-expression it is very
565
convenient if x and (- x) could be given virtually the same position in
566
the ordering so that y is not allowed to separate them. This would
567
allow such rules as (+ i (- i) j) = j to be applied. In support of
568
this, the ordering used in the control of permutative rules allows
569
certain unary functions, e.g., the unary minus function above, to be
570
"invisible" with respect to certain "surrounding" functions, e.g., +
573
Briefly, a unary function symbol fn1 is invisible with respect to a
574
function symbol fn2 if fn2 belongs to the value of fn1 in
575
invisible-fns-table; also see *note SET-INVISIBLE-FNS-TABLE::, which
576
explains its format and how it can be set by the user. Roughly
577
speaking, "invisible" function symbols are ignored for the purposes of
580
Consider the example above, (+ x y (- x)). The translated version of
581
this term is (binary-+ x (binary-+ y (unary- x))). The initial
582
invisible-fns-table makes unary- invisible with repect to binary-+.
583
The commutativity rule for binary-+ will attempt to swap y and (unary-
584
x) and the loop-stopping algorithm is called to approve or disapprove.
585
If term order is used, the swap will be disapproved. But term order is
586
not used. While the loop-stopping algorithm is permuting arguments
587
inside a binary-+ expression, unary- is invisible. Thus, insted of
588
comparing y with (unary- x), the loop-stopping algorithm compares y
589
with x, approving the swap because x comes before y.
591
Here is a more precise specification of the total order used for
592
loop-stopping with respect to a list, fns, of functions that are to be
593
considered invisible. Let x and y be distinct terms; we specify when
594
"x is smaller than y with respect to fns." If x is the application of
595
a unary function symbol that belongs to fns, replace x by its argument.
596
Repeat this process until the result is not the application of such a
597
function; let us call the result x-guts. Similarly obtain y-guts from
598
y. Now if x-guts is the same term as y-guts, then x is smaller than y
599
in this order iff x is smaller than y in the standard term order. On
600
the other hand, if x-guts is different than y-guts, then x is smaller
601
than y in this order iff x-guts is smaller than y-guts in the standard
604
Now we may describe the loop-stopping algorithm. Consider a rewrite
605
rule with conclusion (equiv lhs rhs) that applies to a term x in a
606
given context; see *note REWRITE::. Suppose that this rewrite rule has
607
a loop-stopper field (technically, the :heuristic-info field) of ((x1
608
y1 . fns-1) ... (xn yn . fns-n)). (Note that this field can be
609
observed by using the command :pr with the name of the rule; see *note
610
PR::.) We describe when rewriting is permitted. The simplest case is
611
when the loop-stopper list is nil (i.e., n is 0); in that case,
612
rewriting is permitted. Otherwise, for each i from 1 to n let xi' be
613
the actual term corresponding to the variable xi when lhs is matched
614
against the term to be rewritten, and similarly correspond yi' with y.
615
If xi' and yi' are the same term for all i, then rewriting is not
616
permitted. Otherwise, let k be the least i such that xi' and yi' are
617
distinct. Let fns be the list of all functions that are invisible with
618
respect to every function in fns-k, if fns-k is non-empty; otherwise,
619
let fns be nil. Then rewriting is permitted if and only if yi' is
620
smaller than xi' with respect to fns, in the sense defined in the
623
It remains only to describe how the loop-stopper field is calculated
624
for a rewrite rule when this field is not supplied by the user. (On
625
the other hand, to see how the user may specify the :loop-stopper, see
626
*note RULE-CLASSES::.) Suppose the conclusion of the rule is of the
627
form (equiv lhs rhs). First of all, if rhs is not an instance of the
628
left hand side by a substitution whose range is a list of distinct
629
variables, then the loop-stopper field is nil. Otherwise, consider all
630
pairs (u . v) from this substitution with the property that the first
631
occurrence of v appears in front of the first occurrence of u in the
632
print representation of rhs. For each such u and v, form a list fns of
633
all functions fn in lhs with the property that u or v (or both) appears
634
as a top-level argument of a subterm of lhs with function symbol fn.
635
Then the loop-stopper for this rewrite rule is a list of all lists (u v
639
File: acl2-doc-emacs.info, Node: LP, Next: MACRO-ARGS, Prev: LOOP-STOPPER, Up: MISCELLANEOUS
641
LP the Common Lisp entry to ACL2
643
To enter the ACL2 command loop from Common Lisp, call the Common Lisp
644
program lp (which stands for "loop," as in "read-eval-print loop" or
645
"command loop.") The ACL2 command loop is actually coded in ACL2 as
646
the function ld (which stands for "load"). The command loop is just
647
what you get by loading from the standard object input channel,
648
*standard-oi*. Calling ld directly from Common Lisp is possible but
649
fragile because hard lisp errors or aborts throw you out of ld and back
650
to the top-level of Common Lisp. Lp calls ld in such a way as to
651
prevent this and is thus the standard way to get into the ACL2 command
652
loop. Also see *note ACL2-CUSTOMIZATION:: for information on the
653
loading of an initialization file.
655
All of the visible functionality of lp is in fact provided by ld, which
656
is written in ACL2 itself. Therefore, you should see *note LD:: for
657
detailed documentation of the ACL2 command loop. We sketch it below,
660
Every expression typed to the ACL2 top-level must be an ACL2 expression.
662
Any ACL2 expression may be submitted for evaluation. Well-formedness
663
is checked. Some well-formed expressions cannot be evaluated because
664
they involve (at some level) undefined constrained functions (see *note
665
ENCAPSULATE::). In addition, ACL2 does not allow "global variables" in
666
expressions to be evaluated. Thus, (car '(a b c)) is legal and
667
evaluates to A, but (car x) is not, because there is no "global
668
context" or binding environment that gives meaning to the variable
671
There is an exception to the global variable rule outlined above:
672
single-threaded objects (see *note STOBJ::) may be used as global
673
variables in top-level expressions. The most commonly used such object
674
is the ACL2 "current state," which is the value of the variable symbol
675
state. This variable may occur in the top-level form to be evaluated,
676
but must be passed only to ACL2 functions "expecting" state as
677
described in the documentation for state and for stobjs in general. If
678
the form returns a new state object as one of its values, then that is
679
considered the new "current" state for the evaluation of the subsequent
680
form. See *Note STATE::.
682
ACL2 provides some support for the functionality usually provided by
683
global variables in a read-eval-print loop, namely the saving of the
684
result of a computation for subsequent re-use in another expression.
685
See *Note ASSIGN:: and see *note @: atsign..
687
If the form read is a single keyword, e.g., :pe or :ubt, then special
688
procedures are followed. See *Note KEYWORD-COMMANDS::.
690
The command loop keeps track of the commands you have typed and allows
691
you to review them, display them, and roll the logical state back to
692
that created by any command. See *Note HISTORY::.
694
ACL2 makes the convention that if a top-level form returns three
695
values, the last of which is an ACL2 state, then the first is treated
696
as a flag that means "an error occurred," the second is the value to be
697
printed if no error occurred, and the third is (of course) the new
698
state. When "an error occurs" no value is printed. Thus, if you
699
execute a top-level form that happens to return three such values, only
700
the second will be printed (and that will only happen if the first is
701
nil!). See *Note LD:: for details.
704
File: acl2-doc-emacs.info, Node: MACRO-ARGS, Next: MEASURE, Prev: LP, Up: MISCELLANEOUS
706
MACRO-ARGS the formals list of a macro definition
710
(x y z &optional max (base '10 basep))
715
The "lambda-list" of a macro definition may include simple formal
716
parameter names as well as appropriate uses of the following
717
lambda-list keywords from CLTL (pp. 60 and 145), respecting the order
727
ACL2 does not support &aux and &environment. In addition, we make the
728
following restrictions:
730
(1) initialization forms in &optional and &key specifiers must be
733
(2) &allow-other-keys may only be used once, as the last
736
(3) destructuring is not allowed.
738
You are encouraged to experiment with the macro facility. One way to
739
do so is to define a macro that does nothing but return the quotation
740
of its arguments, e.g.,
742
(defmacro demo (x y &optional opt &key key1 key2)
743
(list 'quote (list x y opt key1 key2)))
745
You may then execute the macro on some sample forms, e.g.,
748
(demo 1 2) (1 2 NIL NIL NIL)
749
(demo 1 2 3) (1 2 3 NIL NIL)
750
(demo 1 2 :key1 3) error: non-even key/value arglist
751
(because :key1 is used as opt)
752
(demo 1 2 3 :key2 5) (1 2 3 NIL 5)
754
In particular, Common Lisp specifies that if you use both &rest and
755
&key, then both will be bound using the same list of arguments. The
756
following example should serve to illustrate how this works.
758
ACL2 !>(defmacro foo (&rest args &key k1 k2 k3)
759
(list 'quote (list args k1 k2 k3)))
762
Form: ( DEFMACRO FOO ...)
1396
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
765
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
1399
Error: Attempt to take the car of 3 which is not listp.
1400
[condition type: TYPE-ERROR]
1402
Restart actions (select using :continue):
1403
0: Abort entirely from this (lisp) process.
1404
[Current process: Initial Lisp Listener]
1405
[1] ACL2(1): [RAW LISP] :pop
1406
ACL2 !>:set-guard-checking :none
1408
Turning off guard checking entirely. To allow execution in raw Lisp
1409
for functions with guards other than T, while continuing to mask guard
1410
violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking.
1414
ACL2 >:set-guard-checking :all
1416
Turning guard checking on, value :ALL.
1421
ACL2 Error in TOP-LEVEL: The guard for the function symbol CAR, which
1422
is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the
1423
call (CAR 3). See :DOC wet for how you might be able to get an error
1424
backtrace. See :DOC set-guard-checking for information about suppressing
1425
this check with (set-guard-checking :none), as recommended for new
767
ACL2 !>(foo :k1 3 :k2 4 :k3 5)
768
((:K1 3 :K2 4 :K3 5) 3 4 5)
769
ACL2 !>(foo :k1 3 :k2 4)
770
((:K1 3 :K2 4) 3 4 NIL)
773
Also see *note TRANS::.
776
File: acl2-doc-emacs.info, Node: MEASURE, Next: MODE, Prev: MACRO-ARGS, Up: MISCELLANEOUS
778
MEASURE xargs keyword :MEASURE
783
File: acl2-doc-emacs.info, Node: MODE, Next: NAME, Prev: MEASURE, Up: MISCELLANEOUS
785
MODE xargs keyword :MODE
790
File: acl2-doc-emacs.info, Node: NAME, Next: NON-EXECUTABLE, Prev: MODE, Up: MISCELLANEOUS
792
NAME syntactic rules on logical names
794
Examples Counter-Examples
796
PRIMEP 91 (not a symbolp)
797
F-AC-23 :CHK-LIST (in KEYWORD package)
798
1AX *PACKAGE* (in the Lisp Package)
799
|Prime Number| 1E3 (not a symbolp)
801
Many different ACL2 entities have names, e.g., functions, macros,
802
variables, constants, packages, theorems, theories, etc. Package names
803
are strings. All other names are symbols and may not be in the
804
"KEYWORD" package. Moreover, names of functions, macros, constrained
805
functions, and constants, other than those that are predefined, must
806
not be in the "main Lisp package" (which is ("LISP" or "COMMON-LISP",
807
according to whether we are following CLTL1 or CLTL2). An analogous
808
restriction on variables is given below.
810
T, nil, and all names above except those that begin with ampersand (&)
811
are names of variables or constants. T, nil, and those names beginning
812
and ending with star (*) are constants. All other such names are
815
Note that names that start with ampersand, such as &rest, may be lambda
816
list keywords and are reserved for such use whether or not they are in
817
the CLTL constant lambda-list-keywords. (See pg 82 of CLTL2.) That
818
is, these may not be used as variables. Unlike constants, variables
819
may be in the main Lisp package as long as they are in the original
820
list of imports from that package to ACL2, the list
821
*common-lisp-symbols-from-main-lisp-package*, and do not belong to a
822
list of symbols that are potentially "global." This latter list is the
823
value of *common-lisp-specials-and-constants*.
825
Our restrictions pertaining to the main Lisp package take into account
826
that some symbols, e.g., lambda-list-keywords and boole-c2, are
827
"special." Permitting them to be bound could have harmful effects. In
828
addition, the Common Lisp language does not allow certain manipulations
829
with many symbols of that package. So, we stay away from them, except
830
for allowing certain variables as indicated above.
833
File: acl2-doc-emacs.info, Node: NON-EXECUTABLE, Next: NON-LINEAR-ARITHMETIC, Prev: NAME, Up: MISCELLANEOUS
835
NON-EXECUTABLE xargs keyword :NON-EXECUTABLE
840
File: acl2-doc-emacs.info, Node: NON-LINEAR-ARITHMETIC, Next: NONLINEARP, Prev: NON-EXECUTABLE, Up: MISCELLANEOUS
842
NON-LINEAR-ARITHMETIC Non-linear Arithmetic
844
This documentation topic is divided into two parts. We first discuss
845
the practical aspect of how to use the non-linear arithmetic extension
846
to ACL2, and then the theory behind it. We assume that the reader is
847
familiar with the material in linear-arithmetic and that on :linear
850
We begin our discussion of how to use non-linear arithmetic with a
851
simple example. Assume that we wish to prove:
854
(implies (and (rationalp x)
861
Note that (floor x y) <= (/ x y). Note also that if we divide both
862
sides of x < (* y z) by y, since 0 < y, we obtain (/ x y) < z. By
863
chaining these two inequalities together, we get the inequality we
866
We now proceed with our example session:
871
; Since the truth of this theorem depends on the linear properties
872
; of floor, we will need the linear lemma:
874
(defthm floor-bounds-1
875
(implies (and (rationalp x)
877
(and (< (+ (/ x y) -1)
881
:rule-classes ((:linear :trigger-terms ((floor x y)))))
883
; We now disable floor, so that the linear lemma will be used.
885
(in-theory (disable floor))
887
; We create five rewrite rules which we will use during non-linear
888
; arithmetic. The necessity for these is due to one of the differences in
889
; ACL2's behaviour when non-linear arithmetic is turned on. Although
890
; the conclusions of linear lemmas have always been rewritten before
891
; they are used, now, when non-linear arithmetic is turned on, the
892
; conclusions are rewritten under a different theory than under ``normal''
893
; rewriting. This theory is also used in other, similar, circumstances
896
(defthm |arith (* -1 x)|
900
(defthm |arith (* 1 x)|
904
(defthm |arith (* x (/ x) y)|
906
(if (equal (fix x) 0)
910
(defthm |arith (* y x)|
914
(defthm |arith (fix x)|
915
(implies (acl2-numberp x)
920
; We disable the above rewrite rules from normal use.
922
(in-theory (disable |arith (* -1 x)|
924
|arith (* x (/ x) y)|
928
; We create an arithmetic-theory. Note that we must give a quoted
929
; constant for the theory --- none of the normal theory-functions
930
; are applicable to in-arithmetic-theory.
932
(in-arithmetic-theory '(|arith (* -1 x)|
934
|arith (* x (/ x) y)|
938
; We turn non-linear arithmetic on.
942
; We can now go ahead and prove our theorem.
945
(implies (and (rationalp x)
952
The above example illustrates the two practical requirements for using
953
non-linear arithmetic in ACL2. First, one must set up an
954
arithmetic-theory. Usually, one would not set up an arithmetic-theory
955
on one's own but would instead load a library book or books which do
956
so. Second, one must turn the non-linear arithmetic extension on.
957
This one must do explicitly -- no book can do this for you.
959
For a brief discussion of why this is so, even though (set-non-linearp
960
t) is an embeddable event, see *note ACL2-DEFAULTS-TABLE:: (in
961
particular, the final paragraph). (Note that (set-non-linearp t)
962
modifies the acl2-defaults-table.) Also see *note SET-NON-LINEARP::,
963
see *note EMBEDDED-EVENT-FORM::, and see *note EVENTS::.
965
You can also enable non-linear arithmetic with the hint :nonlinearp t.
966
See *Note HINTS::. We, in fact, recommend the use of a hint which will
967
enable nonlinear arithmetic only when the goal has stabilized under
968
rewriting. Using default-hints can make this easier.
970
(defun nonlinearp-default-hint (stable-under-simplificationp hist pspv)
971
(cond (stable-under-simplificationp
972
(if (not (access rewrite-constant
973
(access prove-spec-var pspv :rewrite-constant)
975
'(:computed-hint-replacement t :nonlinearp t)
977
((access rewrite-constant
978
(access prove-spec-var pspv :rewrite-constant)
980
(if (not (equal (caar hist) 'SETTLED-DOWN-CLAUSE))
981
'(:computed-hint-replacement t :nonlinearp nil)
985
(set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
988
This has proven to be a helpful strategy which allows faster proof
991
We now proceed to briefly describe the theory behind the non-linear
992
extension to ACL2. In linear-arithmetic it was stated that, "[L]inear
993
polynomial inequalities can be combined by cross-multiplication and
994
addition to permit the deduction of a third inequality...." That is, if
999
and c and d are rational constants, then
1001
0 < c*poly1 + d*poly2.
1003
Similarly, given the above,
1007
In the linear arithmetic case, we are taking advantage of the facts that
1008
multiplication by a positive rational constant does not change the sign
1009
of a polynomial and that the sum of two positive polynomials is itself
1010
positive. In the non-linear arithmetic case, we are using the fact
1011
that the product of two positive polynomials is itself positive.
1013
For example, suppose we have the three assumptions:
1016
p2: 3 < 2*x or p2': 0 < -3 + 2*x
1017
p3: 1 < y or p3': 0 < -1 + y,
1019
and we wish to prove that a < 0. As described elsewhere (see *note
1020
LINEAR-ARITHMETIC::), we proceed by assuming the negation of our goal:
1024
and looking for a contradiction.
1026
There are no cancellations which can be performed by linear arithmetic
1027
in the above situation. (Recall that two polynomials are cancelled
1028
against each other only when they have the same largest unknown.)
1029
However, p1 has a product as its largest unknown, and for each of the
1030
factors of that product there is a poly that has that factor as a
1031
largest unknown. When non-linear arithmetic is enabled, ACL2 will
1032
therefore multiply p1' and p2' obtaining
1034
p5: 0 < 3 + -2*x + -3*y + 2*x*y.
1036
The addition of this polynomial will allow cancelation to continue and,
1037
in this case, we will prove our goal. Thus, just as ACL2 adds two
1038
polynomials together when they have the same largest unknown of
1039
opposite signs in order to create a new "smaller" polynomial; so ACL2
1040
multiplies polynomials together when the product of their largest
1041
unknowns is itself the largest unknown of another polynomial. As the
1042
use of :linear lemmas to further seed the arithmetic data base may
1043
allow cancellation to proceed, so may the use of non-linear arithmetic.
1045
This multiplication of polynomials is the other situation in which
1046
terms are rewritten under the arithemtic-theory rather than the normal
1047
one. Because this may be done so often, and because the individual
1048
factors have presumably already been rewritten, it is important that
1049
this be done in an efficient way. The use of a small, specialized,
1050
theory helps avoid the repeated application of rewrite rules to already
1054
File: acl2-doc-emacs.info, Node: NONLINEARP, Next: NORMALIZE, Prev: NON-LINEAR-ARITHMETIC, Up: MISCELLANEOUS
1056
NONLINEARP hints keyword :NONLINEARP
1061
File: acl2-doc-emacs.info, Node: NORMALIZE, Next: NU-REWRITER, Prev: NONLINEARP, Up: MISCELLANEOUS
1063
NORMALIZE xargs keyword :NORMALIZE
added
removed
doc/EMACS/acl2-doc-emacs.info-23
