/usr/share/acl2-6.3/books/misc/eval.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 | ; 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.
; Here we define macros that employ make-event to check evaluations of forms.
; See community book make-event/eval-tests.lisp (and many other .lisp files in
; that directory) for how these macros may be employed. See also
; make-event/eval-check.lisp for a similar book that adds :check-expansion t to
; its make-event forms.
(in-package "ACL2")
(defmacro must-eval-to (&whole must-eval-to-form
form expr
&key (ld-skip-proofsp ':default))
; Warning: Keep this in sync with the definition of must-eval-to in community
; book make-event/eval-check.lisp.
; Form should evaluate to an error triple (mv erp form-val state). If erp is
; nil and expr-val is the value of expr then (must-eval-to form expr) expands
; to (value-triple 'expr-val); otherwise expansion causes an appropriate soft
; error. Note that both form and expr are evaluated.
(let ((body
`(er-let* ((form-val-use-nowhere-else ,form))
(let ((expr-val (check-vars-not-free
(form-val-use-nowhere-else)
,expr)))
(cond ((eq form-val-use-nowhere-else expr-val)
(value (list 'value-triple (list 'quote expr-val))))
(t (er soft
(msg "( MUST-EVAL-TO ~@0 ~@1)"
(tilde-@-abbreviate-object-phrase ',form)
(tilde-@-abbreviate-object-phrase ',expr))
"Evaluation returned ~X01, not the value ~x2 of ~
the expression ~x3."
form-val-use-nowhere-else
(evisc-tuple 4 3 nil nil)
expr-val
',expr)))))))
`(make-event ,(if (eq ld-skip-proofsp :default)
body
`(state-global-let*
((ld-skip-proofsp ,ld-skip-proofsp))
,body))
:on-behalf-of ,must-eval-to-form)))
(defmacro must-eval-to-t (form &key (ld-skip-proofsp ':default))
; Form should evaluate to an error triple (mv erp val state). If erp is nil
; and val is t then (must-eval-to-t form) expands to (value-triple t);
; otherwise expansion causes an appropriate soft error.
`(must-eval-to ,form t ,@(and (not (eq ld-skip-proofsp :default))
`(:ld-skip-proofsp ,ld-skip-proofsp))))
(defmacro must-succeed (&whole must-succeed-form
form)
; (Must-succeed form) expands to (value-triple t) if evaluation of form is an
; error triple (mv nil val state), and causes a soft error otherwise.
`(make-event
'(must-eval-to-t
(mv-let (erp val state)
,form
(declare (ignore val))
(value (eq erp nil))))
:on-behalf-of ,must-succeed-form))
(defmacro must-fail (&whole must-fail-form
form)
; Form should evaluate to an error triple (mv erp val state). (Must-fail
; form) expands to (value-triple t) if erp is non-nil, and expansion causes a
; soft error otherwise.
; Remark on provisional certification: By default we bind state global
; ld-skip-proofsp to nil when generating the .acl2x file for this book during
; provisional certification. We do this because in some cases must-fail
; expects proofs to fail. Some books in the distributed books/make-event/
; directory have the following comment when this change was necessary for
; .acl2x file generation during provisional certification:
; "; See note about ld-skip-proofsp in the definition of must-fail."
`(make-event
'(must-eval-to-t
(mv-let (erp val state)
,form
(declare (ignore val))
(value (not (eq erp nil))))
:ld-skip-proofsp
(if (eq (cert-op state) :write-acl2xu)
nil
(f-get-global 'ld-skip-proofsp state)))
:on-behalf-of ,must-fail-form))
(defmacro thm? (&rest args)
`(must-succeed (thm ,@args)))
(defmacro not-thm? (&rest args)
`(must-fail (thm ,@args)))
|