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

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

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.

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.

Value: hints (see hints), to be used during the guard verification proofs as opposed to the termination proofs of the defun.

Value: hints (see hints), to be used during the termination proofs as opposed to the guard verification proofs of the defun.

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

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.

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 :stobjs 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.

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

Value is a flag indicating ``onward through the fog'' (see otf-flg).

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.

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.

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.