Changeset 961 for src/Clight/casts.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/Clight/casts.ma

    r824 r961  
    1 include "common/Integers.ma".
     1include "common/Values.ma".
    22
    33definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝
     
    55
    66lemma split_O_n : ∀A,n,x. split A O n x = 〈[[ ]], x〉.
    7 #A #n #x elim x //
     7#A #n cases n [ #x @(vector_inv_n … x) @refl | #m #x @(vector_inv_n … x) // ]
    88qed.
    99
     
    8282lemma truncate_tail : ∀m,n,v.
    8383  truncate (S m) n v = truncate m n (tail … v).
    84   //
     84#m #n #v @(vector_inv_n … v) #h #t >truncate_head @refl
    8585  qed.
    8686
     
    118118qed.
    119119
    120 definition sign_bit : ∀n. BitVector n → bool ≝
    121 λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
    122 
    123120definition sign : ∀m,n. BitVector m → BitVector (n+m) ≝
    124121λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
    125 
     122 
    126123lemma truncate_sign : ∀m,n,x.
    127124  truncate m n (sign … x) = x.
     
    178175#m #n #x @(vector_inv_n … x) #h #t elim n
    179176[ @refl
    180 | #n' #IH >sign_vcons whd in ⊢ (??%?) >IH @refl
     177| #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?) >IH @refl
    181178] qed.
    182179
Note: See TracChangeset for help on using the changeset viewer.