← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/rtl/rel6/user/setbitn.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/user/setbitn.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(local (include-book "../support/support/setbitn"))
 
4
(local (include-book "../support/support/guards"))
 
5
 
 
6
;; Necessary defuns:
 
7
 
 
8
(defun natp (x)
 
9
  (declare (xargs :guard t))
 
10
  (and (integerp x)
 
11
       (<= 0 x)))
 
12
 
 
13
(defund bvecp (x k)
 
14
  (declare (xargs :guard (integerp k)))
 
15
  (and (integerp x)
 
16
       (<= 0 x)
 
17
       (< x (expt 2 k))))
 
18
 
 
19
(defund fl (x)
 
20
  (declare (xargs :guard (real/rationalp x)))
 
21
  (floor x 1))
 
22
 
 
23
(defund bits (x i j)
 
24
  (declare (xargs :guard (and (natp x)
 
25
                              (natp i)
 
26
                              (natp j))))
 
27
  (mbe :logic (if (or (not (integerp i))
 
28
                      (not (integerp j)))
 
29
                  0
 
30
                (fl (/ (mod x (expt 2 (1+ i))) (expt 2 j))))
 
31
       :exec  (if (< i j)
 
32
                  0
 
33
                (logand (ash x (- j)) (1- (ash 1 (1+ (- i j))))))))
 
34
 
 
35
(defund bitn (x n)
 
36
  (declare (xargs :guard (and (natp x)
 
37
                              (natp n))))
 
38
  (mbe :logic (bits x n n)
 
39
       :exec  (if (evenp (ash x (- n))) 0 1)))
 
40
 
 
41
(defund binary-cat (x m y n)
 
42
  (declare (xargs :guard (and (natp x)
 
43
                              (natp y)
 
44
                              (integerp m) (< 0 m)
 
45
                              (integerp n) (< 0 n))))
 
46
  (if (and (natp m) (natp n))
 
47
      (+ (* (expt 2 n) (bits x (1- m) 0))
 
48
         (bits y (1- n) 0))
 
49
    0))
 
50
 
 
51
(defun formal-+ (x y)
 
52
  ;;an auxiliary function that does not appear in translate-rtl output.
 
53
  (declare (xargs :guard t))
 
54
  (if (and (acl2-numberp x) (acl2-numberp y))
 
55
      (+ x y)
 
56
    (list '+ x y)))
 
57
 
 
58
;;X is a list of alternating data values and sizes.  CAT-SIZE returns the
 
59
;;formal sum of the sizes.  X must contain at least 1 data/size pair, but we do
 
60
;;not need to specify this in the guard, and leaving it out of that guard
 
61
;;simplifies the guard proof.
 
62
 
 
63
(defun cat-size (x)
 
64
  ;;an auxiliary function that does not appear in translate-rtl output.
 
65
  (declare (xargs :guard (and (true-listp x) (evenp (length x)))))
 
66
  (if (endp (cddr x))
 
67
      (cadr x)
 
68
    (formal-+ (cadr x)
 
69
              (cat-size (cddr x)))))
 
70
 
 
71
(defmacro cat (&rest x)
 
72
  (declare (xargs :guard (and x (true-listp x) (evenp (length x)))))
 
73
  (cond ((endp (cddr x))
 
74
         `(bits ,(car x) ,(formal-+ -1 (cadr x)) 0))
 
75
        ((endp (cddddr x))
 
76
         `(binary-cat ,@x))
 
77
        (t
 
78
         `(binary-cat ,(car x) 
 
79
                      ,(cadr x) 
 
80
                      (cat ,@(cddr x)) 
 
81
                      ,(cat-size (cddr x))))))
 
82
 
 
83
;Allows things like (in-theory (disable cat)) to refer to binary-cat.
 
84
(add-macro-alias cat binary-cat)
 
85
 
 
86
(defund setbits (x w i j y)
 
87
  (declare (xargs :guard (and (natp x)
 
88
                              (natp y)
 
89
                              (integerp i)
 
90
                              (integerp j)
 
91
                              (<= 0 j)
 
92
                              (<= j i)
 
93
                              (integerp w)
 
94
                              (< i w))))
 
95
  (mbe :logic (cat (bits x (1- w) (1+ i))
 
96
                   (+ -1 w (- i))
 
97
                   (cat (bits y (+ i (- j)) 0)
 
98
                        (+ 1 i (- j))
 
99
                        (bits x (1- j) 0)
 
100
                        j)
 
101
                   (1+ i))
 
102
       :exec  (cond ((int= j 0)
 
103
                     (cond ((int= (1+ i) w)
 
104
                            (bits y (+ i (- j)) 0))
 
105
                           (t
 
106
                            (cat (bits x (1- w) (1+ i))
 
107
                                 (+ -1 w (- i))
 
108
                                 (bits y (+ i (- j)) 0)
 
109
                                 (1+ i)))))
 
110
                    ((int= (1+ i) w)
 
111
                     (cat (bits y (+ i (- j)) 0)
 
112
                          (+ 1 i (- j))
 
113
                          (bits x (1- j) 0)
 
114
                          j))
 
115
                    (t
 
116
                     (cat (bits x (1- w) (1+ i))
 
117
                          (+ -1 w (- i))
 
118
                          (cat (bits y (+ i (- j)) 0)
 
119
                               (+ 1 i (- j))
 
120
                               (bits x (1- j) 0)
 
121
                               j)
 
122
                          (1+ i))))))
 
123
 
 
124
;;
 
125
;; New stuff:
 
126
;;
 
127
 
 
128
(defund setbitn (x w n y)
 
129
  (declare (xargs :guard (and (natp x)
 
130
                              (natp y)
 
131
                              (integerp n)
 
132
                              (<= 0 n)
 
133
                              (integerp w)
 
134
                              (< n w))))
 
135
  (setbits x w n n y))
 
136
 
 
137
(defthm setbitn-nonnegative-integer-type
 
138
  (and (integerp (setbitn x w n y))
 
139
       (<= 0 (setbitn x w n y)))
 
140
  :rule-classes (:type-prescription))
 
141
 
 
142
;this rule is no better than setbits-nonnegative-integer-type and might be worse:
 
143
(in-theory (disable (:type-prescription setbitn)))
 
144
 
 
145
(defthm setbitn-natp
 
146
  (natp (setbitn x w n y)))
 
147
 
 
148
;add setbitn-bvecp-simple?
 
149
 
 
150
(defthm setbitn-bvecp
 
151
  (implies (and (<= w k)
 
152
                (case-split (integerp k)))
 
153
           (bvecp (setbitn x w n y) k)))
 
154
 
 
155
(defthm setbitn-rewrite
 
156
  (implies (syntaxp (quotep n))
 
157
           (equal (setbitn x w n y)
 
158
                  (setbits x w n n y))))
 
159
 
 
160
;gen?
 
161
(defthm bitn-setbitn
 
162
  (implies (and (case-split (bvecp y 1))
 
163
                (case-split (< 0 w))
 
164
                (case-split (< n w))
 
165
                (case-split (< k w))
 
166
                (case-split (<= 0 k))
 
167
                (case-split (integerp w))
 
168
                (case-split (integerp n))
 
169
                (<= 0 n)
 
170
                (case-split (integerp k))
 
171
                )
 
172
           (equal (bitn (setbitn x w n y) k)
 
173
                  (if (equal n k)
 
174
                      y
 
175
                    (bitn x k)))))
 
176
 
 
177
(defthm setbitn-setbitn
 
178
  (implies (and (case-split (<= 0 n))
 
179
                (case-split (< n w))
 
180
                (case-split (integerp w))
 
181
                (case-split (integerp n))
 
182
                )
 
183
           (equal (setbitn (setbitn x w n y) w n y2)
 
184
                  (setbitn x w n y2))))
 
185
 
 
186
(defthm setbitn-does-nothing
 
187
  (implies (and (case-split (<= 0 n))
 
188
                (case-split (< n w))
 
189
                (case-split (integerp w))
 
190
                (case-split (integerp n))
 
191
                )
 
192
           (equal (setbitn x w n (bitn x n))
 
193
                  (bits x (+ -1 w) 0))))
 
194