Changeset 487 for Deliverables/D3.1/Csemantics/AST.ma
 Timestamp:
 Feb 9, 2011, 11:49:17 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/AST.ma
r485 r487 17 17 the abstract syntax trees of many of the intermediate languages. *) 18 18 19 include " datatypes/sums.ma".19 include "basics/types.ma". 20 20 include "extralib.ma". 21 21 include "Integers.ma". … … 28 28 etc) are represented by the type [positive] of positive integers. *) 29 29 30 ndefinition ident ≝ Pos.31 32 ndefinition ident_eq : ∀x,y:ident. (x=y) + (x≠y).33 #x y; nlapply (pos_compare_to_Prop x y); ncases (pos_compare x y);34 ##[ #H; @2; /2/; ## #H; @1; //; ## #H; @2; /2/ ##] nqed.30 definition ident ≝ Pos. 31 32 definition ident_eq : ∀x,y:ident. (x=y) + (x≠y). 33 #x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y); 34 [ #H %2 /2/;  #H %1 //;  #H %2 /2/ ] qed. 35 35 36 36 (* 37 37 (* XXX: we use nats for now, but if in future we use binary like compcert 38 38 then the maps will be easier to define. *) 39 ndefinition ident ≝ nat.40 ndefinition ident_eq : ∀x,y:ident. (x=y) + (x≠y).41 #x ; nelim x;42 ##[ #y; ncases y; /3/;43 ## #x'; #IH; #y; ncases y;44 ##[ @2; @; #H; ndestruct45 ## #y'; nelim (IH y');46 ##[ #e; ndestruct; /2/47 ## #ne; @2;/2/;48 ##]49 ##]50 ##] nqed.39 definition ident ≝ nat. 40 definition ident_eq : ∀x,y:ident. (x=y) + (x≠y). 41 #x elim x; 42 [ #y cases y; /3/; 43  #x' #IH #y cases y; 44 [ %{2} % #H destruct 45  #y' elim (IH y'); 46 [ #e destruct; /2/ 47  #ne %{2} /2/; 48 ] 49 ] 50 ] qed. 51 51 *) 52 52 (* * The intermediate languages are weakly typed, using only two types: … … 54 54 numbers. *) 55 55 56 ninductive typ : Type≝56 inductive typ : Type[0] ≝ 57 57  ASTint : typ 58 58  ASTfloat : typ. 59 59 60 ndefinition typesize : typ → Z ≝ λty.60 definition typesize : typ → Z ≝ λty. 61 61 match ty return λ_.Z with [ ASTint ⇒ 4  ASTfloat ⇒ 8 ]. 62 62 63 nlemma typesize_pos: ∀ty. typesize ty > 0.64 #ty ; ncases ty; //; nqed.65 66 nlemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).67 #t1 ;#t2;ncases t1;ncases t2;/2/; @2; napply nmk; #H; ndestruct; nqed.68 69 nlemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).70 #t1 ;#t2;ncases t1;ncases t2;/2/;71 ##[ ##1,2: #ty; @2; napply nmk; #H; ndestruct;72 ## #ty1;#ty2; nelim (typ_eq ty1 ty2); /2/; #neq; @2; napply nmk; 73 #H ; ndestruct; /2/;74 ##] nqed.63 lemma typesize_pos: ∀ty. typesize ty > 0. 64 #ty cases ty; //; qed. 65 66 lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2). 67 #t1 #t2 cases t1;cases t2;/2/; %2 @nmk #H destruct; qed. 68 69 lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2). 70 #t1 #t2 cases t1;cases t2;/2/; 71 [ 1,2: #ty %2 @nmk #H destruct; 72  #ty1 #ty2 elim (typ_eq ty1 ty2); /2/; #neq %2 @nmk 73 #H destruct; /2/; 74 ] qed. 75 75 76 76 (* * Additionally, function definitions and function calls are annotated … … 80 80 for the function. *) 81 81 82 nrecord signature : Type≝ {82 record signature : Type[0] ≝ { 83 83 sig_args: list typ; 84 84 sig_res: option typ 85 85 }. 86 86 87 ndefinition proj_sig_res : signature → typ ≝ λs.87 definition proj_sig_res : signature → typ ≝ λs. 88 88 match sig_res s with 89 89 [ None ⇒ ASTint … … 93 93 (* Memory spaces *) 94 94 95 ninductive region : Type≝95 inductive region : Type[0] ≝ 96 96  Any : region 97 97  Data : region … … 101 101  Code : region. 102 102 103 ndefinition eq_region : region → region → bool ≝103 definition eq_region : region → region → bool ≝ 104 104 λr1,r2. 105 105 match r1 with … … 112 112 ]. 113 113 114 nlemma eq_region_elim : ∀P:bool → Type. ∀r1,r2.114 lemma eq_region_elim : ∀P:bool → Type[0]. ∀r1,r2. 115 115 (r1 = r2 → P true) → (r1 ≠ r2 → P false) → 116 116 P (eq_region r1 r2). 117 #P r1 r2; ncases r1; ncases r2; #Ptrue Pfalse;118 ntry ( napply Ptrue // ); 119 napply Pfalse; @; #E; ndestruct;120 nqed.121 122 ndefinition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).123 #r1 r2; napply (eq_region_elim ? r1 r2); /2/; nqed.117 #P #r1 #r2 cases r1; cases r2; #Ptrue #Pfalse 118 try ( @Ptrue // ) 119 @Pfalse % #E destruct; 120 qed. 121 122 definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2). 123 #r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed. 124 124 125 125 (* * Memory accesses (load and store instructions) are annotated by … … 127 127 chunk of memory being accessed. *) 128 128 129 ninductive memory_chunk : Type[0] ≝129 inductive memory_chunk : Type[0] ≝ 130 130  Mint8signed : memory_chunk (*r 8bit signed integer *) 131 131  Mint8unsigned : memory_chunk (*r 8bit unsigned integer *) … … 139 139 (* * Initialization data for global variables. *) 140 140 141 ninductive init_data: Type[0] ≝141 inductive init_data: Type[0] ≝ 142 142  Init_int8: int → init_data 143 143  Init_int16: int → init_data … … 160 160 programs are common to all languages. *) 161 161 162 nrecord program (F,V: Type) : Type:= {162 record program (F,V: Type[0]) : Type[0] := { 163 163 prog_funct: list (ident × F); 164 164 prog_main: ident; … … 166 166 }. 167 167 168 ndefinition prog_funct_names ≝ λF,V: Type. λp: program F V.168 definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V. 169 169 map ?? (fst ident F) (prog_funct ?? p). 170 170 171 ndefinition prog_var_names ≝ λF,V: Type. λp: program F V.171 definition prog_var_names ≝ λF,V: Type[0]. λp: program F V. 172 172 map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p). 173 173 (* … … 184 184 *) 185 185 186 ndefinition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝186 definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝ 187 187 λA,B,transf,l. 188 188 map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l. 189 189 190 ndefinition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝190 definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝ 191 191 λA,B,V,transf,p. 192 192 mk_program B V … … 194 194 (prog_main A V p) 195 195 (prog_vars A V p). 196 197 nlemma transform_program_function:196 (* 197 lemma transform_program_function: 198 198 ∀A,B,V,transf,p,i,tf. 199 199 in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) → 200 200 ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf. 201 n normalize; #A B V transf p i tf H; nelim (list_in_map_inv ????? H);202 #x ; nelim x; #i' tf'; *; #e H; ndestruct; @tf';/2/;203 nqed.204 201 normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H); 202 #x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/; 203 qed. 204 *) 205 205 (* 206 206 End TRANSF_PROGRAM. … … 432 432 a type for such functions and some generic transformation functions. *) 433 433 434 nrecord external_function : Type≝ {434 record external_function : Type[0] ≝ { 435 435 ef_id: ident; 436 436 ef_sig: signature 437 437 }. 438 438 (* 439 ninductive fundef (F: Type): Type ≝439 inductive fundef (F: Type): Type ≝ 440 440  Internal: F → fundef F 441 441  External: external_function → fundef F. … … 448 448 Variable transf: A > B. 449 449 *) 450 ndefinition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝450 definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝ 451 451 λA,B,transf,fd. 452 452 match fd with
Note: See TracChangeset
for help on using the changeset viewer.