Changeset 744 for src/Clight/Csyntax.ma


Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (9 years ago)
Author:
campbell
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csyntax.ma

    r725 r744  
    8888  | Tfloat: floatsize → type            (**r floating-point types *)
    8989  | Tpointer: region → type → type      (**r pointer types ([*ty]) *)
    90   | Tarray: region → type → Z → type    (**r array types ([ty[len]]) *)
     90  | Tarray: region → type → nat → type  (**r array types ([ty[len]]) *)
    9191  | Tfunction: typelist → type → type   (**r function types *)
    9292  | Tstruct: ident → fieldlist → type   (**r struct types *)
     
    363363(* * Natural alignment of a type, in bytes. *)
    364364(* FIXME: these are old values for 32 bit machines *)
    365 let rec alignof (t: type) : Z
    366   match t return λ_.Z (* XXX appears to infer nat otherwise *) with
     365let rec alignof (t: type) : nat
     366  match t with
    367367  [ Tvoid ⇒ 1
    368   | Tint sz _ ⇒ match sz return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    369   | Tfloat sz ⇒ match sz return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
     368  | Tint sz _ ⇒ match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
     369  | Tfloat sz ⇒ match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    370370  | Tpointer _ _ ⇒ 4
    371371  | Tarray _ t' n ⇒ alignof t'
     
    376376  ]
    377377
    378 and alignof_fields (f: fieldlist) : Z
     378and alignof_fields (f: fieldlist) : nat
    379379  match f with
    380380  [ Fnil ⇒ 1
    381   | Fcons id t f' ⇒ Zmax (alignof t) (alignof_fields f')
     381  | Fcons id t f' ⇒ max (alignof t) (alignof_fields f')
    382382  ].
    383383
     
    436436  ∀f. alignof_fields f > 0.
    437437@fieldlist_ind //;
    438 #i #t #fs' #IH lapply (Zmax_r (alignof t) (alignof_fields fs'));
    439 @Zlt_to_Zle_to_Zlt //; qed.
     438#i #t #fs' #IH @max_r @IH qed.
    440439
    441440lemma alignof_pos:
    442441  ∀t. alignof t > 0.
    443442#t elim t; normalize; //;
    444 [ 1,2: #z cases z; //;
     443[ 1,2: #z cases z; /2/;
    445444| 3,4: #i @alignof_fields_pos
    446445] qed.
     
    448447(* * Size of a type, in bytes. *)
    449448
    450 let rec sizeof (t: type) : Z
    451   match t return λ_.Z with
     449let rec sizeof (t: type) : nat
     450  match t with
    452451  [ Tvoid ⇒ 1
    453   | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    454   | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
     452  | Tint i _ ⇒ match i with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
     453  | Tfloat f ⇒ match f with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    455454  | Tpointer r _ ⇒ size_pointer r
    456   | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n
     455  | Tarray _ t' n ⇒ sizeof t' * max 1 n
    457456  | Tfunction _ _ ⇒ 1
    458   | Tstruct _ fld ⇒ align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
    459   | Tunion _ fld ⇒ align (Zmax 1 (sizeof_union fld)) (alignof t)
     457  | Tstruct _ fld ⇒ align (max 1 (sizeof_struct fld 0)) (alignof t)
     458  | Tunion _ fld ⇒ align (max 1 (sizeof_union fld)) (alignof t)
    460459  | Tcomp_ptr r _ ⇒ size_pointer r
    461460  ]
    462461
    463 and sizeof_struct (fld: fieldlist) (pos: Z) on fld : Z
     462and sizeof_struct (fld: fieldlist) (pos: nat) on fld : nat
    464463  match fld with
    465464  [ Fnil ⇒ pos
     
    467466  ]
    468467
    469 and sizeof_union (fld: fieldlist) : Z
     468and sizeof_union (fld: fieldlist) : nat
    470469  match fld with
    471470  [ Fnil ⇒ 0
    472   | Fcons id t fld' ⇒ Zmax (sizeof t) (sizeof_union fld')
     471  | Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld')
    473472  ].
    474473(* TODO: needs some Z_times results
     
    518517Open Local Scope string_scope.
    519518*)
    520 let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
    521                               on fld : res Z
     519let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat)
     520                              on fld : res nat
    522521  match fld with
    523522  [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
Note: See TracChangeset for help on using the changeset viewer.