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

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

More work on bitvectors.

File size: 4.1 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* BitVector.ma: Fixed length bitvectors, and common operations on them.      *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5include "Vector.ma".
6include "List.ma".
7include "Nat.ma".
8include "Bool.ma".
9
10(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
11(* Common synonyms.                                                           *)
12(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
13
14ndefinition BitVector ≝ λn: Nat. Vector Bool n.
15ndefinition Bit ≝ BitVector (S Z).
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)))))))))))))))).
20
21(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
22(* Creating bitvectors from scratch.                                          *)
23(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
24
25ndefinition zero ≝
26  λn: Nat.
27    replicate Bool n False.
28   
29ndefinition max ≝
30  λn: Nat.
31    replicate Bool n True.
32   
33ndefinition append ≝
34  λm, n: Nat.
35  λb: BitVector m.
36  λc: BitVector n.
37    append Bool m n b c.
38
39ndefinition pad ≝
40  λm, n: Nat.
41  λb: BitVector n.
42    let padding ≝ replicate Bool m False in
43      append Bool m n padding b.
44
45(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
46(* Logical operations.                                                        *)
47(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
48   
49ndefinition conjunction ≝
50  λn: Nat.
51  λb: BitVector n.
52  λc: BitVector n.
53    zip Bool Bool Bool n conjunction b c.
54   
55ndefinition inclusive_disjunction ≝
56  λn: Nat.
57  λb: BitVector n.
58  λc: BitVector n.
59    zip Bool Bool Bool n inclusive_disjunction b c.
60         
61ndefinition exclusive_disjunction ≝
62  λn: Nat.
63  λb: BitVector n.
64  λc: BitVector n.
65    zip Bool Bool Bool n exclusive_disjunction b c.
66   
67ndefinition complement ≝
68  λn: Nat.
69  λb: BitVector n.
70    map Bool Bool n (negation) b.
71
72(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
73(* Rotates and shifts.                                                        *)
74(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
75
76ndefinition rotate_left ≝
77  λm, n: Nat.
78  λb: BitVector n.
79    rotate_left Bool n m b.
80
81ndefinition rotate_right ≝
82  λm, n: Nat.
83  λb: BitVector n.
84    rotate_right Bool n m b.   
85   
86(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
87(* Conversions to and from lists and natural numbers.                         *)
88(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
89
90ndefinition list_of_bitvector ≝
91  λn: Nat.
92  λb: BitVector n.
93    list_of_vector Bool n b.
94   
95ndefinition bitvector_of_list ≝
96  λl: List Bool.
97    vector_of_list Bool l.
98
99nlet rec bitvector_of_nat_aux (n: Nat) on n ≝
100  let divrem ≝ divide_with_remainder n (S (S Z)) in
101  let div ≝ first Nat Nat divrem in
102  let rem ≝ second Nat Nat divrem in
103    match div with
104      [ Z ⇒
105        match rem with
106          [ Z ⇒ Empty Bool
107          | S r ⇒ ? (True :: (bitvector_of_nat_aux Z))
108          ]
109      | S d ⇒
110        match rem with
111          [ Z ⇒ ? (False :: (bitvector_of_nat_aux (S d)))
112          | S r ⇒ ? (True :: (bitvector_of_nat_aux (S d)))
113          ]
114      ].
115      //.
116nqed.
117
118ndefinition bitvector_of_nat ≝
119  λm, n: Nat.
120    let biglist ≝ reverse Bool (bitvector_of_nat_aux m) in
121    let size ≝ length Bool biglist in
122    let bitvector ≝ bitvector_of_list biglist in
123    let difference ≝ n - size in
124      pad difference size bitvector.
125
126nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
127  match b with
128    [ Empty ⇒ Z
129    | Cons o hd tl ⇒
130      let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in
131        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
132    ].
Note: See TracBrowser for help on using the repository browser.