Filtering...

defmapping-tests-validation

books/std/util/defmapping-tests-validation

Included Books

defmapping must-fail must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "defmapping")
include-book
(include-book "std/testing/must-fail" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
test-titlemacro
(defmacro test-title
  (str)
  `(cw-event (concatenate 'string "~%~%~%********** " ,STR "~%~%")))
other
(defstub dom (*) => *)
other
(defstub dom2 (* *) => *)
idfunction
(defun id (x) (declare (xargs :guard t)) x)
id2function
(defun id2 (x y) (declare (xargs :guard t)) (mv x y))
other
(test-title "NAME input validation.")
other
(must-succeed* (must-fail (defmapping 379 dom dom id id))
  (must-fail (defmapping "map" dom dom id id)))
other
(must-fail (defmapping :map dom dom id id))
other
(test-title "DOMA input validation.")
other
(must-succeed* (must-fail (defmapping map "dom" dom id id))
  (must-fail (defmapping map fffffffff dom id id))
  (must-fail (defmapping map car-cdr-elim dom id id))
  (must-fail (defmapping map (lambda (x)) dom id id))
  (must-fail (defmapping map (lambda (x &y) x) dom id id))
  (must-fail (defmapping map (lambda (x x) x) dom id id)))
other
(must-succeed* (defun p (x) (declare (xargs :mode :program)) x)
  (must-fail (defmapping map p dom id id)))
other
(must-succeed* (defun p (state) (declare (xargs :stobjs state)) state)
  (must-fail (defmapping map p dom id id)))
other
(must-succeed* (defun p (x) (declare (xargs :verify-guards nil)) x)
  (must-fail (defmapping map p dom id id)))
other
(must-fail (defmapping map (lambda (x) (digit-char-p x)) dom id id))
other
(must-fail (defmapping map (lambda (x) (+ x y)) dom id id))
other
(must-succeed* (defun g (state) (declare (xargs :stobjs state)) state)
  (must-fail (defmapping map (lambda (state) (g state)) dom id id)))
other
(must-succeed* (defun g (x) (declare (xargs :verify-guards nil)) x)
  (must-fail (defmapping map (lambda (x) (cons (g x) (g x))) dom id id)))
other
(must-fail (defmapping map digit-char-p dom id id))
other
(must-succeed* (defun g
    (state)
    (declare (xargs :stobjs state))
    (declare (ignore state))
    nil)
  (defmacro m (state) `(g ,STATE))
  (must-fail (defmapping map m dom id id)))
other
(must-succeed* (defmacro m (x) `(+ ,X y))
  (must-fail (defmapping map m dom id id)))
other
(must-succeed* (defun g (x) (declare (xargs :verify-guards nil)) x)
  (defmacro m (x) `(g ,X))
  (must-fail (defmapping map m dom id id)))
other
(test-title "DOMB input validation.")
other
(must-succeed* (must-fail (defmapping map dom "dom" id id))
  (must-fail (defmapping map dom fffffffff id id))
  (must-fail (defmapping map dom car-cdr-elim id id))
  (must-fail (defmapping map dom (lambda (x)) id id))
  (must-fail (defmapping map dom (lambda (x &y) x) id id))
  (must-fail (defmapping map dom (lambda (x x) x) id id)))
other
(must-succeed* (defun p (x) (declare (xargs :mode :program)) x)
  (must-fail (defmapping map dom p id id)))
other
(must-succeed* (defun p (state) (declare (xargs :stobjs state)) state)
  (must-fail (defmapping map dom p id id)))
other
(must-succeed* (defun p (x) (declare (xargs :verify-guards nil)) x)
  (must-fail (defmapping map dom p id id)))
other
(must-fail (defmapping map dom (lambda (x) (digit-char-p x)) id id))
other
(must-fail (defmapping map dom (lambda (x) (+ x y)) id id))
other
(must-succeed* (defun g (state) (declare (xargs :stobjs state)) state)
  (must-fail (defmapping map dom (lambda (state) (g state)) id id)))
other
(must-succeed* (defun g (x) (declare (xargs :verify-guards nil)) x)
  (must-fail (defmapping map dom (lambda (x) (cons (g x) (g x))) id id)))
other
(must-fail (defmapping map dom digit-char-p id id))
other
(must-succeed* (defun g
    (state)
    (declare (xargs :stobjs state))
    (declare (ignore state))
    nil)
  (defmacro m (state) `(g ,STATE))
  (must-fail (defmapping map dom m id id)))
other
(must-succeed* (defmacro m (x) `(+ ,X y))
  (must-fail (defmapping map dom m id id)))
other
(must-succeed* (defun g (x) (declare (xargs :verify-guards nil)) x)
  (defmacro m (x) `(g ,X))
  (must-fail (defmapping map dom m id id)))
other
(test-title "ALPHA input validation.")
other
(must-succeed* (must-fail (defmapping map dom dom "id" id))
  (must-fail (defmapping map dom dom fffffffff id))
  (must-fail (defmapping map dom dom car-cdr-elim id))
  (must-fail (defmapping map dom dom (lambda (x)) id))
  (must-fail (defmapping map dom dom (lambda (x &y) x) id))
  (must-fail (defmapping map dom dom (lambda (x x) x) id)))
other
(must-succeed* (defun p (x) (declare (xargs :mode :program)) x)
  (must-fail (defmapping map dom dom p id)))
other
(must-succeed* (must-fail (defmapping map dom dom2 id2 id)
    :with-output-off nil)
  (must-fail (defmapping map dom2 dom id id2)
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (must-fail (defmapping map dom2 dom id2 id)
    :with-output-off nil)
  (must-fail (defmapping map dom dom2 id id2)
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defun p (state) (declare (xargs :stobjs state)) state)
  (must-fail (defmapping map dom dom p id)))
other
(must-succeed* (defun p (x) (declare (xargs :verify-guards nil)) x)
  (must-fail (defmapping map dom dom p id)))
other
(must-fail (defmapping map dom dom (lambda (x) (digit-char-p x)) id))
other
(must-succeed* (must-fail (defmapping map dom dom (lambda (x y) (+ x y)) id))
  (must-fail (defmapping map dom2 dom2 (lambda (x) x) id2)))
other
(must-succeed* (must-fail (defmapping map dom dom (lambda (x) (mv x y)) id))
  (must-fail (defmapping map dom2 dom2 (lambda (x y) (+ x y)) id2)))
other
(must-fail (defmapping map dom dom (lambda (x) (+ x y)) id))
other
(must-succeed* (defun g (state) (declare (xargs :stobjs state)) state)
  (must-fail (defmapping map dom dom (lambda (state) (g state)) id)))
other
(must-succeed* (defun g (x) (declare (xargs :verify-guards nil)) x)
  (must-fail (defmapping map dom dom (lambda (x) (cons (g x) (g x))) id)))
other
(must-succeed* (defmacro mac (x y) `(cons ,X ,Y))
  (must-fail (defmapping map dom dom mac id)
    :with-output-off nil)
  (defmacro nac (x) `(mv ,X ,X))
  (must-fail (defmapping map dom2 dom2 nac id2)
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defmacro mac (x) `(mv ,X ,X))
  (must-fail (defmapping map dom dom mac id)
    :with-output-off nil)
  (defmacro nac (x y) `(cons ,X ,Y))
  (must-fail (defmapping map dom2 dom2 nac id2)
    :with-output-off nil)
  :with-output-off nil)
other
(must-fail (defmapping map dom dom digit-char-p id))
other
(must-succeed* (defun g
    (state)
    (declare (xargs :stobjs state))
    (declare (ignore state))
    nil)
  (defmacro m (state) `(g ,STATE))
  (must-fail (defmapping map dom dom m id)))
other
(must-succeed* (defmacro m (x) `(+ ,X y))
  (must-fail (defmapping map dom dom m id)))
other
(must-succeed* (defun g (x) (declare (xargs :verify-guards nil)) x)
  (defmacro m (x) `(g ,X))
  (must-fail (defmapping map dom dom m id)))
other
(test-title "BETA input validation.")
other
(must-succeed* (must-fail (defmapping map dom dom id "id"))
  (must-fail (defmapping map dom dom id fffffffff))
  (must-fail (defmapping map dom dom id car-cdr-elim))
  (must-fail (defmapping map dom dom id (lambda (x))))
  (must-fail (defmapping map dom dom id (lambda (x &y) x)))
  (must-fail (defmapping map dom dom id (lambda (x x) x))))
other
(must-succeed* (defun p (x) (declare (xargs :mode :program)) x)
  (must-fail (defmapping map dom dom id p)))
other
(must-succeed* (defun f (x y) (declare (xargs :guard t)) (cons x y))
  (must-fail (defmapping map dom dom id f)
    :with-output-off nil)
  (defun g (x) (declare (xargs :guard t)) (mv x x))
  (must-fail (defmapping map dom2 dom2 id2 g)
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defun f (x) (declare (xargs :guard t)) (mv x x))
  (must-fail (defmapping map dom dom id f)
    :with-output-off nil)
  (defun g (x y) (declare (xargs :guard t)) (cons x y))
  (must-fail (defmapping map dom2 dom2 id2 g)
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defun p (state) (declare (xargs :stobjs state)) state)
  (must-fail (defmapping map dom dom id p)))
other
(must-succeed* (defun p (x) (declare (xargs :verify-guards nil)) x)
  (must-fail (defmapping map dom dom id p)))
other
(must-fail (defmapping map dom dom id (lambda (x) (digit-char-p x))))
other
(must-succeed* (must-fail (defmapping map dom dom id (lambda (x y) (+ x y)))
    :with-output-off nil)
  (must-fail (defmapping map dom2 dom2 id2 (lambda (x) (mv x x)))
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (must-fail (defmapping map dom dom id (lambda (x) (mv x x)))
    :with-output-off nil)
  (must-fail (defmapping map dom2 dom2 id2 (lambda (x y) (cons x y)))
    :with-output-off nil)
  :with-output-off nil)
other
(must-fail (defmapping map dom dom id (lambda (x) (+ x y))))
other
(must-succeed* (defun g (state) (declare (xargs :stobjs state)) state)
  (must-fail (defmapping map dom dom id (lambda (state) (g state)))))
other
(must-succeed* (defun g (x) (declare (xargs :verify-guards nil)) x)
  (must-fail (defmapping map dom dom id (lambda (x) (cons (g x) (g x))))))
other
(must-succeed* (defmacro mac (x y) `(cons ,X ,Y))
  (must-fail (defmapping map dom dom id mac)
    :with-output-off nil)
  (defmacro nac (x) `(mv ,X ,X))
  (must-fail (defmapping map dom2 dom2 id2 nac)
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defmacro mac (x) `(mv ,X ,X))
  (must-fail (defmapping map dom dom id mac)
    :with-output-off nil)
  (defmacro nac (x y) `(cons ,X ,Y))
  (must-fail (defmapping map dom2 dom2 id2 nac)
    :with-output-off nil)
  :with-output-off nil)
other
(must-fail (defmapping map dom dom id digit-char-p))
other
(must-succeed* (defun g
    (state)
    (declare (xargs :stobjs state))
    (declare (ignore state))
    nil)
  (defmacro m (state) `(g ,STATE))
  (must-fail (defmapping map dom dom id m)))
other
(must-succeed* (defmacro m (x) `(+ ,X y))
  (must-fail (defmapping map dom dom id m)))
other
(must-succeed* (defun g (x) (declare (xargs :verify-guards nil)) x)
  (defmacro m (x) `(g ,X))
  (must-fail (defmapping map dom dom id m)))
other
(test-title ":BETA-OF-ALPHA-THM input validation.")
other
(must-succeed* (must-fail (defmapping map dom dom id id :beta-of-alpha-thm "yes"))
  (must-fail (defmapping map dom dom id id :beta-of-alpha-thm :true)))
other
(test-title ":ALPHA-OF-BETA-THM input validation.")
other
(must-succeed* (must-fail (defmapping map dom dom id id :alpha-of-beta-thm "T"))
  (must-fail (defmapping map dom dom id id :alpha-of-beta-thm 1)))
other
(test-title ":GUARD-THMS input validation.")
other
(must-succeed* (must-fail (defmapping map dom dom id id :guard-thms #\n))
  (must-fail (defmapping map dom dom id id :guard-thms '(1 2))))
other
(test-title ":UNCONDITIONAL input validation.")
other
(must-fail (defmapping map dom dom id id :unconditional t))
other
(must-succeed* (must-fail (defmapping map
      dom
      dom
      id
      id
      :alpha-of-beta-thm t
      :unconditional "nil"))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :alpha-of-beta-thm t
      :unconditional #\t)))
other
(test-title ":THM-NAMES input validation.")
other
(must-succeed* (must-fail (defmapping map dom dom id id :thm-names #\a))
  (must-fail (defmapping map dom dom id id :thm-names (1 2 3)))
  (must-fail (defmapping map dom dom id id :thm-names (:alpha-image))))
other
(must-succeed* (must-fail (defmapping map dom dom id id :thm-names (:image3 th)))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :thm-names (:alpha-image th :abc thh))))
other
(must-succeed* (must-fail (defmapping map
      dom
      dom
      id
      id
      :guard-thms nil
      :thm-names (:doma-guard th)))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :guard-thms nil
      :thm-names (:alpha-image th :doma-guard thh))))
other
(must-succeed* (must-fail (defmapping map dom dom id id :thm-names (:alpha-image 33)))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :thm-names (:alpha-injective nil)))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :thm-names (:alpha-of-beta len)))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :thm-names (:alpha-of-beta len :beta-image th))))
other
(must-fail (defmapping map
    dom
    dom
    id
    id
    :thm-names (:alpha-image th :beta-image th)))
other
(test-title ":THM-ENABLE input validation.")
other
(must-succeed* (must-fail (defmapping map dom dom id id :thm-enable 66))
  (must-fail (defmapping map dom dom id id :thm-enable t))
  (must-fail (defmapping map dom dom id id :thm-enable :everyone))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :thm-enable :all-but-guard-thms)))
other
(must-succeed* (must-fail (defmapping map dom dom id id :thm-enable (one something)))
  (must-fail (defmapping map dom dom id id :thm-enable (:unrelated)))
  (must-fail (defmapping map dom dom id id :thm-enable (:alpha-image 6))))
other
(must-succeed* (must-fail (defmapping map
      dom
      dom
      id
      id
      :thm-enable (:alpha-image :alpha-image)))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :thm-enable (:beta-image :alpha-image :beta-image))))
other
(must-succeed* (must-fail (defmapping map dom dom id id :thm-enable (:beta-of-alpha)))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :guard-thms nil
      :thm-enable (:alpha-guard :alpha-image))))
other
(test-title ":HINTS input validation.")
other
(must-succeed* (must-fail (defmapping map dom dom id id :hints #\a))
  (must-fail (defmapping map dom dom id id :hints (1 2 3 . 4)))
  (must-fail (defmapping map dom dom id id :hints :alpha-image)))
other
(must-succeed* (must-fail (defmapping map
      dom
      dom
      id
      id
      :hints (:image3 (("Goal" :in-theory nil)))))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :hints (:alpha-image (("Goal" :in-theory nil))
        :abc (("Goal" :in-theory nil))))))
other
(must-succeed* (must-fail (defmapping map
      dom
      dom
      id
      id
      :hints (:alpha-injective (("Goal" :in-theory nil)))))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :hints (:beta-injective (("Goal" :in-theory nil)))))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :guard-thms nil
      :hints (:doma-guard (("Goal" :in-theory nil)))))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :guard-thms nil
      :hints (:domb-guard (("Goal" :in-theory nil)))))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :guard-thms nil
      :hints (:alpha-guard (("Goal" :in-theory nil)))))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :guard-thms nil
      :hints (:beta-guard (("Goal" :in-theory nil))))))
other
(must-succeed* (must-fail (defmapping map dom dom id id :hints (:alpha-image 33)))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :hints (:alpha-image (("Goal" :in-theory (enable aaaaaaaa))))))
  (must-fail (defmapping map
      dom
      dom
      id
      id
      :hints (:alpha-image (("Goal" :in-theory nil))
        :beta-image (("Goal" :in-theory (enable aaaaaaaa)))))))
other
(test-title ":PRINT input validation.")
other
(must-succeed* (must-fail (defmapping map dom dom id id :print 77))
  (must-fail (defmapping map dom dom id id :print :nil)))
other
(test-title ":SHOW-ONLY input validation.")
other
(must-succeed* (must-fail (defmapping map dom dom id id :show-only 77))
  (must-fail (defmapping map dom dom id id :show-only :nil)))