Irrelevant-formals-info
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, dcls and result are as
described below, and the other arguments are as described above. The case
that def-or-defs is (mutual-recursion def1 ... defk) is treated
identically to the case it is (def1 ... defk).
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
:dcls and :results are omitted, the computation of irrelevant
formals ignores ``irrelevant'' declarations. That key point is probably
all you need to know unless you use the :dcls or :results keywords;
here is their documentation.
The value of :dcls should be a subset of the list
(:measure :guard :ignore :ignorable :irrelevant), where these keywords
mean (respectively) that the :measure and :guard xargs
declarations as well as the ignore, ignorable, and irrelevant
declararations are taken into account when computing the irrelevant formals.
This list is the default unless the value of :result is
:default (which is its default), in which case :dcls defaults to
(:measure :guard :ignore :ignorable). This behavior supports the common
usage of omitting the :dcls and :result arguments in order to
compute irrelevant formals, without considering which irrelevant formals may
be declared.
The legal values of :result and their meanings are as follows.
- :default
If def-or-defs is a single definition (or a list containing just a single
definition), the return value is a list of the irrelevant formals. Otherwise
def-or-defs is a list of two or more definitions. If it defines function
symbols f1, ..., fk where k>1, then the result is an association
list that associates each fi with a list of the formals of of fi
that are irrelevant. As noted above, unless :dcls is supplied
explicitly, the computation of irrelevant formals is done without the use of
any irrelevant declarations.
- :raw
The result is nil if and only if the irrelevant-formals check passes.
The form of a non-nil result is described below.
- :msg
The result is nil 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 :result is :raw and the irrelevant-formals
check fails, a list of two lists is returned: a list the associates each key,
a function name, with the of the formals of that function that are declared
irrelevant but are not; and a list of slots (function-name formal-position
. formal-name), where the positions are zero-based, for the formals that are
irrelevant but not declared so. Here is an example.
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.
