Enhanced variant of uguard.
(uguard+ fn wrld) → guard
This returns the same result as uguard,
but it 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 uguard+ (fn wrld) (declare (xargs :guard (and (pseudo-termfnp fn) (plist-worldp wrld)))) (let ((__function__ 'uguard+)) (declare (ignorable __function__)) (if (and (symbolp fn) (not (function-symbolp fn wrld))) (raise "The symbol ~x0 does not name a function." fn) (b* ((result (uguard fn wrld))) (if (pseudo-termp result) result (raise "Internal error: ~ the guard ~x0 of ~x1 is not a pseudo-term." result fn))))))
(defthm pseudo-termp-of-uguard+ (b* ((guard (uguard+ fn wrld))) (pseudo-termp guard)) :rule-classes :rewrite)