-----------------------------------------------------------------
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)