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

Last change on this file since 246 was 246, checked in by mulligan, 10 years ago

Added physical file (Arithmetic) for arithmetic on bit vectors, and
added sparse bitvector trie for modelling 8051 memory.

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