Changeset 240 for Deliverables/D4.1/Matita/BitVector.ma
 Timestamp:
 Nov 15, 2010, 10:22:41 AM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r238 r240 1 1 (* ===================================== *) 2 2 (* BitVector.ma: Fixed length bitvectors, and common operations on them. *) 3 (* ===================================== *) 4 5 include "Vector.ma". 6 include "List.ma". 7 include "Nat.ma". 8 include "Bool.ma". 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 8 include "Universes/Universes.ma". 9 10 include "Datatypes/Listlike/Vector/Vector.ma". 11 include "Datatypes/Listlike/List/List.ma". 12 13 include "Datatypes/Nat/Nat.ma". 14 include "Datatypes/Nat/Addition.ma". 15 include "Datatypes/Nat/Division_Modulus.ma". 16 include "Datatypes/Nat/Exponential.ma". 17 18 include "Datatypes/Bool.ma". 9 19 10 20 (* ===================================== *) … … 20 30 21 31 (* ===================================== *) 32 (* Lookup. *) 33 (* ===================================== *) 34 35 ndefinition get_index ≝ 36 λn: Nat. 37 λb: BitVector n. 38 λm: Nat. 39 get_index Bool n b m. 40 41 interpretation "BitVector get_index" 'get_index b n = (get_index ? b n). 42 43 ndefinition set_index ≝ 44 λn: Nat. 45 λb: BitVector n. 46 λm: Nat. 47 set_index Bool n b m. 48 49 ndefinition drop ≝ 50 λn: Nat. 51 λb: BitVector n. 52 λm: Nat. 53 drop Bool n b m. 54 55 (* ===================================== *) 22 56 (* Creating bitvectors from scratch. *) 23 57 (* ===================================== *) … … 36 70 λc: BitVector n. 37 71 append Bool m n b c. 72 73 interpretation "BitVector append" 'append b c = (append b c). 38 74 39 75 ndefinition pad ≝ … … 42 78 let padding ≝ replicate Bool m False in 43 79 append Bool m n padding b. 80 81 (* ===================================== *) 82 (* Other manipulations. *) 83 (* ===================================== *) 84 85 ndefinition reverse ≝ 86 λn: Nat. 87 λb: BitVector n. 88 reverse Bool n b. 89 90 ndefinition length ≝ 91 λn: Nat. 92 λb: BitVector n. 93 length Bool n b. 44 94 45 95 (* ===================================== *) … … 51 101 λb: BitVector n. 52 102 λc: BitVector n. 53 zip Bool Bool Bool n conjunction b c. 103 zip_with Bool Bool Bool n conjunction b c. 104 105 interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c). 54 106 55 107 ndefinition inclusive_disjunction ≝ … … 57 109 λb: BitVector n. 58 110 λc: BitVector n. 59 zip Bool Bool Bool n inclusive_disjunction b c. 111 zip_with Bool Bool Bool n inclusive_disjunction b c. 112 113 interpretation "BitVector inclusive disjunction" 114 'inclusive_disjunction b c = (inclusive_disjunction ? b c). 60 115 61 116 ndefinition exclusive_disjunction ≝ … … 63 118 λb: BitVector n. 64 119 λc: BitVector n. 65 zip Bool Bool Bool n exclusive_disjunction b c. 66 67 ndefinition complement ≝ 120 zip_with Bool Bool Bool n exclusive_disjunction b c. 121 122 interpretation "BitVector exclusive disjunction" 123 'exclusive_disjunction b c = (exclusive_disjunction ? b c). 124 125 ndefinition negation ≝ 68 126 λn: Nat. 69 127 λb: BitVector n. 70 128 map Bool Bool n (negation) b. 129 130 interpretation "BitVector negation" 'negation b c = (negation ? b c). 71 131 72 132 (* ===================================== *) … … 82 142 λm, n: Nat. 83 143 λb: BitVector n. 84 rotate_right Bool n m b. 144 rotate_right Bool n m b. 145 146 ndefinition shift_left ≝ 147 λm, n: Nat. 148 λb: BitVector n. 149 λc: Bool. 150 shift_left Bool n m b c. 151 152 ndefinition shift_right ≝ 153 λm, n: Nat. 154 λb: BitVector n. 155 λc: Bool. 156 shift_right Bool n m b c. 85 157 86 158 (* ===================================== *) … … 129 201  Cons o hd tl ⇒ 130 202 let hdval ≝ match hd with [ True ⇒ S Z  False ⇒ Z ] in 131 ((exponential (S (S Z)) o) *hdval) + nat_of_bitvector o tl203 ((exponential (S (S Z)) o) × hdval) + nat_of_bitvector o tl 132 204 ].
Note: See TracChangeset
for help on using the changeset viewer.