A logic-mode guard-verified version of guard-theorem-no-simplify.
This has a stronger guard than guard-theorem-no-simplify
and always returns a pseudo-term (if it does not cause an error).
We use magic-ev-fncall to call guard-theorem-no-simplify,
and check that the result is a pseudo-term.
Hard errors happening in guard-theorem are not suppressed,
Compared to guard-theorem-no-simplify, this utility requires a state argument. It may also be slightly less efficient due the magic-ev-fncall overhead. However, it can be used in logic-mode guard-verified code that follows a statically typed discipline.
(defun guard-theorem-no-simplify$ (fn guard-debug safe-mode gc-off state) (declare (xargs :stobjs (state))) (declare (xargs :guard (symbolp fn))) (let ((__function__ 'guard-theorem-no-simplify$)) (declare (ignorable __function__)) (b* (((mv erp term) (magic-ev-fncall 'guard-theorem-no-simplify (list fn guard-debug (w state) safe-mode gc-off) state nil t)) ((when erp) (raise "Internal error: ~@0" term)) ((unless (pseudo-termp term)) (raise "Internal error: ~x0 is not a pseudo-term." term))) term)))
(defthm pseudo-termp-of-guard-theorem-no-simplify$ (b* ((term (guard-theorem-no-simplify$ fn guard-debug safe-mode gc-off state))) (pseudo-termp term)) :rule-classes :rewrite)