Filtering...

defproxy-test

books/misc/defproxy-test
other
(in-package "ACL2")
other
(set-state-ok t)
other
(defproxy foo (* state *) => (mv * state))
foo-implfunction
(defun foo-impl
  (x state y)
  (declare (xargs :guard (symbolp x)))
  (mv (cons x y) state))
other
(defttag :defproxy-test)
other
(defattach (foo foo-impl) :skip-checks t)
other
(make-event (mv-let (def state)
    (foo-impl 'defun state '(bar (x) (cons x x)))
    (value def)))
other
(assert-event (equal (bar 3) '(3 . 3)))
other
(verify-guards foo-impl)
other
(assert-event (equal (bar 3) '(3 . 3)))
other
(defattach (foo nil) :skip-checks t)
other
(defttag nil)
encapsulate
(encapsulate ((foo (x state y) (mv t state) :guard (and (symbolp x) x)))
  (local (defun foo
      (x state y)
      (declare (ignore x y))
      (mv nil state))))
other
(defattach foo foo-impl)
other
(make-event (mv-let (def state)
    (foo-impl 'defun state '(bar2 (x) (cons x x)))
    (value def)))
other
(assert-event (equal (bar2 3) '(3 . 3)))