/usr/share/acl2-6.3/books/make-event/eval-check-tests.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 | ; Copyright (C) 2013, Regents of the University of Texas
; Written by Matt Kaufmann (sometime before that)
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; This is a variant of eval-tests.lisp that includes eval-check.lisp, which
; employs :check-expansion t, instead of
; eval.lisp. See below for the main change, marked with "New comment for
; eval-check-tests.lisp".
(in-package "ACL2")
; Define must-succeed and must-fail:
(include-book "eval-check")
; A simple test:
(must-succeed
(defthm eval-bar
(equal x (car (cons x y)))
:rule-classes nil))
; The defthm just above was evaluated during expansion. Recall that the ACL2
; logical world is reverted after expansion to its pre-expansion value, before
; the generated event is executed. In this case, the generated event is simply
; (value-triple t). So eval-bar should be gone from the logical world. We
; check that now by executing a different event with name eval-bar and
; observing that there is no redefinition error.
(defun eval-bar (x) x)
; New comment for eval-check-tests.lisp: The following fails when must-fail is
; defined using make-event with :check-expansion t, as above, because thm is
; skipped when ld-skip-proofsp is t -- unless ld-skip-proofsp is set to nil
; under the hood during expansion, which it is.
(must-fail
(with-output :off :all
(thm (equal x (cons x x)))))
(must-succeed
(must-fail
(with-output :off :all
(thm (equal x (cons x x))))))
; Check that a failure implies a failure of a failure of a failure (!). While
; we're at it, we save the length of the ACL2 logical world into our own state
; global variable, for use later.
(must-succeed
(with-output
:off :all
(pprogn
(f-put-global 'saved-world-length (length (w state)) state)
(must-fail
(must-fail
(must-fail
(with-output
:off :all
(thm (equal x (cons x x))))))))))
; Here we drive home the point made with eval-bar above, that expansion does
; not change the world. The next form after this one checks that the length of
; the world is the same as it was before this one.
(must-succeed
(defthm temp
(equal (car (cons x y)) x)))
; See comment above.
(must-fail
(mv (equal (f-get-global 'saved-world-length state)
(length (w state)))
nil
state))
; Just beating to death the point made above. Note that if we execute
; (defun abc (x) x)
; then this will fail.
(must-succeed
(with-output
:off error
(cond ((not (eql (f-get-global 'saved-world-length state)
(length (w state))))
(with-output
:on error
(er soft 'test-failure
"World length changed from ~x0 to ~x1."
(f-get-global 'saved-world-length state)
(length (w state)))))
(t
(must-fail
(must-fail
(must-fail
(with-output
:off error
(thm (equal x (cons x x)))))))))))
; Should fail because the shape is wrong, as expansion expects an ordinary
; value or else (mv erp val state ...) where "..." denotes optional stobjs.
(must-fail
(make-event (mv nil '(value-triple nil))))
; Above is as opposed to:
(must-succeed
(make-event (mv nil '(value-triple nil) state)))
; We should manually inspect the .out file to see that the expansion errors are
; as expected for the following.
; Generic expansion error: "MAKE-EVENT expansion for (MV T NIL STATE) caused an
; error."
(must-fail
(make-event
(mv t nil state)))
; Should print "Sample Expansion Error".
(must-fail
(make-event
(mv "Sample Expansion Error" nil state)))
; Should print "Sample Expansion Error: 17, howdy 23".
(must-fail
(make-event
(mv (msg "Sample Expansion Error: ~x0, ~@1"
17
(msg "howdy ~x0"
23))
nil
state)))
|