/usr/share/acl2-6.3/books/parallel/spec-mv-let.lisp is in acl2-books-source 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 | (in-package "ACL2")
(include-book "misc/assert" :dir :system)
(include-book "misc/eval" :dir :system)
(defun foo (z)
(declare (xargs :verify-guards nil
:guard (acl2-numberp z)))
(spec-mv-let
(x y)
(mv 3 4)
(mv-let (a b)
(mv 5 7)
(if (equal a z)
(+ x y a b z)
(+ a b)))))
(assert! (equal (foo 5) 24))
(assert! (equal (foo 1) 12))
(verify-guards foo)
(assert! (equal (foo 5) 24))
(assert! (equal (foo 1) 12))
(must-fail
; Incorrectly uses X in the false branch.
(defun boozo (z)
(spec-mv-let
(x y)
(mv 3 4)
(mv-let (a b)
(mv 5 7)
(if (equal a z)
(+ x y a b z)
(+ a b x))))))
(must-fail
; Incorrectly uses x in the test
(defun boozo (z)
(spec-mv-let
(x y)
(mv 3 4)
(mv-let (a b)
(mv 5 7)
(if (equal a x)
(+ x y a b z)
(+ a b))))))
(defun foo2 (z)
; Test that we can rebind speculated variables inside the branch that has to
; recompute the speculative variables' values.
(declare (xargs :verify-guards nil
:guard (acl2-numberp z)))
(spec-mv-let
(x y)
(mv 3 4)
(mv-let (a b)
(mv 5 7)
(if (equal a z)
(+ x y a b z)
(mv-let (x y)
(mv 10 11)
(+ a b x y z))))))
(assert! (equal (foo2 5) 24))
(assert! (equal (foo2 4) 37))
(verify-guards foo2)
(assert! (equal (foo2 5) 24))
(assert! (equal (foo2 4) 37))
(must-fail
; Incorrectly uses "the-very-obscure-future", which is used in our raw Lisp
; definition of spec-mv-let.
(defun boozo (the-very-obscure-future)
(spec-mv-let
(x y)
(mv 3 4)
(mv-let (a b)
(mv 5 7)
(if (equal the-very-obscure-future 4)
(+ x y a b)
(+ 7 8))))))
(must-fail
; Incorrectly omits a test for the spec-mv-let.
(defun boozo (z)
(spec-mv-let
(x y)
(mv 3 4)
(mv-let (a b)
(mv 5 7)
(list (equal a z)
(+ x y a b z))))))
(must-fail
; Incorrectly uses a "z" that we define to be ambiguous (if we decided to
; disambiguate the "z", it would have to refer to the given argument). Note
; that the given error message is different for this definition than in the
; following one.
(defun boozo (z)
(spec-mv-let
(z y)
(mv 3 4)
(mv-let (a b)
(mv 5 7)
(if (equal a z)
(+ y a b)
(+ a b))))))
(must-fail
; Incorrectly uses a "z" that we define to be ambiguous (if we decided to
; disambiguate the "z", it would have to refer to the given argument). Note
; that the given error message is different for this definition than in the
; following one.
(defun boozo (z)
(spec-mv-let
(z y)
(mv 3 4)
(mv-let (a b)
(mv 5 7)
(if (equal a 5)
(+ y a b)
(+ z a b))))))
|