Changeset 237 for Deliverables/D4.1/Matita/BitVector.ma
- Timestamp:
- Nov 12, 2010, 4:51:45 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/BitVector.ma
r236 r237 23 23 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 24 24 25 (* @name: zero26 @desc: Produces a bitvector containing <tt>n</tt> copies of <tt>False</tt>.27 *)28 25 ndefinition zero ≝ 29 26 λn: Nat. … … 34 31 replicate Bool n True. 35 32 36 ndefinition append ≝ append. 33 ndefinition append ≝ 34 λm, n: Nat. 35 λb: BitVector m. 36 λc: BitVector n. 37 append Bool m n b c. 38 39 ndefinition pad ≝ 40 λm, n: Nat. 41 λb: BitVector n. 42 let padding ≝ replicate Bool m False in 43 append Bool m n padding b. 37 44 38 45 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 40 47 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 41 48 42 (*43 @name: conjunction44 @desc: The logical conjunction of two bitvectors of length <tt>n</tt>.45 *)46 49 ndefinition conjunction ≝ 47 50 λn: Nat. … … 49 52 λc: BitVector n. 50 53 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 *) 54 57 55 ndefinition inclusive_disjunction ≝ 58 56 λn: Nat. … … 60 58 λc: BitVector n. 61 59 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 *) 60 68 61 ndefinition exclusive_disjunction ≝ 69 62 λn: Nat. … … 72 65 zip Bool Bool Bool n exclusive_disjunction b c. 73 66 74 (*75 @name: complement76 @desc: The logical complement of a bitvector of length <tt>n</tt>.77 *)78 67 ndefinition complement ≝ 79 68 λn: Nat. … … 85 74 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 86 75 87 ndefinition divide_with_remainder ≝ 88 λm, n: Nat. 89 mk_Cartesian Nat Nat (m ÷ n) (modulus m n). 76 ndefinition list_of_bitvector ≝ 77 λn: Nat. 78 λb: BitVector n. 79 list_of_vector Bool n b. 90 80 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 *) 95 ndefinition pad ≝ 96 λm, n: Nat. 97 λb: BitVector n. 98 let padding ≝ replicate Bool m False in 99 append Bool m n padding b. 81 ndefinition bitvector_of_list ≝ 82 λl: List Bool. 83 vector_of_list Bool l. 100 84 101 85 nlet rec bitvector_of_nat_aux (n: Nat) on n ≝ 102 let div _rem ≝ divide_with_remainder n (S (S Z)) in103 let div ≝ first Nat Nat div _rem in104 let rem ≝ second Nat Nat div _rem in86 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 105 89 match div with 106 90 [ Z ⇒ 107 91 match rem with 108 92 [ Z ⇒ Empty Bool 109 | S r ⇒ True :: (bitvector_of_nat_aux Z)93 | S r ⇒ ? (True :: (bitvector_of_nat_aux Z)) 110 94 ] 111 95 | S d ⇒ 112 96 match rem with 113 [ Z ⇒ False :: (bitvector_of_nat_aux (S d))114 | S r ⇒ True :: (bitvector_of_nat_aux (S d))97 [ Z ⇒ ? (False :: (bitvector_of_nat_aux (S d))) 98 | S r ⇒ ? (True :: (bitvector_of_nat_aux (S d))) 115 99 ] 116 100 ]. 101 //. 102 nqed. 117 103 118 (* @name: bitvector_of_nat119 @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 *)122 104 ndefinition bitvector_of_nat ≝ 123 105 λm, n: Nat. 124 106 let biglist ≝ reverse Bool (bitvector_of_nat_aux m) in 125 107 let size ≝ length Bool biglist in 126 let b vector ≝ bitvector_of_list Boolbiglist in108 let bitvector ≝ bitvector_of_list biglist in 127 109 let difference ≝ n - size in 128 pad difference size bvector. 129 130 ndefinition list_of_bitvector ≝ list_of_vector. 131 ndefinition bitvector_of_list ≝ vector_of_list. 110 pad difference size bitvector. 111 112 nlet 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 TracChangeset
for help on using the changeset viewer.