ACL2-defaults-table
A table specifying certain defaults, e.g., the default defun-mode
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.)
:user
The :user key is for ACL2 users; the system does not consult this key
or set it (other than as part of general acl2-defaults-table
maintenance). Its value is required to be an association list (alistp), so that different users can read and write their ``own'' keys. For
example, suppose user Joe uses key :j while user Mary uses key :m;
then we could see a value for :user of ((:j . 3) (:m . 4)) after Joe
sets his value to 3 and Mary sets her value to 4.
: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.
:verify-guards-eagerness
an integer between 0 and 3 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-rule.
:bogus-defun-hints-ok
When this key's value is t, ACL2 allows :hints and also
:measure for nonrecursive function definitions. Otherwise, the value is
nil (the default) or :warn (which makes the check but merely warns
when the check fails). See set-bogus-defun-hints-ok and set-bogus-measure-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-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.
: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. It need not associate a value with
:SYSTEM, to denote the books/ directory (see community-books;
see include-book, in particular the section on ``Books Directory.''
Also see add-include-book-dir, add-include-book-dir!, and
project-dir-alist.
: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 rulers.
:memoize-ideal-okp
This key's 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 executable
counterpart definitions; see evaluation), 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.
:check-invariant-risk
For an explanation of this key, see set-check-invariant-risk.
:register-invariant-risk
For an explanation of this key, see set-register-invariant-risk.
:in-theory-redundant-okp
When this key's value is t, an in-theory event may be
redundant. See set-in-theory-redundant-okp.
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 important observations about the interaction of the
acl2-defaults-table with include-book, certify-book, and
encapsulate. If the acl2-defaults-table has value V and you
evaluate a call of include-book, certify-book, or encapsulate, then the acl2-defaults-table has value V when that
call returns. Thus, 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.
ACL2 disallows (for logical reasons) setting of the
acl2-defaults-table in the context of LOCAL. Often it is easy
simply to avoid wrapping an acl2-defaults-table event, or a macro that
generates such an event, inside a LOCAL; after all, a local context is
not useful when setting the acl2-defaults-table, since that table is
restored as discussed above upon completion of include-book, certify-book, and encapsulate forms. Occasionally a bit more thought
is required to work around this restriction, but usually it's not difficult to
do so. Suppose for example that you attempt to put following event form into
a book.
(local (progn (defttag t) (defun foo (x) (sys-call x nil))))
ACL2 responds with the following error message.
ACL2 Error in ( PROGN (DEFTTAG T) ...): The form (DEFTTAG T)
is not an embedded event form in the context of LOCAL
because it implicitly sets the acl2-defaults-table in
a local context; see :DOC acl2-defaults-table, in particular
the explanation about this error message. See :DOC
embedded-event-form.
A solution is to use encapsulate instead of (or in addition to)
progn, because encapsulate establishes a new context that is
not considered within a surrounding LOCAL. For example, the following
replacement for the form above is legal in a book.
(local (encapsulate () (defttag t) (defun foo (x) (sys-call x nil))))
To see that this works, try creating a file "foo.lisp" whose first
form is (in-package "ACL2") and whose only other form is the one
displayed just above. Then the command (certify-book "foo" 0 t :ttags
:all) will successfully certify that book.
