← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/coi/bags/bind-free-rules.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/bags/bind-free-rules.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
(in-package "BAG")
7
32
 
8
33
(include-book "meta")
24
49
  (:REWRITE MEMBERSHIP-EXTRACTION-INSTANCE)
25
50
  ))
26
51
 
27
 
(in-theory 
28
 
 (disable 
 
52
(in-theory
 
53
 (disable
29
54
  (:REWRITE *TRIGGER*-UNIQUE-SUBBAGPS-IMPLIES-DISJOINTNESS)
30
55
  (:REWRITE *TRIGGER*-SUBBAGP-PAIR-DISJOINT) ;can we get rid of this then?
31
56
 ))
32
57
 
33
 
;we look through HYPS for a term of the form (subbagp x y) 
 
58
;we look through HYPS for a term of the form (subbagp x y)
34
59
;if such an item is found, we return (mv t y).  else, we return (mv nil nil)
35
60
;what if multple such things might be found?
36
61
(defun find-exact-subbagp-instance (x hyps)
64
89
  (if (consp hyps)
65
90
      (let ((entry (car hyps)))
66
91
        (let ((hit ;(not (subbagp term zed))
67
 
               (and 
 
92
               (and
68
93
                (consp entry)
69
94
                (equal (car entry) 'not)
70
95
                (consp (cdr entry))
73
98
                (consp (cdr (cadr entry)))
74
99
                (consp (cddr (cadr entry)))
75
100
                (let ((term (cadr (cadr entry)))
76
 
                      (zed (caddr (cadr entry)))) 
 
101
                      (zed (caddr (cadr entry))))
77
102
                  (and (syntax-subbagp-fn nil x term)
78
103
                       (cons term zed))))))
79
104
          (if hit
101
126
                      (and hit
102
127
                           (or (find-bounded-subbagp-path t   x1 hyps y hyps (1- n) (cons (cons x1 t) (cons (cons x0 nil) res)))
103
128
                               (find-bounded-subbagp-path nil x  nrh  y hyps (1- n) res))))))))))
104
 
  
 
129
 
105
130
(defun reverse-path (path res)
106
131
  (declare (type t path res))
107
132
  (if (consp path)
112
137
    res))
113
138
 
114
139
;what does this do?
115
 
;we look through HYPS for a term of the form (subbagp x BLAH) 
 
140
;we look through HYPS for a term of the form (subbagp x BLAH)
116
141
;if such an item is found, we test whether BLAH equals y.  else, we return nil
117
142
;what if multple such things might be found?
118
143
(defun subbagp-instance (x y hyps)
145
170
               nil))))))
146
171
 
147
172
 
148
 
;add guard?                  
 
173
;add guard?
149
174
(defun subbagp-chain (x xlist x0)
150
175
  (if (consp xlist)
151
176
      (and (if (cdar xlist) (hide-subbagp x (caar xlist)) (meta-subbagp x (caar xlist)))
154
179
        (hide-subbagp x x0)
155
180
      (meta-subbagp x x0))))
156
181
 
157
 
;add guard?                  
 
182
;add guard?
158
183
(defun subbagp-hyp (key x xlist y)
159
184
  (and key (subbagp-chain x xlist y)))
160
185
 
180
205
             (subbagp x z)))
181
206
 
182
207
  (defthmd tester2
183
 
    (implies (subbagp a x) 
 
208
    (implies (subbagp a x)
184
209
             (subbagp a (append x y))))
185
210
 
186
211
  ))
241
266
  (if (consp xlist)
242
267
      (let ((z0 (if (consp (car xlist)) (caar xlist) nil)))
243
268
        (met ((uni syntax) (find-unique-instance z0 hyps))
244
 
          (if uni 
 
269
          (if uni
245
270
              (if syntax
246
271
                  xlist
247
272
                (append `((,uni . nil) (,z0 . t)) (cdr xlist))) ;reversed since list still needs to be reversed
311
336
 
312
337
;; hide-unique is defined in meta as unique
313
338
 
314
 
;add guard?                  
 
339
;add guard?
315
340
(defun unique-chain (x xlist uni)
316
341
  (if (consp xlist)
317
342
      (and (if (cdar xlist) (hide-subbagp x (caar xlist)) (meta-subbagp x (caar xlist)));(subbagp x (car xlist))
322
347
      (and (meta-subbagp x uni)
323
348
           (hide-unique uni)))))
324
349
 
325
 
;add guard?                  
 
350
;add guard?
326
351
(defun unique-hyp (key x xlist uni)
327
352
  (and key (unique-chain x xlist uni)))
328
353
 
409
434
                              (list-whose-caars-are-pseudo-termsp ylist)
410
435
                              (pseudo-term-listp hyps))
411
436
                  ))
412
 
  
 
437
 
413
438
  (if (and (consp ylist)
414
439
           (consp (car ylist)))
415
440
      (met ((hit syn p q) (find-disjointness  x (caar ylist) hyps))
427
452
  (if (and (consp xlist)
428
453
           (consp (car xlist)))
429
454
      (met ((hit syn p q ylist2) (find-disjointness*  (caar xlist) ylist hyps))
430
 
           (if hit 
 
455
           (if hit
431
456
               (mv hit syn xlist ylist2 p q)
432
457
             (find-disjointness** (cdr xlist) ylist hyps)))
433
458
    (mv nil nil nil nil nil nil)))
434
459
 
435
 
;checks for subbagp paths up to disjoint 
 
460
;checks for subbagp paths up to disjoint
436
461
;argument for disjointness comes from a disjoint in hyps
437
462
(defun disjoint-disjointness (x y hyps)
438
463
  (declare (type t x hyps)
452
477
                     x0
453
478
                     (reverse-path newy '(quote t)) ;ylist
454
479
                     y0
455
 
                     `(quote ,syn) 
 
480
                     `(quote ,syn)
456
481
                     p
457
482
                     q)) ;z's are irrelevent in this argument
458
483
;but use z positions for subbagp-pair type argument
625
650
      (let ((xlist (revlist xlist nil))
626
651
            (ylist (revlist ylist nil)))               ; smallest to largest
627
652
        (met ((xlist ylist zlist) (find-shared-ancestor xlist ylist nil)) ; x/y largest to smallest
628
 
             
629
 
             (let ((newzlist (find-unique-instance-list (revlist zlist nil) hyps))) 
 
653
 
 
654
             (let ((newzlist (find-unique-instance-list (revlist zlist nil) hyps)))
630
655
               ;; newzlist path from something unique down subbagps
631
656
               (met ((hit newxlist x0 newylist y0 z zlist z0) (find-unique-subbagp** xlist ylist newzlist hyps))
632
657
                    (mv hit (reverse-path newxlist '(quote t))
657
682
                  )
658
683
           (ignore state))
659
684
  (let ((hyps (mfc-clause mfc)))
660
 
    (and (or flg 
 
685
    (and (or flg
661
686
             t
662
687
             (mfc-ancestors mfc) ;bzo why are we doing these checks?
663
688
             (in-clause-disjoint x y hyps)
664
689
             )
665
 
         (met ((hit xlist* x0* ylist* y0* z* zlist* z0*) (unique-disjointness x y hyps)) 
 
690
         (met ((hit xlist* x0* ylist* y0* z* zlist* z0*) (unique-disjointness x y hyps))
666
691
              (if hit
667
692
                  `((,key . (quote :unique))
668
693
                    (,xlist . ,xlist*)
689
714
  (subbagp-pair x y x y)
690
715
  :hints (("goal" :in-theory (enable subbagp-pair))))
691
716
 
692
 
;add guard?                  
 
717
;add guard?
693
718
(defun unique-subbagp-chain (x0 y0 z zlist z0)
694
719
  (and (unique-subbagps x0 y0 z)
695
720
       (unique-chain z zlist z0)))
696
721
 
697
 
;add guard?                  
 
722
;add guard?
698
723
(defun disjoint-hyp (key x xlist x0 y ylist y0 z-syn zlist-p z0-q)
699
724
  (cond
700
725
   ((equal key ':disjoint)
776
801
   :rule-classes :forward-chaining)
777
802
 
778
803
 (defthm disjoint-computation
779
 
   (implies (and (bind-free (bind-disjoint-argument nil 'key 'xlist 'x0 'ylist 'y0 'z 'zlist 'z0 x y mfc state) 
 
804
   (implies (and (bind-free (bind-disjoint-argument nil 'key 'xlist 'x0 'ylist 'y0 'z 'zlist 'z0 x y mfc state)
780
805
                            (key xlist x0 ylist y0 z zlist z0))
781
806
                 (disjoint-hyp key x xlist x0 y ylist y0 z zlist z0))
782
807
            (disjoint x y))
869
894
                 (consp (cdr (cadr entry)))
870
895
                 (consp (cddr (cadr entry)))
871
896
                 (equal (cadr (cadr entry)) x))
872
 
            (find-memberp-instance-list x (cdr clause) 
 
897
            (find-memberp-instance-list x (cdr clause)
873
898
                                       (cons (caddr (car (cdr entry))) res))
874
899
          (find-memberp-instance-list x (cdr clause) res)))
875
900
    res))
897
922
                (PSEUDO-TERM-LISTP res)
898
923
                )
899
924
           (PSEUDO-TERM-LISTP (FIND-MEMBERP-INSTANCE-LIST x clause res))))
900
 
 
 
925
 
901
926
(defun memberp-membership (x y hyps)
902
927
  (declare (type t x y hyps)
903
928
           (xargs :guard (and (pseudo-termp x)
907
932
  (let ((x0list (find-memberp-instance-list x hyps nil)))
908
933
    (met ((hit x0 path) (find-memberp-subbagp-list x0list y hyps))
909
934
         (mv hit x0 path))))
910
 
        
 
935
 
911
936
(defun in-hyps-memberp (x y hyps)
912
937
  (declare (type t x y hyps))
913
938
  (if (consp hyps)
942
967
                    (,x0 . ,val)
943
968
                    (,xlist . ,list))
944
969
                nil)))))
945
 
         
946
 
 
947
 
;add guard?                  
 
970
 
 
971
 
 
972
;add guard?
948
973
(defun memberp-hyp (key x x0 xlist y)
949
974
  (and key
950
975
       (hide-memberp x x0)
953
978
(defthm memberp-computation
954
979
  (implies
955
980
   (and
956
 
    (bind-free (bind-memberp-argument 'key 'xlist 'x0 x y mfc state) 
 
981
    (bind-free (bind-memberp-argument 'key 'xlist 'x0 x y mfc state)
957
982
               (key x0 xlist))
958
983
    (memberp-hyp key x x0 xlist y)
959
984
    )
975
1000
 
976
1001
 (local
977
1002
  (defthmd memberp-test1
978
 
    (implies (and (memberp x z) 
979
 
                  (subbagp z w) 
980
 
                  (subbagp w y)) 
 
1003
    (implies (and (memberp x z)
 
1004
                  (subbagp z w)
 
1005
                  (subbagp w y))
981
1006
             (memberp x y))))
982
1007
 
983
1008
 
1030
1055
                  ))
1031
1056
  (if (consp memlist)
1032
1057
      (let ((x* (car memlist)))
1033
 
        (let ((disjoint-arg 
 
1058
        (let ((disjoint-arg
1034
1059
               (bind-disjoint-argument t 'key 'xlist 'x0 'ylist 'y0 'z 'zlist 'z0 x* y mfc state)))
1035
1060
          (if disjoint-arg
1036
1061
              (mv t x* disjoint-arg)
1064
1089
                              (,x* . ,x*1))
1065
1090
                            disjoint-arg)
1066
1091
                  nil))))))
1067
 
               
1068
 
;add guard?                  
 
1092
 
 
1093
;add guard?
1069
1094
(defun non-memberp-hyp (hit x* key x xlist x0 y ylist y0 z zlist z0)
1070
1095
  (and hit
1071
1096
       (hide-memberp x x*)
1072
1097
       (disjoint-hyp key x* xlist x0 y ylist y0 z zlist z0)))
1073
 
  
 
1098
 
1074
1099
(defthm non-memberp-computation
1075
1100
  (implies
1076
1101
   (and
1104
1129
                  (disjoint m v)
1105
1130
                  (disjoint i o)
1106
1131
                  )
1107
 
             (not (memberp a p))))) 
 
1132
             (not (memberp a p)))))
1108
1133
 )
1109
1134
 
1110
1135
 
1176
1201
                 (,val   . ,(cdr x)))))))))
1177
1202
 
1178
1203
(defmacro bind-remove-bag-instance (y z which val)
1179
 
  `(bind-free (bind-remove-bag-instance-fn ,y ,z (quote ,which) (quote ,val) mfc state) 
 
1204
  `(bind-free (bind-remove-bag-instance-fn ,y ,z (quote ,which) (quote ,val) mfc state)
1180
1205
              (,which ,val)))
1181
1206
 
1182
 
;add guard?                  
 
1207
;add guard?
1183
1208
(defun disjoint-other-hyp (which x y z)
1184
1209
  (if which
1185
1210
      (disjoint (append x (remove-bag x y))
1186
1211
                z)
1187
1212
    (disjoint (append x (remove-bag x z)) y)))
1188
 
   
 
1213
 
1189
1214
(defthm disjoint-other-memberp
1190
1215
  (implies (and (bind-remove-bag-instance y z which x)
1191
1216
                (disjoint-other-hyp which x y z))
1192
1217
           (disjoint y z)))
1193
1218
 
1194
 
;add guard?                  
 
1219
;add guard?
1195
1220
(defun collect-list (term)
1196
1221
  (if (and (consp term)
1197
1222
           (equal (car term) 'remove-1))
1199
1224
             ,(collect-list (caddr term)))
1200
1225
    `(quote nil)))
1201
1226
 
1202
 
;add guard?                  
 
1227
;add guard?
1203
1228
(defun collect-rest (term)
1204
1229
  (if (and (consp term)
1205
1230
           (equal (car term) 'remove-1))
1206
1231
      (collect-rest (caddr term))
1207
1232
    term))
1208
1233
 
1209
 
;add guard?                  
 
1234
;add guard?
1210
1235
(defun bind-list (list rest term)
1211
1236
  `((,list . ,(collect-list term))
1212
1237
    (,rest . ,(collect-rest term))))
1243
1268
        (if (equal 'binary-append (car term))
1244
1269
            (if (consp (caddr term))
1245
1270
                (if (and ;(consp (cdr term))
1246
 
                 
 
1271
 
1247
1272
                     (equal 'binary-append (car (caddr term)))
1248
1273
    ;(consp (cdaddr term))
1249
1274
                     (equal (cadr term)
1255
1280
                nil))
1256
1281
          nil))
1257
1282
    nil))
1258
 
  
 
1283
 
1259
1284
(defun bind-x-to-repeated-subbag (term)
1260
1285
  (declare (xargs :guard (pseudo-termp term)))
1261
1286
  (let* ((bag (find-repeated-subbag term)))
1286
1311
;; Test it out...
1287
1312
(local
1288
1313
 (defthm test-of-show-not-unique-1
1289
 
   (implies (consp x) 
1290
 
            (not (bag::unique (append x x y))))))
 
1314
   (implies (consp x)
 
1315
            (not (bag::unique (append x x y))))))
 
 
b'\\ No newline at end of file'