Enhanced variant of unwrapped-nonexec-body.
This returns the same result as unwrapped-nonexec-body,
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 unwrapped-nonexec-body+ (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'unwrapped-nonexec-body+)) (declare (ignorable __function__)) (b* (((unless (non-executablep fn wrld)) (raise "The function ~x0 is executable." fn)) (body (ubody+ fn wrld)) ((unless body) (raise "The function ~x0 does not have an unnormalized body." fn)) ((unless (and (throw-nonexec-error-p body fn (formals+ fn wrld)) (consp (cdddr body)))) (raise "Internal error: ~ the body ~x0 of the non-executable function ~x1 ~ does not have the expected wrapper." body fn)) (unwrapped-body (fourth body)) ((unless (pseudo-termp unwrapped-body)) (raise "Internal error: ~ the unwrapped body ~x0 of the non-executable function ~x1 ~ is not a pseudo-term." unwrapped-body fn))) unwrapped-body)))
(defthm pseudo-termp-of-unwrapped-nonexec-body+ (b* ((unwrapped-body (unwrapped-nonexec-body+ fn wrld))) (pseudo-termp unwrapped-body)) :rule-classes :rewrite)