Filtering...

recursive-calls-tests

books/std/system/recursive-calls-tests

Included Books

recursive-calls pseudo-tests-and-call-listp assert-bang assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "recursive-calls")
include-book
(include-book "pseudo-tests-and-call-listp")
include-book
(include-book "std/testing/assert-bang" :dir :system)
include-book
(include-book "std/testing/assert-equal" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(assert! (let ((rc (recursive-calls 'len (w state))))
    (and (pseudo-tests-and-call-listp rc)
      (= (len rc) 1)
      (let ((rc1 (first rc)))
        (and (equal (access tests-and-call rc1 :tests) '((consp x)))
          (equal (access tests-and-call rc1 :call) '(len (cdr x))))))))
other
(must-succeed* (defun fib
    (n)
    (if (zp n)
      1
      (if (= n 1)
        1
        (+ (fib (- n 1)) (fib (- n 2))))))
  (assert! (let ((rc (recursive-calls 'fib (w state))))
      (and (pseudo-tests-and-call-listp rc)
        (= (len rc) 2)
        (let ((rc1 (first rc)))
          (and (equal (access tests-and-call rc1 :tests)
              '((not (zp n)) (not (= n '1))))
            (equal (access tests-and-call rc1 :call)
              '(fib (binary-+ '-1 n)))))
        (let ((rc2 (second rc)))
          (and (equal (access tests-and-call rc2 :tests)
              '((not (zp n)) (not (= n '1))))
            (equal (access tests-and-call rc2 :call)
              '(fib (binary-+ '-2 n)))))))))
other
(must-succeed* (defun fib
    (n)
    (declare (xargs :mode :program))
    (if (zp n)
      1
      (if (= n 1)
        1
        (+ (fib (- n 1)) (fib (- n 2))))))
  (assert! (let ((rc (recursive-calls 'fib (w state))))
      (and (pseudo-tests-and-call-listp rc)
        (= (len rc) 2)
        (let ((rc1 (first rc)))
          (and (equal (access tests-and-call rc1 :tests)
              '((not (zp n)) (not (= n '1))))
            (equal (access tests-and-call rc1 :call)
              '(fib (binary-+ '-1 n)))))
        (let ((rc2 (second rc)))
          (and (equal (access tests-and-call rc2 :tests)
              '((not (zp n)) (not (= n '1))))
            (equal (access tests-and-call rc2 :call)
              '(fib (binary-+ '-2 n)))))))))
other
(must-succeed* (defun nonrec (x) (cons x x))
  (assert-equal (recursive-calls 'nonrec (w state)) nil))
other
(must-succeed* (defun nonrec
    (x)
    (declare (xargs :mode :program))
    (cons x x))
  (assert-equal (recursive-calls 'nonrec (w state)) nil))