File: local-elided.lisp

package info (click to toggle)
acl2 8.0dfsg-1
  • links: PTS
  • area: main
  • in suites: bullseye, buster
  • size: 226,956 kB
  • sloc: lisp: 2,678,900; ansic: 6,101; perl: 5,816; xml: 3,586; cpp: 2,624; ruby: 2,576; makefile: 2,443; sh: 2,312; python: 778; yacc: 764; ml: 763; awk: 260; csh: 186; php: 171; lex: 165; tcl: 44; java: 41; asm: 23; haskell: 17
file content (84 lines) | stat: -rw-r--r-- 2,286 bytes parent folder | download | duplicates (3)
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
; Copyright (C) 2013, Regents of the University of Texas
; Written by Matt Kaufmann
; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.

(in-package "ACL2")

;; [Jared and Sol]: we want to make sure this book gets provisionally certified
;; if we're doing any provisional certification, because
;; local-elided-include.lisp is going to test whether its .pcert0 file exists
;; as a proxy for checking whether it was provisionally or regularly certified,
;; and that's just sort of wrong...

(local (make-event '(defun foo (x) x)))

(make-event '(local (defun foo (x) x)))

(make-event '(local (defun foo-2 (x) x)))

(progn
  (encapsulate
   ((bar1 (x) t))
   (local (defun bar1 (x) (foo x)))
   (defthm bar1-preserves-consp
     (implies (consp x)
              (consp (bar1 x))))))

(progn
  (make-event '(local (defun g (x) x)))
  (local (defun g2 (x) x))
  (make-event
   (value '(encapsulate
            ((bar2 (x) t))
            (local (defun bar2 (x) (foo x)))
            (defthm bar2-preserves-consp
              (implies (consp x)
                       (consp (bar2 x))))))))

; redundant
(make-event
 (value '(encapsulate
          ((bar2 (x) t))
          (local (defun bar2 (x) (foo x)))
          (defthm bar2-preserves-consp
            (implies (consp x)
                     (consp (bar2 x)))))))

(make-event
 (value '(encapsulate
          ((bar3 (x) t))
          (make-event '(local (defun bar3 (x) (foo x))))
          (defthm bar3-preserves-consp
            (implies (consp x)
                     (consp (bar3 x)))))))

; redundant
(encapsulate
 ((bar3 (x) t))
 (make-event '(local (defun bar3 (x) (foo x))))
 (defthm bar3-preserves-consp
   (implies (consp x)
            (consp (bar3 x)))))

; Redundant after Version_7.1 (as of mid-September 2015).
(encapsulate
 ((bar3 (x) t))
 (local (defun bar3 (x) (foo x)))
 (defthm bar3-preserves-consp
   (implies (consp x)
            (consp (bar3 x)))))

(make-event '(defun foo-3 (x) x))

(defmacro my-local (x)
  `(local ,x))

(encapsulate
 ()
 (my-local (defun g3 (x) x))
 (make-event '(my-local (defun g3 (x) x)))
 (make-event '(my-local (defun g4 (x) x)))
 (my-local (defun g4 (x) x))
 (progn (my-local (defun g5 (x) x))
        (my-local (make-event (value '(defun g6 (x) x))))))