Major Section: OTHER
Example Forms: (table acl2-defaults-table :defun-mode) ; current default defun-mode (table acl2-defaults-table :defun-mode :program) ; set default defun-mode to :program
See table for a discussion of tables in general. The legal keys for this table are shown below. They may be accessed and changed via the general mechanisms provided by tables. However, there are often more convenient ways to access and/or change the defaults. (See also the note below.)
:defun-modethe default defun-mode, which must be
logic. See defun-mode for a general discussion of defun-modes. The
defun-modekey may be conveniently set by keyword commands naming the new defun-mode,
logic. See program and see logic.
t, cause ACL2 to insist that most events are redundant (see redundant-events); if
:warn, cause a warning instead of an error for such non-redundant events; else,
nil. See set-enforce-redundancy.
t, cause ACL2 to ignore ill-formed documentation strings rather than causing an error; if
:warn, cause a warning instead of an error in such cases; else,
nil(the default). See set-ignore-doc-string-error.
:verify-guards-eagernessan integer between 0 and 2 indicating how eager the system is to verify the guards of a defun event. See set-verify-guards-eagerness.
:compile-fnsWhen this key's value is
t, functions are compiled when they are
defun'd; otherwise, the value is
nil. (Except, this key's value is ignored when explicit compilation is suppressed; see compilation.) To set the flag, see set-compile-fns.
:measure-functionthe default measure function used by
:measureis supplied in
xargs. The default measure function must be a function symbol of one argument. Let
mfnbe the default measure function and suppose no
:measureis supplied with some recursive function definition. Then
defunfinds the first formal,
var, that is tested along every branch and changed in each recursive call. The system then ``guesses'' that
(mfn var)is the
:well-founded-relationthe default well-founded relation used by
well-founded-relationis supplied in
xargs. The default well-founded relation must be a function symbol,
rel, of two arguments about which a
well-founded-relationrule has been proved. See well-founded-relation.
:bogus-defun-hints-okWhen this key's value is
t, ACL2 allows
:hintsfor nonrecursive function definitions. Otherwise, the value is the
nil(the default) or
:warn(which makes the check but merely warns when the check fails). See set-bogus-defun-hints-ok.
:bogus-mutual-recursion-okWhen this key's value is
t, ACL2 skips the check that every function in a
defuns) ``clique'' calls at least one other function in that ``clique.'' Otherwise, the value is
nil(the default) or
:warn(which makes the check but merely warns when the check fails). See set-bogus-mutual-recursion-ok.
:irrelevant-formals-okWhen this key's value is
t, the check for irrelevant formals is bypassed; otherwise, the value is the keyword
nil(the default) or
:warn(which makes the check but merely warns when the check fails). See irrelevant-formals and see set-irrelevant-formals-ok.
:ignore-okWhen this key's value is
t, the check for ignored variables is bypassed; otherwise, the value is the keyword
nil(the default) or
:warn(which makes the check but merely warns when the check fails). See set-ignore-ok.
:inhibit-warningsACL2 prints warnings that may, from time to time, seem excessive to experienced users. Each warning is ``labeled'' with a string identifying the type of warning. Consider for example
ACL2 Warning [Use] in ( THM ...): It is unusual to :USE ....Here, the label is "Use". The value of the key
:inhibit-warningsis a list of such labels, where case is ignored. Any warning whose label is a member of this list (where again, case is ignored) is suppressed. See set-inhibit-warnings and also see set-inhibit-output-lst.
:bdd-constructorsThis key's value is a list of function symbols used to define the notion of ``BDD normal form.'' See bdd-algorithm and see hints.
:ttagThis key's value, when non-
nil, allows certain operations that extend the trusted code base beyond what is provided by ACL2. See defttag. See defttag.
:state-okThis key's value is either
niland indicates whether the user is aware of the syntactic restrictions on the variable symbol
STATE. See set-state-ok.
:backchain-limitThis key's value is a list of two ``numbers.'' Either ``number'' may optionally be
nil, which is treated like positive infinity. The numbers control backchaining through hypotheses during type-set reasoning and rewriting. See backchain-limit.
:default-backchain-limitThis key's value is a list of two ``numbers.'' Either ``number'' may optionally be
nil, which is treated like positive infinity. The numbers are used respectively to set the backchain limit of a rule if one has not been specified. See backchain-limit.
:step-limitThis key's value is either
nilor a natural number not exceeding the value of
*default-step-limit*. If the value is
nilor the value of
*default-step-limit*, there is no limit on the number of ``steps'' that ACL2 counts during a proof: currently, the number of top-level rewriting calls. Otherwise, the value is the maximum number of such calls allowed during evaluation of any event. See set-prover-step-limit.
:rewrite-stack-limitThis key's value is a nonnegative integer less than
(expt 2 28). It is used to limit the depth of calls of ACL2 rewriter functions. See rewrite-stack-limit.
:let*-abstractionpThis key affects how the system displays subgoals. The value is either
nil. When t, let* expressions are introduced before printing to eliminate common subexpressions. The actual goal being worked on is unchanged.
:nu-rewriter-modeThis key's value is
:literals. When the value is non-
nil, the rewriter gives special treatment to expressions and functions defined in terms of
:case-split-limitationsThis key's value is a list of two ``numbers.'' Either ``number'' may optionally be
nil, which is treated like positive infinity. The numbers control how the system handles case splits in the simplifier. See set-case-split-limitations.
:include-book-dir-alistThis key's value is used by
:DIRargument to associate a directory with a keyword. An exception is the keyword
books/directory; see include-book, in particular the section on ``Books Directory.''
:match-free-defaultThis key's value is either
nil. See set-match-free-default.
:match-free-overrideThis key's value is a list of runes. See add-match-free-override.
:match-free-override-numeThis key's value is an integer used in the implementation of add-match-free-override, so that only existing runes are affected by that event.
:non-linearpThis key's value is either
niland indicates whether the user wishes ACL2 to extend the linear arithmetic decision procedure to include non-linear reasoning. See non-linear-arithmetic.
:tau-auto-modepThis key's value is either
niland indicates whether the user wishes ACL2 to look for opportunities to create
tau-systemrules from all suitable
defuns and from all suitable
defthms (with non-
rule-classes). See set-tau-auto-mode.
:ruler-extendersThis key's value may be a list of symbols, indicating those function symbols that are not to block the collection of rulers; see defun. Otherwise the value is
:allto indicate all function symbols, i.e., so that no function symbol blocks the collection of rulers. If a list is specified (rather than
:all), then it may contain the keyword
:lambdas, which has the special role of specifying all
lambdaapplications. No other keyword is permitted in the list. See ruler-extenders.
:memoize-ideal-okpThis key is only legal in an experimental
honsversion (see hons-and-memoization). Its value must be either
:warn. If the value is
nilor not present, then it is illegal by default to memoize a
logicmode function that has not been guard-verified (see verify-guards), sometimes called an ``ideal-mode'' function. This illegality is the default because such calls of such functions in the ACL2 loop are generally evaluated in the logic (using so-called ``executable counterpart'' definitions), rather than directly by executing calls of the corresponding (memoized) raw Lisp function. However, such a raw Lisp call can be made when the function is called by a
programmode function, so we allow you to override the default behavior by associating the value
:warnwith the key
:memoize-ideal-okp, where with
:warnyou get a suitable warning. Note that you can also allow memoization of ideal-mode functions by supplying argument
:ideal-okpto your memoization event (see memoize), in which case the value of
Note: Unlike all other tables,
acl2-defaults-table can affect the
soundness of the system. The table mechanism therefore enforces on
it a restriction not imposed on other tables: when
table is used to
acl2-defaults-table, the key and value must be
variable-free forms. Thus, while
(table acl2-defaults-table :defun-mode :program), (table acl2-defaults-table :defun-mode ':program), and (table acl2-defaults-table :defun-mode (compute-mode *my-data*))are all examples of legal events (assuming
compute-modeis a function of one non-
stateargument that produces a defun-mode as its single value),
(table acl2-defaults-table :defun-mode (compute-mode (w state)))is not legal because the value form is
Consider for example the following three events which one might make into the text of a book.
(in-package "ACL2") (table acl2-defaults-table :defun-mode (if (ld-skip-proofsp state) :logic :program)) (defun crash-and-burn (x) (car x))The second event is illegal because its value form is
state-sensitive. If it were not illegal, then it would set the
programwhen the book was being certified but would set the defun-mode to
logicwhen the book was being loaded by
include-book. That is because during certification,
nil(proof obligations are generated and proved), but during book inclusion
nil(those obligations are assumed to have been satisfied.) Thus, the above book, when loaded, would create a function in
logicmode that does not actually meet the conditions for such status.
For similar reasons,
table events affecting
illegal within the scope of
local forms. That is, the text
(in-package "ACL2") (local (table acl2-defaults-table :defun-mode :program)) (defun crash-and-burn (x) (car x))is illegal because
acl2-defaults-tableis changed locally. If this text were acceptable as a book, then when the book was certified,
crash-and-burnwould be processed in
programmode, but when the certified book was included later,
logicmode because the
localevent would be skipped.
(in-package "ACL2") (program) ;which is (table acl2-defaults-table :defun-mode :program) (defun crash-and-burn (x) (car x))is acceptable and defines
programmode, both during certification and subsequent inclusion.
We conclude with an important observation about the relation between
encapsulate. Including or certifying a book never has an effect on the
acl2-defaults-table, nor does executing an
encapsulate event; we
always restore the value of this table as a final act. (Also
see include-book, see encapsulate, and see certify-book.) That is, no
matter how a book fiddles with the
acl2-defaults-table, its value
immediately after including that book is the same as immediately before
including that book. If you want to set the
acl2-defaults-table in a way
that persists, you need to do so using commands that are not inside
books. It may be useful to set your favorite defaults in your
acl2-customization file; see acl2-customization.