← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/coi/records/mem-domain.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/records/mem-domain.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 "ACL2")
7
32
 
8
33
;; What we want to do is export the primary theories here into
65
90
          nil)
66
91
      (set::union (cons-onto-all '0 (mem::domain-aux (car mem-tree) (+ -1 depth)))
67
92
                  (cons-onto-all '1 (mem::domain-aux (cdr mem-tree) (+ -1 depth)))))))
68
 
  
 
93
 
69
94
 
70
95
;this bits are in reverse order (least significant bit comes first in the list)
71
96
(defun convert-reversed-bit-list-to-integer (bit-list)
74
99
    (+ (car bit-list)
75
100
       (* 2 (convert-reversed-bit-list-to-integer (cdr bit-list))))))
76
101
 
77
 
;; (defmacro def-set-processor (&key (processor-name 'unsupplied) 
 
102
;; (defmacro def-set-processor (&key (processor-name 'unsupplied)
78
103
;;                                   (element-processor 'unsupplied)  ;can this be a term?
79
104
;;                                   (predicate 'unsupplied))
80
105
;;   `(defun ,processor-name (set) ;can this take more than one arg?
109
134
                          (lambda (x) (convert-reversed-bit-lists-to-integers x))))
110
135
                        (a lst)
111
136
                        (x lst-of-lsts)
112
 
                 
 
137
 
113
138
                        ))))
114
 
  
 
139
 
115
140
(defun mem::mem-tree-domain (mem-tree depth)
116
141
  (convert-reversed-bit-lists-to-integers (mem::domain-aux mem-tree depth)))
117
142
 
135
160
                ;;always return nats less than size?  Not necessarily.  There
136
161
                ;;may be nats less than 2^depth but greater than size.  We
137
162
                ;;have to filter them out.
138
 
                
 
163
 
139
164
                (SET::FILTER<not-NATP-LESS-THAN-SIZE> (set::rkeys record-part) size)
140
165
                )))
141
166
 
165
190
(encapsulate
166
191
 ()
167
192
 (local (include-book "data-structures/memories/memory-impl" :dir :system))
168
 
 
 
193
 
169
194
 ;;dup
170
195
 (defthm mem::_store-memory
171
196
   (mem::_memory-p (mem::_store mem::addr mem::elem mem::mem))
172
197
   :hints(("Goal" :in-theory (enable mem::_memory-p))))
173
 
 
 
198
 
174
199
 (defthm mem::_store-memory-main
175
200
   (equal (mem::memory-p (mem::_store mem::addr mem::elem mem::mem))
176
201
          (mem::memory-p mem::mem)))
177
 
 
 
202
 
178
203
 (defthm mem::_memtree-store-memtree-2
179
204
   (mem::_memtree-p (mem::_memtree-store-nil mem::addr mem::mtree mem::depth) mem::depth)
180
 
   :hints(("Goal"))) 
 
205
   :hints(("Goal")))
181
206
 
182
207
 )
183
208
 
201
226
   :hints (("Goal" :in-theory (enable MEM::|_ADDRESS-P| EXPT-SPLIT))))
202
227
 
203
228
    ;what should we do with 0?
204
 
    ;we could also represent 0 with the bit-list nil, but consider (mem::domain (mem::store 0 4 (mem::new 4))) = '(0) 
 
229
    ;we could also represent 0 with the bit-list nil, but consider (mem::domain (mem::store 0 4 (mem::new 4))) = '(0)
205
230
    ;len is the lenght of the bit list.  we need it. consider whether 0 should be '(0) or '(0 0) of '(0 0 0), etc.
206
231
 (defun convert-integer-to-reversed-bit-list (n len)
207
232
   (if (zp len)
208
233
       nil ;the empty bit list
209
234
     (cons (mod n 2)
210
235
           (convert-integer-to-reversed-bit-list (floor n 2) (+ -1 len)))))
211
 
 
 
236
 
212
237
 (defthm mod-by-2-cases
213
238
   (implies (and (not (EQUAL 0 (MOD ADDR 2)))
214
239
                 (integerp addr))
215
 
            (EQUAL (MOD ADDR 2) 
 
240
            (EQUAL (MOD ADDR 2)
216
241
                   1))
217
242
   :hints (("Goal" :cases ((integerp addr))
218
243
            :in-theory (enable mod-by-2))))
220
245
 (defthm floor-non-negative-hack
221
246
   (implies (<= 0 x)
222
247
            (not (< (FLOOR x 2) 0))))
223
 
 
 
248
 
224
249
 (defthm floor-hack
225
250
   (implies (< ADDR (* 2 (EXPT 2 (+ -1 DEPTH))))
226
251
            (< (FLOOR ADDR 2)
232
257
                   A))
233
258
   :hints (("Goal" :use (:instance mod-fl-2 (x a) (y 2)))))
234
259
 
235
 
 
236
 
 
 
260
 
 
261
 
237
262
 )
238
263
 
239
264
 
249
274
                          (lambda (x) (cons-onto-all item x))))
250
275
                        (a lst)
251
276
                        (x lst-of-lsts)
252
 
                 
 
277
 
253
278
                        ))))
254
279
 
255
280
 
303
328
                                    MEM::|_ADDRESS-FIX|)
304
329
          :do-not '(generalize eliminate-destructors)
305
330
          :EXPAND ((MEM::|_MEMTREE-STORE| ADDR ELEM NIL DEPTH)))))
306
 
        
 
331
 
307
332
 
308
333
 
309
334
 
334
359
                              MEM::|_ADDRESS-P|
335
360
                              MEM::|_MEMTREE-FIX|
336
361
    ;MEM::|_MEMTREE-P|
337
 
                              MEM::|_ADDRESS-FIX|) 
 
362
                              MEM::|_ADDRESS-FIX|)
338
363
                           (;LIST::EQUAL-CONS-CASES ;bzo why?
339
364
                            )))))
340
365
 
389
414
 
390
415
;bzo drop?
391
416
       (if (equal 1 (cadr mem)) ;log2 on 0 is weird, so we handle this case specially
392
 
           (equal 1 (caddr mem))        
 
417
           (equal 1 (caddr mem))
393
418
         (equal (mem::|_LOG2| (+ -1 (cadr mem)))
394
419
                (caddr mem)))))
395
420
 
413
438
                   (lambda (x) (SET::FILTER<NOT-NATP-LESS-THAN-SIZE> x size))))
414
439
                 (a a)
415
440
                 (x x)
416
 
                 
 
441
 
417
442
                 ))))
418
443
 
419
444
(defthm FILTER<NATP-LESS-THAN-SIZE>-of-insert
433
458
                          (lambda (x) (SET::FILTER<NATP-LESS-THAN-SIZE> x size))))
434
459
                        (a a)
435
460
                        (x x)
436
 
                 
 
461
 
437
462
                        ))))
438
 
          
 
463
 
439
464
(defthm domain-of-store-v-non-nil
440
465
  (implies (and ;(MEM::MEMORY-P mem)
441
466
;(WFR (CDDDR MEM))
451
476
                              MEM::|_ADDRESS-P|
452
477
                              MEM::SIZE
453
478
                              MEM::STORE MEM::|_STORE|
454
 
                              MEM::|_FROM-MEM| 
 
479
                              MEM::|_FROM-MEM|
455
480
                              MEM::|_BAD-MEMORY-P|
456
481
                              MEM::|_MEMORY-P|
457
482
                              MEM::|_MEMORY-MTREE|
461
486
                              MEM::|_MEMORY-FAST|
462
487
                              MEM::|_MEMORY-SIZE|
463
488
                              MEM::|_MEMORY-RECORD|
464
 
                              
465
 
                              ) 
466
 
                           (SET::DOUBLE-CONTAINMENT
 
489
 
 
490
                              )
 
491
                           (SET::DOUBLE-CONTAINMENT-expensive
467
492
                            )))))
468
493
 
469
494
;show how s affects this...
470
495
 
471
496
;for typed records gotta unwrap the domain...
472
497
 
473
 
(in-theory (disable mem::domain)) ;move back               
 
498
(in-theory (disable mem::domain)) ;move back
474
499
 
475
500
;bzo add to sets library
476
501
(defthm delete-of-insert-diff
560
585
;;     (and (equal len (len (set::head x)))
561
586
;;          (all-have-len len (set::tail x)))))
562
587
 
563
 
(defun len-equal (a len) 
 
588
(defun len-equal (a len)
564
589
  (declare (xargs :guard t))
565
590
  (equal (len a) (rfix len)))
566
 
  
 
591
 
567
592
(set::quantify-predicate (len-equal a len))
568
593
 
569
594
 
680
705
  (implies (and (not (natp a))
681
706
                (force (set::all<bit-listp> bit-lists)))
682
707
           (not (set::in a (convert-reversed-bit-lists-to-integers bit-lists))))
683
 
  :hints (("Goal" :in-theory (enable SET::ALL<BIT-LISTP> 
 
708
  :hints (("Goal" :in-theory (enable SET::ALL<BIT-LISTP>
684
709
                                     )
685
710
           :do-not '(generalize eliminate-destructors))))
686
711
 
772
797
   (NOT
773
798
    (SET::IN (CONVERT-REVERSED-BIT-LIST-TO-INTEGER a)
774
799
             (CONVERT-REVERSED-BIT-LISTS-TO-INTEGERS x))))
775
 
  :hints (("Goal" :in-theory (enable set::in 
 
800
  :hints (("Goal" :in-theory (enable set::in
776
801
                                     )
777
802
           :do-not '(generalize eliminate-destructors))))
778
803
 
871
896
(defthm all-bit-listp-of-domain-aux
872
897
  (set::all<bit-listp> (mem::domain-aux tree depth))
873
898
    :hints (("Goal" :in-theory (enable mem::domain-aux acl2::equal-booleans-reducton))))
874
 
;; LIST::EQUAL-OF-BOOLEANS-REWRITE 
 
899
;; LIST::EQUAL-OF-BOOLEANS-REWRITE
875
900
 
876
901
(defthm setp-of-domain-aux
877
902
  (set::setp (mem::domain-aux tree depth))
923
948
                                                (CAR (CDR (CDR MEM))))))
924
949
           :do-not '(generalize eliminate-destructors)
925
950
           :in-theory (e/d (set::delete-of-union-push-into-both
926
 
                              
 
951
 
927
952
                            good-memoryp
928
953
                            MEM::DOMAIN
929
954
                            MEM::|_ADDRESS-P|
930
955
                            MEM::SIZE
931
956
                            MEM::STORE MEM::|_STORE|
932
 
                            MEM::|_FROM-MEM| 
 
957
                            MEM::|_FROM-MEM|
933
958
                            MEM::|_BAD-MEMORY-P|
934
959
                            MEM::|_MEMORY-P|
935
960
                            MEM::|_MEMORY-MTREE|
939
964
                            MEM::|_MEMORY-FAST|
940
965
                            MEM::|_MEMORY-SIZE|
941
966
                            MEM::|_MEMORY-RECORD|
942
 
                            ) 
943
 
                           (SET::DOUBLE-CONTAINMENT
 
967
                            )
 
968
                           (SET::DOUBLE-CONTAINMENT-expensive
944
969
                            SET::UNION-DELETE-y
945
970
                            SET::UNION-DELETE-x)))))
946
971
 
965
990
  (equal (mem::domain (mem::new size))
966
991
         nil)
967
992
  :hints (("Goal" :in-theory (enable MEM::DOMAIN-AUX
968
 
                                     mem::new 
 
993
                                     mem::new
969
994
                                     mem::domain
970
995
                                     mem::mem-tree-domain))))
971
996
 
1158
1183
                               MEM::|_MEMORY-P|
1159
1184
                               )))))
1160
1185
 
1161
 
(in-theory (disable MEM::MEM-TREE-DOMAIN))                             
 
1186
(in-theory (disable MEM::MEM-TREE-DOMAIN))
1162
1187
 
1163
1188
(defthm mem-tree-domain-after-store
1164
1189
  (implies (good-memoryp mem)
1165
1190
           (equal (MEM::MEM-TREE-DOMAIN (CAAR (MEM::STORE A V MEM))
1166
 
                                        (CADDR ;(MEM::STORE A V 
 
1191
                                        (CADDR ;(MEM::STORE A V
1167
1192
                                         MEM
1168
1193
                                         ;)
1169
1194
                                         ))
1180
1205
;           :use (:instance domain-of-store) ;gross way to prove this...
1181
1206
           :cases ((SET::EMPTY (MEM::DOMAIN-AUX (CAR (CAR MEM))
1182
1207
                                                      (CAR (CDR (CDR MEM))))))
1183
 
           
 
1208
 
1184
1209
           :in-theory (e/d (MEM::DOMAIN
1185
 
                            
 
1210
 
1186
1211
                            MEM::MEM-TREE-DOMAIN
1187
1212
                            MEM::STORE
1188
1213
                            MEM::MEMORY-P
1199
1224
                            MEM::|_MEMORY-FIX|
1200
1225
                            GOOD-MEMORYP
1201
1226
                            MEM::|_MEMORY-RECORD|
1202
 
                            ) 
1203
 
                           (domain-of-store)))))            
 
1227
                            )
 
1228
                           (domain-of-store)))))
1204
1229
 
1205
1230
 
1206
1231
(local (in-theory (disable SIGNED-BYTE-P)))
1244
1269
(defthm good-memoryp-of-clear
1245
1270
  (implies (acl2::good-memoryp mem)
1246
1271
           (acl2::good-memoryp (mem::clear addr mem)))
1247
 
  :hints (("Goal" :in-theory (enable mem::clear))))
1248
 
 
 
1272
  :hints (("Goal" :in-theory (enable mem::clear))))
 
 
b'\\ No newline at end of file'