Filtering...

defmapping-tests-template-1-2

books/std/util/defmapping-tests-template-1-2

Included Books

defmapping-templates defmapping-tests-utils must-fail must-fail-local must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "defmapping-templates")
include-book
(include-book "defmapping-tests-utils")
include-book
(include-book "std/testing/must-fail" :dir :system)
include-book
(include-book "std/testing/must-fail-local" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(definputs-guarded-1-2)
other
(progn (defun doma* (a) (doma a))
  (defun domb* (b1 b2) (domb b1 b2))
  (defun alpha* (a) (alpha a))
  (defun beta* (b1 b2) (beta b1 b2)))
other
(must-succeed* (test-title "Default options.")
  (must-be-before-defmapping)
  (enable-all)
  (defmapping map doma domb alpha beta)
  (must-be-after-defmapping :b1...bm (b1 b2)
    :bb1...bbm (b1$ b2$))
  :with-output-off nil)
other
(must-succeed* (test-title "Injective alpha.")
  (must-be-before-defmapping :beta-of-alpha-thm t)
  (enable-all)
  (defmapping map doma domb alpha beta :beta-of-alpha-thm t)
  (must-be-after-defmapping :beta-of-alpha-thm t
    :b1...bm (b1 b2)
    :bb1...bbm (b1$ b2$))
  :with-output-off nil)
other
(must-succeed* (test-title "Surjective alpha.")
  (must-be-before-defmapping :alpha-of-beta-thm t)
  (enable-all)
  (defmapping map doma domb alpha beta :alpha-of-beta-thm t)
  (must-be-after-defmapping :alpha-of-beta-thm t
    :b1...bm (b1 b2)
    :bb1...bbm (b1$ b2$))
  :with-output-off nil)
other
(must-succeed* (test-title "Bijective alpha.")
  (must-be-before-defmapping :beta-of-alpha-thm t
    :alpha-of-beta-thm t)
  (enable-all)
  (defmapping map
    doma
    domb
    alpha
    beta
    :beta-of-alpha-thm t
    :alpha-of-beta-thm t)
  (must-be-after-defmapping :beta-of-alpha-thm t
    :alpha-of-beta-thm t
    :b1...bm (b1 b2)
    :bb1...bbm (b1$ b2$))
  :with-output-off nil)
other
(must-succeed* (test-title "No guard theorems.")
  (must-be-before-defmapping :guard-thms nil)
  (enable-all)
  (defmapping map doma domb alpha beta :guard-thms nil)
  (must-be-after-defmapping :guard-thms nil
    :b1...bm (b1 b2)
    :bb1...bbm (b1$ b2$))
  :with-output-off nil)
other
(must-succeed* (test-title "Injective alpha, no guard theorems.")
  (must-be-before-defmapping :beta-of-alpha-thm t
    :guard-thms nil)
  (enable-all)
  (defmapping map
    doma
    domb
    alpha
    beta
    :beta-of-alpha-thm t
    :guard-thms nil)
  (must-be-after-defmapping :beta-of-alpha-thm t
    :guard-thms nil
    :b1...bm (b1 b2)
    :bb1...bbm (b1$ b2$))
  :with-output-off nil)
other
(must-succeed* (test-title "Surjective alpha, no guard theorems.")
  (must-be-before-defmapping :alpha-of-beta-thm t
    :guard-thms nil)
  (enable-all)
  (defmapping map
    doma
    domb
    alpha
    beta
    :alpha-of-beta-thm t
    :guard-thms nil)
  (must-be-after-defmapping :alpha-of-beta-thm t
    :guard-thms nil
    :b1...bm (b1 b2)
    :bb1...bbm (b1$ b2$))
  :with-output-off nil)
other
(must-succeed* (test-title "Bijective alpha, no guard theorems.")
  (must-be-before-defmapping :beta-of-alpha-thm t
    :alpha-of-beta-thm t
    :guard-thms nil)
  (enable-all)
  (defmapping map
    doma
    domb
    alpha
    beta
    :beta-of-alpha-thm t
    :alpha-of-beta-thm t
    :guard-thms nil)
  (must-be-after-defmapping :beta-of-alpha-thm t
    :alpha-of-beta-thm t
    :guard-thms nil
    :b1...bm (b1 b2)
    :bb1...bbm (b1$ b2$))
  :with-output-off nil)
other
(must-succeed* (test-title "Some custom theorem names.")
  (must-be-before-defmapping :alpha-image my-alpha-image
    :alpha-guard my-alpha-guard)
  (enable-all)
  (defmapping map
    doma
    domb
    alpha
    beta
    :thm-names (:alpha-image my-alpha-image :alpha-guard my-alpha-guard))
  (must-be-after-defmapping :alpha-image my-alpha-image
    :alpha-guard my-alpha-guard
    :b1...bm (b1 b2)
    :bb1...bbm (b1$ b2$))
  :with-output-off nil)
other
(must-succeed* (test-title "All (for default options) custom theorem names.")
  (must-be-before-defmapping :alpha-image my-alpha-image
    :beta-image my-beta-image
    :doma-guard my-doma-guard
    :domb-guard my-domb-guard
    :alpha-guard my-alpha-guard
    :beta-guard my-beta-guard)
  (enable-all)
  (defmapping map
    doma
    domb
    alpha
    beta
    :thm-names (:alpha-image my-alpha-image
      :beta-image my-beta-image
      :doma-guard my-doma-guard
      :domb-guard my-domb-guard
      :alpha-guard my-alpha-guard
      :beta-guard my-beta-guard))
  (must-be-after-defmapping :alpha-image my-alpha-image
    :beta-image my-beta-image
    :doma-guard my-doma-guard
    :domb-guard my-domb-guard
    :alpha-guard my-alpha-guard
    :beta-guard my-beta-guard
    :b1...bm (b1 b2)
    :bb1...bbm (b1$ b2$))
  :with-output-off nil)
other
(must-succeed* (test-title "Some theorems enabled.")
  (must-be-before-defmapping)
  (enable-all)
  (defmapping map
    doma
    domb
    alpha
    beta
    :thm-enable (:alpha-image :domb-guard))
  (must-be-after-defmapping :alpha-image-enable t
    :domb-guard-enable t
    :b1...bm (b1 b2)
    :bb1...bbm (b1$ b2$))
  :with-output-off nil)
other
(must-succeed* (test-title "All (for default options) theorems enabled.")
  (must-be-before-defmapping)
  (enable-all)
  (defmapping map
    doma
    domb
    alpha
    beta
    :thm-enable (:alpha-image :beta-image :doma-guard :domb-guard :alpha-guard :beta-guard))
  (must-be-after-defmapping :alpha-image-enable t
    :beta-image-enable t
    :doma-guard-enable t
    :domb-guard-enable t
    :alpha-guard-enable t
    :beta-guard-enable t
    :b1...bm (b1 b2)
    :bb1...bbm (b1$ b2$))
  :with-output-off nil)
other
(must-succeed* (test-title "Some applicability condition hints.")
  (in-theory (enable alpha-image doma-guard alpha-guard beta-guard))
  (defmapping map
    doma
    domb
    alpha
    beta
    :hints (:beta-image (("Goal" :by beta-image))
      :domb-guard (("Goal" :in-theory (enable domb-guard)))))
  :with-output-off nil)
other
(must-succeed* (test-title "All (for default options) applicability condition hints.")
  (defmapping map
    doma
    domb
    alpha
    beta
    :hints (:alpha-image (("Goal" :use alpha-image))
      :beta-image (("Goal" :use beta-image))
      :doma-guard (("Goal" :use doma-guard))
      :domb-guard (("Goal" :use domb-guard))
      :alpha-guard (("Goal" :use alpha-guard))
      :beta-guard (("Goal" :use beta-guard))))
  :with-output-off nil)
other
(must-succeed* (test-title "Uniform applicability condition hints.")
  (defmapping map
    doma
    domb
    alpha
    beta
    :hints (("Goal" :use (alpha-image beta-image
         doma-guard
         domb-guard
         alpha-guard
         beta-guard))))
  :with-output-off nil)
other
(must-succeed* (test-title "No output.")
  (enable-all)
  (defmapping map doma domb alpha beta :print nil)
  :with-output-off nil)
other
(must-succeed* (test-title "Error output.")
  (enable-all)
  (defmapping map doma domb alpha beta :print :error)
  :with-output-off nil)
other
(must-succeed* (test-title "Error and result output.")
  (enable-all)
  (defmapping map doma domb alpha beta :print :result)
  :with-output-off nil)
other
(must-succeed* (test-title "Error, result, and information output.")
  (enable-all)
  (defmapping map doma domb alpha beta :print :info)
  :with-output-off nil)
other
(must-succeed* (test-title "All output.")
  (enable-all)
  (defmapping map doma domb alpha beta :print :all)
  :with-output-off nil)
other
(must-succeed* (test-title "Events only displayed.")
  (enable-all)
  (defmapping map doma domb alpha beta :show-only t)
  :with-output-off nil)
other
(must-succeed* (test-title "Lambda expressions.")
  (enable-all)
  (defmapping map
    (lambda (a) (doma a))
    (lambda (b1 b2) (domb b1 b2))
    (lambda (a) (alpha a))
    (lambda (b1 b2) (beta b1 b2)))
  :with-output-off nil)
other
(must-succeed* (test-title "Macros.")
  (enable-all)
  (defmacro doma$ (a) `(doma ,A))
  (defmacro domb$ (b1 b2) `(domb ,B1 ,B2))
  (defmacro alpha$ (a) `(alpha ,A))
  (defmacro beta$ (b1 b2) `(beta ,B1 ,B2))
  (defmapping map doma$ domb$ alpha$ beta$)
  :with-output-off nil)
other
(must-succeed* (test-title "Non-guard-verified variants.")
  (must-be-before-defmapping)
  (enable-all)
  (must-fail (defmapping map doma* domb* alpha* beta*))
  (defmapping map doma* domb* alpha* beta* :guard-thms nil)
  (must-be-after-defmapping :guard-thms nil
    :doma doma*
    :domb domb*
    :alpha alpha*
    :beta beta*
    :b1...bm (b1 b2)
    :bb1...bbm (b1$ b2$))
  :with-output-off nil)
other
(test-title "Redundancy handling.")
other
(must-succeed* (enable-all)
  (defmapping map doma domb alpha beta)
  (must-be-redundant (defmapping map doma domb alpha beta)
    (defmapping map doma domb alpha beta :print :all)
    (defmapping map doma domb alpha beta :show-only t)
    (defmapping map
      doma
      domb
      alpha
      beta
      :print nil
      :show-only t))
  :with-output-off nil)
other
(must-succeed* (enable-all)
  (defmapping map doma domb alpha beta :print :info)
  (must-be-redundant (defmapping map doma domb alpha beta)
    (defmapping map doma domb alpha beta :print :error)
    (defmapping map doma domb alpha beta :show-only t)
    (defmapping map
      doma
      domb
      alpha
      beta
      :print nil
      :show-only t))
  :with-output-off nil)
other
(must-succeed* (enable-all)
  (defmapping map doma domb alpha beta :show-only t)
  (must-fail-local (must-be-redundant (defmapping map doma domb alpha beta)))
  (must-fail-local (must-be-redundant (defmapping map doma domb alpha beta :print :all)))
  :with-output-off nil)
other
(must-succeed* (enable-all)
  (defmapping map
    doma
    domb
    alpha
    beta
    :print :info :show-only t)
  (must-fail-local (must-be-redundant (defmapping map doma domb alpha beta)))
  (must-fail-local (must-be-redundant (defmapping map doma domb alpha beta :print :result)))
  (must-be-redundant (defmapping map doma domb alpha beta :show-only t))
  (must-be-redundant (defmapping map
      doma
      domb
      alpha
      beta
      :print :all :show-only t))
  :with-output-off nil)
other
(must-succeed* (enable-all)
  (defmapping map doma domb alpha beta)
  (must-fail (defmapping map doma* domb* alpha* beta*))
  :with-output-off nil)
other
(test-title "Proof failures.")
other
(must-fail (defmapping map doma domb alpha beta))
other
(must-fail (defmapping map
    doma
    domb
    alpha
    beta
    :hints (:alpha-image (("Goal" :by alpha-image)))))
other
(must-fail (defmapping map
    doma
    domb
    alpha
    beta
    :hints (:alpha-image (("Goal" :by alpha-image))
      :beta-image (("Goal" :by beta-image)))))
other
(must-fail (defmapping map
    doma
    domb
    alpha
    beta
    :hints (:alpha-image (("Goal" :by alpha-image))
      :beta-image (("Goal" :by beta-image))
      :doma-guard (("Goal" :by doma-guard)))))
other
(must-fail (defmapping map
    doma
    domb
    alpha
    beta
    :hints (:alpha-image (("Goal" :by alpha-image))
      :beta-image (("Goal" :by beta-image))
      :doma-guard (("Goal" :by doma-guard))
      :domb-guard (("Goal" :by domb-guard)))))
other
(must-fail (defmapping map
    doma
    domb
    alpha
    beta
    :hints (:alpha-image (("Goal" :by alpha-image))
      :beta-image (("Goal" :by beta-image))
      :doma-guard (("Goal" :by doma-guard))
      :domb-guard (("Goal" :by domb-guard))
      :alpha-guard (("Goal" :by alpha-guard)))))