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

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