Changeset 961 for src/ASM/Arithmetic.ma
 Timestamp:
 Jun 15, 2011, 4:15:52 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r949 r961 344 344 λb, c: BitVector n. 345 345 full_add n b c false. 346 347 definition sign_bit : ∀n. BitVector n → bool ≝ 348 λn,v. match v with [ VEmpty ⇒ false  VCons _ h _ ⇒ h ]. 349 350 definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝ 351 λm,n,v. pad_vector ? (sign_bit ? v) ?? v. 352 353 definition zero_ext : ∀m,n. BitVector m → BitVector n ≝ 354 λm,n. 355 match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with 356 [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v) 357  nat_eq n' ⇒ λv. v 358  nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v)) 359 ]. 360 361 definition sign_ext : ∀m,n. BitVector m → BitVector n ≝ 362 λm,n. 363 match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with 364 [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v) 365  nat_eq n' ⇒ λv. v 366  nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v)) 367 ]. 368
Note: See TracChangeset
for help on using the changeset viewer.