		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Guard-theorem-no-simplify$

A logic-mode guard-verified version of guard-theorem-no-simplify.

Signature
(guard-theorem-no-simplify$ fn guard-debug safe-mode gc-off state) → term
Arguments: fn — Guard (symbolp fn).
Returns: term — Type (pseudo-termp term).

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, i.e. cause guard-theorem$ to stop with those hard errors. If magic-ev-fncall fails, or if the result is not a pseudo-term, we also stop with hard errors.

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.

Definitions and Theorems

Function: guard-theorem-no-simplify$

(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)))

Theorem: pseudo-termp-of-guard-theorem-no-simplify$

(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)