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

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

Changes to bitvector.

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