Changeset 744 for src/Clight/Csyntax.ma
 Timestamp:
 Apr 7, 2011, 6:53:59 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Csyntax.ma
r725 r744 88 88  Tfloat: floatsize → type (**r floatingpoint types *) 89 89  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]]) *) 91 91  Tfunction: typelist → type → type (**r function types *) 92 92  Tstruct: ident → fieldlist → type (**r struct types *) … … 363 363 (* * Natural alignment of a type, in bytes. *) 364 364 (* 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 *)with365 let rec alignof (t: type) : nat ≝ 366 match t with 367 367 [ Tvoid ⇒ 1 368  Tint sz _ ⇒ match sz return λ_.Zwith [ I8 ⇒ 1  I16 ⇒ 2  I32 ⇒ 4 ]369  Tfloat sz ⇒ match sz return λ_.Zwith [ 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 ] 370 370  Tpointer _ _ ⇒ 4 371 371  Tarray _ t' n ⇒ alignof t' … … 376 376 ] 377 377 378 and alignof_fields (f: fieldlist) : Z≝378 and alignof_fields (f: fieldlist) : nat ≝ 379 379 match f with 380 380 [ Fnil ⇒ 1 381  Fcons id t f' ⇒ Zmax (alignof t) (alignof_fields f')381  Fcons id t f' ⇒ max (alignof t) (alignof_fields f') 382 382 ]. 383 383 … … 436 436 ∀f. alignof_fields f > 0. 437 437 @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. 440 439 441 440 lemma alignof_pos: 442 441 ∀t. alignof t > 0. 443 442 #t elim t; normalize; //; 444 [ 1,2: #z cases z; / /;443 [ 1,2: #z cases z; /2/; 445 444  3,4: #i @alignof_fields_pos 446 445 ] qed. … … 448 447 (* * Size of a type, in bytes. *) 449 448 450 let rec sizeof (t: type) : Z≝451 match t return λ_.Zwith449 let rec sizeof (t: type) : nat ≝ 450 match t with 452 451 [ Tvoid ⇒ 1 453  Tint i _ ⇒ match i return λ_.Zwith [ I8 ⇒ 1  I16 ⇒ 2  I32 ⇒ 4 ]454  Tfloat f ⇒ match f return λ_.Zwith [ 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 ] 455 454  Tpointer r _ ⇒ size_pointer r 456  Tarray _ t' n ⇒ sizeof t' * Zmax 1 n455  Tarray _ t' n ⇒ sizeof t' * max 1 n 457 456  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) 460 459  Tcomp_ptr r _ ⇒ size_pointer r 461 460 ] 462 461 463 and sizeof_struct (fld: fieldlist) (pos: Z) on fld : Z≝462 and sizeof_struct (fld: fieldlist) (pos: nat) on fld : nat ≝ 464 463 match fld with 465 464 [ Fnil ⇒ pos … … 467 466 ] 468 467 469 and sizeof_union (fld: fieldlist) : Z≝468 and sizeof_union (fld: fieldlist) : nat ≝ 470 469 match fld with 471 470 [ Fnil ⇒ 0 472  Fcons id t fld' ⇒ Zmax (sizeof t) (sizeof_union fld')471  Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld') 473 472 ]. 474 473 (* TODO: needs some Z_times results … … 518 517 Open Local Scope string_scope. 519 518 *) 520 let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)521 on fld : res Z≝519 let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat) 520 on fld : res nat ≝ 522 521 match fld with 523 522 [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
Note: See TracChangeset
for help on using the changeset viewer.