source: Deliverables/D4.1/Matita/BitVector.ma @ 248

Last change on this file since 248 was 248, checked in by mulligan, 9 years ago

More changes. Added datatype for addressing modes.

File size: 6.2 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* BitVector.ma: Fixed length bitvectors, and common operations on them.      *)
3(*               Most functions are specialised versions of those found in    *)
4(*               Vector.ma as a courtesy, or Boolean functions lifted into    *)
5(*               BitVector variants.                                          *)
6(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
7
8include "Universes.ma".
9
10include "Vector.ma".
11include "List.ma".
12include "Nat.ma".
13include "Bool.ma".
14
15(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
16(* Common synonyms.                                                           *)
17(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
18
19ndefinition BitVector ≝ λn: Nat. Vector Bool n.
20ndefinition Bit ≝ BitVector (S Z).
21ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
22ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
23ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
24ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
25ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))).
26
27(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
28(* Lookup.                                                                    *)
29(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
30
31ndefinition get_index ≝
32  λn: Nat.
33  λb: BitVector n.
34  λm: Nat.
35    get_index Bool n b m.
36   
37interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
38   
39ndefinition set_index ≝
40  λn: Nat.
41  λb: BitVector n.
42  λm: Nat.
43    set_index Bool n b m.
44   
45ndefinition drop ≝
46  λn: Nat.
47  λb: BitVector n.
48  λm: Nat.
49    drop Bool n b m.
50
51(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
52(* Creating bitvectors from scratch.                                          *)
53(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
54
55ndefinition zero ≝
56  λn: Nat.
57    replicate Bool n False.
58   
59ndefinition max ≝
60  λn: Nat.
61    replicate Bool n True.
62   
63ndefinition append ≝
64  λm, n: Nat.
65  λb: BitVector m.
66  λc: BitVector n.
67    append Bool m n b c.
68   
69interpretation "BitVector append" 'append b c = (append b c).
70
71ndefinition pad ≝
72  λm, n: Nat.
73  λb: BitVector n.
74    let padding ≝ replicate Bool m False in
75      append Bool m n padding b.
76     
77(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
78(* Other manipulations.                                                       *)
79(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
80
81ndefinition reverse ≝
82  λn: Nat.
83  λb: BitVector n.
84    reverse Bool n b.
85
86ndefinition length ≝
87  λn: Nat.
88  λb: BitVector n.
89    length Bool n b.
90
91(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
92(* Logical operations.                                                        *)
93(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
94   
95ndefinition conjunction ≝
96  λn: Nat.
97  λb: BitVector n.
98  λc: BitVector n.
99    zip_with Bool Bool Bool n conjunction b c.
100   
101interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c).
102   
103ndefinition inclusive_disjunction ≝
104  λn: Nat.
105  λb: BitVector n.
106  λc: BitVector n.
107    zip_with Bool Bool Bool n inclusive_disjunction b c.
108   
109interpretation "BitVector inclusive disjunction"
110  'inclusive_disjunction b c = (inclusive_disjunction ? b c).
111         
112ndefinition exclusive_disjunction ≝
113  λn: Nat.
114  λb: BitVector n.
115  λc: BitVector n.
116    zip_with Bool Bool Bool n exclusive_disjunction b c.
117   
118interpretation "BitVector exclusive disjunction"
119  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
120   
121ndefinition negation ≝
122  λn: Nat.
123  λb: BitVector n.
124    map Bool Bool n (negation) b.
125   
126interpretation "BitVector negation" 'negation b c = (negation ? b c).
127
128(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
129(* Rotates and shifts.                                                        *)
130(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
131
132ndefinition rotate_left ≝
133  λm, n: Nat.
134  λb: BitVector n.
135    rotate_left Bool n m b.
136
137ndefinition rotate_right ≝
138  λm, n: Nat.
139  λb: BitVector n.
140    rotate_right Bool n m b.
141   
142ndefinition shift_left ≝
143  λm, n: Nat.
144  λb: BitVector n.
145  λc: Bool.
146    shift_left Bool n m b c.
147   
148ndefinition shift_right ≝
149  λm, n: Nat.
150  λb: BitVector n.
151  λc: Bool.
152    shift_right Bool n m b c.
153   
154(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
155(* Conversions to and from lists and natural numbers.                         *)
156(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
157
158ndefinition list_of_bitvector ≝
159  λn: Nat.
160  λb: BitVector n.
161    list_of_vector Bool n b.
162   
163ndefinition bitvector_of_list ≝
164  λl: List Bool.
165    vector_of_list Bool l.
166
167nlet rec bitvector_of_nat_aux (n: Nat) on n ≝
168  let divrem ≝ divide_with_remainder n (S (S Z)) in
169  let div ≝ first Nat Nat divrem in
170  let rem ≝ second Nat Nat divrem in
171    match div with
172      [ Z ⇒
173        match rem with
174          [ Z ⇒ Empty Bool
175          | S r ⇒ ? (True :: (bitvector_of_nat_aux Z))
176          ]
177      | S d ⇒
178        match rem with
179          [ Z ⇒ ? (False :: (bitvector_of_nat_aux (S d)))
180          | S r ⇒ ? (True :: (bitvector_of_nat_aux (S d)))
181          ]
182      ].
183      //.
184nqed.
185
186ndefinition bitvector_of_nat ≝
187  λm, n: Nat.
188    let biglist ≝ reverse Bool (bitvector_of_nat_aux m) in
189    let size ≝ length Bool biglist in
190    let bitvector ≝ bitvector_of_list biglist in
191    let difference ≝ n - size in
192      pad difference size bitvector.
193
194nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
195  match b with
196    [ Empty ⇒ Z
197    | Cons o hd tl ⇒
198      let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in
199        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
200    ].
Note: See TracBrowser for help on using the repository browser.