Determine whether irrelevant-formals are OK in definitions.

For a related utility that can cause an error, see chk-irrelevant-formals-ok.

General Form: (irrelevant-formals-info def-or-defs ; a definition, a list of definitions, or of the form ; (mutual-recursion def1 ... defk) &key wrld ; ACL2 world; if missing or nil, this is (w state) ctx ; a ctxp to use in error messages; if this is nil or missing, ; then ctx is 'irrelevant-formals-info statep ; certain defaults come from state when statep is true; ; default is nil dcls ; which parts of the given declare forms to use result ; the form of the result; default is :default )

where all arguments are evaluated,

Simple Example Form: ; This returns the list (X1 X3 X4 X5) of irrelevant formals. (irrelevant-formals-info '(defun f (x0 x1 x2 x3 x4 x5) (declare (xargs :guard (natp x2))) (if (consp x0) (f (cdr x0) x1 x2 x5 x4 x3) nil)))

The keyword arguments have defaults that may suffice for most users. When

The value of `xargs`
declarations as well as the

The legal values of

:default

Ifdef-or-defs is a single definition (or a list containing just a single definition), the return value is a list of the irrelevant formals. Otherwisedef-or-defs is a list of two or more definitions. If it defines function symbolsf1 , ...,fk where k>1, then the result is an association list that associates eachfi with a list of the formals of offi that are irrelevant. As noted above, unless:dcls is supplied explicitly, the computation of irrelevant formals is done without the use of anyirrelevant declarations.:raw

The result isnil if and only if the irrelevant-formals check passes. The form of a non-nil result is described below.:msg

The result isnil if and only if the irrelevant-formals check passes. If the result is non-nil , then it is a message (see msgp) explaining the failure, which is suitable for printing with the~@ directive of`fmt`.

More Example Forms: ; This returns (X1 X3 X4 X5) as in the ``Simple Example Form'' above, ; thus illustrating that by default, `irrelevant' declarations are ; ignored (as explained earlier above). (irrelevant-formals-info '(defun f (x0 x1 x2 x3 x4 x5) (declare (irrelevant x1 x3 x5 x4) (xargs :guard (natp x2))) (if (consp x0) (f (cdr x0) x1 x2 x5 x4 x3) nil))) ; Same as above. (irrelevant-formals-info '((defun f (x0 x1 x2 x3 x4 x5) (declare (xargs :guard (natp x2))) (if (consp x0) (f (cdr x0) x1 x2 x5 x4 x3) nil)))) ; Unlike the examples above, this time X2 is included in the result, ; because :guard is not in the list specified by :dcls. (irrelevant-formals-info '((defun f (x0 x1 x2 x3 x4 x5) (declare (xargs :guard (natp x2))) (if (consp x0) (f (cdr x0) x1 x2 x5 x4 x3) nil))) :dcls nil) ; This returns ((F1 Y) (F2 Y)) because y is an irrelevant formal ; for both f1 and f2. (irrelevant-formals-info '((defun f1 (x y) (if (consp x) (f2 (cdr x) y) t)) (defun f2 (x y) (if (consp x) (f1 (cdr x) y) nil)))) ; This is handled exactly as just above. (irrelevant-formals-info '(mutual-recursion (defun f1 (x y) (if (consp x) (f2 (cdr x) y) t)) (defun f2 (x y) (if (consp x) (f1 (cdr x) y) nil)))) ; This is as just above, except that the missing argument in the call ; of f2 in the body of f1, a hard ACL2 error occurs: (irrelevant-formals-info '(mutual-recursion (defun f1 (x y) (if (consp x) (f2 (cdr x)) t)) (defun f2 (x y) (if (consp x) (f1 (cdr x) y) nil)))) ; Because of the :result argument below, we get a msgp from the ; irrelevance check. Try running (fmx "~@0" x) where x is bound ; to this result. (irrelevant-formals-info '(mutual-recursion (defun f1 (x y) (if (consp x) (f2 (cdr x) y) t)) (defun f2 (x y) (if (consp x) (f1 (cdr x) y) nil))) :result :msg)

When keyword

ACL2 !>(irrelevant-formals-info '(mutual-recursion (defund f1 (x y z) (declare (irrelevant z)) (if (consp x) (f2 (cdr x) y z) z)) (defund f2 (x y z) (if (consp x) (f1 (cdr x) y z) nil))) :result :raw) (((F1 Z)) ((F1 1 . Y) (F2 1 . Y))) ACL2 !>

Remarks.

- The use of
`set-irrelevant-formals-ok`has no effect on the result; that is, the value of:irrelevant-formals-info in the`ACL2-defaults-table`does not affect this utility. - Each definition must be a call of a macro in the following list:
(defun defund defun-nx defund-nx defun$ defunt defun-inline defund-inline defun-notinline defund-notinline) . - As noted above, an error occurs by default if the given definitions are
determined to be ill-formed. However, only some of the usual checks for
`defun`events are performed; for example, translation of measures, guards, and bodies is only for logic, not execution, and only partial checks are made for the declare forms. The point of this tool is to perform irrelevant-formals checks, not to do complete checks for the given forms.