Matt Kaufmann

See patch.lisp for a solution.  This file records some thoughts I had as
I developed that solution in June 2016.  Some parts may be a bit
out-of-date, for example, it says "Make sure I got five "compile" hits
in the log", but now we only expect four.

.....

I happened to remember plausible-dclsp, which led me to
plausible-dclsp1 -- but really, what that did for me was to suggest
that I tags-search for ignorable.  There were 219 occurrences:

dunnottar:/projects/acl2/acl2% fgrep -i ignorable *.lisp | wc -l
219
dunnottar:/projects/acl2/acl2%

I didn't care about any occurrence that was inside a declare form.

I skipped doc.lisp; later I'll look at acl2-doc.lisp, and initially I
put this into my patch file:

; !! Don't forget acl2-doc.lisp, including note-7-3.

Initially I found there 28 forms to consider changing:

ACL2 !>(er-let* ((forms (read-file "/projects/acl2/devel-misc/patches/irrelevant-dcl.lisp" state))) (value (length forms)))
 28
ACL2 !>

Oops.  I realized that I had my tags-table tied to a different
directory than I wanted.  (I tend to have two development directories,
and I like to modify the one less recently subjected to a regression,
in case something goes wrong and I want to compare with something
recent.)  So I did this:

# Someone else would do "git pull" here:
bin/pull.sh
cd /projects/acl2/acl2-git-scratch/
# Alias for:
# mv make-ccl.log make-ccl.old.log ; (time nice make PREFIX=ccl- LISP=ccl) >& make-ccl.log&
make-ccl-acl2
meta-x visit-tags-table

Make sure I got five "compile" hits in the log:

dunnottar:/projects/acl2/acl2-git-scratch% fgrep -i compiler make-ccl.log
echo '(DEFPARAMETER *ACL2-COMPILER-ENABLED* NIL)' >> acl2r.lisp ;\
 SET-COMPILER-ENABLED
 SET-COMPILER-ENABLED
     (COMPILER-ENABLED)
                              GC$-FN SET-COMPILER-ENABLED GOOD-BYE-FN
dunnottar:/projects/acl2/acl2-git-scratch%

Kill all .lisp buffers from the wrong directory.

With that done, I started to review :doc irrelevant-formals.  Here's
something key:

  .... Note however
  that if a variable is [declare]d ignored or ignorable, then it will
  not be reported as irrelevant.

That's enough for me!  Now I'll get started on modifying the patch
file that has the 28 forms to consider.

I've made a !! note in the patch file to write a few tests.  I'll
probably add a book containing them.

==============================

Specific functions not modified from those 28, and why:

process-defabbrev-declares: from :doc irrelevant-formals, I *think*
that only recursive definitions have irrelevant-formals.  I'll assume
that here; if I'm wrong someone can complain later that defabbrev
should allow (declare (irrelevant ...)).

ignorable-vars: used in translating let/let*/flet/mv-let/defmacro
forms, but also in get-ignorables and in calls of
labels-form-for-*1*.  But the latter is for raw Lisp so we don't need
to think about irrelevant.

get-ignorables: Aha, used in chk-acceptable-defuns1.  I've made a note
in the patch file to deal with irrelevant there too, and I've added
get-irrelevants and thus irrelevant-vars.

translate11-flet-alist1, translate11-let, translate11-mv-let:
No changes, as these have nothing to do with irrelevance.

chk-free-and-ignored-vars, chk-free-and-ignored-vars-lsts: I see that
the call in chk-acceptable-defuns1 and defmacro-fn, but these having
nothing to do with irrelevance, which is handled just below that call
in chk-acceptable-defuns1 with a call of chk-irrelevant-formals.

relevant-posns{xxx}, irrelevant{xxx}: No changes except a comment
(mentioned under "Other observations" below.  Here's my thinking:

To see whether I need to change relevant-posns-clique-init or
relevant-posns-clique, I did a tags-search for "(relevant-posns".  I
found many functions defined together with that prefix, and then I
found irrelevant-non-lambda-slots-clique2, so next I did a tags-search
for "(irrelevant".  I found that "(relevant" only occurs once outside
the functions defined with that prefix: in
irrelevant-non-lambda-slots-clique.  So it really is down to looking
for "(irrelevant".  Note that "irrelevant-lits" has nothing to do with
this, and as usual, I'm skipping doc.lisp.  As with "(relevant-posns",
I'm skipping over definitions starting with "irrelevant".  Note that
irrelevant-loop-stopper-pairs is not relevant here.  The ultimate
single caller I found was chk-irrelevant-formals, which is called
just once: in chk-acceptable-defuns1, just below
chk-free-and-ignored-vars-lsts, which I've seen already.

defmacro-fn: No, because irrelevant-formals are only for defun, not
defmacro.  Note that "irrelevan" doesn't occur in the definition of
defmacro-fn.

print-gv-form: No irrelevance in non-recursive flet definitions.

labels-form-for-*1*, oneify-cltl-code: This is for generating raw
Lisp, where "irrelevance" isn't relevant.

==============================

Other observations:


The key change is in chk-acceptable-defuns1, as shown below.  The only
change to relevant-posns-clique-init is a comment:

; Ignores is actually the union of ignores and the variables declared
; irrelevant.

Here's the changed code from chk-acceptable-defuns1:

                       (chk-irrelevant-formals names arglists
                                               guards
                                               split-types-terms
                                               measures
                                               (union-eq ignores

; Irrelevants are treated like ignores for purposes of irrelevancy checking;
; see relevant-posns-clique-init.

                                                         irrelevants)
                                               ignorables
                                               bodies ctx state)

I've completed the patch file and am ready to test.  First I surround
everything with the usual:

(redef+)
....
(redef-)
(reset-prehistory)

Also, I look for my "!!" marks -- all are about documentation, so they
can wait (best to get things right before putting too much energy into
that).  Since there is no occurrence of "acl2-loop-only" and no raw
Lisp code (I think -- if there is I'll likely find out!), I don't need
to use LP!.

Now a test, after
(ld "/projects/acl2/devel-misc/patches/irrelevant-dcl.lisp"):

ACL2 !>(defun foo (x y)
	 (declare (irrelevant y))
	 (if (consp x)
	     (foo (cdr x) y)
	   x))


ACL2 Error in ( DEFUN FOO ...):  The second formal of FOO, Y, is irrelevant.
See :DOC irrelevant-formals.


Summary
Form:  ( DEFUN FOO ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

ACL2 Error in ( DEFUN FOO ...):  See :DOC failure.

******** FAILED ********
ACL2 !>

Ouch.  Did I pass in the irrelevants as expected?

ACL2 !>(trace$ chk-irrelevant-formals)
 ((CHK-IRRELEVANT-FORMALS))
ACL2 !>(defun foo (x y)
	 (declare (irrelevant y))
	 (if (consp x)
	     (foo (cdr x) y)
	   x))
1> (CHK-IRRELEVANT-FORMALS (FOO)
                           ((X Y))
                           ('T)
                           ('T)
                           ('NIL)
                           (NIL (Y))
                           (NIL)
                           ((IF (CONSP X) (FOO (CDR X) Y) X))
                           (DEFUN . FOO)
                           |*the-live-state*|)

Oops; (NIL (Y)) doesn't look right.

So I started over, did NOT load the patch file this time, traced as
before but omitted the declare form, and found (NIL) instead of (NIL
Y) -- but not NIL, so obviously I was confused.  Aha --
relevant-posns-clique-init (the function that finally used the
ignores) expects a list of lists, one for each function in the
mutual-recursion nest (or a list of just one list in the
single-function case).

So I did meta-x tags-apropos union, to see if there's a function that
does pairwise union.  There's pairwise-union-geneqv -- no.  I searched
the results for "lst" and "list" -- no.  So I just read through all
the results quickly -- nope.  So I defined pairwise-union-eq and
called it in the chk-irrelevant-formals call in
chk-acceptable-defuns1.

Now my example worked, with no warnings.  But I found that odd,
because I never told Common Lisp about the new kind of declaration.
Indeed, in raw Lisp, there's a warning for irrelevant but not for
xargs.

? (defun foo (x y)
	 (declare (irrelevant y))
	 (if (consp x)
	     (foo (cdr x) y)
	   x))
;Compiler warnings :
;   In FOO: Unknown or invalid declaration (IRRELEVANT Y)
FOO
? (defun foo (x y)
	 (declare (xargs :guard (true-listp y)))
	 (if (consp x)
	     (foo (cdr x) y)
	   x))
FOO
?

So I did a tags-apropos for xargs.  Nothing there.  Next I tried a
tags-search, hoping that I don't get overwhelmed by the number of
hints before finding what I'm looking for -- perhaps that will turn up
in one of the early acl2*.lisp files.  AHA!  In acl2.lisp:

; We use XARGS in DECLARE forms.  By making this proclamation, we
; suppress compiler warnings.

(declaim (declaration xargs))

So I'll add the same thing for irrelevant.

? (declaim (declaration irrelevant))
NIL
? (defun foo (x y)
	 (declare (irrelevant y))
	 (if (consp x)
	     (foo (cdr x) y)
	   x))
FOO
?

I'll install the patch file now in the one of the two directories that
less recently had a regression.

OK, looks good, but... no warning here!

ACL2 !>(defun foo (x y)
	 (declare (irrelevant x y))
	 (if (consp x)
	     (foo (cdr x) y)
	   x))

The admission of FOO is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of FOO is described by the
theorem (NOT (CONSP (FOO X Y))).

Summary
Form:  ( DEFUN FOO ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 FOO
ACL2 !>

I see now why: I didn't do anything to check that the
allegedly-irrelevant formal truly was irrelevant.  Should I do that?
Pros and cons etc.:

(a) We do that check for (declare (ignore ...)), so one would
    reasonably expect such a check.

(b) We don't do any such check for (declare (ignorable ...)), so there
    is a sort of precedent.  Maybe instead of "irrelevant" we should
    call it "irrelevant?".

(c) Someone might want "irrelevant?" anyhow once we have "irrelevant".

(d) I'd like to be done with this, so I'm looking for a way to
    rationalize that.

(e) I don't think it would be hard to redo my changes to enforce
    irrelevance.  Instead of extending the "seed" by extending the
    ignores, I'd compute the irrelevants and see if they match up
    perfectly with what was claimed.

As for (c): they can use set-irrelevant-ok globally to get that
effect, but if someone comes up with a convincing reason to have both
flavors of irrelevant, we can do that later.

In summary, (a) is pretty convincing, especially given (e).  I'll do
that.  My starting point, where I've completed what's above, is
irrelevant-dcl-1.lisp.

Function chk-irrelevant-formals is what I need to modify.  I see that
currently, it skips the check if there's been a
(set-irrelevant-formals-ok t), or even :warn with warnings off, and if
so it skips the check.  But if someone explicitly declared (irrelevant
...), then should that take priority and we do the check after all?
Oh, but how about a mutual-recursion, where some functions declare
irrelevant and others do not?  Simplest for me would be simply to skip
the check just as we do now based on set-irrelevant-formals-ok.
That's actually the right thing to do, because perhaps the user
invoked set-irrelevant-formals-ok not to permit irrelevant formals,
but rather, to avoid the expense of doing the check (which at AMD
years ago, at least, was very expensive for a mutual-recursion nest of
4000+ defun forms).

Looking at chk-irrelevant-formals, I see that the key computation is
with a call of irrelevant-non-lambda-slots-clique.  It has this
comment:

; A "slot" is a triple of the form (fn n . var), where fn is a function symbol,
; n is some nonnegative integer less than the arity of fn, and var is the nth
; formal of fn.  If (fn n . var) is in the list returned by this function, then
; the nth formal of fn, namely var, is irrelevant to the value computed by fn.

So my plan is to pass in an alist mapping each fn to the corresponding
irrelevants.  (I'm making a note to delete pairwise-union-eq.)  So in
chk-acceptable-defuns1, I need to change (get-irrelevants fives) to
(get-irrelevants-alist fives) -- but what is fives?  Looking for calls
of chk-acceptable-defuns1, I found this comment in
chk-acceptable-defuns:

; Fives is a list in 1:1 correspondence with lst.  Each element of
; fives is a 5-tuple of the form (name args doc edcls body).
....

Sure enough, there is a function get-names that is really strip-cars.

Looking at chk-irrelevant-formals I see another issue.  Consider the
following example.

(defun foo (x y z)
  (declare (irrelevant y))
  (if (consp x)
      (foo (cdr x) z y)
    x))

This should cause an error (if set-irrelevant-formals-ok hasn't been
invoked), because z is irrelevant.  But if our algorithm is to deem y
as relevant, then z will also be deemed as relevant.  So our original
implementation (in irrelevant-dcl-1.lisp) was truly wrong-headed;
indeed, it accepts the defun form above!

Fortunately, our plan for modifying chk-irrelevant-formals doesn't
have this problem.  Instead, the plan is to compute all the
irrelevants and then make sure that they perfectly match what was
declared.

While modifying chk-irrelevant-formals, I looked at the warning/error
messages and realized that I probably need to update some :doc, so I
put this note in my patch file:

; !! Update :doc irrelevant-formals

When I was ready to LD the patch file, I got a weird Lisp hard error.
But it happened at the last form, which redefined
chk-acceptable-defuns1.  I'm never very surprised when I get an error
while redefining code that processes definitions.  In this case, I
submitted the definition in raw Lisp, and then was able to complete
the redefinition (after another (redef+)) in the ACL2 loop.

Testing time: I added the following in my patch file.  Perhaps I
should have somehow done such testing in books, but it didn't seem
worth the bother of trying to capture the error messages.

(i-am-here)
; Examples (all errors):

Bug!  I had this:

(defun bogus-irrelevants-alist2 (irrelevant-slots fn vars)
  (cond ((endp vars) nil)
        ((find-slot fn (car vars) irrelevant-slots)
         (cons (car vars)
               (bogus-irrelevants-alist2 irrelevant-slots fn (cdr vars))))
        (t (bogus-irrelevants-alist2 irrelevant-slots fn (cdr vars)))))

But then:

ACL2 !>(defun foo (x y)
  (declare (irrelevant y))
  (if (consp x)
      (foo (cdr x) y)
    x))


ACL2 Error in ( DEFUN FOO ...):  The formal Y of FOO is declared irrelevant
while not actually being irrelevant.  See :DOC irrelevant-formals.


Summary
Form:  ( DEFUN FOO ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

ACL2 Error in ( DEFUN FOO ...):  See :DOC failure.

******** FAILED ********
ACL2 !>

So I did some tracing.  Each trace suggested that I try the next trace.

(trace$ bogus-irrelevants-alist)
(trace$ bogus-irrelevants-alist2)
(trace$ find-slot)

Finally:

ACL2 !>(defun foo (x y)
  (declare (irrelevant y))
  (if (consp x)
      (foo (cdr x) y)
    x))
1> (BOGUS-IRRELEVANTS-ALIST ((FOO 1 . Y))
                            ((FOO Y)))
  2> (BOGUS-IRRELEVANTS-ALIST2 ((FOO 1 . Y))
                               FOO (Y))
    3> (FIND-SLOT FOO Y ((FOO 1 . Y)))
    <3 (FIND-SLOT T)
    3> (BOGUS-IRRELEVANTS-ALIST2 ((FOO 1 . Y))
                                 FOO NIL)
    <3 (BOGUS-IRRELEVANTS-ALIST2 NIL)
  <2 (BOGUS-IRRELEVANTS-ALIST2 (Y))
<1 (BOGUS-IRRELEVANTS-ALIST ((FOO Y)))

Aha -- find-slot got the right answer but the line

  <2 (BOGUS-IRRELEVANTS-ALIST2 (Y))

is wrong.  I had two COND clauses switched!  The fixed version:

(defun bogus-irrelevants-alist2 (irrelevant-slots fn vars)
  (cond ((endp vars) nil)
        ((find-slot fn (car vars) irrelevant-slots)
         (bogus-irrelevants-alist2 irrelevant-slots fn (cdr vars)))
        (t
         (cons (car vars)
               (bogus-irrelevants-alist2 irrelevant-slots fn (cdr vars))))))

Now foo, above is admitted.

Having completed all my tests and tweaked the error messages (e.g.,
replacing "mistakenly" by (the more polite?) "falsely", it remains to
deal with the !! markers I left in the patch file, which are all about
documentation and comments.

One comment suggested taking a look at the following essay;
fortunately, a quick scan doesn't suggest any changes to consider.

; Essay on the Identification of Irrelevant Formals

Next:

; !! Don't forget acl2-doc.lisp, including note-7-3.
; In particular, :doc declare probably needs to change (as per
; "Keep this in sync" comment in *acceptable-dcls-alist*).

; !! Update :doc irrelevant-formals

For :doc note-7-3, I added the following to (defxdoc note-7-3 ...).  I
always try to thank the requestor, not only because it's polite, but
also because it shows that ACL2 improvements are driven by users.
Notice also the liberal uses of hyperlinks.

 <p>It is now possible to @(tsee declare) formal parameters of @(tsee defun)
 events to be irrelevant.  See @(see irrelevant-formals).  Thanks to Eric Smith
 for requesting this feature.</p>

I then submitted the defxdoc form after starting some version of ACL2.

(include-book "xdoc/top" :dir :system)
(defxdoc note-7-3
 ...)
:doc note-7-3

The :doc command helps ensure that the xdoc parses.  It's also helpful
to read the result, without xdoc markups.  When I'm happy with the
result, I typically put it into a file tmp.msg in my ACL2 directory,
towards crafting a commit message that I'll eventually use like this:

git commit -a -F tmp.msg

Note that git gives special treatment to the first line of the
message.  So here's what I have.

dunnottar:/projects/acl2/acl2% cat tmp.msg
Support (declare (irrelevant ...)) in defun forms.

Quoting :doc note-7-3:

  It is now possible to [declare] formal parameters of [defun] events
  to be irrelevant. See [irrelevant-formals]. Thanks to Eric Smith
  for requesting this feature.
dunnottar:/projects/acl2/acl2%

Finally, build and then:

dunnottar:/projects/acl2/acl2% (time nice make -j 8 regression-everything-fresh USE_QUICKLISP=1 TB_LISP=ccl ACL2=/projects/acl2/acl2/ccl-saved_acl2) >& logs/make-regression-everything-ccl-quicklisp-glucose-j-8-jun8.log&
[1] 17306
dunnottar:/projects/acl2/acl2%

Total time:

@TOTAL@ 04:39:31