Allow rewriting of calls of IF.

Quoting :doc note-7-3:

  It is now legal for a [rewrite] rule to rewrite of a call of [if]. We
  thank Eric Smith for pointing us to examples where this can be
  useful, such as breaking into cases based on the test. One such
  example is much like the following, where we may have a good reason
  for leaving my-or disabled in general, but we wish for a call of
  my-or to expand when it is the test of an if-expression.

    (defund my-or (x y)
      (or x y))

    (defthm my-or-opener
      (equal (if (my-or t1 t2) x y)
             (if t1 x (if t2 x y)))
      :hints (("Goal" :in-theory (enable my-or))))

    ; succeeds
    (thm (equal (if (my-or a b) u v)
                (if a u (if b u v))))

Also made a fix to define-sk that more properly checks proposed
rewrite rules (especially important after the change above).

books/kestrel/utilities/acceptable-rewrite-rule-p.lisp

@@ -0,0 +1,40 @@
+; Copyright (C) 2016, Regents of the University of Texas
+; Written by Matt Kaufmann
+; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.
+
+; This book introduces a Boolean-valued version of chk-acceptable-rewrite-rule,
+; returning t when the form of the proposed rewrite rule is acceptable.  Note
+; that it avoids the call chk-rewrite-rule-warnings that is found in
+; chk-rewrite-rule-warnings.
+
+(in-package "ACL2")
+
+(program)
+
+(defun acceptable-rewrite-rule-p1 (name lst ens wrld)
+
+; Based on ACL2 function chk-acceptable-rewrite-rule1.  Thus:
+
+; Each element of lst is a pair, (hyps . concl) and we check that each
+; such pair, when interpreted as the term (implies (and . hyps)
+; concl), generates a legal :REWRITE rule.
+
+  (cond
+   ((null lst) t)
+   (t (mv-let
+        (msg eqv lhs rhs ttree)
+        (interpret-term-as-rewrite-rule name
+                                        (caar lst) ; hyps
+                                        (cdar lst) ; concl
+                                        ens wrld)
+        (declare (ignore eqv lhs rhs ttree))
+        (and (null msg)
+             (acceptable-rewrite-rule-p1 name (cdr lst) ens wrld))))))
+
+(defun acceptable-rewrite-rule-p (term ens wrld)
+
+; Based on ACL2 function chk-acceptable-rewrite-rule.
+
+  (acceptable-rewrite-rule-p1 :some-proposed-rewrite-rule
+                              (unprettyify (remove-guard-holders term))
+                              ens wrld))

books/kestrel/utilities/define-sk-tests.lisp

@@ -122,14 +122,17 @@
                    (integerp y)
                  (consp y))))
 
-(encapsulate ;; Make sure that we don't infer :rewrite :direct for the goofy one.
+;; Originally, we made sure here that we don't infer :rewrite :direct for the
+;; goofy one.  But Matt K. changed this 8/23/2016 when it became legal to have
+;; rewrite rules for IF-expressions.
+(encapsulate
   ()
   (set-enforce-redundancy t) ;; implicitly local
   (defthm goofy-bad-rewrite-rule-p-necc
-    (implies (not (if (< elem x)
-                      (integerp y)
-                    (consp y)))
-             (not (goofy-bad-rewrite-rule-p x y)))))
+    (implies (goofy-bad-rewrite-rule-p x y)
+             (if (< elem x)
+                 (integerp y)
+               (consp y)))))
 
 
 (define-sk positive-intersection-p

books/kestrel/utilities/define-sk.lisp

@@ -14,6 +14,7 @@
 
 (in-package "STD")
 (include-book "std/util/define" :dir :system)
+(include-book "acceptable-rewrite-rule-p")
 (set-state-ok t)
 (program)
 
@@ -597,10 +598,11 @@ so execution differences don't matter.</p>")
         ;; can report about it then.
         (mv :default state))
        ;; Call ACL2's function that checks whether the rule is okay or not.
-       ((mv msg ?eqv ?lhs ?rhs ?ttree)
-        (acl2::interpret-term-as-rewrite-rule
-         'temporary-name-for-define-sk nil translated-body (acl2::ens state) (acl2::w state)))
-       ((when msg)
+       (okp
+        (acl2::acceptable-rewrite-rule-p translated-body
+                                         (acl2::ens state)
+                                         (acl2::w state)))
+       ((when (not okp))
         ;; It's an error message, so there's some problem, don't use :direct.
         (mv :default state)))
     ;; Otherwise seems OK.
@@ -616,7 +618,15 @@ so execution differences don't matter.</p>")
                ((unless (eq mode1 :direct))
                 (er soft 'infer-rewrite-mode "sanity check 1 failed"))
                ((mv mode2 state) (define-sk-infer-rewrite-mode `(if x (integerp y) (consp z)) state))
-               ((unless (eq mode2 :default))
+               ((unless (eq mode2
+
+; Matt K. mod, now that rewrite rules are permitted for IF-expressions
+; (formerly :default).
+
+                            :direct))
+                (er soft 'infer-rewrite-mode "sanity check 2 failed"))
+               ((mv mode3 state) (define-sk-infer-rewrite-mode ''t state))
+               ((unless (eq mode3 :default))
                 (er soft 'infer-rewrite-mode "sanity check 2 failed")))
             (value '(value-triple :success))))))
 

books/system/doc/acl2-doc.lisp

@@ -87310,7 +87310,11 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.</p>")
  <p>We create a @(':rewrite') rule for each such conjunct, if possible, and
  otherwise cause an error.  It is possible to create a rewrite rule from such a
  conjunct provided @('lhs') is not a variable, a quoted constant, a @(tsee
- let)-expression, a @('lambda') application, or an @(tsee if)-expression.</p>
+ let)-expression, or a @('lambda') application.  Although it is legal to create
+ a rewrite rule from an @(tsee if)-expression @('(if tst tbr fbr)'), note that
+ the rewriter uses the truth or falsity of the test, @('tst'), when rewriting
+ the true and false branches @('tbr') and @('fbr'), respectively; so rewrite
+ rules are often unnecessary for @('if')-expressions.</p>
 
  <p>A @(':rewrite') rule is used when any instance of the @('lhs') occurs in a
  context in which the @(see equivalence) relation is an admissible @(see

defthm.lisp

@@ -87,7 +87,7 @@
 ; so is the result.
 
   (declare (xargs :guard (pseudo-termp term)
-                  :verify-guards nil))  
+                  :verify-guards nil))
   (mv-let (changedp ans)
     (remove-lambdas1 term)
     (declare (ignore changedp))
@@ -111,8 +111,7 @@
      lhs))
    ((or (variablep lhs)
         (fquotep lhs)
-        (flambda-applicationp lhs)
-        (eq (ffn-symb lhs) 'if))
+        (flambda-applicationp lhs))
     (msg
      "A :REWRITE rule generated from ~x0 is illegal because it rewrites the ~
       ~@1 ~x2.  For general information about rewrite rules in ACL2, see :DOC ~
@@ -121,7 +120,8 @@
      (cond ((variablep lhs) "variable symbol")
            ((fquotep lhs) "quoted constant")
            ((flambda-applicationp lhs) "LET-expression")
-           (t "IF-expression"))
+           (t (er hard 'interpret-term-as-rewrite-rule2
+                  "Implementation error: forgot a case.  LHS:~|~x0.")))
      lhs))
    (t (let ((bad-synp-hyp-msg (bad-synp-hyp-msg
                                hyps (all-vars lhs) nil wrld)))

doc.lisp

@@ -88259,8 +88259,12 @@ Subtopics
   We create a :rewrite rule for each such conjunct, if possible, and
   otherwise cause an error. It is possible to create a rewrite rule
   from such a conjunct provided lhs is not a variable, a quoted
-  constant, a [let]-expression, a lambda application, or an
-  [if]-expression.
+  constant, a [let]-expression, or a lambda application. Although it
+  is legal to create a rewrite rule from an [if]-expression (if tst
+  tbr fbr), note that the rewriter uses the truth or falsity of the
+  test, tst, when rewriting the true and false branches tbr and fbr,
+  respectively; so rewrite rules are often unnecessary for
+  if-expressions.
 
   A :rewrite rule is used when any instance of the lhs occurs in a
   context in which the [equivalence] relation is an admissible

rewrite.lisp

@@ -11966,14 +11966,17 @@
                          (rewrite-entry (rewrite right alist 3)
                                         :type-alist false-type-alist
                                         :ttree (rw-cache-enter-context ttree))
-                         (let ((ttree (rw-cache-exit-context ttree ttree1)))
-                           (prepend-step-limit
-                            2
-                            (rewrite-if1 test
-                                         rewritten-left rewritten-right
-                                         type-alist geneqv ens
-                                         (ok-to-force rcnst)
-                                         wrld ttree))))))))))))))
+                         (mv-let
+                           (rewritten-term ttree)
+                           (rewrite-if1 test
+                                        rewritten-left rewritten-right
+                                        type-alist geneqv ens
+                                        (ok-to-force rcnst)
+                                        wrld
+                                        (rw-cache-exit-context ttree ttree1))
+                           (rewrite-entry
+                            (rewrite-with-lemmas
+                             rewritten-term))))))))))))))
 
 (defun rewrite-args (args alist bkptr rewritten-args-rev
                           deep-pequiv-lst shallow-pequiv-lst