← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/coi/records/records-definitions.lsp

  • 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/records-definitions.lsp
 
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
 
1
31
; Jared: what's this file for?  It's not certifiable, so I'm
2
32
; renaming it to a .lsp extension for Make compatibility
3
33
 
10
40
;(in-package "RECORDS")
11
41
 
12
42
;;
13
 
;; This file isolates records definitions and types. The file currently 
 
43
;; This file isolates records definitions and types. The file currently
14
44
;; contains the following ACL2 constructs as they occur in the records book:
15
45
;; - defun
16
46
;; - defund
22
52
 
23
53
; For write tests we will just zero out a block of memory.  It doesn't really
24
54
; matter what addresses we use, because they're all the same depth from the
25
 
; root.  For read tests, we'll just sequentially scan a block of memory. 
 
55
; root.  For read tests, we'll just sequentially scan a block of memory.
26
56
 
27
57
(defun zero-memory (i mem)
28
58
  (declare (xargs :guard (and (memory-p mem)
29
59
                              (address-p i mem)))
30
 
           (type (signed-byte 29) i))                              
 
60
           (type (signed-byte 29) i))
31
61
  (if (mbe :logic (zp i)
32
62
           :exec (= i 0))
33
63
      (store 0 0 mem)
44
74
    (let ((element (load i mem)))
45
75
      (declare (ignore element))
46
76
      (scan-memory (the-fixnum (1- i)) mem))))
47
 
                  
 
77
 
48
78
(local (defthm signed-byte-natural
49
79
         (implies (force (natp x))
50
80
                  (equal (signed-byte-p 29 x)
81
111
  (if (mbt (_memtree-p mtree depth))
82
112
      mtree
83
113
    nil))
84
 
  
 
114
 
85
115
(defthm _memtree-fix-memtree
86
116
  (_memtree-p (_memtree-fix mtree depth) depth))
87
117
 
145
175
  (and (integerp (_address-fix addr depth))
146
176
       (<= 0 (_address-fix addr depth)))
147
177
  :rule-classes :type-prescription)
148
 
                      
 
178
 
149
179
(in-theory (disable _address-fix _memtree-fix))
150
180
 
151
181
(defthm _address-floor-2
201
231
  (mbe :logic (_memtree-load addr mtree depth)
202
232
       :exec (if (= depth 0)
203
233
                 mtree
204
 
               (_fix-addr/depth-memtree-load 
 
234
               (_fix-addr/depth-memtree-load
205
235
                (the-fixnum (ash addr -1))
206
236
                (if (= (the-fixnum (logand addr 1)) 0)
207
237
                    (car mtree)
236
266
 
237
267
 
238
268
; We now provide a store function.  I think this definition is pretty standard
239
 
; following from the definition of load.  
 
269
; following from the definition of load.
240
270
;
241
271
; One interesting aspect is that we require that our element is non-nil.  This
242
272
; is because we would really like to keep our trees in a canonical form, where
243
273
; "nil" elements are not even stored, and paths to them are not created.  But,
244
 
; this function would not preserve this property if we gave it "nil" to store. 
 
274
; this function would not preserve this property if we gave it "nil" to store.
245
275
; For example, (_memtree-store 0 nil nil 2) = ((nil)) instead of nil, violating
246
 
; our notion of canonicality.  Indeed, this creates problems when we try to 
 
276
; our notion of canonicality.  Indeed, this creates problems when we try to
247
277
; prove properties of the form (store addr (load addr mem) mem) = mem.
248
278
;
249
279
; To address this, we actually provide a separate function below,
266
296
            (cons (_memtree-store quotient elem (car mtree) (1- depth))
267
297
                  (cdr mtree))
268
298
          (cons (car mtree)
269
 
                (_memtree-store quotient elem (cdr mtree) 
 
299
                (_memtree-store quotient elem (cdr mtree)
270
300
                                (1- depth))))))))
271
301
 
272
302
; As with loading, we create an efficient version that assumes addr and depth
284
314
                 elem
285
315
               (let ((quotient (the-fixnum (ash addr -1))))
286
316
                 (if (= (the-fixnum (logand addr 1)) 0)
287
 
                     (cons (_fix-addr/depth-memtree-store 
 
317
                     (cons (_fix-addr/depth-memtree-store
288
318
                            quotient elem (car mtree) (the-fixnum (1- depth)))
289
319
                           (cdr mtree))
290
320
                   (cons (car mtree)
291
 
                         (_fix-addr/depth-memtree-store 
292
 
                          quotient elem (cdr mtree) 
 
321
                         (_fix-addr/depth-memtree-store
 
322
                          quotient elem (cdr mtree)
293
323
                          (the-fixnum (1- depth)))))))))
294
324
 
295
325
; And as before, we create a "self-optimizing" version which drops the
306
336
                 (_fix-addr/depth-memtree-store addr elem mtree depth)
307
337
               (let ((quotient (ash addr -1)))
308
338
                 (if (= (the-fixnum (logand addr 1)) 0)
309
 
                     (cons (_fixnum-memtree-store 
 
339
                     (cons (_fixnum-memtree-store
310
340
                            quotient elem (car mtree) (the-fixnum (1- depth)))
311
341
                           (cdr mtree))
312
342
                   (cons (car mtree)
313
 
                         (_fixnum-memtree-store 
314
 
                          quotient elem (cdr mtree) 
 
343
                         (_fixnum-memtree-store
 
344
                          quotient elem (cdr mtree)
315
345
                          (the-fixnum (1- depth)))))))))
316
346
 
317
347
 
318
 
; Now we are ready to implement "memory erasing", that is, storing nils into 
 
348
; Now we are ready to implement "memory erasing", that is, storing nils into
319
349
; our memory.  We want to keep our trees in canonical format, so we go to some
320
350
; lengths to eliminate branches that are no longer needed.
321
351
 
331
361
      (if (atom mtree)
332
362
          nil
333
363
        (let ((quotient (floor addr 2)))
334
 
          (if (= (mod addr 2) 0)              
335
 
              (let ((left (_memtree-store-nil quotient (car mtree) 
 
364
          (if (= (mod addr 2) 0)
 
365
              (let ((left (_memtree-store-nil quotient (car mtree)
336
366
                                              (1- depth)))
337
367
                    (right (cdr mtree)))
338
368
                (if (and (null left) (null right)) ; canonicalize away!
357
387
                   nil
358
388
                 (let ((quotient (the-fixnum (ash addr -1))))
359
389
                   (if (= (the-fixnum (logand addr 1)) 0)
360
 
                       (let ((left (_fix-addr/depth-memtree-store-nil 
361
 
                                    quotient (car mtree) 
 
390
                       (let ((left (_fix-addr/depth-memtree-store-nil
 
391
                                    quotient (car mtree)
362
392
                                    (the-fixnum (1- depth))))
363
393
                             (right (cdr mtree)))
364
394
                         (if (and (null left)
366
396
                             nil
367
397
                           (cons left right)))
368
398
                     (let ((left (car mtree))
369
 
                           (right (_fix-addr/depth-memtree-store-nil 
370
 
                                   quotient (cdr mtree) 
 
399
                           (right (_fix-addr/depth-memtree-store-nil
 
400
                                   quotient (cdr mtree)
371
401
                                   (the-fixnum (1- depth)))))
372
402
                       (if (and (null left)
373
403
                                (null right))
386
416
                   nil
387
417
                 (let ((quotient (ash addr -1)))
388
418
                   (if (= (the-fixnum (logand addr 1)) 0)
389
 
                       (let ((left (_fixnum-memtree-store-nil 
390
 
                                    quotient (car mtree) 
 
419
                       (let ((left (_fixnum-memtree-store-nil
 
420
                                    quotient (car mtree)
391
421
                                    (the-fixnum (1- depth))))
392
422
                             (right (cdr mtree)))
393
423
                         (if (and (null left)
395
425
                             nil
396
426
                           (cons left right)))
397
427
                     (let ((left (car mtree))
398
 
                           (right (_fixnum-memtree-store-nil 
399
 
                                   quotient (cdr mtree) 
 
428
                           (right (_fixnum-memtree-store-nil
 
429
                                   quotient (cdr mtree)
400
430
                                   (the-fixnum (1- depth)))))
401
431
                       (if (and (null left)
402
432
                                (null right))
425
455
;
426
456
; This is the same technique used in my ordered sets book in order to enforce
427
457
; the non-sets convention, and you can think of these as "a poor man's
428
 
; congruence rules".  Take for example _memtree-load-fix-a below, which 
 
458
; congruence rules".  Take for example _memtree-load-fix-a below, which
429
459
; says that the following:
430
460
;
431
461
; (defthm _memtree-load-fix-addr
471
501
(defthm _memtree-load-fix-depth
472
502
  (equal (_memtree-load addr mtree (nfix depth))
473
503
         (_memtree-load addr mtree depth))
474
 
  :hints(("Goal" 
 
504
  :hints(("Goal"
475
505
          :in-theory (disable _memtree-fix-nfix)
476
506
          :use ((:instance _memtree-fix-nfix)))))
477
507
 
525
555
;;; Key Lemmas: "equivalent" _addresses can be interchanged in stores
526
556
 
527
557
; These lemmas needs to stay disabled because they can easily cause loops.  It
528
 
; doesn't seem that simple loop stoppers fix the issue, and I'm too lazy to 
 
558
; doesn't seem that simple loop stoppers fix the issue, and I'm too lazy to
529
559
; figure out a better solution.
530
560
 
531
561
(local (defthmd _memtree-store-addr-switch-1
572
602
              (_memtree-p mtree depth)))))
573
603
 
574
604
; We implement a typical fixing function for memories.  Our default memory is
575
 
; an empty tree with size 1 and depth 1.  
 
605
; an empty tree with size 1 and depth 1.
576
606
 
577
607
(defun _memory-fix (mem)
578
608
  (declare (xargs :guard (_memory-p mem)))
624
654
           (signed-byte-p 29 (_memory-depth mem))))
625
655
 
626
656
(defthm _memory-mtree-length/depth
627
 
  (<= (_memory-size mem) 
 
657
  (<= (_memory-size mem)
628
658
      (expt 2 (_memory-depth mem)))
629
659
  :rule-classes :linear)
630
660
 
676
706
  (implies (not (_memory-p mem))
677
707
           (equal (_memory-record mem) nil)))
678
708
 
679
 
(in-theory (disable _memory-depth 
680
 
                    _memory-mtree 
681
 
                    _memory-fast 
 
709
(in-theory (disable _memory-depth
 
710
                    _memory-mtree
 
711
                    _memory-fast
682
712
                    _memory-record
683
713
                    _memory-size))
684
714
 
689
719
; give a multi-step process for removing hyptheses:
690
720
;
691
721
;  (1) determine a normal form for the data structure such that "equivalent"
692
 
;  structures are equal. 
 
722
;  structures are equal.
693
723
;
694
724
;  (2) define the desired operations assuming well formed data structures (we
695
725
;  already did this too, our load and store operations)
771
801
(defthm _to-mem-identity
772
802
  (implies (not (_bad-memory-p x))
773
803
           (equal (_to-mem x) x)))
774
 
               
 
804
 
775
805
(in-theory (disable _to-mem))
776
806
 
777
807
 
824
854
;
825
855
; Below is the "user's notion" of what a memory is.  It should always be
826
856
; disabled.  Basically, we require that a user's memory is always has a depth
827
 
; and size of at least one.  
 
857
; and size of at least one.
828
858
;
829
859
; This gives us the crucial property that "bad memories" are not memories in
830
860
; the user's sense.  Why is this so important?  Well, we are very much
831
 
; concerned with efficiency of operations.  As long as we know that our 
832
 
; arguments are not bad, we can skip all of this mapping and just provide 
 
861
; concerned with efficiency of operations.  As long as we know that our
 
862
; arguments are not bad, we can skip all of this mapping and just provide
833
863
; high speed execution using MBE.
834
864
 
835
865
(defun memory-p (mem)
887
917
          (equal size 1))
888
918
      (cons (cons nil t) (cons 1 (cons 1 nil)))
889
919
    (let ((depth (_log2 (1- size))))
890
 
      (cons 
 
920
      (cons
891
921
       (cons nil (signed-byte-p 29 depth))
892
 
       (cons size 
 
922
       (cons size
893
923
             (cons depth nil))))))
894
924
 
895
925
(defthm _new-memory
898
928
 
899
929
(defthm new-memory
900
930
  (memory-p (new size))
901
 
  :hints(("Goal" 
 
931
  :hints(("Goal"
902
932
          :in-theory (enable _memory-p
903
933
                             _memory-size
904
934
                             _memory-depth))))
946
976
       :exec (let* ((fast (cdar mem))
947
977
                    (mtree (caar mem))
948
978
                    (depth (caddr mem)))
949
 
               (if fast 
 
979
               (if fast
950
980
                   (_fixnum-memtree-load addr mtree depth)
951
981
                 (_memtree-load addr mtree depth)))))
952
982
 
953
983
(defun _store (addr elem mem)
954
984
  (declare (xargs :guard (and (memory-p mem)
955
985
                              (address-p addr mem))
956
 
                  :guard-hints (("Goal" 
 
986
                  :guard-hints (("Goal"
957
987
                                 :use (:instance _address-from-address)
958
988
                                 :in-theory (enable _memory-p
959
989
                                                    _memory-mtree
960
990
                                                    _memory-fast
961
991
                                                    _memory-depth
962
 
                                                    _memory-record                                                    
 
992
                                                    _memory-record
963
993
                                                    _memory-size)))))
964
994
  (mbe :logic (let ((fast   (_memory-fast mem))
965
995
                    (mtree  (_memory-mtree mem))
978
1008
                    (fast   (cdar mem))
979
1009
                    (memcdr (cdr mem))
980
1010
                    (depth  (cadr memcdr)))
981
 
               (cons (cons (if fast 
 
1011
               (cons (cons (if fast
982
1012
                               (if elem
983
1013
                                   (_fixnum-memtree-store addr elem mtree depth)
984
1014
                                 (_fixnum-memtree-store-nil addr mtree depth))
997
1027
(defthm _store-size
998
1028
  (equal (_memory-size (_store addr elem mem))
999
1029
         (_memory-size mem))
1000
 
  :hints(("Goal" :in-theory (e/d (_memory-size) 
 
1030
  :hints(("Goal" :in-theory (e/d (_memory-size)
1001
1031
                                 (_store-memory))
1002
1032
          :use (:instance _store-memory))))
1003
1033
 
1004
1034
(defthm _store-fast
1005
1035
  (equal (_memory-fast (_store addr elem mem))
1006
1036
         (_memory-fast mem))
1007
 
  :hints(("Goal" :in-theory (e/d (_memory-fast) 
 
1037
  :hints(("Goal" :in-theory (e/d (_memory-fast)
1008
1038
                                 (_store-memory))
1009
1039
          :use (:instance _store-memory))))
1010
1040
 
1012
1042
  (equal (_memory-mtree (_store addr elem mem))
1013
1043
         (if (address-p addr mem)
1014
1044
             (if elem
1015
 
                 (_memtree-store addr elem 
 
1045
                 (_memtree-store addr elem
1016
1046
                                 (_memory-mtree mem)
1017
1047
                                 (_memory-depth mem))
1018
 
               (_memtree-store-nil addr 
 
1048
               (_memtree-store-nil addr
1019
1049
                                   (_memory-mtree mem)
1020
1050
                                   (_memory-depth mem)))
1021
1051
           (_memory-mtree mem)))
1022
 
  :hints(("Goal" :in-theory (e/d (_memory-mtree) 
 
1052
  :hints(("Goal" :in-theory (e/d (_memory-mtree)
1023
1053
                                 (_store-memory))
1024
1054
          :use (:instance _store-memory))))
1025
1055
 
1026
1056
(defthm _store-depth
1027
1057
  (equal (_memory-depth (_store addr elem mem))
1028
1058
         (_memory-depth mem))
1029
 
  :hints(("Goal" :in-theory (e/d (_memory-depth) 
 
1059
  :hints(("Goal" :in-theory (e/d (_memory-depth)
1030
1060
                                 (_store-memory))
1031
1061
          :use (:instance _store-memory))))
1032
1062
 
1035
1065
          (if (address-p addr mem)
1036
1066
              (_memory-record mem)
1037
1067
            (s addr elem (_memory-record mem))))
1038
 
  :hints(("Goal" :in-theory (e/d (_memory-record) 
 
1068
  :hints(("Goal" :in-theory (e/d (_memory-record)
1039
1069
                                 (_store-memory))
1040
1070
          :use (:instance _store-memory))))
1041
1071
 
1096
1126
       :exec  (let* ((fast (cdar mem))
1097
1127
                     (mtree (caar mem))
1098
1128
                     (depth (caddr mem)))
1099
 
                (if fast 
 
1129
                (if fast
1100
1130
                    (_fixnum-memtree-load addr mtree depth)
1101
1131
                  (_memtree-load addr mtree depth)))))
1102
1132
 
1103
1133
(defun store (addr elem mem)
1104
1134
  (declare (xargs :guard (and (memory-p mem)
1105
1135
                              (address-p addr mem))
1106
 
                  :guard-hints(("Goal" 
 
1136
                  :guard-hints(("Goal"
1107
1137
                                :use (:instance _address-from-address)
1108
1138
                                :in-theory (enable _memory-p
1109
1139
                                                   _memory-mtree
1116
1146
                    (fast   (cdar mem))
1117
1147
                    (memcdr (cdr mem))
1118
1148
                    (depth  (cadr memcdr)))
1119
 
               (cons (cons (if fast 
 
1149
               (cons (cons (if fast
1120
1150
                               (if elem
1121
1151
                                   (_fixnum-memtree-store addr elem mtree depth)
1122
1152
                                 (_fixnum-memtree-store-nil addr mtree depth))
1183
1213
       :exec (_log2-tr n 0)))
1184
1214
 
1185
1215
(defthm _log2-equiv
1186
 
  (implies (and (natp n) 
 
1216
  (implies (and (natp n)
1187
1217
                (natp acc))
1188
1218
           (equal (_log2-tr n acc)
1189
1219
                  (+ (_log2 n) acc))))
1254
1284
 
1255
1285
 
1256
1286
 
1257
 
; We also note that upon creation, the value of every address in a memory 
 
1287
; We also note that upon creation, the value of every address in a memory
1258
1288
; happens to be nil.
1259
1289
 
1260
1290
(defthm load-new
1345
1375
     (integerp x)
1346
1376
     (<= (- (expt 2 15)) x)
1347
1377
     (< x (expt 2 15))))
1348
 
  
 
1378
 
1349
1379
  (defun fix-sbp16 (x)
1350
1380
    (declare (xargs :guard t))
1351
1381
    (if (sbp16 x) x 0))
1352
 
  
 
1382
 
1353
1383
  (defrecord sbp :rd getbv :wr putbv :fix fix-sbp16 :typep sbp16)
1354
 
  
 
1384
 
1355
1385
The "raw" record structure introduced in the standard records book is
1356
1386
used to define records defined using defrecord, and the functions for
1357
1387
accessing and updating a record that are introduced by defrecord are
1362
1392
following lemmas, each of which also holds of "raw" records:
1363
1393
 
1364
1394
(defthm g-same-s
1365
 
  (equal (g a (s a v r)) 
 
1395
  (equal (g a (s a v r))
1366
1396
         v))
1367
1397
 
1368
1398
(defthm g-diff-s
1371
1401
                  (g a r))))
1372
1402
 
1373
1403
(defthm s-same-g
1374
 
  (equal (s a (g a r) r) 
 
1404
  (equal (s a (g a r) r)
1375
1405
         r))
1376
1406
 
1377
1407
(defthm s-same-s
1387
1417
In addition, the defrecord macro proves one additional lemma that is
1388
1418
not provable about raw records:
1389
1419
 
1390
 
(defthm typep-g 
 
1420
(defthm typep-g
1391
1421
  (typep (g a r)))
1392
1422
 
1393
 
for a typep predicate provided by the user.  
 
1423
for a typep predicate provided by the user.
1394
1424
 
1395
1425
What makes this implementation of records interesting is that it has
1396
1426
the peculiar property that each of the lemmas has no "type"
1633
1663
(defthmd abstract-localfixedpoint
1634
1664
  (equal (localfixedpoint x)
1635
1665
         (subsetp (rkeys x) (list nil)))
1636
 
  :hints (("Goal" :in-theory (enable 
 
1666
  :hints (("Goal" :in-theory (enable
1637
1667
                              localfixedpoint
1638
1668
                              g
1639
1669
                              rkeys
1768
1798
 
1769
1799
;; AUX
1770
1800
(defun ifrp-s-aux (a v r)
1771
 
  (if (endp r) 
 
1801
  (if (endp r)
1772
1802
      (and (ifrp v) (not a))
1773
 
    (if (null (cdr r)) 
 
1803
    (if (null (cdr r))
1774
1804
        (if (<< a (caar r))
1775
1805
            (and (not v) (ifrp r))
1776
1806
          (and (null (caar r))
2012
2042
 
2013
2043
(defthm iff-s
2014
2044
  (iff (s a v r)
2015
 
       (or v 
 
2045
       (or v
2016
2046
           (and r (if (acl2::fixedpoint r) a
2017
2047
                    (not (subsetp (rkeys r) (list a)))))))
2018
2048
  :hints (("Goal" :in-theory (e/d (iff-s-to-iff-s-fixedpoint
2019
 
                                   gar-as-memberp 
 
2049
                                   gar-as-memberp
2020
2050
                                   fixedpoint-impact-on-keys)
2021
2051
                                  (LIST::MEMBERP-WHEN-NOT-MEMBERP-OF-CDR-CHEAP)))
2022
2052
          ("Subgoal 3''" :in-theory (enable list::memberp))))
2023
2053
 
2024
2054
(defthm fixedpoint-s
2025
2055
  (equal (fixedpoint (s a v r))
2026
 
         (or 
 
2056
         (or
2027
2057
          ;; Results from (not (s a v r))
2028
2058
          (not (or v
2029
2059
                   (and r (if (acl2::fixedpoint r) a
2030
2060
                            (not (subsetp (rkeys r) (list a)))))))
2031
 
          (and 
 
2061
          (and
2032
2062
           ;; Results from (localfixedpoint (s a v r))
2033
2063
           (if v (subsetp (cons a (rkeys r)) (list nil))
2034
2064
             (subsetp (rkeys r) (list a nil)))
2082
2112
          nil)
2083
2113
      (set::union (cons-onto-all '0 (mem::domain-aux (car mem-tree) (+ -1 depth)))
2084
2114
                  (cons-onto-all '1 (mem::domain-aux (cdr mem-tree) (+ -1 depth)))))))
2085
 
  
 
2115
 
2086
2116
 
2087
2117
;this bits are in reverse order (least significant bit comes first in the list)
2088
2118
(defun convert-reversed-bit-list-to-integer (bit-list)
2091
2121
    (+ (car bit-list)
2092
2122
       (* 2 (convert-reversed-bit-list-to-integer (cdr bit-list))))))
2093
2123
 
2094
 
;; (defmacro def-set-processor (&key (processor-name 'unsupplied) 
 
2124
;; (defmacro def-set-processor (&key (processor-name 'unsupplied)
2095
2125
;;                                   (element-processor 'unsupplied)  ;can this be a term?
2096
2126
;;                                   (predicate 'unsupplied))
2097
2127
;;   `(defun ,processor-name (set) ;can this take more than one arg?
2126
2156
                          (lambda (x) (convert-reversed-bit-lists-to-integers x))))
2127
2157
                        (a lst)
2128
2158
                        (x lst-of-lsts)
2129
 
                 
 
2159
 
2130
2160
                        ))))
2131
 
  
 
2161
 
2132
2162
(defun mem::mem-tree-domain (mem-tree depth)
2133
2163
  (convert-reversed-bit-lists-to-integers (mem::domain-aux mem-tree depth)))
2134
2164
 
2150
2180
                ;;always return nats less than size?  Not necessarily.  There
2151
2181
                ;;may be nats less than 2^depth but greater than size.  We
2152
2182
                ;;have to filter them out.
2153
 
                
 
2183
 
2154
2184
                (SET::FILTER<not-NATP-LESS-THAN-SIZE> (set::rkeys record-part) size)
2155
2185
                )))
2156
2186
 
2193
2223
                          (lambda (x) (cons-onto-all item x))))
2194
2224
                        (a lst)
2195
2225
                        (x lst-of-lsts)
2196
 
                 
 
2226
 
2197
2227
                        ))))
2198
2228
 
2199
2229
;bzo may ben expensive?
2246
2276
                                    MEM::|_ADDRESS-FIX|)
2247
2277
          :do-not '(generalize eliminate-destructors)
2248
2278
          :EXPAND ((MEM::|_MEMTREE-STORE| ADDR ELEM NIL DEPTH)))))
2249
 
        
 
2279
 
2250
2280
 
2251
2281
 
2252
2282
 
2277
2307
                              MEM::|_ADDRESS-P|
2278
2308
                              MEM::|_MEMTREE-FIX|
2279
2309
    ;MEM::|_MEMTREE-P|
2280
 
                              MEM::|_ADDRESS-FIX|) 
 
2310
                              MEM::|_ADDRESS-FIX|)
2281
2311
                           (;LIST::EQUAL-CONS-CASES ;bzo why?
2282
2312
                            )))))
2283
2313
 
2332
2362
 
2333
2363
;bzo drop?
2334
2364
       (if (equal 1 (cadr mem)) ;log2 on 0 is weird, so we handle this case specially
2335
 
           (equal 1 (caddr mem))        
 
2365
           (equal 1 (caddr mem))
2336
2366
         (equal (mem::|_LOG2| (+ -1 (cadr mem)))
2337
2367
                (caddr mem)))))
2338
2368
 
2356
2386
                   (lambda (x) (SET::FILTER<NOT-NATP-LESS-THAN-SIZE> x size))))
2357
2387
                 (a a)
2358
2388
                 (x x)
2359
 
                 
 
2389
 
2360
2390
                 ))))
2361
2391
 
2362
2392
(defthm FILTER<NATP-LESS-THAN-SIZE>-of-insert
2376
2406
                          (lambda (x) (SET::FILTER<NATP-LESS-THAN-SIZE> x size))))
2377
2407
                        (a a)
2378
2408
                        (x x)
2379
 
                 
 
2409
 
2380
2410
                        ))))
2381
 
          
 
2411
 
2382
2412
(defthm domain-of-store-v-non-nil
2383
2413
  (implies (and ;(MEM::MEMORY-P mem)
2384
2414
;(WFR (CDDDR MEM))
2394
2424
                              MEM::|_ADDRESS-P|
2395
2425
                              MEM::SIZE
2396
2426
                              MEM::STORE MEM::|_STORE|
2397
 
                              MEM::|_FROM-MEM| 
 
2427
                              MEM::|_FROM-MEM|
2398
2428
                              MEM::|_BAD-MEMORY-P|
2399
2429
                              MEM::|_MEMORY-P|
2400
2430
                              MEM::|_MEMORY-MTREE|
2404
2434
                              MEM::|_MEMORY-FAST|
2405
2435
                              MEM::|_MEMORY-SIZE|
2406
2436
                              MEM::|_MEMORY-RECORD|
2407
 
                              
2408
 
                              ) 
 
2437
 
 
2438
                              )
2409
2439
                           (SET::DOUBLE-CONTAINMENT
2410
2440
                            )))))
2411
2441
 
2413
2443
 
2414
2444
;for typed records gotta unwrap the domain...
2415
2445
 
2416
 
(in-theory (disable mem::domain)) ;move back               
 
2446
(in-theory (disable mem::domain)) ;move back
2417
2447
 
2418
2448
;bzo add to sets library
2419
2449
(defthm delete-of-insert-diff
2500
2530
;;     (and (equal len (len (set::head x)))
2501
2531
;;          (all-have-len len (set::tail x)))))
2502
2532
 
2503
 
(defun len-equal (a len) 
 
2533
(defun len-equal (a len)
2504
2534
  (declare (xargs :guard t))
2505
2535
  (equal (len a) (rfix len)))
2506
 
  
 
2536
 
2507
2537
(defthm all-len-equal-of-union
2508
2538
  (equal (set::all<len-equal> (set::union x y) depth)
2509
2539
         (and (set::all<len-equal> x depth)
2589
2619
  (implies (and (not (natp a))
2590
2620
                (force (set::all<bit-listp> bit-lists)))
2591
2621
           (not (set::in a (convert-reversed-bit-lists-to-integers bit-lists))))
2592
 
  :hints (("Goal" :in-theory (enable SET::ALL<BIT-LISTP> 
 
2622
  :hints (("Goal" :in-theory (enable SET::ALL<BIT-LISTP>
2593
2623
                                     )
2594
2624
           :do-not '(generalize eliminate-destructors))))
2595
2625
 
2681
2711
   (NOT
2682
2712
    (SET::IN (CONVERT-REVERSED-BIT-LIST-TO-INTEGER a)
2683
2713
             (CONVERT-REVERSED-BIT-LISTS-TO-INTEGERS x))))
2684
 
  :hints (("Goal" :in-theory (enable set::in 
 
2714
  :hints (("Goal" :in-theory (enable set::in
2685
2715
                                     )
2686
2716
           :do-not '(generalize eliminate-destructors))))
2687
2717
 
2780
2810
(defthm all-bit-listp-of-domain-aux
2781
2811
  (set::all<bit-listp> (mem::domain-aux tree depth))
2782
2812
    :hints (("Goal" :in-theory (enable mem::domain-aux acl2::equal-booleans-reducton))))
2783
 
;; LIST::EQUAL-OF-BOOLEANS-REWRITE 
 
2813
;; LIST::EQUAL-OF-BOOLEANS-REWRITE
2784
2814
 
2785
2815
(defthm setp-of-domain-aux
2786
2816
  (set::setp (mem::domain-aux tree depth))
2829
2859
                                                (CAR (CDR (CDR MEM))))))
2830
2860
           :do-not '(generalize eliminate-destructors)
2831
2861
           :in-theory (e/d (set::delete-of-union-push-into-both
2832
 
                              
 
2862
 
2833
2863
                            good-memoryp
2834
2864
                            MEM::DOMAIN
2835
2865
                            MEM::|_ADDRESS-P|
2836
2866
                            MEM::SIZE
2837
2867
                            MEM::STORE MEM::|_STORE|
2838
 
                            MEM::|_FROM-MEM| 
 
2868
                            MEM::|_FROM-MEM|
2839
2869
                            MEM::|_BAD-MEMORY-P|
2840
2870
                            MEM::|_MEMORY-P|
2841
2871
                            MEM::|_MEMORY-MTREE|
2845
2875
                            MEM::|_MEMORY-FAST|
2846
2876
                            MEM::|_MEMORY-SIZE|
2847
2877
                            MEM::|_MEMORY-RECORD|
2848
 
                            ) 
 
2878
                            )
2849
2879
                           (SET::DOUBLE-CONTAINMENT
2850
2880
                            SET::UNION-DELETE-y
2851
2881
                            SET::UNION-DELETE-x)))))
2871
2901
  (equal (mem::domain (mem::new size))
2872
2902
         nil)
2873
2903
  :hints (("Goal" :in-theory (enable MEM::DOMAIN-AUX
2874
 
                                     mem::new 
 
2904
                                     mem::new
2875
2905
                                     mem::domain
2876
2906
                                     mem::mem-tree-domain))))
2877
2907
 
3064
3094
                               MEM::|_MEMORY-P|
3065
3095
                               )))))
3066
3096
 
3067
 
(in-theory (disable MEM::MEM-TREE-DOMAIN))                             
 
3097
(in-theory (disable MEM::MEM-TREE-DOMAIN))
3068
3098
 
3069
3099
(defthm mem-tree-domain-after-store
3070
3100
  (implies (good-memoryp mem)
3071
3101
           (equal (MEM::MEM-TREE-DOMAIN (CAAR (MEM::STORE A V MEM))
3072
 
                                        (CADDR ;(MEM::STORE A V 
 
3102
                                        (CADDR ;(MEM::STORE A V
3073
3103
                                         MEM
3074
3104
                                         ;)
3075
3105
                                         ))
3086
3116
;           :use (:instance domain-of-store) ;gross way to prove this...
3087
3117
           :cases ((SET::EMPTY (MEM::DOMAIN-AUX (CAR (CAR MEM))
3088
3118
                                                      (CAR (CDR (CDR MEM))))))
3089
 
           
 
3119
 
3090
3120
           :in-theory (e/d (MEM::DOMAIN
3091
 
                            
 
3121
 
3092
3122
                            MEM::MEM-TREE-DOMAIN
3093
3123
                            MEM::STORE
3094
3124
                            MEM::MEMORY-P
3105
3135
                            MEM::|_MEMORY-FIX|
3106
3136
                            GOOD-MEMORYP
3107
3137
                            MEM::|_MEMORY-RECORD|
3108
 
                            ) 
3109
 
                           (domain-of-store)))))            
 
3138
                            )
 
3139
                           (domain-of-store)))))
3110
3140
 
3111
3141
 
3112
3142
(local (in-theory (disable SIGNED-BYTE-P)))
3218
3248
 
3219
3249
(defthm g-of-clr
3220
3250
  (equal (g a1 (clr a2 r))
3221
 
         (if (equal a1 a2) 
 
3251
         (if (equal a1 a2)
3222
3252
             nil
3223
3253
           (g a1 r)))
3224
3254
  :hints (("Goal" :in-theory (enable clr))))
3255
3285
                       (<< e a)
3256
3286
                       (<< e (caar r)))
3257
3287
                  (<< e (caar (s-aux a v r))))))
3258
 
 
 
3288
 
3259
3289
; jcd - extracted this from later encapsulate and made it local to this book
3260
3290
; so that it won't be exported
3261
3291
(local (defthm s-aux-preserves-rcdp
3277
3307
(local (defthm iff-s-aux-cases
3278
3308
         (implies (rcdp r)
3279
3309
                  (iff (s-aux a v r)
3280
 
                       (not (or (and (ENDP R) 
 
3310
                       (not (or (and (ENDP R)
3281
3311
                                     (not V))
3282
 
                                (and (consp r) 
3283
 
                                     (not v) 
3284
 
                                     (EQUAL A (CAAR R)) 
 
3312
                                (and (consp r)
 
3313
                                     (not v)
 
3314
                                     (EQUAL A (CAAR R))
3285
3315
                                     (not (cdr r)))))))))
3286
3316
 
3287
3317
; jcd - change this to more simple if form
3320
3350
 
3321
3351
; jcd - made this local to this book, so it won't be exported
3322
3352
; ews - doh! I needed this (at least temporarily) to be non-local
3323
 
(local 
 
3353
(local
3324
3354
 (defthm wfkeyed-s-aux
3325
3355
         (implies (and (not (ifrp r))
3326
3356
                       (rcdp r)