irrelevant-formals

(in-package "ACL2")

(program)

(defxdoc irrelevant-formals-info
  :parents (std/system system-utilities-non-built-in
    irrelevant-formals)
  :short "Determine whether @(see irrelevant-formals) are OK in definitions."
  :long "<p>For a related utility that can
 cause an error, see @(see chk-irrelevant-formals-ok).</p>

 @({
 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
  )
 })

 <p>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)').</p>

 @({
 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)))
 })

 <p>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.</p>

 <p>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') @(tsee 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.</p>

 <p>The legal values of @(':result') and their meanings are as follows.</p>

 <ul>

 <li>@(':default')<br/>
 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&gt;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.</li>

 <li>@(':raw')<br/>
 The result is @('nil') if and only if the irrelevant-formals check passes.
 The form of a non-@('nil') result is described below.</li>

 <li>@(':msg')<br/>
 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 @(see msgp))
 explaining the failure, which is suitable for printing with the @('~@')
 directive of @(tsee fmt).</li>

 </ul>

 @({
 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)
 })

 <p>When keyword @(':result') is @(':raw') and the @(see 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.</p>

 @({
 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 !>
 })

 <p>Remarks.</p>

 <ul>

 <li>The use of @(tsee set-irrelevant-formals-ok) has no effect on the result;
 that is, the value of @(':irrelevant-formals-info') in the @(tsee
 acl2-defaults-table) does not affect this utility.</li>

 <li>Each definition must be a call of a macro in the following list:
 @(`*defun-macros*`).</li>

 <li>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
 @(tsee 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 @(see declare) forms.  The point of this tool is to perform
 @(see irrelevant-formals) checks, not to do complete checks for the given
 forms.</li>

 </ul>")

(defxdoc chk-irrelevant-formals-ok
  :parents (std/system system-utilities-non-built-in
    irrelevant-formals)
  :short "Check @(see irrelevant-formals) in definitions."
  :long "@({General Form:

 (chk-irrelevant-formals-ok def-or-defs)
 })

 <p>where @('def-or-defs') evaluates to a definition, a list of definitions, or
 a list of definitions preceded by @('mutual-recursion').  Each definition must
 be a call of a macro in the following list: @(`*defun-macros*`).</p>

 @({
 Example Forms:

 ; Success: Returns (value t).
 (chk-irrelevant-formals-ok
  '(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)))

 ; Failure: Error message reports y irrelevant for both definitions.
 (chk-irrelevant-formals-ok
  '(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))))
 })

 <p>See @(see irrelevant-formals-info) for a related utility that returns a
 single value.  By contrast, @('chk-irrelevant-formals-ok') returns an @(see
 error-triple), which is @('(mv nil t state)') when the @(see
 irrelevant-formals) check passes for the given definition or list of
 definitions, and otherwise returns a soft error as in @('(er soft
 ...)').  Note that all relevant @(see declare) forms, including
 ``@('irrelevant')'', are taken into account.  For finer-grained control of the
 use of declarations, see @(see irrelevant-formals-info).</p>")