← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/coi/dtrees/royalp.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/coi/dtrees/royalp.lisp
1
 
#|-*-Lisp-*-=================================================================|#
2
 
#|                                                                           |#
3
 
#| coi: Computational Object Inference                                       |#
4
 
#|                                                                           |#
5
 
#|===========================================================================|#
 
1
; Computational Object Inference
 
2
; Copyright (C) 2005-2014 Kookamara LLC
 
3
;
 
4
; Contact:
 
5
;
 
6
;   Kookamara LLC
 
7
;   11410 Windermere Meadows
 
8
;   Austin, TX 78759, USA
 
9
;   http://www.kookamara.com/
 
10
;
 
11
; License: (An MIT/X11-style license)
 
12
;
 
13
;   Permission is hereby granted, free of charge, to any person obtaining a
 
14
;   copy of this software and associated documentation files (the "Software"),
 
15
;   to deal in the Software without restriction, including without limitation
 
16
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
17
;   and/or sell copies of the Software, and to permit persons to whom the
 
18
;   Software is furnished to do so, subject to the following conditions:
 
19
;
 
20
;   The above copyright notice and this permission notice shall be included in
 
21
;   all copies or substantial portions of the Software.
 
22
;
 
23
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
24
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
25
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
26
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
27
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
28
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
29
;   DEALINGS IN THE SOFTWARE.
 
30
 
6
31
;;
7
32
;; Dependency Trees for Data Dependency Analysis
8
 
;; Jared Davis 
 
33
;; Jared Davis
9
34
;;
10
35
;;
11
36
;; INTRODUCTION
15
40
;;
16
41
;;   (1) p is in the dtree, i.e., (in p dtree)
17
42
;;
18
 
;;   (2) the localdeps of p are nonempty, i.e., 
 
43
;;   (2) the localdeps of p are nonempty, i.e.,
19
44
;;        (not (set::empty (localdeps (get p dtree))))
20
45
;;
21
46
;;   (3) for all a, the following is true:
94
119
  (implies (royalp path dtree)
95
120
           (equal (set::empty (deps dtree))
96
121
                  nil))
97
 
  :hints(("Goal" 
 
122
  :hints(("Goal"
98
123
          :in-theory (disable empty-of-deps-when-nonempty-of-localdeps-of-get)
99
124
          :use (:instance empty-of-deps-when-nonempty-of-localdeps-of-get))))
100
125
 
139
164
 
140
165
  (defthmd royalp-constraint-localdeps
141
166
    (implies (royalp-hyps)
142
 
             (not (set::empty 
 
167
             (not (set::empty
143
168
                   (localdeps (get (royalp-path) (royalp-dtree)))))))
144
169
 
145
170
  (defthmd royalp-constraint-domination
149
174
             (set::empty (localdeps (get royalp-member (royalp-dtree)))))))
150
175
 
151
176
 ;; Suppose that (royalp-hyps) is true, that our constraints are true, and
152
 
 ;; suppose towards contradiction that the following is true: 
 
177
 ;; suppose towards contradiction that the following is true:
153
178
 ;;  (not (royalp (royalp-path) (royalp-dtree)))
154
179
 
155
180
 ;; Now, since the domination constraint is true for any royalp-member, it is
167
192
                                  (map::get (car path) (children dtree))))
168
193
              nil))))
169
194
 
170
 
 ;; To generate our contradiction, we will need to show that the hypotheses in 
 
195
 ;; To generate our contradiction, we will need to show that the hypotheses in
171
196
 ;; our constraints are satisifed.  Of course, the hypothesis for the localdeps
172
 
 ;; constraint is trivial, since we assumed (royalp-hyps) is true.  For the 
 
197
 ;; constraint is trivial, since we assumed (royalp-hyps) is true.  For the
173
198
 ;; domination constraint, this also relieves the first hypothesis.
174
199
 
175
200
 ;; The second hypothesis of the domination constraint can be shown using a
190
215
          (and (set::empty (localdeps dtree))
191
216
               (or (atom path)
192
217
                   (and (map::in (car path) (children dtree))
193
 
                        (voidp (cdr path) 
 
218
                        (voidp (cdr path)
194
219
                               (map::get (car path) (children dtree))))))))
195
220
 
196
221
 ;; We observe that no royal path is ever void:
230
255
                          (not (voidp path dtree))))
231
256
          :hints(("Goal" :in-theory (enable path::strictly-dominates)
232
257
                  :use find-royal-does-nothing))))
233
 
        
234
 
 ;; Here is how we argue that the final hypothesis is true.  Since we assumed 
 
258
 
 
259
 ;; Here is how we argue that the final hypothesis is true.  Since we assumed
235
260
 ;; (towards contradiction) that (not (royalp (royalp-path) (royalp-dtree))),
236
 
 ;; then we know that 
 
261
 ;; then we know that
237
262
 ;;  (path::strictly-dominates (find-royal (royalp-path) (royalp-dtree))
238
263
 ;;                            (royalp-path))
239
264
 ;; exactly when (not (voidp (royalp-path) (royalp-dtree))).  But by our
244
269
 
245
270
 (local (defthm localdeps-of-find-royal-nonempty-when-input-nonempty
246
271
          (implies (not (set::empty (localdeps (get path dtree))))
247
 
                   (not (set::empty (localdeps 
 
272
                   (not (set::empty (localdeps
248
273
                                     (get (find-royal path dtree) dtree)))))
249
274
          :hints(("Goal" :in-theory (enable find-royal get)))))
250
275
 
251
276
 (defthm royalp-by-membership-driver
252
277
   (implies (royalp-hyps)
253
278
            (royalp (royalp-path) (royalp-dtree)))
254
 
   :hints(("Goal" 
 
279
   :hints(("Goal"
255
280
           :use ((:instance royalp-constraint-localdeps)
256
281
                 (:instance royalp-constraint-domination
257
282
                            (royalp-member
260
285
 (defadvice royalp-by-membership
261
286
   (implies (royalp-hyps)
262
287
            (royalp (royalp-path) (royalp-dtree)))
263
 
   :rule-classes (:pick-a-point :driver royalp-by-membership-driver))          
 
288
   :rule-classes (:pick-a-point :driver royalp-by-membership-driver))
264
289
 
265
290
 )
266
291
 
296
321
  (equal (set::in path (royaldomain1 paths dtree))
297
322
         (and (set::in path paths)
298
323
              (royalp path dtree)))
299
 
  :hints(("Goal" :in-theory (e/d (royaldomain1) 
 
324
  :hints(("Goal" :in-theory (e/d (royaldomain1)
300
325
                                 (set::in)))))
301
326
 
302
327
(verify-guards royaldomain1)
311
336
(defthm listsetp-of-royaldomain
312
337
  (set::listsetp (royaldomain dtree))
313
338
  :hints(("Goal" :in-theory (enable royaldomain))))
314
 
       
 
339
 
315
340
(defthm in-royaldomain
316
341
  (equal (set::in path (royaldomain dtree))
317
342
         (and (in path dtree)
318
343
              (royalp path dtree)
319
344
              (true-listp path)))
320
 
  :hints(("Goal" :in-theory (enable royaldomain))))
 
345
  :hints(("Goal" :in-theory (enable royaldomain))))
 
 
b'\\ No newline at end of file'