XARGS

giving hints to 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))


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

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

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