Changeset 718 for src/Clight/AST.ma
 Timestamp:
 Mar 29, 2011, 5:54:37 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/AST.ma
r700 r718 34 34 [ #H %2 /2/;  #H %1 //;  #H %2 /2/ ] qed. 35 35 36 (*37 (* XXX: we use nats for now, but if in future we use binary like compcert38 then the maps will be easier to define. *)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 destruct45  #y' elim (IH y');46 [ #e destruct; /2/47  #ne %{2} /2/;48 ]49 ]50 ] qed.51 *)52 (* * The intermediate languages are weakly typed, using only two types:53 [Tint] for integers and pointers, and [Tfloat] for floatingpoint54 numbers. *)55 56 inductive typ : Type[0] ≝57  ASTint : typ58  ASTfloat : typ.59 60 definition typesize : typ → Z ≝ λty.61 match ty return λ_.Z with [ ASTint ⇒ 4  ASTfloat ⇒ 8 ].62 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 @nmk73 #H destruct; /2/;74 ] qed.75 76 (* * Additionally, function definitions and function calls are annotated77 by function signatures indicating the number and types of arguments,78 as well as the type of the returned value if any. These signatures79 are used in particular to determine appropriate calling conventions80 for the function. *)81 82 record signature : Type[0] ≝ {83 sig_args: list typ;84 sig_res: option typ85 }.86 87 definition proj_sig_res : signature → typ ≝ λs.88 match sig_res s with89 [ None ⇒ ASTint90  Some t ⇒ t91 ].92 93 36 (* Memory spaces *) 94 37 … … 122 65 definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2). 123 66 #r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed. 67 68 definition size_pointer : region → Z ≝ 69 λsp. match sp return λ_.Z with [ Data ⇒ 1  IData ⇒ 1  PData ⇒ 1  XData ⇒ 2  Code ⇒ 2  Any ⇒ 3 ]. 70 71 (* * The intermediate languages are weakly typed, using only three types: 72 [ASTint] for integers, [ASTptr] for pointers, and [ASTfloat] for floatingpoint 73 numbers. *) 74 75 inductive typ : Type[0] ≝ 76  ASTint : typ 77  ASTptr : region → typ 78  ASTfloat : typ. 79 80 (* FIXME: ASTint size is not 1 for Clight32 *) 81 definition typesize : typ → Z ≝ λty. 82 match ty return λ_.Z with [ ASTint ⇒ 1  ASTptr r ⇒ size_pointer r  ASTfloat ⇒ 8 ]. 83 84 lemma typesize_pos: ∀ty. typesize ty > 0. 85 #ty cases ty [ 2: * ] // qed. 86 87 lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2). 88 #t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct; qed. 89 90 lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2). 91 #t1 #t2 cases t1 cases t2 92 [ %1 @refl 93  2,3: #ty %2 % #H destruct 94  #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl  %2 % #E' destruct /2/ 95 ] 96 qed. 97 98 (* * Additionally, function definitions and function calls are annotated 99 by function signatures indicating the number and types of arguments, 100 as well as the type of the returned value if any. These signatures 101 are used in particular to determine appropriate calling conventions 102 for the function. *) 103 104 record signature : Type[0] ≝ { 105 sig_args: list typ; 106 sig_res: option typ 107 }. 108 109 definition proj_sig_res : signature → typ ≝ λs. 110 match sig_res s with 111 [ None ⇒ ASTint 112  Some t ⇒ t 113 ]. 124 114 125 115 (* * Memory accesses (load and store instructions) are annotated by
Note: See TracChangeset
for help on using the changeset viewer.