Enhanced variant of non-executablep.
This returns the same result as non-executablep,
but it includes run-time checks (which should always succeed) on the result
that allow us to prove the return type theorems
without strengthening the guard on
(defun non-executablep+ (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'non-executablep+)) (declare (ignorable __function__)) (if (not (function-symbolp fn wrld)) (raise "The symbol ~x0 does not name a function." fn) (b* ((result (non-executablep fn wrld)) ((unless (or (booleanp result) (eq result :program))) (raise "Internal error: ~ the non-executable status ~x0 of ~x1 is not ~ T, NIL, or :PROGRAM." result fn)) ((when (and (logicp fn wrld) (eq result :program))) (raise "Internal error: ~ the non-executable status of the logic-mode function ~x0 ~ is :PROGRAM instead of T or NIL." fn))) result))))
(defthm return-type-of-non-executablep+ (b* ((nonexec (non-executablep+ fn wrld))) (or (booleanp nonexec) (eq nonexec :program))) :rule-classes :rewrite)