defmapping-tests-utils

Included Books

defmapping rune-disabledp rune-enabledp theorem-symbolp assert-bang must-be-redundant must-be-table-key must-not-be-table-key

other

(in-package "ACL2")

include-book

(include-book "defmapping")

include-book

(include-book "std/system/rune-disabledp" :dir :system)

include-book

(include-book "std/system/rune-enabledp" :dir :system)

include-book

(include-book "std/system/theorem-symbolp" :dir :system)

include-book

(include-book "std/testing/assert-bang" :dir :system)

include-book

(include-book "std/testing/must-be-redundant" :dir :system)

include-book

(include-book "std/testing/must-be-table-key" :dir :system)

include-book

(include-book "std/testing/must-not-be-table-key" :dir :system)

test-titlemacro

(defmacro test-title
  (str)
  `(cw-event (concatenate 'string "~%~%~%********** " ,STR "~%~%")))

must-be-theoremmacro

(defmacro must-be-theorem
  (name)
  (declare (xargs :guard (symbolp name)))
  `(assert! (theorem-symbolp ',NAME (w state))))

other

(define must-be-theorems-fn
  ((names symbol-listp))
  :returns (events pseudo-event-form-listp)
  (cond ((endp names) nil)
    (t (cons `(must-be-theorem ,(CAR NAMES))
        (must-be-theorems-fn (cdr names))))))

must-be-theoremsmacro

(defmacro must-be-theorems
  (&rest names)
  (declare (xargs :guard (symbol-listp names)))
  `(progn ,@(MUST-BE-THEOREMS-FN NAMES)))

must-not-be-theoremmacro

(defmacro must-not-be-theorem
  (name)
  (declare (xargs :guard (symbolp name)))
  `(assert! (not (theorem-symbolp ',NAME (w state)))))

other

(define must-not-be-theorems-fn
  ((names symbol-listp))
  :returns (events pseudo-event-form-listp)
  (cond ((endp names) nil)
    (t (cons `(must-not-be-theorem ,(CAR NAMES))
        (must-not-be-theorems-fn (cdr names))))))

must-not-be-theoremsmacro

(defmacro must-not-be-theorems
  (&rest names)
  (declare (xargs :guard (symbol-listp names)))
  `(progn ,@(MUST-NOT-BE-THEOREMS-FN NAMES)))

must-be-enabled-rewrite-rulemacro

(defmacro must-be-enabled-rewrite-rule
  (name yes/no)
  (if yes/no
    `(assert! (rune-enabledp '(:rewrite ,NAME) state))
    `(assert! (rune-disabledp '(:rewrite ,NAME) state))))

must-not-be-defmapping-entrymacro

(defmacro must-not-be-defmapping-entry
  (&key (name 'map))
  (declare (xargs :guard (symbolp name)))
  `(must-not-be-table-key ,NAME ,*DEFMAPPING-TABLE-NAME*))

must-be-defmapping-entrymacro

(defmacro must-be-defmapping-entry
  (&key (name 'map)
    (doma 'doma)
    (domb 'domb)
    (alpha 'alpha)
    (beta 'beta)
    unconditional
    (alpha-image 'map.alpha-image)
    (beta-image 'map.beta-image)
    (beta-of-alpha 'map.beta-of-alpha)
    (alpha-of-beta 'map.alpha-of-beta)
    (alpha-injective 'map.alpha-injective)
    (beta-injective 'map.beta-injective)
    (doma-guard 'map.doma-guard)
    (domb-guard 'map.domb-guard)
    (alpha-guard 'map.alpha-guard)
    (beta-guard 'map.beta-guard))
  `(assert! (b* ((table (table-alist *defmapping-table-name* (w state))) (pair (assoc-eq ',NAME table))
        ((unless pair) nil)
        (info (cdr pair))
        ((unless (defmapping-infop info)) nil))
      (and (equal (defmapping-info->doma info) ',DOMA)
        (equal (defmapping-info->domb info) ',DOMB)
        (equal (defmapping-info->alpha info) ',ALPHA)
        (equal (defmapping-info->beta info) ',BETA)
        (equal (defmapping-info->alpha-image info) ',ALPHA-IMAGE)
        (equal (defmapping-info->beta-image info) ',BETA-IMAGE)
        (equal (defmapping-info->beta-of-alpha info)
          ',BETA-OF-ALPHA)
        (equal (defmapping-info->alpha-of-beta info)
          ',ALPHA-OF-BETA)
        (equal (defmapping-info->alpha-injective info)
          ',ALPHA-INJECTIVE)
        (equal (defmapping-info->beta-injective info)
          ',BETA-INJECTIVE)
        (equal (defmapping-info->doma-guard info) ',DOMA-GUARD)
        (equal (defmapping-info->domb-guard info) ',DOMB-GUARD)
        (equal (defmapping-info->alpha-guard info) ',ALPHA-GUARD)
        (equal (defmapping-info->beta-guard info) ',BETA-GUARD)
        (equal (defmapping-info->unconditional info) ,UNCONDITIONAL)))))

must-be-defmapping-theoremsmacro

(defmacro must-be-defmapping-theorems
  (&key (doma 'doma)
    (domb 'domb)
    (alpha 'alpha)
    (beta 'beta)
    unconditional
    (alpha-image 'map.alpha-image)
    (beta-image 'map.beta-image)
    (beta-of-alpha 'map.beta-of-alpha)
    (alpha-of-beta 'map.alpha-of-beta)
    (alpha-injective 'map.alpha-injective)
    (beta-injective 'map.beta-injective)
    (doma-guard 'map.doma-guard)
    (domb-guard 'map.domb-guard)
    (alpha-guard 'map.alpha-guard)
    (beta-guard 'map.beta-guard)
    (g-doma 'g-doma)
    (g-domb 'g-domb)
    (g-alpha 'g-alpha)
    (g-beta 'g-beta)
    (a1...an '(a))
    (b1...bm '(b))
    (aa1...aan '(a$))
    (bb1...bbm '(b$)))
  `(must-be-redundant (defthm-all :alpha-image ,ALPHA-IMAGE
      :beta-image ,BETA-IMAGE
      :beta-of-alpha ,BETA-OF-ALPHA
      :alpha-of-beta ,ALPHA-OF-BETA
      :alpha-injective ,ALPHA-INJECTIVE
      :beta-injective ,BETA-INJECTIVE
      :doma-guard ,DOMA-GUARD
      :domb-guard ,DOMB-GUARD
      :alpha-guard ,ALPHA-GUARD
      :beta-guard ,BETA-GUARD
      :unconditional ,UNCONDITIONAL
      :doma ,DOMA
      :domb ,DOMB
      :alpha ,ALPHA
      :beta ,BETA
      :g-doma ,G-DOMA
      :g-domb ,G-DOMB
      :g-alpha ,G-ALPHA
      :g-beta ,G-BETA
      :a1...an ,A1...AN
      :b1...bm ,B1...BM
      :aa1...aan ,AA1...AAN
      :bb1...bbm ,BB1...BBM)))

must-be-before-defmappingmacro

(defmacro must-be-before-defmapping
  (&key (name 'map)
    beta-of-alpha-thm
    alpha-of-beta-thm
    (guard-thms 't)
    (alpha-image 'map.alpha-image)
    (beta-image 'map.beta-image)
    (beta-of-alpha 'map.beta-of-alpha)
    (alpha-of-beta 'map.alpha-of-beta)
    (alpha-injective 'map.alpha-injective)
    (beta-injective 'map.beta-injective)
    (doma-guard 'map.doma-guard)
    (domb-guard 'map.domb-guard)
    (alpha-guard 'map.alpha-guard)
    (beta-guard 'map.beta-guard))
  `(progn (must-not-be-defmapping-entry :name ,NAME)
    (must-not-be-theorems ,ALPHA-IMAGE
      ,BETA-IMAGE
      ,@(AND BETA-OF-ALPHA-THM (LIST BETA-OF-ALPHA))
      ,@(AND ALPHA-OF-BETA-THM (LIST ALPHA-OF-BETA))
      ,@(AND BETA-OF-ALPHA-THM (LIST ALPHA-INJECTIVE))
      ,@(AND ALPHA-OF-BETA-THM (LIST BETA-INJECTIVE))
      ,@(AND GUARD-THMS (LIST DOMA-GUARD))
      ,@(AND GUARD-THMS (LIST DOMB-GUARD))
      ,@(AND GUARD-THMS (LIST ALPHA-GUARD))
      ,@(AND GUARD-THMS (LIST BETA-GUARD)))))

must-be-after-defmappingmacro

(defmacro must-be-after-defmapping
  (&key (name 'map)
    (doma 'doma)
    (domb 'domb)
    (alpha 'alpha)
    (beta 'beta)
    beta-of-alpha-thm
    alpha-of-beta-thm
    (guard-thms 't)
    unconditional
    (alpha-image 'map.alpha-image)
    (beta-image 'map.beta-image)
    (beta-of-alpha 'map.beta-of-alpha)
    (alpha-of-beta 'map.alpha-of-beta)
    (alpha-injective 'map.alpha-injective)
    (beta-injective 'map.beta-injective)
    (doma-guard 'map.doma-guard)
    (domb-guard 'map.domb-guard)
    (alpha-guard 'map.alpha-guard)
    (beta-guard 'map.beta-guard)
    (alpha-image-enable 'nil)
    (beta-image-enable 'nil)
    (beta-of-alpha-enable 'nil)
    (alpha-of-beta-enable 'nil)
    (alpha-injective-enable 'nil)
    (beta-injective-enable 'nil)
    (doma-guard-enable 'nil)
    (domb-guard-enable 'nil)
    (alpha-guard-enable 'nil)
    (beta-guard-enable 'nil)
    (g-doma 'g-doma)
    (g-domb 'g-domb)
    (g-alpha 'g-alpha)
    (g-beta 'g-beta)
    (a1...an '(a))
    (b1...bm '(b))
    (aa1...aan '(a$))
    (bb1...bbm '(b$)))
  `(progn (must-be-defmapping-entry :name ,NAME
      :doma ,DOMA
      :domb ,DOMB
      :alpha ,ALPHA
      :beta ,BETA
      :alpha-image ,ALPHA-IMAGE
      :beta-image ,BETA-IMAGE
      :beta-of-alpha ,(AND BETA-OF-ALPHA-THM BETA-OF-ALPHA)
      :alpha-of-beta ,(AND ALPHA-OF-BETA-THM ALPHA-OF-BETA)
      :alpha-injective ,(AND BETA-OF-ALPHA-THM ALPHA-INJECTIVE)
      :beta-injective ,(AND ALPHA-OF-BETA-THM BETA-INJECTIVE)
      :doma-guard ,(AND GUARD-THMS DOMA-GUARD)
      :domb-guard ,(AND GUARD-THMS DOMB-GUARD)
      :alpha-guard ,(AND GUARD-THMS ALPHA-GUARD)
      :beta-guard ,(AND GUARD-THMS BETA-GUARD)
      :unconditional ,UNCONDITIONAL)
    (must-be-defmapping-theorems :alpha-image ,ALPHA-IMAGE
      :beta-image ,BETA-IMAGE
      :beta-of-alpha ,(AND BETA-OF-ALPHA-THM BETA-OF-ALPHA)
      :alpha-of-beta ,(AND ALPHA-OF-BETA-THM ALPHA-OF-BETA)
      :alpha-injective ,(AND BETA-OF-ALPHA-THM ALPHA-INJECTIVE)
      :beta-injective ,(AND ALPHA-OF-BETA-THM BETA-INJECTIVE)
      :doma-guard ,(AND GUARD-THMS DOMA-GUARD)
      :domb-guard ,(AND GUARD-THMS DOMB-GUARD)
      :alpha-guard ,(AND GUARD-THMS ALPHA-GUARD)
      :beta-guard ,(AND GUARD-THMS BETA-GUARD)
      :unconditional ,UNCONDITIONAL
      :doma ,DOMA
      :domb ,DOMB
      :alpha ,ALPHA
      :beta ,BETA
      :g-doma ,G-DOMA
      :g-domb ,G-DOMB
      :g-alpha ,G-ALPHA
      :g-beta ,G-BETA
      :a1...an ,A1...AN
      :b1...bm ,B1...BM
      :aa1...aan ,AA1...AAN
      :bb1...bbm ,BB1...BBM)
    (must-not-be-theorems ,@(AND (NOT BETA-OF-ALPHA-THM) (LIST BETA-OF-ALPHA))
      ,@(AND (NOT ALPHA-OF-BETA-THM) (LIST ALPHA-OF-BETA))
      ,@(AND (NOT BETA-OF-ALPHA-THM) (LIST ALPHA-INJECTIVE))
      ,@(AND (NOT ALPHA-OF-BETA-THM) (LIST BETA-INJECTIVE))
      ,@(AND (NOT GUARD-THMS) (LIST DOMA-GUARD))
      ,@(AND (NOT GUARD-THMS) (LIST DOMB-GUARD))
      ,@(AND (NOT GUARD-THMS) (LIST ALPHA-GUARD))
      ,@(AND (NOT GUARD-THMS) (LIST BETA-GUARD)))
    (must-be-enabled-rewrite-rule ,ALPHA-IMAGE
      ,ALPHA-IMAGE-ENABLE)
    (must-be-enabled-rewrite-rule ,BETA-IMAGE
      ,BETA-IMAGE-ENABLE)
    ,@(AND BETA-OF-ALPHA-THM
       `((MUST-BE-ENABLED-REWRITE-RULE ,BETA-OF-ALPHA ,BETA-OF-ALPHA-ENABLE)))
    ,@(AND ALPHA-OF-BETA-THM
       `((MUST-BE-ENABLED-REWRITE-RULE ,ALPHA-OF-BETA ,ALPHA-OF-BETA-ENABLE)))
    ,@(AND BETA-OF-ALPHA-THM
       `((MUST-BE-ENABLED-REWRITE-RULE ,ALPHA-INJECTIVE
          ,ALPHA-INJECTIVE-ENABLE)))
    ,@(AND ALPHA-OF-BETA-THM
       `((MUST-BE-ENABLED-REWRITE-RULE ,BETA-INJECTIVE ,BETA-INJECTIVE-ENABLE)))
    ,@(AND GUARD-THMS
       `((MUST-BE-ENABLED-REWRITE-RULE ,DOMA-GUARD ,DOMA-GUARD-ENABLE)))
    ,@(AND GUARD-THMS
       `((MUST-BE-ENABLED-REWRITE-RULE ,DOMB-GUARD ,DOMB-GUARD-ENABLE)))
    ,@(AND GUARD-THMS
       `((MUST-BE-ENABLED-REWRITE-RULE ,ALPHA-GUARD ,ALPHA-GUARD-ENABLE)))
    ,@(AND GUARD-THMS
       `((MUST-BE-ENABLED-REWRITE-RULE ,BETA-GUARD ,BETA-GUARD-ENABLE)))))