Changeset 124 for C-semantics/Csyntax.ma
- Timestamp:
- Sep 24, 2010, 10:31:32 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/Csyntax.ma
r24 r124 46 46 | F32: floatsize 47 47 | F64: floatsize. 48 49 (* Pointers can point to particular memory spaces. *) 50 ninductive mem_space : Type ≝ 51 | Generic : mem_space 52 | Data : mem_space 53 | IData : mem_space 54 | XData : mem_space 55 | Code : mem_space. 48 56 49 57 (* * The syntax of type expressions. Some points to note: … … 86 94 | Tint: intsize → signedness → type (**r integer types *) 87 95 | Tfloat: floatsize → type (**r floating-point types *) 88 | Tpointer: type → type(**r pointer types ([*ty]) *)89 | Tarray: type → Z → type(**r array types ([ty[len]]) *)96 | Tpointer: mem_space → type → type (**r pointer types ([*ty]) *) 97 | Tarray: mem_space → type → Z → type (**r array types ([ty[len]]) *) 90 98 | Tfunction: typelist → type → type (**r function types *) 91 99 | Tstruct: ident → fieldlist → type (**r struct types *) … … 107 115 (it:∀i,s. P (Tint i s)) 108 116 (fl:∀f. P (Tfloat f)) 109 (pt:∀ t. P t → P (Tpointert))110 (ar:∀ t,n. P t → P (Tarrayt n))117 (pt:∀s,t. P t → P (Tpointer s t)) 118 (ar:∀s,t,n. P t → P (Tarray s t n)) 111 119 (fn:∀tl,t. P t → P (Tfunction tl t)) 112 120 (st:∀i,fl. P (Tstruct i fl)) … … 118 126 | Tint i s ⇒ it i s 119 127 | Tfloat s ⇒ fl s 120 | Tpointer t' ⇒ ptt' (type_ind P vo it fl pt ar fn st un cp t')121 | Tarray t' n ⇒ art' n (type_ind P vo it fl pt ar fn st un cp t')128 | Tpointer s t' ⇒ pt s t' (type_ind P vo it fl pt ar fn st un cp t') 129 | Tarray s t' n ⇒ ar s t' n (type_ind P vo it fl pt ar fn st un cp t') 122 130 | Tfunction tl t' ⇒ fn tl t' (type_ind P vo it fl pt ar fn st un cp t') 123 131 | Tstruct i fs ⇒ st i fs … … 357 365 | Tint sz _ ⇒ match sz return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ] 358 366 | Tfloat sz ⇒ match sz return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ] 359 | Tpointer _ ⇒ 4360 | Tarray t' n ⇒ alignof t'367 | Tpointer _ _ ⇒ 4 368 | Tarray _ t' n ⇒ alignof t' 361 369 | Tfunction _ _ ⇒ 1 362 370 | Tstruct _ fld ⇒ alignof_fields fld … … 382 390 (it:∀i,s. P (Tint i s)) 383 391 (fl:∀f. P (Tfloat f)) 384 (pt:∀ t. P t → P (Tpointert))385 (ar:∀ t,n. P t → P (Tarrayt n))392 (pt:∀s,t. P t → P (Tpointer s t)) 393 (ar:∀s,t,n. P t → P (Tarray s t n)) 386 394 (fn:∀tl,t. P t → P (Tfunction tl t)) 387 395 (st:∀i,fl. Q fl → P (Tstruct i fl)) … … 395 403 | Tint i s ⇒ it i s 396 404 | Tfloat s ⇒ fl s 397 | Tpointer t' ⇒ ptt' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')398 | Tarray t' n ⇒ art' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')405 | Tpointer s t' ⇒ pt s t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t') 406 | Tarray s t' n ⇒ ar s t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t') 399 407 | Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t') 400 408 | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs) … … 407 415 (it:∀i,s. P (Tint i s)) 408 416 (fl:∀f. P (Tfloat f)) 409 (pt:∀ t. P t → P (Tpointert))410 (ar:∀ t,n. P t → P (Tarrayt n))417 (pt:∀s,t. P t → P (Tpointer s t)) 418 (ar:∀s,t,n. P t → P (Tarray s t n)) 411 419 (fn:∀tl,t. P t → P (Tfunction tl t)) 412 420 (st:∀i,fl. Q fl → P (Tstruct i fl)) … … 442 450 | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ] 443 451 | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ] 444 | Tpointer _ ⇒ 4445 | Tarray t' n ⇒ sizeof t' * Zmax 1 n452 | Tpointer _ _ ⇒ 4 453 | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n 446 454 | Tfunction _ _ ⇒ 1 447 455 | Tstruct _ fld ⇒ align (Zmax 1 (sizeof_struct fld 0)) (alignof t) … … 631 639 | F64 ⇒ By_value Mfloat64 ] 632 640 | Tvoid ⇒ By_nothing 633 | Tpointer _ ⇒ By_value Mint32634 | Tarray _ _ ⇒ By_reference641 | Tpointer _ _ ⇒ By_value Mint32 642 | Tarray _ _ _ ⇒ By_reference 635 643 | Tfunction _ _ ⇒ By_reference 636 644 | Tstruct _ fList ⇒ By_nothing … … 672 680 match ty2 with 673 681 [ Tint _ _ ⇒ add_case_ii 674 | Tpointer ty ⇒ add_case_ip ty675 | Tarray ty _ ⇒ add_case_ip ty682 | Tpointer _ ty ⇒ add_case_ip ty 683 | Tarray _ ty _ ⇒ add_case_ip ty 676 684 | _ ⇒ add_default ] 677 685 | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ add_case_ff | _ ⇒ add_default ] 678 | Tpointer ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]679 | Tarray ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]686 | Tpointer _ ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ] 687 | Tarray _ ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ] 680 688 | _ ⇒ add_default 681 689 ]. … … 704 712 [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ sub_case_ii | _ ⇒ sub_default ] 705 713 | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ sub_case_ff | _ ⇒ sub_default ] 706 | Tpointer ty ⇒714 | Tpointer _ ty ⇒ 707 715 match ty2 with 708 716 [ Tint _ _ ⇒ sub_case_pi ty 709 | Tpointer _ ⇒ sub_case_pp ty710 | Tarray _ _ ⇒ sub_case_pp ty717 | Tpointer _ _ ⇒ sub_case_pp ty 718 | Tarray _ _ _ ⇒ sub_case_pp ty 711 719 | _ ⇒ sub_default ] 712 | Tarray ty _ ⇒720 | Tarray _ ty _ ⇒ 713 721 match ty2 with 714 722 [ Tint _ _ ⇒ sub_case_pi ty 715 | Tpointer _ ⇒ sub_case_pp ty716 | Tarray _ _ ⇒ sub_case_pp ty723 | Tpointer _ _ ⇒ sub_case_pp ty 724 | Tarray _ _ _ ⇒ sub_case_pp ty 717 725 | _ ⇒ sub_default ] 718 726 | _ ⇒ sub_default … … 831 839 | _ ⇒ cmp_default ] 832 840 | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff | _ ⇒ cmp_default ] 833 | Tpointer _ ⇒841 | Tpointer _ _ ⇒ 834 842 match ty2 with 835 843 [ Tint _ _ ⇒ cmp_case_ipip 836 | Tpointer _ ⇒ cmp_case_ipip837 | Tarray _ _ ⇒ cmp_case_ipip844 | Tpointer _ _ ⇒ cmp_case_ipip 845 | Tarray _ _ _ ⇒ cmp_case_ipip 838 846 | _ ⇒ cmp_default ] 839 | Tarray _ _ ⇒847 | Tarray _ _ _ ⇒ 840 848 match ty2 with 841 849 [ Tint _ _ ⇒ cmp_case_ipip 842 | Tpointer _ ⇒ cmp_case_ipip843 | Tarray _ _ ⇒ cmp_case_ipip850 | Tpointer _ _ ⇒ cmp_case_ipip 851 | Tarray _ _ _ ⇒ cmp_case_ipip 844 852 | _ ⇒ cmp_default ] 845 853 | _ ⇒ cmp_default … … 869 877 match ty with 870 878 [ Tfunction args res ⇒ fun_case_f args res 871 | Tpointer ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res872 | _ ⇒ fun_default873 ]879 | Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res 880 | _ ⇒ fun_default 881 ] 874 882 | _ ⇒ fun_default 875 883 ].
Note: See TracChangeset
for help on using the changeset viewer.