← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2004/smith-et-al/support/syntax/syntax.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:
books/workshops/2004/smith-et-al/support/syntax/syntax.lisp
 
1
(in-package "SYN")
 
2
 
 
3
(defun syn::len (n list)
 
4
  (declare (type (integer 0 *) n))
 
5
  (acl2::if (acl2::consp list)
 
6
      (acl2::if (zp n) acl2::nil
 
7
        (len (1- n) (acl2::cdr list)))
 
8
    (acl2::and (acl2::null list) (= n 0))))
 
9
 
 
10
(defthm open-len
 
11
  (implies
 
12
   (syntaxp (acl2::quotep n))
 
13
   (equal (len n list)
 
14
          (acl2::if (acl2::consp list)
 
15
              (acl2::if (zp n) acl2::nil
 
16
                (len (1- n) (acl2::cdr list)))
 
17
            (acl2::and (acl2::null list) (= n 0))))))
 
18
 
 
19
(defun nth (n l)
 
20
  (declare (type (integer 0 *) n))
 
21
  (acl2::and (acl2::consp l)
 
22
             (acl2::if (zp n)
 
23
                 (acl2::car l)
 
24
               (nth (+ -1 n) (acl2::cdr l)))))
 
25
 
 
26
(defthm open-nth
 
27
  (implies
 
28
   (syntaxp (acl2::quotep n))
 
29
   (equal (nth n l)
 
30
          (acl2::and (acl2::consp l)
 
31
                     (acl2::if (zp n)
 
32
                         (acl2::car l)
 
33
                         (nth (+ -1 n) (acl2::cdr l)))))))
 
34
          
 
35
(defthm len-implies-true-listp
 
36
  (implies
 
37
   (len n list)
 
38
   (true-listp list))
 
39
  :rule-classes (:forward-chaining))
 
40
 
 
41
(defthm len-implies-acl2-len
 
42
  (implies
 
43
   (len n list)
 
44
   (equal (acl2::len list) n))
 
45
  :rule-classes (:linear :forward-chaining))
 
46
 
 
47
(defun syn::consp (term)
 
48
  (declare (type t term))
 
49
  (acl2::and 
 
50
   (len 3 term)
 
51
   (equal (acl2::car term) 'acl2::cons)))
 
52
 
 
53
(defun syn::cons (a b)
 
54
  (declare (type t a b))
 
55
  `(acl2::cons ,a ,b))
 
56
 
 
57
(defun syn::car (term)
 
58
  (declare (type (satisfies syn::consp) term))
 
59
  (cadr term))
 
60
 
 
61
(defun syn::cdr (term)
 
62
  (declare (type (satisfies syn::consp) term))
 
63
  (caddr term))
 
64
 
 
65
(local
 
66
 (defthm cons-reconstruction
 
67
   (implies
 
68
    (syn::consp term)
 
69
    (equal (syn::cons (syn::car term) (syn::cdr term))
 
70
           term))))
 
71
 
 
72
(defun syn::quotep (term)
 
73
  (declare (type t term))
 
74
  (acl2::and (len 2 term)
 
75
             (equal (acl2::car term) 'acl2::quote)))
 
76
 
 
77
(defun syn::enquote (term)
 
78
  (declare (type t term))
 
79
  `(acl2::quote ,term))
 
80
 
 
81
(defun syn::dequote (term)
 
82
  (declare (type (satisfies syn::quotep) term))
 
83
  (cadr term))
 
84
 
 
85
(local
 
86
 (defthm quote-reconstruction
 
87
   (implies
 
88
    (syn::quotep term)
 
89
    (equal (syn::enquote (syn::dequote term))
 
90
           term))))
 
91
 
 
92
(defmacro syn::arg (n term)
 
93
  `(nth ,n ,term))
 
94
 
 
95
(defun syn::appendp (term)
 
96
  (declare (type t term))
 
97
  (acl2::and (syn::len 3 term)
 
98
             (equal (acl2::car term) 'binary-append)))
 
99
 
 
100
(defun syn::append (x y)
 
101
  (declare (type t x y))
 
102
  `(acl2::binary-append ,x ,y))
 
103
 
 
104
(local
 
105
 (defthm append-reconstruction
 
106
   (implies
 
107
    (syn::appendp term)
 
108
    (equal (syn::append (syn::arg 1 term) (syn::arg 2 term))
 
109
           term))))
 
110
 
 
111
(defun syn::ifp (term)
 
112
  (declare (type t term))
 
113
  (acl2::and (syn::len 4 term)
 
114
             (equal (acl2::car term) 'acl2::if)))
 
115
 
 
116
(defun syn::if (a b c)
 
117
  (declare (type t a b c))
 
118
  `(acl2::if ,a ,b ,c))
 
119
 
 
120
(local
 
121
 (defthm if-reconstruction
 
122
   (implies
 
123
    (syn::ifp term)
 
124
    (equal (syn::if (syn::arg 1 term) (syn::arg 2 term) (syn::arg 3 term))
 
125
           term))))
 
126
 
 
127
(defun syn::nil ()
 
128
  (declare (xargs :verify-guards t))
 
129
  `(syn::quote acl2::nil))
 
130
 
 
131
(defun syn::null (x)
 
132
  (declare (type t x))
 
133
  (equal x (syn::nil)))
 
134
 
 
135
(defun syn::true ()
 
136
  (declare (xargs :verify-guards t))
 
137
  `(syn::quote t))
 
138
 
 
139
(defun syn::conjoin (x y)
 
140
  (declare (type t x y))
 
141
  (acl2::cond
 
142
   ((acl2::not (acl2::and x y))
 
143
    acl2::nil)
 
144
   ((acl2::equal y (syn::true))
 
145
    x)
 
146
   ((acl2::equal x (syn::true))
 
147
    y)
 
148
   (acl2::t
 
149
    (syn::if x y (syn::nil)))))
 
150
 
 
151
(defun syn::and-fn (args)
 
152
  (declare (type t args))
 
153
  (acl2::if (acl2::consp args)
 
154
            `(syn::conjoin ,(acl2::car args) ,(syn::and-fn (acl2::cdr args)))
 
155
            `(syn::true)))
 
156
 
 
157
(defmacro syn::and (&rest args)
 
158
  (syn::and-fn args))
 
159
 
 
160
(defun syn::funcall (fn args term)
 
161
  (declare (type (integer 0 *) args))
 
162
  (acl2::and (syn::len (1+ args) term)
 
163
             (equal (acl2::car term) fn)))
 
164
 
 
165
(defmacro syn::apply (fn &rest args)
 
166
  `(list ',fn ,@args)) 
 
167
 
 
168
(defevaluator eval eval-list
 
169
  (
 
170
   (acl2::equal x y)
 
171
   (acl2::consp x)
 
172
   (acl2::cons x y)
 
173
   (acl2::binary-append x y)
 
174
   (acl2::if a b c)
 
175
   ))
 
176
 
 
177
(defmacro extend-eval (name fns)
 
178
  `(defevaluator ,name ,(symbol-fns::suffix name '-list)
 
179
     (
 
180
      (acl2::equal x y)
 
181
      (acl2::consp x)
 
182
      (acl2::cons x y)
 
183
      (acl2::binary-append x y)
 
184
      (acl2::if a b c)
 
185
      ,@fns
 
186
      )))
 
187
 
 
188
(defun syn::consp-rec (x)
 
189
  (declare (type t x))
 
190
  (cond
 
191
   ((syn::consp x) t)
 
192
   ((syn::appendp x)
 
193
    (or (syn::consp-rec (syn::arg 1 x))
 
194
        (syn::consp-rec (syn::arg 2 x))))
 
195
   ((syn::quotep x)
 
196
    (acl2::consp (syn::dequote x)))
 
197
   (t
 
198
    acl2::nil)))
 
199
 
 
200
(defthm consp-rec-implies-consp
 
201
  (implies
 
202
   (syn::consp-rec term)
 
203
   (acl2::consp (syn::eval term a))))
 
204
 
 
205
(defun free-var-bindings (w1 w2 term)
 
206
  (declare (type symbol w1 w2))
 
207
  (acl2::let ((list (symbol-fns::collect-variables term)))
 
208
    (symbol-fns::join-lists (symbol-fns::map-symbol-list-to-package list w1)
 
209
                            (symbol-fns::map-symbol-list-to-package list w2))))
 
210
 
 
211
(defmacro defevthm (ev name thm &rest key-args)
 
212
  `(defthm ,(symbol-fns::prefix ev '- name)
 
213
     ,thm
 
214
     :hints (("Goal" :use (:functional-instance 
 
215
                           (:instance ,name
 
216
                                      ,@(free-var-bindings name ev thm))
 
217
                           (syn::eval      ,ev)
 
218
                           (syn::eval-list ,(symbol-fns::suffix ev '-list)))))
 
219
     ,@key-args))
 
220
 
 
221
#+joe
 
222
(defevthm ev1 foo-bar
 
223
  (implies
 
224
   (and
 
225
    (pred a 1)
 
226
    (pred 2))
 
227
   (concl a b)))