		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)