Xargs
Extra arguments, for example to give hints to defun
Common Lisp's defun function does not easily allow one to
pass extra arguments such as ``hints''. ACL2 therefore supports a
peculiar new declaration (see declare) designed explicitly for passing
additional arguments to defun via a keyword-like syntax. This
declaration can also be used with defmacro, but only for xargs
keyword :guard; so we restrict attention below to use of xargs in
defun events.
The following declaration is nonsensical but does illustrate all of the
xargs keywords for defun (which are the members of the list
*xargs-keywords*).
(declare (xargs :guard (symbolp x)
:guard-debug t
:guard-simplify :limited
:guard-hints (("Goal" :in-theory (theory batch1)))
:hints (("Goal" :in-theory (theory batch1)))
:loop$-recursion t
:measure (- i j)
:measure-debug t
:mode :logic
:non-executable t
:normalize nil
:otf-flg t ; the default for defun
:ruler-extenders :basic
:split-types t
:stobjs ($s)
:dfs (v1 v2)
:type-prescription (natp (foo x y))
:verify-guards t
:well-founded-relation my-wfr))
General Form:
(xargs :key1 val1 ... :keyn valn)
where the keywords and their respective values are as shown below. Note
that once ``inside'' the xargs form, the ``extra arguments'' to defun
are passed exactly as though they were keyword arguments.
:guard
Value is a term involving only the formals of the function being defined.
The actual guard used for the definition is the conjunction of all the
guards and types declared, in the order lexically given, preceded by
conjuncts corresponding to the :stobj declarations (if any, and
including (state-p state) if state is a formal). Also see declare.
Note that if no :guard is specified explicitly, then a
guard of t is assumed, as though one had declared (xargs :guard
t). (Note that t is indeed a term involving only the formals; it
specifies that the guard requirement is always met.) However, by default, a
:logic mode function definition will not attempt to verify guards
unless an explicit xargs :guard declaration is provided. For
details on this point, as well as how to change that default behavior, see
set-verify-guards-eagerness.
:guard-debug
Value: nil by default, else directs ACL2 to decorate each guard
proof obligation with hypotheses indicating its sources. See guard-debug.
:guard-hints
Value: hints (see hints), to be used during the guard
verification proofs as opposed to the termination proofs of the defun. Note that these hints apply only to guard proofs, not to the
generation of guard proof obligations; for that, see guard-simplification.
:guard-simplify
Value: t by default, which supports simplification performed while
generating the guard proof obligation. The value can also be :limited,
which directs ACL2 to skip such simplification that depends on which rules are
currently enabled. This has the same effect as the corresponding
keyword argument to verify-guards. Also see guard-simplification and guard-formula-utilities.
:hints
Value: hints (see hints), to be used during the termination proofs as
opposed to the guard verification proofs of the defun.
:loop$-recursion
Value: this flag must be set to t or nil; nil is the default.
The flag must be t if and only if the function being defined calls itself
recursively from within a loop$ body or within a when or
until clause. See loop$-recursion.
:measure
Value is a term involving only the formals of the function being defined.
This term indicates what is getting smaller in the recursion. The
well-founded relation with which successive measures are compared is o< by default, but can be changed using the :well-founded-relation
keyword or with the set-well-founded-relation event. Also allowed is a
special case, (:? v1 ... vk), where (v1 ... vk) enumerates a subset
of the formal parameters such that some valid measure involves only those
formal parameters. However, this special case is only allowed for definitions
that are redundant (see redundant-events) or are executed when skipping
proofs (see skip-proofs). Another special case is :measure nil,
which is treated the same as if :measure is omitted. Note that a
:measure is not allowed for a non-recursive definition (other than the
``measure'' nil) unless the definition is part of a mutual-recursion;
moreover, if a :measure is supplied, then it must be a legal term. Apart
from these restrictions, the :measure is ignored in :program mode; see
defun-mode.
:measure-debug
Value: nil by default, else directs ACL2 to decorate each
termination proof obligation with hypotheses indicating its sources. See
measure-debug.
:mode
Value is :program or :logic, indicating the
defun mode of the function introduced. See defun-mode. If
unspecified, the defun mode defaults to the default defun mode
of the current world. To convert a function from :program
mode to :logic mode, see verify-termination.
:non-executable
Value is normally t or nil (the default). Rather than stating
:non-executable t directly, which requires :logic mode and
that the definitional body has a certain form, we suggest using the macro
defun-nx or defund-nx; see defun-nx. A third value of
:non-executable for advanced users is :program, which is generated
by expansion of defproxy forms; see defproxy. For another way to
deal with non-executability, see non-exec.
:normalize
Value is a flag telling defun whether to perform certain
simplification before storing the body of the function; see normalize.
Since the default is to do such normalization, the value supplied is
only of interest when it is nil. (See defun).
:otf-flg
Value is a flag indicating “Onward Through the Fog”, to keep the
prover from starting over when it encounters a second subgoal to be pushed for
later proof by induction. See otf-flg). The default is t when
processing a defun or verify-termination event and nil
otherwise.
:ruler-extenders
For recursive definitions (possibly mutually recursive), value controls
termination analysis and the resulting stored induction scheme. See rulers for a discussion of legal values and their effects. See induction-coarse-v-fine-grained for a discussion of how a well-chosen
:ruler-extenders setting may improve the induction scheme suggested by a
function.
:split-types
Value is t or nil, indicating whether or not types are
to be proved from the guards. The default is nil, indicating that
type declarations (see declare) contribute to the guards. If
the value is t, then instead, the expressions corresponding to the type
declarations (see type-spec) are conjoined into a ``split-type
expression,'' and guard verification insists that this term is implied by the
specified :guard. Suppose for example that a definition has the
following declare form.
(declare (xargs :guard (p x y) :split-types t)
(type integer x)
(type (satisfies good-bar-p) y))
Then for guard verification, (p x y) is assumed, and in addition to
the usual proof obligations derived from the body of the definition, guard
verification requires a proof that (p x y) implies both (integerp x)
and (good-bar-p y). See community book
demos/split-types-examples.lisp for small examples.
:stobjs
Value is either a single stobj name or a true list of stobj names
(see stobj and see defstobj, and perhaps see defabsstobj). Every stobj name among the formals of the function must be
listed, if the corresponding actual is to be treated as a stobj. That is, if
a function uses a stobj name as a formal parameter but the name is not
declared among the :stobjs then the corresponding argument is treated as
ordinary. The only exception to this rule is state: whether you
include it or not, state is always treated as a single-threaded object.
This declaration has two effects. One is to enforce the syntactic
restrictions on single-threaded objects. The other is to strengthen the
guard of the function being defined so that it includes conjuncts
specifying that each declared single-threaded object argument satisfies the
recognizer for the corresponding single-threaded object.
:dfs
Value is either a single variable or a true list of variables. See df.
:type-prescription
Value is either nil (the default) or a formula that is suitable for
a hypothesis-free :type-prescription rule. That rule must be
appropriate for the :typed-term that is the application of the defined
function symbol to its formal parameters. For example, a legal value for
:type-prescription in (defun f (x y) ...) could be (or (consp (f
x y)) (equal (f x y) y)), but not (or (consp (f u v)) (equal (f u v)
v)). The specified formula must provide a type that is implied by the
built-in type that is computed for the defined function. Normally these will
be equal, but if the value of :type-prescription specifies a strictly
weaker type than the computed built-in type then a warning will be printed
(unless of course such warnings have been suppressed; see set-inhibit-output-lst and set-inhibit-warnings). It is an error to
supply a non-nil value for :type-prescription if there is no
built-in type computed for the function. See also type-prescription.
:verify-guards
Value is t or nil, indicating whether or not guards are
to be verified upon completion of the termination proof. This flag should
only be t if the :mode is unspecified but the default defun
mode is :logic, or else the :mode is :logic.
:well-founded-relation
Value is a function symbol that is known to be a well-founded relation in
the sense that a rule of class :well-founded-relation has been proved
about it. The effect is to replace the default well-founded relation, which
is typically o<, by the specified value. See well-founded-relation-rule and see set-well-founded-relation for
further discussion, including how to change the default
well-founded-relation.
Subtopics
- Guard
- Restricting the domain of a function
- Otf-flg
- Allow more than one initial subgoal to be pushed for induction
- Normalize
- Storing simplified definition bodies and guards
