look-up-tests

(in-package "STD")

(include-book "look-up")

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

(encapsulate nil
  (local (progn (assert! (not (var-is-stobj-p 'foo (w state))))
      (assert! (var-is-stobj-p 'state (w state)))
      (defstobj foo (field1 :initially 0))
      (assert! (var-is-stobj-p 'foo (w state))))))

(encapsulate nil
  (local (progn (assert! (equal (look-up-formals 'look-up-formals
            (w state))
          '(fn world))))))

(encapsulate nil
  (local (progn (defun f1 (x) x)
      (defun f2
        (x)
        (declare (xargs :guard (natp x)))
        x)
      (defun f3
        (x)
        (declare (xargs :guard (and (integerp x) (<= 3 x) (<= x 13))))
        x)
      (assert! (equal (look-up-guard 'f1 (w state)) 't))
      (assert! (equal (look-up-guard 'f2 (w state))
          '(natp x)))
      (assert! (equal (look-up-guard 'f3 (w state))
          '(if (integerp x)
            (if (not (< x '3))
              (not (< '13 x))
              'nil)
            'nil))))))

(encapsulate nil
  (local (progn (defun f1 (x) x)
      (defun f2 (x) (mv x x))
      (defun f3
        (x state)
        (declare (xargs :stobjs state))
        (mv x state))
      (assert! (equal (look-up-return-vals 'f1 (w state))
          '(nil)))
      (assert! (equal (look-up-return-vals 'f2 (w state))
          '(nil nil)))
      (assert! (equal (look-up-return-vals 'f3 (w state))
          '(nil state))))))

(encapsulate nil
  (local (progn (defun f1 (x) x)
      (defmacro f2 (x) x)
      (defmacro f3
        (x y &key (c '5) (d '7))
        (list x y c d))
      (assert! (equal (look-up-wrapper-args 'f1 (w state))
          '(x)))
      (assert! (equal (look-up-wrapper-args 'f2 (w state))
          '(x)))
      (assert! (equal (look-up-wrapper-args 'f3 (w state))
          '(x y &key (c '5) (d '7)))))))

(encapsulate nil
  (local (progn (defun f
        (x)
        (declare (xargs :mode :program))
        x)
      (defun g (x) x)
      (defun h
        (x)
        (declare (xargs :verify-guards t))
        x)
      (assert! (logic-mode-p 'g (w state)))
      (assert! (logic-mode-p 'h (w state)))
      (assert! (not (logic-mode-p 'f (w state)))))))