ACL2-DEFAULTS-TABLE.html -- ACL2 Version 6.3

ACL2-DEFAULTS-TABLE

a table specifying certain defaults, e.g., the default defun-mode

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-mode

the default defun-mode, which must be :program or :logic. See defun-mode for a general discussion of defun-modes. The :defun-mode key may be conveniently set by keyword commands naming the new defun-mode, :program and :logic. See program and see logic.

:enforce-redundancy

if 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.

:ignore-doc-string-error

if 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-eagerness

an 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-fns

When 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-function

the default measure function used by defun when no :measure is supplied in xargs. The default measure function must be a function symbol of one argument. Let mfn be the default measure function and suppose no :measure is supplied with some recursive function definition. Then defun finds 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 :measure for that defun.

:well-founded-relation

the default well-founded relation used by defun when no :well-founded-relation is supplied in xargs. The default well-founded relation must be a function symbol, rel, of two arguments about which a :well-founded-relation rule has been proved. See well-founded-relation.

:bogus-defun-hints-ok

When this key's value is t, ACL2 allows :hints for 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-ok

When this key's value is t, ACL2 skips the check that every function in a mutual-recursion (or 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-ok

When 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-ok

When 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.

:bdd-constructors

This key's value is a list of function symbols used to define the notion of ``BDD normal form.'' See bdd-algorithm and see hints.

:ttag

This 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-ok

This key's value is either t or nil and indicates whether the user is aware of the syntactic restrictions on the variable symbol STATE. See set-state-ok.

:backchain-limit

This 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-limit

This 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-limit

This key's value is either nil or a natural number not exceeding the value of *default-step-limit*. If the value is nil or 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-limit

This 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*-abstractionp

This key affects how the system displays subgoals. The value is either t or nil. When t, let* expressions are introduced before printing to eliminate common subexpressions. The actual goal being worked on is unchanged.

:nu-rewriter-mode

This key's value is nil, t, or :literals. When the value is non-nil, the rewriter gives special treatment to expressions and functions defined in terms of nth and update-nth. See set-nu-rewriter-mode.

:case-split-limitations

This 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-alist

This key's value is used by include-book's :DIR argument to associate a directory with a keyword. An exception is the keyword :SYSTEM for the books/ directory; see include-book, in particular the section on ``Books Directory.''

:match-free-default

This key's value is either :all, :once, or nil. See set-match-free-default.

:match-free-override

This key's value is a list of runes. See add-match-free-override.

:match-free-override-nume

This 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-linearp

This key's value is either t or nil and indicates whether the user wishes ACL2 to extend the linear arithmetic decision procedure to include non-linear reasoning. See non-linear-arithmetic.

:tau-auto-modep

This key's value is either t or nil and indicates whether the user wishes ACL2 to look for opportunities to create :tau-system rules from all suitable defuns and from all suitable defthms (with non-nil :rule-classes). See set-tau-auto-mode.

:ruler-extenders

This 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 :all to 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 lambda applications. No other keyword is permitted in the list. See ruler-extenders.

:memoize-ideal-okp

This key is only legal in an experimental hons version (see hons-and-memoization). Its value must be either t, nil, or :warn. If the value is nil or not present, then it is illegal by default to memoize a :logic mode 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 :program mode function, so we allow you to override the default behavior by associating the value t or :warn with the key :memoize-ideal-okp, where with :warn you get a suitable warning. Note that you can also allow memoization of ideal-mode functions by supplying argument :ideal-okp to your memoization event (see memoize), in which case the value of :memoize-ideal-okp in the acl2-defaults-table is irrelevant.

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 update the 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-mode is a function of one non-state argument 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 state-sensitive.

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 :defun-mode to :program when the book was being certified but would set the defun-mode to :logic when the book was being loaded by include-book. That is because during certification, ld-skip-proofsp is nil (proof obligations are generated and proved), but during book inclusion ld-skip-proofsp is non-nil (those obligations are assumed to have been satisfied.) Thus, the above book, when loaded, would create a function in :logic mode that does not actually meet the conditions for such status.

For similar reasons, table events affecting acl2-defaults-table are 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-table is changed locally. If this text were acceptable as a book, then when the book was certified, crash-and-burn would be processed in :program mode, but when the certified book was included later, crash-and-burn would have :logic mode because the local event would be skipped.

The text

(in-package "ACL2")

(program) ;which is (table acl2-defaults-table :defun-mode :program)

(defun crash-and-burn (x) (car x))

is acceptable and defines crash-and-burn in :program mode, both during certification and subsequent inclusion.

We conclude with an important observation about the relation between acl2-defaults-table and include-book, certify-book, and 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.