Changeset 961 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r949 r961  
    344344  λb, c: BitVector n.
    345345    full_add n b c false.
     346
     347definition sign_bit : ∀n. BitVector n → bool ≝
     348λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
     349
     350definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
     351λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
     352
     353definition 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
     361definition 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.