Changeset 744 for src/ASM/Arithmetic.ma
 Timestamp:
 Apr 7, 2011, 6:53:59 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r724 r744 149 149 λb, c: BitVector n. 150 150 addition_n n b (two_complement_negation n c). 151 152 definition multiplication ≝ 153 λn: nat. 154 λb, c: BitVector n. 155 let b_nat ≝ nat_of_bitvector ? b in 156 let c_nat ≝ nat_of_bitvector ? c in 157 let result ≝ b_nat * c_nat in 158 bitvector_of_nat (n + n) result. 159 160 definition division_u ≝ 161 λn: nat. 162 λb, c: BitVector n. 163 let b_nat ≝ nat_of_bitvector ? b in 164 let c_nat ≝ nat_of_bitvector ? c in 165 match c_nat with 166 [ O ⇒ None ? 167  _ ⇒ 168 let result ≝ b_nat ÷ c_nat in 169 Some ? (bitvector_of_nat n result) 151 152 let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝ 153 match b with 154 [ VEmpty ⇒ acc 155  VCons m' hd tl ⇒ 156 let acc' ≝ if hd then addition_n ? c acc else acc in 157 mult_aux m' n tl (shift_right_1 ?? c false) acc' 158 ]. 159 160 definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝ 161 λn: nat. 162 match n return λn.BitVector n → BitVector n → BitVector (n + n) with 163 [ O ⇒ λ_.λ_.[[ ]] 164  S m ⇒ 165 λb, c : BitVector (S m). 166 let c' ≝ pad (S m) (S m) c in 167 mult_aux ?? b (shift_left ?? m c' false) (zero ?) 168 ]. 169 170 (* Division: 001...000 divided by 000...010 171 Shift the divisor as far left as possible, 172 100...000 173 then try subtracting it at each 174 bit position, shifting left as we go. 175 001...000  100...000 X ⇒ 0 176 001...000  010...000 X ⇒ 0 177 001...000  001...000 Y ⇒ 1 (use subtracted value as new quotient) 178 ... 179 Then pad out the remaining bits at the front 180 00..001... 181 *) 182 inductive fbs_diff : nat → Type[0] ≝ 183  fbs_diff' : ∀n,m. fbs_diff (S (n+m)). 184 185 let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝ 186 match b return λn.λ_. option (fbs_diff n) with 187 [ VEmpty ⇒ None ? 188  VCons m h t ⇒ 189 if h then Some ? (fbs_diff' O m) 190 else match first_bit_set m t with 191 [ None ⇒ None ? 192  Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ] 193 ] 194 ]. 195 196 let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝ 197 match m with 198 [ O ⇒ 〈[[ ]], q〉 199  S m' ⇒ 200 let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in 201 let bit ≝ head' … flags in 202 let q'' ≝ if bit then q' else q in 203 let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in 204 〈bit:::tl, md〉 205 ]. 206 207 definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝ 208 λn: nat. 209 λb, c: BitVector (S n). 210 211 match first_bit_set ? c with 212 [ None ⇒ None ? 213  Some fbs' ⇒ 214 match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒ 215 let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in 216 Some ? 〈switch_bv_plus ??? (pad ?? d), m〉 217 ] 170 218 ]. 219 220 definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝ 221 λn,q,d. match divmod_u n q d with [ None ⇒ None ?  Some p ⇒ Some ? (\fst p) ]. 171 222 172 223 definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝ … … 177 228 let b_sign_bit ≝ get_index_v ? ? b O ? in 178 229 let c_sign_bit ≝ get_index_v ? ? c O ? in 179 let b_as_nat ≝ nat_of_bitvector ? b in 180 let c_as_nat ≝ nat_of_bitvector ? c in 181 match c_as_nat with 182 [ O ⇒ None ? 183  S o ⇒ 184 match b_sign_bit with 230 match b_sign_bit with 231 [ true ⇒ 232 let neg_b ≝ two_complement_negation ? b in 233 match c_sign_bit with 185 234 [ true ⇒ 186 let temp_b ≝ b_as_nat  (2^p) in 187 match c_sign_bit with 188 [ true ⇒ 189 let temp_c ≝ c_as_nat  (2^p) in 190 Some ? (bitvector_of_nat ? (temp_b ÷ temp_c)) 191  false ⇒ 192 let result ≝ (temp_b ÷ c_as_nat) + (2^p) in 193 Some ? (bitvector_of_nat ? result) 194 ] 235 (* I was worrying slightly about 2^(n1), whose negation can't 236 be represented in an n bit signed number. However, it's 237 negation comes out as 2^(n1) as an n bit *unsigned* number, 238 so it's fine. *) 239 division_u ? neg_b (two_complement_negation ? c) 195 240  false ⇒ 196 match c_sign_bit with 197 [ true ⇒ 198 let temp_c ≝ c_as_nat  (2^p) in 199 let result ≝ (b_as_nat ÷ temp_c) + (2^p) in 200 Some ? (bitvector_of_nat ? result) 201  false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat)) 202 ] 241 match division_u ? neg_b c with 242 [ None ⇒ None ? 243  Some r ⇒ Some ? (two_complement_negation ? r) 244 ] 245 ] 246  false ⇒ 247 match c_sign_bit with 248 [ true ⇒ 249 match division_u ? b (two_complement_negation ? c) with 250 [ None ⇒ None ? 251  Some r ⇒ Some ? (two_complement_negation ? r) 252 ] 253  false ⇒ division_u ? b c 203 254 ] 204 255 ] 205 256 ]. 206 257 // 207 258 qed. 208 259 209 definition modulus_u ≝ 210 λn. 211 λb, c: BitVector n. 212 let b_nat ≝ nat_of_bitvector ? b in 213 let c_nat ≝ nat_of_bitvector ? c in 214 match c_nat with 215 [ O ⇒ None ? 216  _ ⇒ 217 let result ≝ modulus b_nat c_nat in 218 Some ? (bitvector_of_nat n result) 219 ]. 260 definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝ 261 λn,q,d. match divmod_u n q d with [ None ⇒ None ?  Some p ⇒ Some ? (\snd p) ]. 220 262 221 263 definition modulus_s ≝
Note: See TracChangeset
for help on using the changeset viewer.