← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to .pc/remove-pcert-local-elided-for-final-file/books/make-event/local-elided.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
.pc/remove-pcert-local-elided-for-final-file/books/make-event/local-elided.lisp
 
1
; Copyright (C) 2013, Regents of the University of Texas
 
2
; Written by Matt Kaufmann
 
3
; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.
 
4
 
 
5
(in-package "ACL2")
 
6
 
 
7
;; [Jared and Sol]: we want to make sure this book gets provisionally certified
 
8
;; if we're doing any provisional certification, because
 
9
;; local-elided-include.lisp is going to test whether its .pcert0 file exists
 
10
;; as a proxy for checking whether it was provisionally or regularly certified,
 
11
;; and that's just sort of wrong...
 
12
 
 
13
; cert_param: (pcert)
 
14
 
 
15
(local (make-event '(defun foo (x) x)))
 
16
 
 
17
(make-event '(local (defun foo (x) x)))
 
18
 
 
19
(make-event '(local (defun foo-2 (x) x)))
 
20
 
 
21
(progn
 
22
  (encapsulate
 
23
   ((bar1 (x) t))
 
24
   (local (defun bar1 (x) (foo x)))
 
25
   (defthm bar1-preserves-consp
 
26
     (implies (consp x)
 
27
              (consp (bar1 x))))))
 
28
 
 
29
(progn
 
30
  (make-event '(local (defun g (x) x)))
 
31
  (local (defun g2 (x) x))
 
32
  (make-event
 
33
   (value '(encapsulate
 
34
            ((bar2 (x) t))
 
35
            (local (defun bar2 (x) (foo x)))
 
36
            (defthm bar2-preserves-consp
 
37
              (implies (consp x)
 
38
                       (consp (bar2 x))))))))
 
39
 
 
40
; redundant
 
41
(make-event
 
42
 (value '(encapsulate
 
43
          ((bar2 (x) t))
 
44
          (local (defun bar2 (x) (foo x)))
 
45
          (defthm bar2-preserves-consp
 
46
            (implies (consp x)
 
47
                     (consp (bar2 x)))))))
 
48
 
 
49
(make-event
 
50
 (value '(encapsulate
 
51
          ((bar3 (x) t))
 
52
          (make-event '(local (defun bar3 (x) (foo x))))
 
53
          (defthm bar3-preserves-consp
 
54
            (implies (consp x)
 
55
                     (consp (bar3 x)))))))
 
56
 
 
57
; redundant
 
58
(encapsulate
 
59
 ((bar3 (x) t))
 
60
 (make-event '(local (defun bar3 (x) (foo x))))
 
61
 (defthm bar3-preserves-consp
 
62
   (implies (consp x)
 
63
            (consp (bar3 x)))))
 
64
 
 
65
; not still redundant
 
66
(include-book "misc/eval" :dir :system)
 
67
(must-fail
 
68
 (encapsulate
 
69
  ((bar3 (x) t))
 
70
  (local (defun bar3 (x) (foo x)))
 
71
  (defthm bar3-preserves-consp
 
72
    (implies (consp x)
 
73
             (consp (bar3 x))))))
 
74
 
 
75
(make-event '(defun foo-3 (x) x))
 
76
 
 
77
(defmacro my-local (x)
 
78
  `(local ,x))
 
79
 
 
80
(encapsulate
 
81
 ()
 
82
 (my-local (defun g3 (x) x))
 
83
 (make-event '(my-local (defun g3 (x) x)))
 
84
 (make-event '(my-local (defun g4 (x) x)))
 
85
 (my-local (defun g4 (x) x))
 
86
 (progn (my-local (defun g5 (x) x))
 
87
        (my-local (make-event (value '(defun g6 (x) x))))))
 
88