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

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

Updated Vector / BitVector? files taken from my Matita library.

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