Filtering...

utils

books/std/util/tests/utils
other
(in-package "STD")
other
(include-book "../look-up")
assert-disabledmacro
(defmacro assert-disabled
  (fn)
  `(make-event (b* ((ens (ens state)) ((when (active-runep '(:definition ,STD::FN))) (er soft
            'assert-disabled
            "Function ~x0 is enabled (expected disabled)!"
            ',STD::FN)))
      (value '(value-triple :success)))))
assert-enabledmacro
(defmacro assert-enabled
  (fn)
  `(make-event (b* ((ens (ens state)) ((when (active-runep '(:definition ,STD::FN))) (value '(value-triple :success))))
      (er soft
        'assert-enabled
        "Function ~x0 is disabled (expected enabled)!"
        ',STD::FN))))
other
(assert-enabled binary-append)
other
(local (defund disabled-fn (x) x))
other
(local (assert-disabled disabled-fn))
assert-logic-modemacro
(defmacro assert-logic-mode
  (fn)
  `(make-event (if (logic-mode-p ',STD::FN (w state))
      (value '(value-triple :success))
      (er soft
        'assert-logic-mode
        "Function ~x0 is program mode (expected logic)!"
        ',STD::FN))))
assert-program-modemacro
(defmacro assert-program-mode
  (fn)
  `(make-event (if (logic-mode-p ',STD::FN (w state))
      (er soft
        'assert-program-mode
        "Function ~x0 is logic mode (expected program)!"
        ',STD::FN)
      (value '(value-triple :success)))))
other
(assert-logic-mode binary-append)
other
(local (defun program-fn
    (x)
    (declare (xargs :mode :program))
    x))
other
(local (assert-program-mode program-fn))
assert-guard-verifiedmacro
(defmacro assert-guard-verified
  (fn)
  `(make-event (if (eq (fgetprop ',STD::FN
          'symbol-class
          nil
          (w state))
        :common-lisp-compliant)
      (value '(value-triple :success))
      (er soft
        'assert-guard-verified
        "Function ~x0 is not guard verified!"
        ',STD::FN))))
assert-guard-unverifiedmacro
(defmacro assert-guard-unverified
  (fn)
  `(make-event (if (eq (fgetprop ',STD::FN
          'symbol-class
          nil
          (w state))
        :common-lisp-compliant)
      (er soft
        'assert-guard-verified
        "Function ~x0 is unexpectedly guard verified!"
        ',STD::FN)
      (value '(value-triple :success)))))
other
(local (assert-guard-verified binary-append))
other
(local (defun unverified-fn
    (x)
    (declare (xargs :verify-guards nil))
    x))
other
(local (assert-guard-unverified unverified-fn))
other
(local (verify-guards unverified-fn))
other
(local (assert-guard-verified unverified-fn))