Enhanced variant of measure.
This returns the same result as measure,
but it is guard-verified
and includes a run-time check (which should always succeed) on the result
that allows us to prove the return type theorem
without strengthening the guard on
(defun measure+ (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'measure+)) (declare (ignorable __function__)) (if (not (irecursivep+ fn wrld)) (raise "The function ~x0 is not recursive." fn) (b* ((justification (getpropc fn 'justification nil wrld)) ((unless (weak-justification-p justification)) (raise "Internal error: ~ the JUSTIFICATION property ~x0 of ~x1 is not well-formed." justification fn)) (measure (access justification justification :measure)) ((unless (pseudo-termp measure)) (raise "Internal error: ~ the measure ~x0 of ~x1 is not a pseudo-term." measure fn))) measure))))
(defthm pseudo-termp-of-measure+ (b* ((measure (measure+ fn wrld))) (pseudo-termp measure)) :rule-classes :rewrite)