defun
Major Section: MISCELLANEOUS
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.
The following declaration is nonsensical but does illustrate all of
the xargs
keywords:
(declare (xargs :guard (symbolp x) :guard-hints (("Goal" :in-theory (theory batch1))) :hints (("Goal" :in-theory (theory batch1))) :measure (- i j) :mode :logic :non-executable t :normalize nil :otf-flg t :stobjs ($s) :verify-guards t :well-founded-relation my-wfr))
:GUARD-HINTS
:MEASURE
:MODE
:NON-EXECUTABLE
:NORMALIZE
:STOBJS
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 (see declare) declared.
:GUARD-HINTS
Value
: hints (see hints), to be used during the guard
verification proofs as opposed to the termination proofs of the
defun
.
:
HINTS
Value: hints (see hints), to be used during the termination
proofs as opposed to the guard verification proofs of the defun
.
:MEASURE
Value
is a term involving only the formals of the function being
defined. This term is indicates what is getting smaller in the
recursion. The well-founded relation with which successive measures
are compared is o<
.
: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 t
or nil
(the default). If t
, the function has no
executable counterpart and is permitted to use single-threaded object names
and functions arbitrarily, as in theorems rather than as in executable
definitions. Such functions are not permitted to declare any names to be
:
stobj
s but accessors, etc., may be used, just as in theorems.
Since the default is nil
, the value supplied is only of interest when it
is t
.
:NORMALIZE
Value is a flag telling defun
whether to propagate if
tests
upward. Since the default is to do so, the value supplied is only of
interest when it is nil
.
(See defun).
:
OTF-FLG
Value is a flag indicating ``onward through the fog''
(see otf-flg).
:STOBJS
Value
is either a single stobj
name or a true list of stobj names.
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.
:
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. See well-founded-relation.