← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/make-event/assert.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/make-event/assert.lisp
4
4
(in-package "ACL2")
5
5
 
6
6
(defun assert!-body (assertion form)
 
7
 
 
8
; Note that assertion should evaluate to a single non-stobj value.  See also
 
9
; assert!-stobj-body.
 
10
 
7
11
  `(let ((assertion ,assertion))
8
12
     (er-progn
9
13
      (if assertion
15
19
 
16
20
(defmacro assert! (&whole whole-form
17
21
                          assertion &optional form)
 
22
 
 
23
; Note that assertion should evaluate to a single non-stobj value.  See also
 
24
; assert!-stobj.
 
25
 
18
26
  (list 'make-event (assert!-body assertion form)
19
27
        :on-behalf-of whole-form))
20
28
 
52
60
(assert! (equal (access-command-tuple-form
53
61
                 (cddr (car (scan-to-command (w state)))))
54
62
                '(exit-boot-strap-mode)))
 
63
 
 
64
; We turn now to developing an extension of assert! that works with stobjs, in
 
65
; this case for assertions that return (mv val st) where val is an ordinary
 
66
; value and st is a stobj.  Our intention is to illustrate how to write other
 
67
; versions of assert!.  If you understand this extension, you can then write
 
68
; your own extensions that can similarly handle other signatures for the
 
69
; assertion.
 
70
 
 
71
(defun assert!-stobj-body (assertion st form)
 
72
 
 
73
; Assertion should evaluate to (mv val st), where val is an ordinary value and
 
74
; st is a stobj.  See also assert!-body.
 
75
 
 
76
  `(mv-let (result ,st)
 
77
           ,assertion
 
78
           (if result
 
79
               (mv nil ',(or form '(value-triple nil)) state ,st)
 
80
             (mv-let (erp val state)
 
81
                     (er soft 'assert!
 
82
                         "Assertion failed:~%~x0"
 
83
                         ',assertion)
 
84
                     (declare (ignore erp val))
 
85
                     (mv t nil state ,st)))))
 
86
 
 
87
(defmacro assert!-stobj (&whole whole-form
 
88
                                assertion st &optional form)
 
89
 
 
90
; Assertion should evaluate to (mv val st), where val is an ordinary value and
 
91
; st is a stobj.  See also assert!.
 
92
 
 
93
  (list 'make-event (assert!-stobj-body assertion st form)
 
94
        :on-behalf-of whole-form))
 
95
 
 
96
; Test-stobj example from David Rager.
 
97
(local
 
98
 (encapsulate
 
99
  ()
 
100
 
 
101
  (defstobj foo field1 field2)
 
102
 
 
103
  (defun test-stobj (x foo)
 
104
    (declare (xargs :stobjs foo))
 
105
    (let ((foo (update-field1 17 foo)))
 
106
      (update-field2 x foo)))
 
107
 
 
108
; Passes.
 
109
  (assert!-stobj (let* ((foo (test-stobj 14 foo)))
 
110
                   (mv (equal (field1 foo)
 
111
                              17)
 
112
                       foo))
 
113
                 foo)
 
114
 
 
115
  (must-fail
 
116
   (assert!-stobj (let* ((foo (test-stobj 14 foo)))
 
117
                    (mv (equal (field1 foo)
 
118
                               14)
 
119
                        foo))
 
120
                  foo))
 
121
  ))