Filtering...

defprojection

books/std/util/tests/defprojection
other
(in-package "STD")
other
(include-book "../defprojection")
other
(include-book "std/testing/assert-bang" :dir :system)
other
(make-event (prog2$ (cw "~%~%~%WARNING!  PRINTER ON FIRE!~%You are loading ~
       std/util/tests/defprojection! Don't do that!~%~%")
    '(value-triple :invisible))
  :check-expansion t)
other
(in-theory nil)
dupefunction
(defun dupe
  (x)
  (declare (xargs :guard t))
  (cons x x))
other
(defprojection dupe-list
  (x)
  (dupe x)
  :optimize nil)
other
(defprojection dupe-list2
  (x)
  (dupe x)
  :optimize t)
other
(defprojection dupe-list3
  (x)
  (dupe x)
  :verify-guards nil)
other
(defprojection dupe-list4
  (x)
  (dupe x)
  :mode :program)
other
(local (in-theory (enable integer-listp)))
other
(defund square
  (x)
  (declare (xargs :guard (integerp x)))
  (* x x))
other
(defprojection slow-square-list
  (x)
  (square x)
  :guard (integer-listp x)
  :optimize nil)
other
(defprojection square-list
  (x)
  (square x)
  :guard (integer-listp x))
other
(defprojection program-square-list
  (x)
  (square x)
  :guard (integer-listp x)
  :mode :program)
other
(assert! (let ((x '(1 2 3 4 5 6 7 8 9 10)))
    (and (equal (square-list x)
        (slow-square-list x))
      (equal (square-list x)
        (program-square-list x)))))
other
(local (in-theory (enable car-cons cdr-cons car-cdr-elim)))
other
(defthm integerp-of-square
  (implies (integerp x)
    (integerp (square x)))
  :hints (("Goal" :in-theory (enable square))))
other
(defprojection square-list-r
  (x)
  (square x)
  :guard (integer-listp x)
  :result-type integer-listp
  :optimize nil)
other
(defprojection square-list-r2
  (x)
  (square x)
  :guard (integer-listp x)
  :result-type integer-listp
  :optimize nil
  :parallelize t)
other
(defprojection add1-list
  (x)
  (+ 1 x)
  :guard (integer-listp x)
  :parents (foo)
  :rest ((defthm add1-list-integer-list
     (implies (integer-listp x)
       (integer-listp (add1-list x))))))
other
(local (in-theory (enable symbol-listp)))
other
(defprojection symbol<-foo-list
  (x)
  (symbol< :foo x)
  :guard (symbol-listp x))
other
(defprojection symbol<-bar-list
  (x)
  (symbol< 'bar x)
  :guard (symbol-listp x))
other
(local (in-theory (enable alistp)))
other
(defprojection my-strip-cars
  (x)
  (car x)
  :nil-preservingp t
  :guard (alistp x))
other
(defund f
  (x)
  (declare (xargs :guard (consp x)))
  (car x))
other
(defprojection my-strip-cars2
  (x)
  (f x)
  :nil-preservingp t
  :guard (alistp x))
other
(defprojection m0 (x) (cons 1 x))
other
(assert! (let ((topic (find-topic 'm0
         (get-xdoc-table (w state)))))
    (not topic)))
other
(set-default-parents foo bar)
other
(defprojection m1 (x) (cons 1 x))
other
(assert! (let ((topic (find-topic 'm1
         (get-xdoc-table (w state)))))
    (and topic
      (equal (cdr (assoc :parents topic))
        '(foo bar)))))
other
(defprojection m2
  (x)
  (cons 1 x)
  :parents (bar))
other
(assert! (let ((topic (find-topic 'm2
         (get-xdoc-table (w state)))))
    (and topic
      (equal (cdr (assoc :parents topic)) '(bar)))))
other
(defprojection m3
  (x)
  (cons 1 x)
  :parents nil)
other
(assert! (let ((topic (find-topic 'm3
         (get-xdoc-table (w state)))))
    (not topic)))
other
(defprojection new-square-list
  ((x integer-listp))
  (square x)
  :verbosep t)
other
(local (in-theory (enable nat-listp
      (:compound-recognizer natp-compound-recognizer)
      (:type-prescription nfix))))
other
(defprojection nfix-list1
  ((x nat-listp))
  (nfix x)
  :returns (new-x nat-listp))
other
(defprojection nfix-list2
  ((x integer-listp))
  (nfix x)
  :returns (new-x nat-listp :hyp :guard))
other
(local (encapsulate nil
    (set-enforce-redundancy t)
    (defthm nat-listp-of-nfix-list2
      (implies (and (integer-listp x))
        (b* ((new-x (nfix-list2 x)))
          (nat-listp new-x))))))
other
(defprojection ifix-list
  ((x integer-listp))
  (nfix x)
  :returns (new-x nat-listp :hyp (nat-listp x)))
other
(local (encapsulate nil
    (set-enforce-redundancy t)
    (defthm nat-listp-of-ifix-list
      (implies (nat-listp x)
        (b* ((new-x (ifix-list x)))
          (nat-listp new-x))))))
other
(defund incr-if-greater
  (x n)
  (declare (xargs :guard (and (integerp x) (integerp n))))
  (ifix (if (< n x)
      (+ 1 x)
      x)))
other
(defthm incr-if-greater-type
  (integerp (incr-if-greater x n))
  :hints (("Goal" :in-theory (enable incr-if-greater ifix)))
  :rule-classes :type-prescription)
other
(include-book "centaur/nrev/fast" :dir :system)
other
(defprojection incr-if-greater-list
  ((x integer-listp) (k integerp))
  :share-suffix t
  :returns (new-x integer-listp)
  (incr-if-greater x k))
my-eqfunction
(defun my-eq
  (x y)
  (declare (xargs :mode :program))
  (eq x y))
other
(make-event (if (let* ((x '(6 8 9 1 2 3)) (incr (incr-if-greater-list x 5)))
      (and (equal incr '(7 9 10 1 2 3))
        (my-eq (nthcdr 3 incr) (nthcdr 3 x))))
    '(value-triple :ok)
    (er hard?
      'incr-if-greater-test
      "Problem with share-suffix argument")))
other
(defprojection incr-if-greater-list-ns
  ((x integer-listp) (k integerp))
  :returns (new-x integer-listp)
  (incr-if-greater x k))
other
(make-event (if (let* ((x '(6 8 9 1 2 3)) (incr (incr-if-greater-list-ns x 5)))
      (and (equal incr '(7 9 10 1 2 3))
        (not (my-eq (nthcdr 3 incr) (nthcdr 3 x)))))
    '(value-triple :ok)
    (er hard?
      'incr-if-greater-test
      "Problem with share-suffix argument")))