Changeset 961 for src/ASM


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

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

Location:
src/ASM
Files:
3 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
  • src/ASM/BitVector.ma

    r868 r961  
    110110#Q * *; normalize /3/
    111111qed.
     112
     113lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
     114@eq_v_true * @refl
     115qed.
     116
     117lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
     118#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
     119qed.
    112120   
    113121axiom bitvector_of_string:
  • src/ASM/Vector.ma

    r889 r961  
    477477] qed.
    478478
     479lemma eq_v_true : ∀A,f. (∀a. f a a = true) → ∀n,v. eq_v A n f v v = true.
     480#A #f #f_true #n #v elim v
     481[ //
     482| #m #h #t #IH whd in ⊢ (??%%) >f_true >IH @refl
     483] qed.
     484
     485lemma vector_neq_tail : ∀A,n,h. ∀t,t':Vector A n. h:::t≠h:::t' → t ≠ t'.
     486#A #n #h #t #t' * #NE % #E @NE >E @refl
     487qed.
     488
     489lemma  eq_v_false : ∀A,f. (∀a,a'. f a a' = true → a = a') → ∀n,v,v'. v≠v' → eq_v A n f v v' = false.
     490#A #f #f_true #n elim n
     491[ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl
     492| #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t'
     493  #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE /2/
     494] qed.
     495
    479496(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    480497(* Subvectors.                                                                *)
Note: See TracChangeset for help on using the changeset viewer.