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

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

More functions on bitvectors written.

File size: 3.7 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(* Conversions to and from lists and natural numbers.                         *)
74(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
75
76ndefinition list_of_bitvector ≝
77  λn: Nat.
78  λb: BitVector n.
79    list_of_vector Bool n b.
80   
81ndefinition bitvector_of_list ≝
82  λl: List Bool.
83    vector_of_list Bool l.
84
85nlet rec bitvector_of_nat_aux (n: Nat) on n ≝
86  let divrem ≝ divide_with_remainder n (S (S Z)) in
87  let div ≝ first Nat Nat divrem in
88  let rem ≝ second Nat Nat divrem in
89    match div with
90      [ Z ⇒
91        match rem with
92          [ Z ⇒ Empty Bool
93          | S r ⇒ ? (True :: (bitvector_of_nat_aux Z))
94          ]
95      | S d ⇒
96        match rem with
97          [ Z ⇒ ? (False :: (bitvector_of_nat_aux (S d)))
98          | S r ⇒ ? (True :: (bitvector_of_nat_aux (S d)))
99          ]
100      ].
101      //.
102nqed.
103
104ndefinition bitvector_of_nat ≝
105  λm, n: Nat.
106    let biglist ≝ reverse Bool (bitvector_of_nat_aux m) in
107    let size ≝ length Bool biglist in
108    let bitvector ≝ bitvector_of_list biglist in
109    let difference ≝ n - size in
110      pad difference size bitvector.
111
112nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
113  match b with
114    [ Empty ⇒ Z
115    | Cons o hd tl ⇒
116      let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in
117        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
118    ].
Note: See TracBrowser for help on using the repository browser.