-----------------------------------------------------------------

how-to-make-patches.txt

-----------------------------------------------------------------

The Greve Improvement to Forward Chaining

(defthm clock-fn-is-natp
  (implies (exitpoint (run-fn s k))
           (natp (clock-fn s)))
  :rule-classes (:rewrite
                 :forward-chaining
                 :type-prescription))

(defthm |clock fn is minimal|
  (implies (and (pre s)
                (natp n)
                (exitpoint (run-fn s n)))
           (<= (clock-fn s) n))
  :rule-classes :linear)

-----------------------------------------------------------------

Verifying Guards for Too-Many-IFs

(mutual-recursion

(defun occur-cnt-bounded (term1 term2 a m bound-m)

; Let bound = (+ m bound-m).  Return (+ a (* m (occur-cnt term1 term2))) unless
; it exceeds bound, in which case return -1.  We assume (<= a bound).

; Occur-cnt is no longer defined, but was defined (as is this function) so as
; not to go inside of quotes, returning a lower bound on the number of times
; term1 occurs in term2.

  (declare (type (signed-byte 30) a m bound-m))
  (the-fixnum
   (cond ((equal term1 term2)
          (if (<= a bound-m)
              (the-fixnum (+ a m))
            -1))
         ((variablep term2) a)
         ((fquotep term2) a)
         (t (occur-cnt-bounded-lst term1 (fargs term2) a m bound-m)))))

(defun occur-cnt-bounded-lst (term1 lst a m bound-m)
  (declare (type (signed-byte 30) a m bound-m))
  (the-fixnum
   (cond ((endp lst) a)
         (t (let ((new (occur-cnt-bounded term1 (car lst) a m bound-m)))
              (declare (type (signed-byte 30) new))
              (if (eql new -1)
                  -1
                (occur-cnt-bounded-lst term1 (cdr lst) new m bound-m)))))))
)

(defun too-many-ifs1 (args val lhs rhs ctx)
  (declare (type (signed-byte 30) lhs rhs))
  (cond
   ((endp args) nil)
   (t (let ((x (the-fixnum! (count-ifs (car args)) ctx)))
        (declare (type (signed-byte 30) x))
        (cond ((eql x 0)
               (too-many-ifs1 (cdr args) val lhs rhs ctx))
              (t (let ((lhs
                        (occur-cnt-bounded (car args) val lhs x
                                           (the-fixnum (- rhs x)))))
                   (declare (type (signed-byte 30) lhs))
                   (if (eql lhs -1)
                       -1
                     (too-many-ifs1 (cdr args) val lhs rhs ctx)))))))))

(defun too-many-ifs-post-rewrite (args val)

; This function implements the part of the too-many-ifs heuristic after the
; right-hand-side of a definition has been rewritten, to see if that expansion
; is to be kept or thrown away.  See the Essay on Too-many-ifs.

  (let* ((ctx 'too-many-ifs-post-rewrite)
         (rhs (the-fixnum! (count-ifs-lst args) ctx)))
    (cond ((int= rhs 0) nil)
          (t (too-many-ifs1 args val 0 rhs ctx)))))

-----------------------------------------------------------------
(mutual-recursion

(defun occur-cnt-bounded (term1 term2 a m bound-m)

; Let bound = (+ m bound-m).  Return (+ a (* m (occur-cnt term1 term2))) unless
; it exceeds bound, in which case return -1.  We assume (<= a bound).

; Occur-cnt is no longer defined, but was defined (as is this function) so as
; not to go inside of quotes, returning a lower bound on the number of times
; term1 occurs in term2.

  (declare (type (signed-byte 30) a m bound-m)
           (xargs :measure (acl2-count term2)
                  :ruler-extenders (:lambdas)
                  :guard (and (pseudo-termp term2)
                              (signed-byte-p 30 (+ bound-m m))
                              (<= 0 a)
                              (<= 0 m)
                              (<= 0 bound-m)
                              (<= a (+ bound-m m)))
                  :verify-guards nil))
  (the-fixnum
   (cond ((equal term1 term2)
          (if (<= a bound-m)
              (the-fixnum (+ a m))
            -1))
         ((variablep term2) a)
         ((fquotep term2) a)
         (t (occur-cnt-bounded-lst term1 (fargs term2) a m bound-m)))))

(defun occur-cnt-bounded-lst (term1 lst a m bound-m)
  (declare (type (signed-byte 30) a m bound-m)
           (xargs :measure (acl2-count lst)
                  :ruler-extenders (:lambdas)
                  :guard (and (pseudo-term-listp lst)
                              (signed-byte-p 30 (+ bound-m m))
                              (<= 0 a)
                              (<= 0 m)
                              (<= 0 bound-m)
                              (<= a (+ bound-m m)))))
  (the-fixnum
   (cond ((endp lst) a)
         (t (let ((new (occur-cnt-bounded term1 (car lst) a m bound-m)))
              (declare (type (signed-byte 30) new))
              (if (eql new -1)
                  -1
                (occur-cnt-bounded-lst term1 (cdr lst) new m bound-m)))))))
)

(defun too-many-ifs1 (args val lhs rhs ctx)

; See also too-many-ifs-post-rewrite.

; We assume (<= lhs rhs).

  (declare (type (signed-byte 30) lhs rhs)
           (xargs :guard (and (pseudo-term-listp args)
                              (pseudo-termp val)
                              (<= 0 lhs)
                              (<= lhs rhs)
                              (<= (count-ifs-lst args) rhs))))
  (cond
   ((endp args) nil)
   (t (let ((x (the-fixnum! (count-ifs (car args)) ctx)))
        (declare (type (signed-byte 30) x))
        (cond ((eql x 0)
               (too-many-ifs1 (cdr args) val lhs rhs ctx))
              (t (let ((lhs
                        (occur-cnt-bounded (car args) val lhs x
                                           (the-fixnum (- rhs x)))))
                   (declare (type (signed-byte 30) lhs))
                   (if (eql lhs -1)
                       -1
                     (too-many-ifs1 (cdr args) val lhs rhs ctx)))))))))

(defun too-many-ifs-post-rewrite (args val)

; This function implements the part of the too-many-ifs heuristic after the
; right-hand-side of a definition has been rewritten, to see if that expansion
; is to be kept or thrown away.  See the Essay on Too-many-ifs.

  (declare (xargs :guard (and (pseudo-term-listp args)
                              (pseudo-termp val))))

  (let* ((ctx 'too-many-ifs-post-rewrite)
         (rhs (the-fixnum! (count-ifs-lst args) ctx)))
    (cond ((int= rhs 0) nil)
          (t (too-many-ifs1 args val 0 rhs ctx)))))

-----------------------------------------------------------------
(verify-termination occur-cnt-bounded)

(make-flag occur-cnt-bounded-flg
           occur-cnt-bounded
           :flag-var flg
           :flag-mapping ((occur-cnt-bounded . term)
                          (occur-cnt-bounded-lst . list))
           :defthm-macro-name defthm-occur-cnt-bounded
           :local t)

(defthm-occur-cnt-bounded integerp-occur-cnt-bounded
  (term
   (implies (and (integerp a)
                 (integerp m))
            (integerp (occur-cnt-bounded term1 term2 a m bound-m)))
   :rule-classes :type-prescription)
  (list
   (implies (and (integerp a)
                 (integerp m))
            (integerp (occur-cnt-bounded-lst term1 lst a m bound-m)))
   :rule-classes :type-prescription)
  :hints (("Goal" :induct (occur-cnt-bounded-flg flg term2 term1 lst a m bound-m))))

(defthm-occur-cnt-bounded signed-byte-p-30-occur-cnt-bounded-flg
  (term
   (implies (and (force (signed-byte-p 30 a))
                 (signed-byte-p 30 m)
                 (signed-byte-p 30 (+ bound-m m))
                 (force (<= 0 a))
                 (<= 0 m)
                 (<= 0 bound-m)
                 (<= a (+ bound-m m)))
            (and (<= -1 (occur-cnt-bounded term1 term2 a m bound-m))
                 (<= (occur-cnt-bounded term1 term2 a m bound-m) (+ bound-m m))))
   :rule-classes :linear)
  (list
   (implies (and (force (signed-byte-p 30 a))
                 (signed-byte-p 30 m)
                 (signed-byte-p 30 (+ bound-m m))
                 (force (<= 0 a))
                 (<= 0 m)
                 (<= 0 bound-m)
                 (<= a (+ bound-m m)))
            (and (<= -1 (occur-cnt-bounded-lst term1 lst a m bound-m))
                 (<= (occur-cnt-bounded-lst term1 lst a m bound-m) (+ bound-m m))))
   :rule-classes :linear)
  :hints (("Goal" :induct (occur-cnt-bounded-flg flg term2 term1 lst a m bound-m))))

(verify-guards occur-cnt-bounded)

(verify-termination too-many-ifs1) ; and guards

(verify-termination too-many-ifs-post-rewrite)