← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/lib/rtlarr.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel6/lib/rtlarr.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(set-enforce-redundancy t)
 
4
 
 
5
;; (local (include-book "../support/support/rtlarr"))
 
6
;; (local (include-book "../support/support/bvecp-helpers"))
 
7
;; (local (include-book "../support/support/guards"))
 
8
;; Fri Oct 27 15:38:29 2006
 
9
 
 
10
(local (include-book "../support/top/top"))
 
11
 
 
12
(set-inhibit-warnings "theory") ; avoid warning in the next event
 
13
(local (in-theory nil))
 
14
;(set-inhibit-warnings) ; restore theory warnings (optional)
 
15
 
 
16
;;We define generic record accessing and updating functions to be used 
 
17
;;with RTL arrays.  The basic functions are (ag a r) and (as a v r)
 
18
;;where a is an array index, v is a value, r is an "array" or record.
 
19
;;(ag a r) returns the value at index a in array r, and (as a v r) returns 
 
20
;;a new array with index a set to value v in array r.
 
21
 
 
22
(include-book "misc/total-order" :dir :system)
 
23
 
 
24
(include-book "rtl")
 
25
 
 
26
(defmacro default-get-valu () 0)
 
27
 
 
28
(defun rcdp (x)
 
29
  (declare (xargs :guard t))
 
30
  (or (null x)
 
31
      (and (consp x)
 
32
           (consp (car x))
 
33
           (rcdp (cdr x))
 
34
           (not (equal (cdar x) 
 
35
                       (default-get-valu)))
 
36
           (or (null (cdr x))
 
37
               (<< (caar x) (caadr x))))))
 
38
 
 
39
(defthm rcdp-implies-alistp
 
40
  (implies (rcdp x) (alistp x)))
 
41
 
 
42
(defmacro ifrp-tag ()
 
43
  ''unlikely-to-ever-occur-in-an-executable-counterpart)
 
44
 
 
45
(defun ifrp (x) ;; ill-formed rcdp 
 
46
  (declare (xargs :guard t))
 
47
  (or (not (rcdp x))
 
48
      (and (consp x)
 
49
           (null (cdr x))
 
50
           (consp (car x))
 
51
           (equal (cdar x) (ifrp-tag))
 
52
           (ifrp (caar x)))))
 
53
 
 
54
(defun acl2->rcd (x)  ;; function mapping acl2 objects to well-formed records.
 
55
  (declare (xargs :guard t))
 
56
  (if (ifrp x) (list (cons x (ifrp-tag))) x))
 
57
 
 
58
(defun rcd->acl2 (r)  ;; inverse of acl2->rcd.
 
59
  (declare (xargs :guard (rcdp r)))
 
60
  (if (ifrp r) (caar r) r))
 
61
 
 
62
(defun ag-aux (a r) ;; record g(et) when r is a well-formed record.
 
63
  (declare (xargs :guard (rcdp r)))
 
64
  (cond ((or (endp r)
 
65
             (<< a (caar r)))
 
66
         (default-get-valu))
 
67
        ((equal a (caar r))
 
68
         (cdar r))
 
69
        (t
 
70
         (ag-aux a (cdr r)))))
 
71
 
 
72
(defun ag (a x) ;; the generic record g(et) which works on any ACL2 object.
 
73
  (declare (xargs :guard t))
 
74
  (ag-aux a (acl2->rcd x)))
 
75
 
 
76
(defun acons-if (a v r)
 
77
  (declare (xargs :guard (rcdp r)))
 
78
  (if (equal v (default-get-valu)) r (acons a v r)))
 
79
 
 
80
(defun as-aux (a v r) ;; record s(et) when x is a well-formed record.
 
81
  (declare (xargs :guard (rcdp r)))
 
82
  (cond ((or (endp r)
 
83
             (<< a (caar r)))
 
84
         (acons-if a v r))
 
85
        ((equal a (caar r))
 
86
         (acons-if a v (cdr r)))
 
87
        (t 
 
88
         (cons (car r) (as-aux a v (cdr r))))))
 
89
 
 
90
(defun as (a v x) ;; the generic record s(et) which works on any ACL2 object.
 
91
  (declare (xargs :guard t))
 
92
  (rcd->acl2 (as-aux a v (acl2->rcd x))))
 
93
 
 
94
 
 
95
;;Basic properties of arrays:
 
96
 
 
97
(defthm ag-same-as
 
98
  (equal (ag a (as a v r)) 
 
99
         v))
 
100
 
 
101
(defthm ag-diff-as
 
102
  (implies (not (equal a b))
 
103
           (equal (ag a (as b v r))
 
104
                  (ag a r))))
 
105
 
 
106
;;;; NOTE: The following can be used instead of the above rules to force ACL2
 
107
;;;; to do a case-split. We disable this rule by default since it can lead to
 
108
;;;; an expensive case explosion, but in many cases, this rule may be more
 
109
;;;; effective than two rules above and should be enabled.
 
110
 
 
111
(defthm ag-of-as-redux
 
112
  (equal (ag a (as b v r))
 
113
         (if (equal a b) v (ag a r))))
 
114
 
 
115
(in-theory (disable ag-of-as-redux))
 
116
 
 
117
(defthm as-same-ag
 
118
  (equal (as a (ag a r) r) 
 
119
         r))
 
120
 
 
121
(defthm as-same-as
 
122
  (equal (as a y (as a x r))
 
123
         (as a y r)))
 
124
 
 
125
(defthm as-diff-as
 
126
  (implies (not (equal a b))
 
127
           (equal (as b y (as a x r))
 
128
                  (as a x (as b y r))))
 
129
  :rule-classes ((:rewrite :loop-stopper ((b a as)))))
 
130
 
 
131
;; the following theorems are less relevant but have been useful in dealing
 
132
;; with a default record of NIL.
 
133
 
 
134
(defthm ag-of-nil-is-default
 
135
  (equal (ag a nil) (default-get-valu)))
 
136
 
 
137
(defthm as-non-default-cannot-be-nil
 
138
  (implies (not (equal v (default-get-valu)))
 
139
           (as a v r)))
 
140
 
 
141
(defthm non-nil-if-ag-not-default
 
142
  (implies (not (equal (ag a r) 
 
143
                       (default-get-valu)))
 
144
           r)
 
145
  :rule-classes :forward-chaining)
 
146
 
 
147
;; OK, we add here some properties for typing the records and the values which
 
148
;; are stored in the records. This "typing" is pretty generic, but we choose the
 
149
;; "bvecp" types for record values because it suits AMD's RTL modeling needs.
 
150
 
 
151
(defun bv-arrp (x k)
 
152
  (declare (xargs :guard (integerp k)))
 
153
  (or (null x)
 
154
      (and (consp x)
 
155
           (consp (car x))
 
156
           (bv-arrp (cdr x) k)
 
157
           (not (equal (cdar x) 
 
158
                       (default-get-valu)))
 
159
           (bvecp (cdar x) k)
 
160
           (or (null (cdr x))
 
161
               (<< (caar x) (caadr x))))))
 
162
 
 
163
(defthm as-maps-bv-arr-to-bv-arr
 
164
  (implies (and (bv-arrp r k)
 
165
                (bvecp v k))
 
166
           (bv-arrp (as a v r) k)))
 
167
 
 
168
(defthm ag-maps-bv-arr-to-bvecp
 
169
  (implies (bv-arrp r k)
 
170
           (bvecp (ag a r) k)))
 
171
 
 
172
(defun mk-bvarr (r k)
 
173
  (declare (xargs :guard (integerp k)))
 
174
  (if (bv-arrp r k) r ()))
 
175
 
 
176
(defthm mk-bvarr-is-bv-arrp
 
177
  (bv-arrp (mk-bvarr r k) k))
 
178
 
 
179
(defthm mk-bvarr-identity
 
180
  (implies (bv-arrp r k)
 
181
           (equal (mk-bvarr r k) r)))
 
182
 
 
183
(in-theory (disable bv-arrp mk-bvarr))
 
184
 
 
185
;;We also define as2 and ag2 for 2-dimensional arrays but these simply
 
186
;;macro-expand into appropriate as and ag calls.
 
187
 
 
188
(defmacro ag2 (a b r)
 
189
  `(ag (cons ,a ,b) ,r))
 
190
 
 
191
(defmacro as2 (a b v r)
 
192
  `(as (cons ,a ,b) ,v ,r))
 
193
 
 
194
 
 
195
;;We disable as and ag, assuming the rules proved in this book are 
 
196
;;sufficient to manipulate any record terms that are encountered.
 
197
 
 
198
(in-theory (disable as ag))
 
199
 
 
200
(defun positive-integer-listp (l)
 
201
  (declare (xargs :guard t))
 
202
  (cond ((atom l)
 
203
         (equal l nil))
 
204
        (t (and (integerp (car l))
 
205
                (< 0 (car l))
 
206
                (positive-integer-listp (cdr l))))))
 
207
 
 
208
(defmacro arr0 (&rest dims)
 
209
  (declare (ignore dims)
 
210
           (xargs :guard (positive-integer-listp dims)))
 
211
  nil)
 
212
 
 
213
;;Functions representing bit vectors of determined length but undetermined value:
 
214
 
 
215
(encapsulate 
 
216
 ((reset2 (key size) t))
 
217
 (local (defun reset2 (key size) (declare (ignore key size)) nil))
 
218
 (defthm bv-arrp-reset2
 
219
   (bv-arrp (reset2 key size) size)
 
220
   :hints
 
221
   (("goal" :in-theory (enable bv-arrp)))))
 
222
 
 
223
(encapsulate 
 
224
 ((unknown2 (key size n) t))
 
225
 (local (defun unknown2 (key size n) (declare (ignore key size n)) nil))
 
226
 (defthm bv-arrp-unknown2
 
227
   (bv-arrp (unknown2 key size n) size)
 
228
   :hints
 
229
   (("goal" :in-theory (enable bv-arrp)))))
 
230
 
 
231
;BOZO where in lib/ should this go?
 
232
(defthm bv-arrp-if1
 
233
  (equal (bv-arrp (if1 x y z) n)
 
234
         (if1 x (bv-arrp y n) (bv-arrp z n))))
 
235
 
 
236
 
 
237