defredundant

(in-package "STD")

(include-book "../defredundant")

(include-book "misc/definline" :dir :system)

(include-book "../defines")

(encapsulate nil
  (local (progn (defun f1
        (x)
        (declare (xargs :normalize nil))
        (+ 1 x))
      (defthm natp-of-f1
        (implies (natp x)
          (natp (f1 x))))
      (defund f2
        (x)
        (declare (xargs :verify-guards nil))
        (+ 1 x))
      (defthmd natp-of-f2
        (implies (natp x)
          (natp (f2 x)))
        :rule-classes :type-prescription :hints (("Goal" :in-theory (enable f2))))
      (defun f3
        (x)
        (declare (xargs :guard (natp x) :verify-guards t))
        (+ 1 x))
      (in-theory (disable (:e f3)))
      (mutual-recursion (defun f4-term
          (x)
          (declare (xargs :guard (pseudo-termp x)))
          (if (atom x)
            1
            (if (quotep x)
              2
              (cons (car x) (f4-list (cdr x))))))
        (defund f4-list
          (x)
          (declare (xargs :guard (pseudo-term-listp x)))
          (if (atom x)
            nil
            (cons (f4-term (car x))
              (f4-list (cdr x))))))
      (definline f5
        (x)
        (declare (xargs :guard t))
        x)
      (definlined f6
        (x)
        (declare (xargs :guard (natp x)))
        (+ 1 x))
      (defun f7
        (x)
        (declare (xargs :mode :program))
        (+ 1 x))
      (definline f8
        (x)
        (declare (xargs :mode :program :guard (natp x)))
        (+ 1 x))
      (defun m
        (x y)
        (+ (acl2-count x) (acl2-count y)))
      (defund f9
        (x y)
        (declare (xargs :measure (m x y)))
        (if (and (atom x) (atom y))
          0
          (+ (f9 (cdr x) (cdr y)))))
      (defines g0
        (define g0-term
          (x)
          :inline t
          :guard (pseudo-termp x)
          (if (atom x)
            1
            (if (quotep x)
              2
              (cons (car x) (g0-list (cdr x))))))
        (define g0-list
          (x)
          :guard (pseudo-term-listp x)
          :enabled t
          (if (atom x)
            nil
            (cons (g0-term (car x))
              (g0-list (cdr x))))))
      (defun test-irrelevant
        (x y)
        (declare (irrelevant y))
        (if (atom x)
          nil
          (test-irrelevant (cdr x) y)))
      (defun test-optimize
        (x)
        (declare (optimize (safety 3)))
        x)))
  (defredundant :names (f1 natp-of-f1
      f2
      natp-of-f2
      f3
      f4-term
      f5
      f9
      g0-list
      test-irrelevant
      test-optimize)))

(defmacro assert-enabled
  (rune enabled-p)
  `(make-event (b* ((rune ',STD::RUNE) (ens (ens state))
        (actual (if (active-runep rune)
            t
            nil))
        ((when (equal actual ',STD::ENABLED-P)) (value '(value-triple :success))))
      (er soft
        'assert-enabled
        "Expected (active-runep ~x0) to be ~x1, found ~x2.~%"
        rune
        ',STD::ENABLED-P
        actual))))

(defmacro assert-macro
  (name)
  `(make-event (b* ((macro-args (getprop ',STD::NAME
           'macro-args
           :bad 'current-acl2-world
           (w state))) ((unless (eq macro-args :bad)) (value '(value-triple :success))))
      (er soft
        'assert-macro
        "Expected ~x0 to be a macro, but found no macro args."
        ',STD::NAME))))

(assert-enabled (:definition f1) t)

(assert-enabled (:definition f2) nil)

(assert-enabled (:definition f3) t)

(assert-enabled (:definition f4-term) t)

(assert-enabled (:definition f4-list) nil)

(assert-enabled (:definition f5$inline) t)

(assert-enabled (:type-prescription f5$inline) t)

(assert-macro f5)

(assert-enabled (:definition f9) nil)

(assert-enabled (:definition g0-term) nil)

(assert-enabled (:definition g0-list) t)

(assert-macro g0-term)

(assert-enabled (:rewrite natp-of-f1) t)

(assert-enabled (:type-prescription natp-of-f2)
  nil)

(assert-enabled (:executable-counterpart f1) t)

(assert-enabled (:executable-counterpart f2) t)

(assert-enabled (:executable-counterpart f3) nil)

(assert-enabled (:executable-counterpart f9) t)

(assert-enabled (:definition test-irrelevant) t)

(assert-enabled (:definition test-optimize) t)