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

Last change on this file since 362 was 362, checked in by sacerdot, 9 years ago

Less ambiguous definitions.

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
26(*
27ndefinition get_index_bv ≝
28  λn: Nat.
29  λb: BitVector n.
30  λm: Nat.
31  λp: m < n.
32    get_index_bv Bool n b m p.
33   
34interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
35   
36ndefinition set_index_bv ≝
37  λn: Nat.
38  λb: BitVector n.
39  λm: Nat.
40  λp: m < n.
41  λc: Bool.
42    set_index Bool n b m c.
43   
44ndefinition drop ≝
45  λn: Nat.
46  λb: BitVector n.
47  λm: Nat.
48    drop Bool n b m.
49*)
50
51(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
52(* Creating bitvectors from scratch.                                          *)
53(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
54
55ndefinition zero: ∀n:Nat. BitVector n ≝
56  λn: Nat. replicate Bool n false.
57   
58ndefinition max: ∀n:Nat. BitVector n ≝
59  λn: Nat. replicate Bool n true.
60
61(*
62ndefinition append ≝
63  λm, n: Nat.
64  λb: BitVector m.
65  λc: BitVector n.
66    append Bool m n b c.
67*)
68 
69ndefinition pad ≝
70  λm, n: Nat.
71  λb: BitVector n.
72    let padding ≝ replicate Bool m false in
73      append Bool m n padding b.
74     
75(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
76(* Other manipulations.                                                       *)
77(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
78
79(*
80ndefinition reverse ≝
81  λn: Nat.
82  λb: BitVector n.
83    reverse Bool n b.
84
85ndefinition length ≝
86  λn: Nat.
87  λb: BitVector n.
88    length Bool n b.
89*)
90
91(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
92(* Logical operations.                                                        *)
93(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
94   
95ndefinition conjunction_bv ≝
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_bv ≝
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_bv ≝
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_bv ≝
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
132(*
133ndefinition rotate_left_bv ≝
134  λn, m: Nat.
135  λb: BitVector n.
136    rotate_left Bool n m b.
137
138ndefinition rotate_right_bv ≝
139  λn, m: Nat.
140  λb: BitVector n.
141    rotate_right Bool n m b.
142   
143ndefinition shift_left_bv ≝
144  λn, m: Nat.
145  λb: BitVector n.
146  λc: Bool.
147    shift_left Bool n m b c.
148   
149ndefinition shift_right_bv ≝
150  λn, m: Nat.
151  λb: BitVector n.
152  λc: Bool.
153    shift_right Bool n m b c.
154*)
155 
156(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
157(* Conversions to and from lists and natural numbers.                         *)
158(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
159
160(*
161ndefinition list_of_bitvector ≝
162  λn: Nat.
163  λb: BitVector n.
164    list_of_vector Bool n b.
165   
166ndefinition bitvector_of_list ≝
167  λl: List Bool.
168    vector_of_list Bool l.
169*)
170
171nlet rec bitvector_of_nat_aux (n: Nat) (bound: Nat) on bound ≝
172 match bound with
173  [ Z ⇒ Empty Bool (* IT WILL NOT HAPPEN *)
174  | S bound ⇒
175    let divrem ≝ divide_with_remainder n (S (S Z)) in
176    let div ≝ first Nat Nat divrem in
177    let rem ≝ second Nat Nat divrem in
178      match div with
179        [ Z ⇒
180          match rem with
181            [ Z ⇒ Empty Bool
182            | S r ⇒ true :: (bitvector_of_nat_aux Z bound)
183            ]
184        | S d ⇒
185          match rem with
186            [ Z ⇒ false :: (bitvector_of_nat_aux (S d) bound)
187            | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound)
188            ]
189        ]].
190
191ndefinition eq_bv ≝
192  λn: Nat.
193  λb, c: BitVector n.
194    eq_v Bool n (λd, e.
195      if inclusive_disjunction (conjunction d e) (conjunction (negation d)
196                                                              (negation e)) then
197        true
198      else
199        false) b c.
200
201nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝
202  let biglist ≝ reverse ? (bitvector_of_nat_aux m m) in
203  let size ≝ length ? biglist in
204  let bitvector ≝ vector_of_list ? biglist in
205  let difference ≝ n - size in
206   less_than_or_equal_b_elim …
207    (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector n ↦ BitVector (difference+size)⌉))
208    (λH:¬(size ≤ n). max n).
209 nnormalize; nrewrite > (plus_minus_inverse_right n ?); //; nassumption.
210nqed.
211
212nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
213  match b with
214    [ Empty ⇒ Z
215    | Cons o hd tl ⇒
216      let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z ] in
217        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
218    ].
Note: See TracBrowser for help on using the repository browser.