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

Last change on this file since 246 was 246, checked in by mulligan, 9 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.