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

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

Using bitvectortries for a dictionary doesn't work even if we hypothesise conversion functions from bitvectors to string, and back again. Many changes, including most of the assembly function implemented.

File size: 6.9 KB
RevLine 
[236]1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* BitVector.ma: Fixed length bitvectors, and common operations on them.      *)
[240]3(*               Most functions are specialised versions of those found in    *)
4(*               Vector.ma as a courtesy, or Boolean functions lifted into    *)
5(*               BitVector variants.                                          *)
[236]6(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
7
[246]8include "Vector.ma".
[410]9include "String.ma".
[240]10
[236]11(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
12(* Common synonyms.                                                           *)
13(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
14
[228]15ndefinition BitVector ≝ λn: Nat. Vector Bool n.
[263]16ndefinition Bit ≝ Bool.
[230]17ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
18ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
19ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
20ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
[271]21ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S Z))))))))))).
[224]22
[236]23(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[240]24(* Lookup.                                                                    *)
25(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
26
[362]27(*
[337]28ndefinition get_index_bv ≝
[240]29  λn: Nat.
30  λb: BitVector n.
31  λm: Nat.
[266]32  λp: m < n.
[362]33    get_index_bv Bool n b m p.
[240]34   
35interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
36   
[337]37ndefinition set_index_bv ≝
[240]38  λn: Nat.
39  λb: BitVector n.
40  λm: Nat.
[266]41  λp: m < n.
42  λc: Bool.
[314]43    set_index Bool n b m c.
[240]44   
45ndefinition drop ≝
46  λn: Nat.
47  λb: BitVector n.
48  λm: Nat.
49    drop Bool n b m.
[362]50*)
[240]51
52(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[236]53(* Creating bitvectors from scratch.                                          *)
54(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
55
[362]56ndefinition zero: ∀n:Nat. BitVector n ≝
57  λn: Nat. replicate Bool n false.
[228]58   
[362]59ndefinition max: ∀n:Nat. BitVector n ≝
60  λn: Nat. replicate Bool n true.
61
62(*
[237]63ndefinition append ≝
64  λm, n: Nat.
65  λb: BitVector m.
66  λc: BitVector n.
67    append Bool m n b c.
[362]68*)
69 
[237]70ndefinition pad ≝
71  λm, n: Nat.
72  λb: BitVector n.
[260]73    let padding ≝ replicate Bool m false in
[237]74      append Bool m n padding b.
[240]75     
76(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
77(* Other manipulations.                                                       *)
78(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[237]79
[362]80(*
[240]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.
[362]90*)
[240]91
[236]92(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
93(* Logical operations.                                                        *)
94(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
95   
[343]96ndefinition conjunction_bv ≝
[228]97  λn: Nat.
98  λb: BitVector n.
99  λc: BitVector n.
[240]100    zip_with Bool Bool Bool n conjunction b c.
101   
102interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c).
[237]103   
[343]104ndefinition inclusive_disjunction_bv ≝
[228]105  λn: Nat.
106  λb: BitVector n.
107  λc: BitVector n.
[240]108    zip_with Bool Bool Bool n inclusive_disjunction b c.
109   
110interpretation "BitVector inclusive disjunction"
111  'inclusive_disjunction b c = (inclusive_disjunction ? b c).
[237]112         
[343]113ndefinition exclusive_disjunction_bv ≝
[228]114  λn: Nat.
115  λb: BitVector n.
116  λc: BitVector n.
[240]117    zip_with Bool Bool Bool n exclusive_disjunction b c.
[232]118   
[240]119interpretation "BitVector exclusive disjunction"
120  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
121   
[337]122ndefinition negation_bv ≝
[234]123  λn: Nat.
124  λb: BitVector n.
125    map Bool Bool n (negation) b.
[240]126   
127interpretation "BitVector negation" 'negation b c = (negation ? b c).
[238]128
129(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
130(* Rotates and shifts.                                                        *)
131(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
132
[362]133(*
[337]134ndefinition rotate_left_bv ≝
135  λn, m: Nat.
[238]136  λb: BitVector n.
137    rotate_left Bool n m b.
138
[337]139ndefinition rotate_right_bv ≝
140  λn, m: Nat.
[238]141  λb: BitVector n.
[240]142    rotate_right Bool n m b.
[236]143   
[337]144ndefinition shift_left_bv ≝
145  λn, m: Nat.
[240]146  λb: BitVector n.
147  λc: Bool.
148    shift_left Bool n m b c.
149   
[337]150ndefinition shift_right_bv ≝
151  λn, m: Nat.
[240]152  λb: BitVector n.
153  λc: Bool.
154    shift_right Bool n m b c.
[362]155*)
156 
[236]157(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
158(* Conversions to and from lists and natural numbers.                         *)
159(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[232]160
[362]161(*
[237]162ndefinition list_of_bitvector ≝
163  λn: Nat.
164  λb: BitVector n.
165    list_of_vector Bool n b.
[236]166   
[237]167ndefinition bitvector_of_list ≝
168  λl: List Bool.
169    vector_of_list Bool l.
[362]170*)
[234]171
[353]172nlet rec bitvector_of_nat_aux (n: Nat) (bound: Nat) on bound ≝
173 match bound with
174  [ Z ⇒ Empty Bool (* IT WILL NOT HAPPEN *)
175  | S bound ⇒
176    let divrem ≝ divide_with_remainder n (S (S Z)) in
177    let div ≝ first Nat Nat divrem in
178    let rem ≝ second Nat Nat divrem in
179      match div with
180        [ Z ⇒
181          match rem with
182            [ Z ⇒ Empty Bool
183            | S r ⇒ true :: (bitvector_of_nat_aux Z bound)
184            ]
185        | S d ⇒
186          match rem with
187            [ Z ⇒ false :: (bitvector_of_nat_aux (S d) bound)
188            | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound)
189            ]
190        ]].
[236]191
[315]192ndefinition eq_bv ≝
193  λn: Nat.
194  λb, c: BitVector n.
195    eq_v Bool n (λd, e.
196      if inclusive_disjunction (conjunction d e) (conjunction (negation d)
197                                                              (negation e)) then
198        true
199      else
200        false) b c.
201
[273]202nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝
[353]203  let biglist ≝ reverse ? (bitvector_of_nat_aux m m) in
[273]204  let size ≝ length ? biglist in
[362]205  let bitvector ≝ vector_of_list ? biglist in
[273]206  let difference ≝ n - size in
[351]207   less_than_or_equal_b_elim …
[374]208    (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector (difference+size) ↦ BitVector n⌉))
[351]209    (λH:¬(size ≤ n). max n).
210 nnormalize; nrewrite > (plus_minus_inverse_right n ?); //; nassumption.
[273]211nqed.
212
[237]213nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
214  match b with
[374]215    [ VEmpty ⇒ Z
216    | VCons o hd tl ⇒
[260]217      let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z ] in
[248]218        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
[410]219    ].
220   
221naxiom bitvector_of_string:
222  ∀n: Nat.
223  ∀s: String.
224    BitVector n.
225   
226naxiom string_of_bitvector:
227  ∀n: Nat.
228  ∀b: BitVector n.
229    String.
Note: See TracBrowser for help on using the repository browser.