acl2-books-source 6.3-5 / usr / share / acl2-6.3 / books / make-event / eval-tests.lisp

This file is indexed.

/usr/share/acl2-6.3/books/make-event/eval-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
125
126
127
; 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.

; Here we illustrate the must-succeed and must-fail macros, which use
; make-event to check that a form evaluates as expected.

; While we're at it, we also illustrate the use of state globals to manage
; information about expansions and check that expansion does not modify the
; world.

(in-package "ACL2")

; Define must-succeed and must-fail:
(include-book "misc/eval" :dir :system)

; 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)

; The following should not generate any output.  An interesting thing to do is
; (assign make-event-debug t) to see the expansion process.
(must-fail ; See note about ld-skip-proofsp in the definition of must-fail.
 (with-output :off :all
              (thm (equal x (cons x x)))))

; The following should not generate any output, and illustrates that we can
; nest macros that use make-event.  An interesting thing to do is (assign
; make-event-debug t) to see the expansion process.
(must-succeed
 (must-fail ; See note about ld-skip-proofsp in the definition of 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 ; See note about ld-skip-proofsp in the definition of 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 ; See note about ld-skip-proofsp in the definition of 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)))

APT Browse - Built by Thomas Orozco.