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 floating-point 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.