Filtering...

defmapping-tests-concrete

books/std/util/defmapping-tests-concrete

Included Books

defmapping must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "defmapping")
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
test-titlemacro
(defmacro test-title
  (str)
  `(cw-event (concatenate 'string "~%~%~%********** " ,STR "~%~%")))
other
(test-title "Identity isomorphisms over all values.")
other
(must-succeed (defmapping all-id
    any-p
    any-p
    identity
    identity
    :beta-of-alpha-thm t
    :alpha-of-beta-thm t))
other
(must-succeed (defmapping all-id
    any-p
    any-p
    identity
    identity
    :beta-of-alpha-thm t
    :alpha-of-beta-thm t
    :unconditional t))
other
(test-title "Identity isomorphisms over natural numbers.")
other
(must-succeed (defmapping nat-id
    natp
    natp
    identity
    identity
    :beta-of-alpha-thm t
    :alpha-of-beta-thm t))
other
(must-succeed (defmapping nat-id
    natp
    natp
    identity
    identity
    :beta-of-alpha-thm t
    :alpha-of-beta-thm t
    :unconditional t))
other
(test-title "Isomorphisms between naturals and integers.")
other
(must-succeed* (defun nat-to-int
    (n)
    (declare (xargs :guard (natp n)))
    (if (evenp n)
      (/ n 2)
      (- (/ (1+ n) 2))))
  (defun int-to-nat
    (i)
    (declare (xargs :guard (integerp i)))
    (if (>= i 0)
      (* 2 i)
      (1- (- (* 2 i)))))
  (local (include-book "arithmetic-5/top" :dir :system))
  (defmapping nat-int
    natp
    integerp
    nat-to-int
    int-to-nat
    :beta-of-alpha-thm t
    :alpha-of-beta-thm t)
  (defmapping int-nat
    integerp
    natp
    int-to-nat
    nat-to-int
    :beta-of-alpha-thm t
    :alpha-of-beta-thm t))
other
(test-title "Isomorphisms between {0, ..., 9} and {9, ..., 0}.")
other
(must-succeed* (defun swap-range
    (x)
    (declare (xargs :guard (integer-range-p 0 10 x)))
    (- 9 x))
  (defmapping zeronine
    (lambda (x) (integer-range-p 0 10 x))
    (lambda (x) (integer-range-p 0 10 x))
    swap-range
    swap-range
    :beta-of-alpha-thm t
    :alpha-of-beta-thm t))
other
(test-title "Isomorphisms between (MV X Y) and (MV Y X).")
other
(must-succeed* (defun swap-pair (x y) (declare (xargs :guard t)) (mv y x))
  (defmapping swap-pair
    (lambda (x y) t)
    (lambda (x y) t)
    swap-pair
    swap-pair
    :beta-of-alpha-thm t
    :alpha-of-beta-thm t))
other
(test-title "Isomorphism between (MV X Y Z) and (MV (CONS X Y) Z).")
other
(must-succeed* (defun groupedp
    (xy z)
    (declare (xargs :guard t))
    (declare (ignore z))
    (consp xy))
  (defun group
    (x y z)
    (declare (xargs :guard t))
    (mv (cons x y) z))
  (defun ungroup
    (xy z)
    (declare (xargs :guard (consp xy)))
    (mv (car xy) (cdr xy) z))
  (defmapping grouping
    (lambda (x y z) t)
    groupedp
    group
    ungroup
    :beta-of-alpha-thm t
    :alpha-of-beta-thm t))
other
(test-title "Identity isomorphisms over pairs in an unspecified domain.")
other
(must-succeed* (defstub dom2 (* *) => *)
  (defmapping id-pair
    dom2
    dom2
    (lambda (x y) (mv x y))
    (lambda (x y) (mv x y))
    :beta-of-alpha-thm t
    :alpha-of-beta-thm t))