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

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

Strange problem with matita and the Maybe file? Cannot find Maybe.ng.

File size: 4.2 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
25(* @name: zero
26   @desc: Produces a bitvector containing <tt>n</tt> copies of <tt>False</tt>.
27*)
28ndefinition zero ≝
29  λn: Nat.
30    replicate Bool n False.
31   
32ndefinition max ≝
33  λn: Nat.
34    replicate Bool n True.
35   
36ndefinition append ≝ append.
37
38(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
39(* Logical operations.                                                        *)
40(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
41   
42(*
43 @name: conjunction
44 @desc: The logical conjunction of two bitvectors of length <tt>n</tt>.
45*)
46ndefinition conjunction ≝
47  λn: Nat.
48  λb: BitVector n.
49  λc: BitVector n.
50    zip Bool Bool Bool n conjunction b c.
51
52(*
53 @name: inclusive_disjunction
54 @desc: The logical inclusive disjunction of two bitvectors of length
55        <tt>n</tt>.
56*)   
57ndefinition inclusive_disjunction ≝
58  λn: Nat.
59  λb: BitVector n.
60  λc: BitVector n.
61    zip Bool Bool Bool n inclusive_disjunction b c.
62   
63(*
64 @name: exclusive_disjunction
65 @desc: The logical exclusive disjunction of two bitvectors of length
66        <tt>n</tt>.  (XOR).
67*)       
68ndefinition exclusive_disjunction ≝
69  λn: Nat.
70  λb: BitVector n.
71  λc: BitVector n.
72    zip Bool Bool Bool n exclusive_disjunction b c.
73   
74(*
75 @name: complement
76 @desc: The logical complement of a bitvector of length <tt>n</tt>.
77*)   
78ndefinition complement ≝
79  λn: Nat.
80  λb: BitVector n.
81    map Bool Bool n (negation) b.
82   
83(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
84(* Conversions to and from lists and natural numbers.                         *)
85(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
86
87ndefinition divide_with_remainder ≝
88  λm, n: Nat.
89    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
90   
91(* @name: pad
92   @desc: Pads the front of a bitvector of length <tt>n</tt> with <tt>m</tt>
93          copies of <tt>False</tt>.
94*)
95ndefinition pad ≝
96  λm, n: Nat.
97  λb: BitVector n.
98    let padding ≝ replicate Bool m False in
99      append Bool m n padding b.
100
101nlet rec bitvector_of_nat_aux (n: Nat) on n ≝
102  let div_rem ≝ divide_with_remainder n (S (S Z)) in
103  let div ≝ first Nat Nat div_rem in
104  let rem ≝ second Nat Nat div_rem in
105    match div with
106      [ Z ⇒
107        match rem with
108          [ Z ⇒ Empty Bool
109          | S r ⇒ True :: (bitvector_of_nat_aux Z)
110          ]
111      | S d ⇒
112        match rem with
113          [ Z ⇒ False :: (bitvector_of_nat_aux (S d))
114          | S r ⇒ True :: (bitvector_of_nat_aux (S d))
115          ]
116      ].
117
118(* @name: bitvector_of_nat
119   @desc: Constructs a bitvector whose integer value is the same as <tt>m</tt>.
120          Size of the resulting bitvector is clamped to <tt>n</tt>.
121*)
122ndefinition bitvector_of_nat ≝
123  λm, n: Nat.
124    let biglist ≝ reverse Bool (bitvector_of_nat_aux m) in
125    let size ≝ length Bool biglist in
126    let bvector ≝ bitvector_of_list Bool biglist in
127    let difference ≝ n - size in
128      pad difference size bvector.
129     
130ndefinition list_of_bitvector ≝ list_of_vector.
131ndefinition bitvector_of_list ≝ vector_of_list.
Note: See TracBrowser for help on using the repository browser.