Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (9 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Csyntax.ma

    r483 r487  
    3232  flag and a bit size: 8, 16 or 32 bits. *)
    3333
    34 ninductive signedness : Type
     34inductive signedness : Type[0]
    3535  | Signed: signedness
    3636  | Unsigned: signedness.
    3737
    38 ninductive intsize : Type
     38inductive intsize : Type[0]
    3939  | I8: intsize
    4040  | I16: intsize
     
    4444  and 64-bit (double precision). *)
    4545
    46 ninductive floatsize : Type
     46inductive floatsize : Type[0]
    4747  | F32: floatsize
    4848  | F64: floatsize.
     
    8383*)
    8484
    85 ninductive type : Type
     85inductive type : Type[0]
    8686  | Tvoid: type                         (**r the [void] type *)
    8787  | Tint: intsize → signedness → type   (**r integer types *)
     
    9494  | Tcomp_ptr: region → ident → type    (**r pointer to named struct or union *)
    9595
    96 with typelist : Type
     96with typelist : Type[0]
    9797  | Tnil: typelist
    9898  | Tcons: type → typelist → typelist
    9999
    100 with fieldlist : Type
     100with fieldlist : Type[0]
    101101  | Fnil: fieldlist
    102102  | Fcons: ident → type → fieldlist → fieldlist.
    103103
    104104(* XXX: no induction scheme! *)
    105 nlet rec type_ind
     105let rec type_ind
    106106  (P:type → Prop)
    107107  (vo:P Tvoid)
     
    127127  ].
    128128 
    129 nlet rec fieldlist_ind
     129let rec fieldlist_ind
    130130  (P:fieldlist → Prop)
    131131  (nl:P Fnil)
     
    141141(* * Arithmetic and logical operators. *)
    142142
    143 ninductive unary_operation : Type
     143inductive unary_operation : Type[0]
    144144  | Onotbool : unary_operation          (**r boolean negation ([!] in C) *)
    145145  | Onotint : unary_operation           (**r integer complement ([~] in C) *)
    146146  | Oneg : unary_operation.             (**r opposite (unary [-]) *)
    147147
    148 ninductive binary_operation : Type
     148inductive binary_operation : Type[0]
    149149  | Oadd : binary_operation             (**r addition (binary [+]) *)
    150150  | Osub : binary_operation             (**r subtraction (binary [-]) *)
     
    174174*)
    175175
    176 ninductive expr : Type
     176inductive expr : Type[0]
    177177  | Expr: expr_descr → type → expr
    178178
    179 with expr_descr : Type
     179with expr_descr : Type[0]
    180180  | Econst_int: int → expr_descr       (**r integer literal *)
    181181  | Econst_float: float → expr_descr   (**r float literal *)
     
    198198(* * Extract the type part of a type-annotated Clight expression. *)
    199199
    200 ndefinition typeof : expr → type ≝ λe.
     200definition typeof : expr → type ≝ λe.
    201201  match e with [ Expr de te ⇒ te ].
    202202
     
    208208  are not supported. *)
    209209
    210 ndefinition label ≝ ident.
    211 
    212 ninductive statement : Type
     210definition label ≝ ident.
     211
     212inductive statement : Type[0]
    213213  | Sskip : statement                   (**r do nothing *)
    214214  | Sassign : expr → expr → statement   (**r assignment [lvalue = rvalue] *)
     
    227227  | Scost : costlabel → statement → statement
    228228
    229 with labeled_statements : Type ≝            (**r cases of a [switch] *)
     229with labeled_statements : Type[0] ≝            (**r cases of a [switch] *)
    230230  | LSdefault: statement → labeled_statements
    231231  | LScase: int → statement → labeled_statements → labeled_statements.
    232232
    233 nlet rec statement_ind2
     233let rec statement_ind2
    234234  (P:statement → Prop) (Q:labeled_statements → Prop)
    235235  (Ssk:P Sskip)
     
    308308].
    309309
    310 ndefinition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo,Scs.
     310definition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo,Scs.
    311311  statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs
    312312  (λ_,_. I) (λ_,_,_,_,_.I).
     
    319319  function (a statement, [fn_body]). *)
    320320
    321 nrecord function : Type ≝ {
     321record function : Type[0] ≝ {
    322322  fn_return: type;
    323323  fn_params: list (ident × type);
     
    329329  external functions ([External]). *)
    330330
    331 ninductive fundef : Type
     331inductive fundef : Type[0]
    332332  | Internal: function → fundef
    333333  | External: ident → typelist → type → fundef.
     
    339339  data.  See module [AST] for more details. *)
    340340
    341 ndefinition clight_program : Type ≝ program fundef type.
     341definition clight_program : Type[0] ≝ program fundef type.
    342342
    343343(* * * Operations over types *)
     
    345345(* * The type of a function definition. *)
    346346
    347 nlet rec type_of_params (params: list (ident × type)) : typelist ≝
     347let rec type_of_params (params: list (ident × type)) : typelist ≝
    348348  match params with
    349349  [ nil ⇒ Tnil
    350   | cons h rem ⇒ match h with [ mk_pair id ty ⇒ Tcons ty (type_of_params rem) ]
    351   ].
    352 
    353 ndefinition type_of_function : function → type ≝ λf.
     350  | cons h rem ⇒ match h with [ pair id ty ⇒ Tcons ty (type_of_params rem) ]
     351  ].
     352
     353definition type_of_function : function → type ≝ λf.
    354354  Tfunction (type_of_params (fn_params f)) (fn_return f).
    355355
    356 ndefinition type_of_fundef : fundef → type ≝ λf.
     356definition type_of_fundef : fundef → type ≝ λf.
    357357  match f with
    358358  [ Internal fd ⇒ type_of_function fd
     
    362362(* * Natural alignment of a type, in bytes. *)
    363363(* FIXME: these are old values for 32 bit machines *)
    364 nlet rec alignof (t: type) : Z ≝
     364let rec alignof (t: type) : Z ≝
    365365  match t return λ_.Z (* XXX appears to infer nat otherwise *) with
    366366  [ Tvoid ⇒ 1
     
    387387
    388388(* XXX: automatic generation? *)
    389 nlet rec type_ind2
     389let rec type_ind2
    390390  (P:type → Prop) (Q:fieldlist → Prop)
    391391  (vo:P Tvoid)
     
    432432  ].
    433433
    434 nlemma alignof_fields_pos:
     434lemma alignof_fields_pos:
    435435  ∀f. alignof_fields f > 0.
    436 napply fieldlist_ind; //;
    437 #i;#t;#fs';#IH; nlapply (Zmax_r (alignof t) (alignof_fields fs'));
    438 napply Zlt_to_Zle_to_Zlt; //; nqed.
    439 
    440 nlemma alignof_pos:
     436@fieldlist_ind //;
     437#i #t #fs' #IH lapply (Zmax_r (alignof t) (alignof_fields fs'));
     438@Zlt_to_Zle_to_Zlt //; qed.
     439
     440lemma alignof_pos:
    441441  ∀t. alignof t > 0.
    442 #t;nelim t; nnormalize; //;
    443 ##[ ##1,2: #z; ncases z; //;
    444 ##| ##3,4: #i;napply alignof_fields_pos
    445 ##] nqed.
     442#t elim t; normalize; //;
     443[ 1,2: #z cases z; //;
     444| 3,4: #i @alignof_fields_pos
     445] qed.
    446446
    447447(* * Size of a type, in bytes. *)
    448448
    449 ndefinition sizeof_pointer : region → Z ≝
    450 λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
    451 
    452 nlet rec sizeof (t: type) : Z ≝
     449definition sizeof_pointer : region → Z ≝
     450λsp. match sp return λ_.Z with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
     451
     452let rec sizeof (t: type) : Z ≝
    453453  match t return λ_.Z with
    454454  [ Tvoid ⇒ 1
     
    475475  ].
    476476(* TODO: needs some Z_times results
    477 nlemma sizeof_pos:
     477lemma sizeof_pos:
    478478  ∀t. sizeof t > 0.
    479 #t0;
     479#t0
    480480napply (type_ind2 (λt. sizeof t > 0)
    481481                  (λf. sizeof_union f ≥ 0 ∧ ∀pos:Z. pos ≥ 0 → sizeof_struct f pos ≥ 0));
    482 ##[ ##1,4,6,9: //;
    483 ##| #i;ncases i;#s;//;
    484 ##| #f;ncases f;//
    485 ##| #t;#n;#H; nwhd in ⊢ (?%?);
     482[ 1,4,6,9: //;
     483| #i cases i;#s //;
     484| #f cases f;//
     485| #t #n #H whd in ⊢ (?%?);
    486486Proof.
    487487  intro t0.
     
    520520Open Local Scope string_scope.
    521521*)
    522 nlet rec field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
     522let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
    523523                              on fld : res Z ≝
    524524  match fld with
     
    531531  ].
    532532
    533 ndefinition field_offset ≝ λid: ident. λfld: fieldlist.
     533definition field_offset ≝ λid: ident. λfld: fieldlist.
    534534  field_offset_rec id fld 0.
    535535
    536 nlet rec field_type (id: ident) (fld: fieldlist) on fld : res type :=
     536let rec field_type (id: ident) (fld: fieldlist) on fld : res type :=
    537537  match fld with
    538538  [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
     
    626626*)
    627627
    628 ninductive mode: Type
     628inductive mode: Type[0]
    629629  | By_value: memory_chunk → mode
    630630  | By_reference: mode
    631631  | By_nothing: mode.
    632632
    633 ndefinition access_mode : type → mode ≝ λty.
     633definition access_mode : type → mode ≝ λty.
    634634  match ty with
    635635  [ Tint i s ⇒
     
    662662*)
    663663
    664 ninductive classify_add_cases : Type
     664inductive classify_add_cases : Type[0]
    665665  | add_case_ii: classify_add_cases         (**r int , int *)
    666666  | add_case_ff: classify_add_cases         (**r float , float *)
     
    669669  | add_default: classify_add_cases.        (**r other *)
    670670
    671 ndefinition classify_add ≝ λty1: type. λty2: type.
     671definition classify_add ≝ λty1: type. λty2: type.
    672672(*
    673673  match ty1, ty2 with
     
    694694  ].
    695695
    696 ninductive classify_sub_cases : Type
     696inductive classify_sub_cases : Type[0]
    697697  | sub_case_ii: classify_sub_cases          (**r int , int *)
    698698  | sub_case_ff: classify_sub_cases          (**r float , float *)
     
    701701  | sub_default: classify_sub_cases .        (**r other *)
    702702
    703 ndefinition classify_sub ≝ λty1: type. λty2: type.
     703definition classify_sub ≝ λty1: type. λty2: type.
    704704(*  match ty1, ty2 with
    705705  | Tint _ _ , Tint _ _ ⇒ sub_case_ii
     
    732732  ].
    733733
    734 ninductive classify_mul_cases : Type
     734inductive classify_mul_cases : Type[0]
    735735  | mul_case_ii: classify_mul_cases (**r int , int *)
    736736  | mul_case_ff: classify_mul_cases (**r float , float *)
    737737  | mul_default: classify_mul_cases . (**r other *)
    738738
    739 ndefinition classify_mul ≝ λty1: type. λty2: type.
     739definition classify_mul ≝ λty1: type. λty2: type.
    740740  match ty1 with
    741741  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ mul_case_ii | _ ⇒ mul_default ]
     
    750750end.
    751751*)
    752 ninductive classify_div_cases : Type
     752inductive classify_div_cases : Type[0]
    753753  | div_case_I32unsi: classify_div_cases (**r unsigned int32 , int *)
    754754  | div_case_ii: classify_div_cases    (**r int , int *)
     
    756756  | div_default: classify_div_cases. (**r other *)
    757757
    758 ndefinition classify_32un_aux ≝ λT:Type.λi.λs.λr1:T.λr2:T.
     758definition classify_32un_aux ≝ λT:Type[0].λi.λs.λr1:T.λr2:T.
    759759  match i with [ I32 ⇒
    760760    match s with [ Unsigned ⇒ r1 | _ ⇒ r2 ]
    761761  | _ ⇒ r2 ].
    762762
    763 ndefinition classify_div ≝ λty1: type. λty2: type.
     763definition classify_div ≝ λty1: type. λty2: type.
    764764  match ty1 with
    765765  [ Tint i1 s1 ⇒
     
    773773  ].
    774774(*
    775 ndefinition classify_div ≝ λty1: type. λty2: type.
     775definition classify_div ≝ λty1: type. λty2: type.
    776776  match ty1,ty2 with
    777777  | Tint I32 Unsigned, Tint _ _ ⇒ div_case_I32unsi
     
    782782end.
    783783*)
    784 ninductive classify_mod_cases : Type
     784inductive classify_mod_cases : Type[0]
    785785  | mod_case_I32unsi: classify_mod_cases  (**r unsigned I32 , int *)
    786786  | mod_case_ii: classify_mod_cases  (**r int , int *)
    787787  | mod_default: classify_mod_cases . (**r other *)
    788788
    789 ndefinition classify_mod ≝ λty1:type. λty2:type.
     789definition classify_mod ≝ λty1:type. λty2:type.
    790790  match ty1 with
    791791  [ Tint i1 s1 ⇒
     
    806806end .
    807807*)
    808 ninductive classify_shr_cases :Type
     808inductive classify_shr_cases :Type[0]
    809809  | shr_case_I32unsi:  classify_shr_cases (**r unsigned I32 , int *)
    810810  | shr_case_ii :classify_shr_cases (**r int , int *)
    811811  | shr_default : classify_shr_cases . (**r other *)
    812812
    813 ndefinition classify_shr ≝ λty1: type. λty2: type.
     813definition classify_shr ≝ λty1: type. λty2: type.
    814814  match ty1 with
    815815  [ Tint i1 s1 ⇒
     
    829829  end.
    830830*)
    831 ninductive classify_cmp_cases : Type
     831inductive classify_cmp_cases : Type[0]
    832832  | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
    833833  | cmp_case_ipip: classify_cmp_cases  (**r int|ptr|array , int|ptr|array*)
     
    835835  | cmp_default: classify_cmp_cases . (**r other *)
    836836
    837 ndefinition classify_cmp ≝ λty1:type. λty2:type.
     837definition classify_cmp ≝ λty1:type. λty2:type.
    838838  match ty1 with
    839839  [ Tint i1 s1 ⇒
     
    875875  end.
    876876*)
    877 ninductive classify_fun_cases : Type
     877inductive classify_fun_cases : Type[0]
    878878  | fun_case_f: typelist → type → classify_fun_cases   (**r (pointer to) function *)
    879879  | fun_default: classify_fun_cases . (**r other *)
    880880
    881 ndefinition classify_fun ≝ λty: type.
     881definition classify_fun ≝ λty: type.
    882882  match ty with
    883883  [ Tfunction args res ⇒ fun_case_f args res
     
    891891  and external functions. *)
    892892
    893 ndefinition typ_of_type : type → typ ≝ λt.
     893definition typ_of_type : type → typ ≝ λt.
    894894  match t with
    895895  [ Tfloat _ ⇒ ASTfloat
     
    897897  ].
    898898
    899 ndefinition opttyp_of_type : type → option typ ≝ λt.
     899definition opttyp_of_type : type → option typ ≝ λt.
    900900  match t with
    901901  [ Tvoid ⇒ None ?
     
    904904  ].
    905905
    906 nlet rec typlist_of_typelist (tl: typelist) : list typ ≝
     906let rec typlist_of_typelist (tl: typelist) : list typ ≝
    907907  match tl with
    908908  [ Tnil ⇒ nil ?
     
    910910  ].
    911911
    912 ndefinition signature_of_type : typelist → type → signature ≝ λargs. λres.
     912definition signature_of_type : typelist → type → signature ≝ λargs. λres.
    913913  mk_signature (typlist_of_typelist args) (opttyp_of_type res).
    914914
    915 ndefinition external_function
     915definition external_function
    916916    : ident → typelist → type → external_function ≝ λid. λtargs. λtres.
    917917  mk_external_function id (signature_of_type targs tres).
Note: See TracChangeset for help on using the changeset viewer.