/usr/share/acl2-6.5/books/misc/assert.lisp is in acl2-books-source 6.5-2.
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 | ; Copyright (C) 2013, Regents of the University of Texas
; Written by Matt Kaufmann (some years before that)
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; The macro assert!, defined and illustrated below, allows for assertions
; within an ACL2 book, as requested by David Rager.
; 2012-03-12: David Rager made the calls to assert! that fail local, so that
; break-on-error wouldn't break when including this book. Also, it's nice to
; have less clutter when including the book.
(in-package "ACL2")
(defun assert!-body (assertion form)
; Note that assertion should evaluate to a single non-stobj value. See also
; assert!-stobj-body.
`(let ((assertion ,assertion))
(er-progn
(if assertion
(value nil)
(er soft 'assert!
"Assertion failed:~%~x0"
',assertion))
(value ',(or form '(value-triple :success))))))
(defmacro assert! (&whole whole-form
assertion &optional form)
; Note that assertion should evaluate to a single non-stobj value. See also
; assert!-stobj.
(list 'make-event (assert!-body assertion form)
:on-behalf-of whole-form))
(assert! (equal 3 3)
(defun assert-test1 (x) x))
; Check that above defun was evaluated.
(value-triple (or (equal (assert-test1 3) 3)
(er hard 'top-level
"Failed to evaluate (assert-test1 3) to 3.")))
(include-book "eval")
(local
(must-fail
(assert! (equal 3 4)
(defun assert-test2 (x) x))))
; Check that above defun was not evaluated.
(defun assert-test2 (x)
(cons x x))
; Simple test with no second argument:
(assert! (equal (append '(a b c) '(d e f))
'(a b c d e f)))
; Check failure of assertion when condition is false:
(local
(must-fail
(assert! (equal (append '(a b c) '(d e f))
'(a b)))))
; The following requires that this book be certified in the initial
; certification world. It also succeeds at include-book time even if we
; include the book after executing another command, because assert! uses
; make-event with :check-expansion nil. See assert-include.lisp.
(local (assert! (equal (access-command-tuple-form
(cddr (car (scan-to-command (w state)))))
'(exit-boot-strap-mode))))
; We turn now to developing an extension of assert! that works with stobjs, in
; this case for assertions that return (mv val st) where val is an ordinary
; value and st is a stobj. Our intention is to illustrate how to write other
; versions of assert!. If you understand this extension, you can then write
; your own extensions that can similarly handle other signatures for the
; assertion.
(defun assert!-stobj-body (assertion st form)
; Assertion should evaluate to (mv val st), where val is an ordinary value and
; st is a stobj. See also assert!-body.
`(mv-let (result ,st)
,assertion
(if result
(mv nil ',(or form '(value-triple :success)) state ,st)
(mv-let (erp val state)
(er soft 'assert!
"Assertion failed:~%~x0"
',assertion)
(declare (ignore erp val))
(mv t nil state ,st)))))
(defmacro assert!-stobj (&whole whole-form
assertion st &optional form)
; Assertion should evaluate to (mv val st), where val is an ordinary value and
; st is a stobj. See also assert!.
(list 'make-event (assert!-stobj-body assertion st form)
:on-behalf-of whole-form))
; Test-stobj example from David Rager.
(local
(encapsulate
()
(defstobj foo field1 field2)
(defun test-stobj (x foo)
(declare (xargs :stobjs foo))
(let ((foo (update-field1 17 foo)))
(update-field2 x foo)))
; Passes.
(assert!-stobj (let* ((foo (test-stobj 14 foo)))
(mv (equal (field1 foo)
17)
foo))
foo)
(must-fail
(assert!-stobj (let* ((foo (test-stobj 14 foo)))
(mv (equal (field1 foo)
14)
foo))
foo))
))
|