Changeset 2176 for src/Clight/Csyntax.ma
 Timestamp:
 Jul 12, 2012, 1:28:28 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Csyntax.ma
r1920 r2176 65 65  Tint: intsize → signedness → type (**r integer types *) 66 66  Tfloat: floatsize → type (**r floatingpoint types *) 67  Tpointer: region →type → type (**r pointer types ([*ty]) *)68  Tarray: region →type → nat → type (**r array types ([ty[len]]) *)67  Tpointer: (*region →*) type → type (**r pointer types ([*ty]) *) 68  Tarray: (*region →*) type → nat → type (**r array types ([ty[len]]) *) 69 69  Tfunction: typelist → type → type (**r function types *) 70 70  Tstruct: ident → fieldlist → type (**r struct types *) 71 71  Tunion: ident → fieldlist → type (**r union types *) 72  Tcomp_ptr: region →ident → type (**r pointer to named struct or union *)72  Tcomp_ptr: (*region →*) ident → type (**r pointer to named struct or union *) 73 73 74 74 with typelist : Type[0] ≝ … … 86 86 (it:∀i,s. P (Tint i s)) 87 87 (fl:∀f. P (Tfloat f)) 88 (pt:∀ s,t. P t → P (Tpointer st))89 (ar:∀ s,t,n. P t → P (Tarray st n))88 (pt:∀t. P t → P (Tpointer t)) 89 (ar:∀t,n. P t → P (Tarray t n)) 90 90 (fn:∀tl,t. P t → P (Tfunction tl t)) 91 91 (st:∀i,fl. P (Tstruct i fl)) 92 92 (un:∀i,fl. P (Tunion i fl)) 93 (cp:∀ rg,i. P (Tcomp_ptr rgi))93 (cp:∀i. P (Tcomp_ptr i)) 94 94 (t:type) on t : P t ≝ 95 95 match t return λt'.P t' with … … 97 97  Tint i s ⇒ it i s 98 98  Tfloat s ⇒ fl s 99  Tpointer s t' ⇒ pt st' (type_ind P vo it fl pt ar fn st un cp t')100  Tarray s t' n ⇒ ar st' n (type_ind P vo it fl pt ar fn st un cp t')99  Tpointer t' ⇒ pt t' (type_ind P vo it fl pt ar fn st un cp t') 100  Tarray t' n ⇒ ar t' n (type_ind P vo it fl pt ar fn st un cp t') 101 101  Tfunction tl t' ⇒ fn tl t' (type_ind P vo it fl pt ar fn st un cp t') 102 102  Tstruct i fs ⇒ st i fs 103 103  Tunion i fs ⇒ un i fs 104  Tcomp_ptr rg i ⇒ cp rgi104  Tcomp_ptr i ⇒ cp i 105 105 ]. 106 106 … … 350 350 351 351 (* * Natural alignment of a type, in bytes. *) 352 (* FIXME: these are old values for 32 bit machines *) 353 let rec alignof (t: type) : nat ≝ 352 let rec alignof (t: type) : nat ≝ (*1*) 353 (* these are old values for 32 bit machines *) 354 354 match t with 355 355 [ Tvoid ⇒ 1 356 356  Tint sz _ ⇒ match sz with [ I8 ⇒ 1  I16 ⇒ 2  I32 ⇒ 4 ] 357 357  Tfloat sz ⇒ match sz with [ F32 ⇒ 4  F64 ⇒ 8 ] 358  Tpointer _ _⇒ 4359  Tarray _t' n ⇒ alignof t'358  Tpointer _ ⇒ 4 359  Tarray t' n ⇒ alignof t' 360 360  Tfunction _ _ ⇒ 1 361 361  Tstruct _ fld ⇒ alignof_fields fld 362 362  Tunion _ fld ⇒ alignof_fields fld 363  Tcomp_ptr _ _⇒ 4363  Tcomp_ptr _ ⇒ 4 364 364 ] 365 365 … … 381 381 (it:∀i,s. P (Tint i s)) 382 382 (fl:∀f. P (Tfloat f)) 383 (pt:∀ s,t. P t → P (Tpointer st))384 (ar:∀ s,t,n. P t → P (Tarray st n))383 (pt:∀t. P t → P (Tpointer t)) 384 (ar:∀t,n. P t → P (Tarray t n)) 385 385 (fn:∀tl,t. P t → P (Tfunction tl t)) 386 386 (st:∀i,fl. Q fl → P (Tstruct i fl)) 387 387 (un:∀i,fl. Q fl → P (Tunion i fl)) 388 (cp:∀ r,i. P (Tcomp_ptrr i))388 (cp:∀i. P (Tcomp_ptr i)) 389 389 (nl:Q Fnil) 390 390 (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f')) … … 394 394  Tint i s ⇒ it i s 395 395  Tfloat s ⇒ fl s 396  Tpointer s t' ⇒ pt st' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')397  Tarray s t' n ⇒ ar st' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')396  Tpointer t' ⇒ pt t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t') 397  Tarray t' n ⇒ ar t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t') 398 398  Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t') 399 399  Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs) 400 400  Tunion i fs ⇒ un i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs) 401  Tcomp_ptr r i ⇒ cp ri401  Tcomp_ptr i ⇒ cp i 402 402 ] 403 403 and fieldlist_ind2 … … 406 406 (it:∀i,s. P (Tint i s)) 407 407 (fl:∀f. P (Tfloat f)) 408 (pt:∀ s,t. P t → P (Tpointer st))409 (ar:∀ s,t,n. P t → P (Tarray st n))408 (pt:∀t. P t → P (Tpointer t)) 409 (ar:∀t,n. P t → P (Tarray t n)) 410 410 (fn:∀tl,t. P t → P (Tfunction tl t)) 411 411 (st:∀i,fl. Q fl → P (Tstruct i fl)) 412 412 (un:∀i,fl. Q fl → P (Tunion i fl)) 413 (cp:∀ r,i. P (Tcomp_ptrr i))413 (cp:∀i. P (Tcomp_ptr i)) 414 414 (nl:Q Fnil) 415 415 (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f')) … … 440 440  Tint i _ ⇒ match i with [ I8 ⇒ 1  I16 ⇒ 2  I32 ⇒ 4 ] 441 441  Tfloat f ⇒ match f with [ F32 ⇒ 4  F64 ⇒ 8 ] 442  Tpointer r _ ⇒ size_pointer r443  Tarray _t' n ⇒ sizeof t' * max 1 n442  Tpointer _ ⇒ size_pointer 443  Tarray t' n ⇒ sizeof t' * max 1 n 444 444  Tfunction _ _ ⇒ 1 445 445  Tstruct _ fld ⇒ align (max 1 (sizeof_struct fld 0)) (alignof t) 446 446  Tunion _ fld ⇒ align (max 1 (sizeof_union fld)) (alignof t) 447  Tcomp_ptr r _ ⇒ size_pointer r447  Tcomp_ptr _ ⇒ size_pointer 448 448 ] 449 449 … … 611 611  Tint sz sg ⇒ ASTint sz sg 612 612  Tfloat sz ⇒ ASTfloat sz 613  Tpointer r _ ⇒ ASTptrr614  Tarray r _ _ ⇒ ASTptrr615  Tfunction _ _ ⇒ ASTptr Code616  Tcomp_ptr r _ ⇒ ASTptrr613  Tpointer _ ⇒ ASTptr 614  Tarray _ _ ⇒ ASTptr 615  Tfunction _ _ ⇒ ASTptr 616  Tcomp_ptr _ ⇒ ASTptr 617 617  _ ⇒ ASTint I32 Unsigned (* structs and unions shouldn't be converted? *) 618 618 ]. … … 623 623  Tint sz sg ⇒ Some ? (ASTint sz sg) 624 624  Tfloat sz ⇒ Some ? (ASTfloat sz) 625  Tpointer r _ ⇒ Some ? (ASTptr r)626  Tarray r _ _ ⇒ Some ? (ASTptr r)627  Tfunction _ _ ⇒ Some ? (ASTptr Code)628  Tcomp_ptr r _ ⇒ Some ? (ASTptr r)625  Tpointer _ ⇒ Some ? ASTptr 626  Tarray _ _ ⇒ Some ? ASTptr 627  Tfunction _ _ ⇒ Some ? ASTptr 628  Tcomp_ptr _ ⇒ Some ? ASTptr 629 629  _ ⇒ None ? (* structs and unions shouldn't be converted? *) 630 630 ]. … … 651 651 inductive mode: typ → Type[0] ≝ 652 652  By_value: ∀t:typ. mode t 653  By_reference: ∀r:region. mode (ASTptr r)653  By_reference: (*∀r:region.*) mode ASTptr 654 654  By_nothing: ∀t. mode t. 655 655 … … 659 659  Tfloat sz ⇒ By_value (ASTfloat sz) 660 660  Tvoid ⇒ By_nothing … 661  Tpointer r _ ⇒ By_value (ASTptr r)662  Tarray r _ _ ⇒ By_reference r663  Tfunction _ _ ⇒ By_reference Code661  Tpointer _ ⇒ By_value ASTptr 662  Tarray _ _ ⇒ By_reference 663  Tfunction _ _ ⇒ By_reference 664 664  Tstruct _ fList ⇒ By_nothing … 665 665  Tunion _ fList ⇒ By_nothing … 666  Tcomp_ptr r _ ⇒ By_value (ASTptr r)666  Tcomp_ptr _ ⇒ By_value ASTptr 667 667 ]. 668 668
Note: See TracChangeset
for help on using the changeset viewer.