Filtering...

check-mv-let-call-tests

books/std/system/check-mv-let-call-tests

Included Books

check-mv-let-call assert-equal
other
(in-package "ACL2")
include-book
(include-book "check-mv-let-call")
include-book
(include-book "std/testing/assert-equal" :dir :system)
check-mv-let-call-untransmacro
(defmacro check-mv-let-call-untrans
  (x)
  `(b* (((mv & term &) (translate1-cmp ',X
         :stobjs-out '((:stobjs-out . :stobjs-out))
         t
         'top
         (w state)
         (default-state-vars nil))))
    (mv-list 7 (check-mv-let-call term))))
other
(assert-equal (mv-list 7 (check-mv-let-call 'var))
  '(nil nil nil nil nil nil nil))
other
(assert-equal (mv-list 7 (check-mv-let-call ''"const"))
  '(nil nil nil nil nil nil nil))
other
(assert-equal (mv-list 7 (check-mv-let-call '(f a b c)))
  '(nil nil nil nil nil nil nil))
other
(assert-equal (mv-list 7 (check-mv-let-call '((lambda (x) (cons x x)) y)))
  '(nil nil nil nil nil nil nil))
other
(assert-equal (mv-list 7
    (check-mv-let-call '((lambda (mv) ((lambda nil (body)))) mv-val)))
  '(t mv nil nil nil mv-val (body)))
other
(assert-equal (mv-list 7
    (check-mv-let-call '((lambda (mv) ((lambda (a) (body a)) (mv-nth '0 mv))) mv-val)))
  '(t mv (a) (0) (nil) mv-val (body a)))
other
(assert-equal (mv-list 7
    (check-mv-let-call '((lambda (mv)
         ((lambda (a b) (body a b)) (mv-nth '0 mv) (mv-nth '1 mv))) mv-val)))
  '(t mv (a b) (0 1) (nil nil) mv-val (body a b)))
other
(assert-equal (mv-list 7
    (check-mv-let-call '((lambda (mv)
         ((lambda (a b c) (body a b c)) (mv-nth '0 mv)
           (mv-nth '1 mv)
           (mv-nth '2 mv))) mv-val)))
  '(t mv (a b c) (0 1 2) (nil nil nil) mv-val (body a b c)))
other
(assert-equal (mv-list 7
    (check-mv-let-call '((lambda (mvvv)
         ((lambda (a b) (body a b)) (mv-nth '0 mv) (mv-nth '1 mv))) mv-val)))
  '(nil nil nil nil nil nil nil))
other
(assert-equal (mv-list 7
    (check-mv-let-call '((lambda (mv)
         ((lambda (a b) (body a b)) (mv-nth '1 mv) (mv-nth '0 mv))) mv-val)))
  '(nil nil nil nil nil nil nil))
other
(assert-equal (mv-list 7
    (check-mv-let-call '((lambda (mv) ((lambda (a b) (body a b)) (f mv) (g mv))) mv-val)))
  '(nil nil nil nil nil nil nil))
other
(assert-equal (mv-list 7
    (check-mv-let-call '((lambda (mv)
         ((lambda (x z) (cons x z)) (mv-nth '0 mv) (mv-nth '2 mv))) mv-val)))
  '(t mv (x z) (0 2) (nil nil) mv-val (cons x z)))
ffunction
(defun f (x) (mv x x))
other
(assert-equal (check-mv-let-call-untrans (mv-let (x y) (f u) (cons x y)))
  '(t mv (x y) (0 1) (nil nil) (f u) (cons x y)))
other
(assert-equal (check-mv-let-call-untrans (mv-let (x y) (f mv) (list x y mv)))
  '(t mv0
    (x y)
    (0 1)
    (nil nil)
    (f mv)
    (cons x (cons y (cons mv 'nil)))))
other
(assert-equal (check-mv-let-call-untrans (mv-let (x y) (f u) (declare (ignore x)) y))
  '(t mv (x y) (0 1) (t nil) (f u) y))
other
(assert-equal (check-mv-let-call-untrans (mv-let (x y) (f u) (declare (ignore y)) x))
  '(t mv (x y) (0 1) (nil t) (f u) x))