bstar - ACL2 Book

Included Books

bstar

other

(in-package "ACL2")

include-book

(include-book "../bstar")

other

(set-state-ok t)

return-two-valuesfunction

(defun return-two-values (a b) (mv a b))

transl-equal-tests-fnfunction

(defun transl-equal-tests-fn
  (tests)
  (if (atom tests)
    `(mv nil state)
    `(mv-let (err val state)
      (transl-equal ',(CAAR TESTS) ',(CADAR TESTS))
      (if (or err (not val))
        (mv ',(CAR TESTS) state)
        ,(TRANSL-EQUAL-TESTS-FN (CDR TESTS))))))

transl-equal-testsmacro

(defmacro transl-equal-tests
  (&rest tests)
  (transl-equal-tests-fn tests))

other

(defstobj st1 (arr1 :type (array t (0)) :resizable t))

other

(defstobj st2 (arr2 :type (array t (0)) :resizable t))

patbind-tests-fnfunction

(defun patbind-tests-fn
  (tests state)
  (declare (xargs :mode :program))
  (if (atom tests)
    (value '(value-triple :invisible))
    (mv-let (erp val state)
      (thm-fn `(equal ,(CAAR TESTS) ,(CADAR TESTS))
        state
        nil
        '(("goal" :in-theory nil))
        nil
        nil)
      (if erp
        (mv (msg "~% ****** ERROR ******~%~
Testing of the patbind macro failed on expression ~x0~%~%"
            (car tests))
          val
          state)
        (patbind-tests-fn (cdr tests) state)))))

patbind-run-testsmacro

(defmacro patbind-run-tests
  (&rest tests)
  `(make-event (patbind-tests-fn ',TESTS state)))

other

(patbind-run-tests ((patbind (cons (cons a b) c) (x) (list a b c)) (let* ((|(CAR X)| (car x)) (c (cdr x)))
      (let* ((a (car |(CAR X)|)) (b (cdr |(CAR X)|)))
        (list a b c))))
  ((patbind x ((cons 'a 'b)) x) (let ((x (cons 'a 'b)))
      x))
  ((patbind (mv a b) ((mv 'a 'b)) (list a b)) (mv-let (a b) (mv 'a 'b) (list a b)))
  ((patbind & ((cw "Hello")) nil) nil)
  ((patbind - ((cw "Hello")) nil) (prog2$ (cw "Hello") nil))
  ((patbind (cons a &) ('(a b)) a) (let ((a (car '(a b))))
      a))
  ((patbind (cons (cons a b) c) (x) (list a b c)) (let ((|(CONS A B)| (car x)) (c (cdr x)))
      (let ((a (car |(CONS A B)|)) (b (cdr |(CONS A B)|)))
        (list a b c))))
  ((patbind (cons (cons a b) c) ((cons x y)) (list a b c)) (let ((|(CONS (CONS A B) C)| (cons x y)))
      (let ((|(CONS A B)| (car |(CONS (CONS A B) C)|)) (c (cdr |(CONS (CONS A B) C)|)))
        (let ((a (car |(CONS A B)|)) (b (cdr |(CONS A B)|)))
          (list a b c)))))
  ((patbind (cons (cons & b) c) ((cons x y)) (list b c)) (let ((|(CONS (CONS & B) C)| (cons x y)))
      (let ((|(CONS & B)| (car |(CONS (CONS & B) C)|)) (c (cdr |(CONS (CONS & B) C)|)))
        (let ((b (cdr |(CONS & B)|)))
          (list b c)))))
  ((patbind (cons (cons a &) c) ((cons x y)) (list a c)) (let ((|(CONS (CONS A &) C)| (cons x y)))
      (let ((|(CONS A &)| (car |(CONS (CONS A &) C)|)) (c (cdr |(CONS (CONS A &) C)|)))
        (let ((a (car |(CONS A &)|)))
          (list a c)))))
  ((patbind (mv (cons a (cons b c)) d)
     ((return-two-values x y))
     (list a b c d)) (mv-let (|(CONS A (CONS B C))| d)
      (return-two-values x y)
      (let ((a (car |(CONS A (CONS B C))|)) (|(CONS B C)| (cdr |(CONS A (CONS B C))|)))
        (let ((b (car |(CONS B C)|)) (c (cdr |(CONS B C)|)))
          (list a b c d)))))
  ((patbind (mv (cons a (cons b c)) &)
     ((return-two-values x y))
     (list a b c d)) (mv-let (|(CONS A (CONS B C))| ignore-0)
      (return-two-values x y)
      (declare (ignore ignore-0))
      (let ((a (car |(CONS A (CONS B C))|)) (|(CONS B C)| (cdr |(CONS A (CONS B C))|)))
        (let ((b (car |(CONS B C)|)) (c (cdr |(CONS B C)|)))
          (list a b c d)))))
  ((patbind (mv (cons a (cons & c)) &)
     ((return-two-values x y))
     (list a c d)) (mv-let (|(CONS A (CONS & C))| ignore-0)
      (return-two-values x y)
      (declare (ignore ignore-0))
      (let ((a (car |(CONS A (CONS & C))|)) (|(CONS & C)| (cdr |(CONS A (CONS & C))|)))
        (let ((c (cdr |(CONS & C)|)))
          (list a c d)))))
  ((patbind `(,A ,B) ((cons x y)) (list a b)) (let ((|(CONS A (CONS B (QUOTE NIL)))| (cons x y)))
      (let ((a (car |(CONS A (CONS B (QUOTE NIL)))|)) (|(CONS B (QUOTE NIL))| (cdr |(CONS A (CONS B (QUOTE NIL)))|)))
        (let ((b (car |(CONS B (QUOTE NIL))|)))
          (list a b))))))

len-resize-listtheorem

(defthm len-resize-list
  (equal (len (resize-list a b c)) (nfix b)))

localstobjtestfunction

(defun localstobjtest
  (a b c)
  (declare (xargs :guard t))
  (b* ((d (cons b c)) ((local-stobjs st1 st2) (mv g st2 h st1))
      (a (nfix a))
      (st1 (resize-arr1 (+ 1 a) st1))
      (st2 (resize-arr2 (+ 1 (nfix b)) st2))
      (st1 (update-arr1i a d st1))
      (st2 (update-arr2i (nfix b) a st2)))
    (mv (arr2i (nfix b) st2) st2 (arr1i a st1) st1)))

other

(make-event (mv-let (res1 res2)
    (localstobjtest nil 10 'c)
    (if (and (equal res1 0) (equal res2 '(10 . c)))
      '(value-triple :passed)
      (er hard 'test-local-stobj "test failed"))))

patbind-macro-test0encapsulate

(encapsulate nil
  (defun patbind-macro-test0
    (x y)
    (b* (((macro (add a b)) `(+ ,A ,B))) (add x y)))
  (make-event (if (equal (patbind-macro-test0 1 2) 3)
      '(value-triple :passed)
      (er hard 'test patbind-macro-test0 "test failed"))))

patbind-macro-test1encapsulate

(encapsulate nil
  (defun patbind-macro-test1
    (x y)
    (b* (((macro notinline (add a b)) `(+ ,A ,B)) ((macro inline (minus a b)) `(- ,A ,B)))
      (minus 0 (add x y))))
  (make-event (if (equal (patbind-macro-test1 1 2) -3)
      '(value-triple :passed)
      (er hard 'test patbind-macro-test1 "test failed"))))