Changeset 879 for src/common/AST.ma
 Timestamp:
 Jun 3, 2011, 5:35:30 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/AST.ma
r849 r879 78 78 λsp. match sp with [ Data ⇒ 1  IData ⇒ 1  PData ⇒ 1  XData ⇒ 2  Code ⇒ 2  Any ⇒ 3 ]. 79 79 80 (* * The intermediate languages are weakly typed, using only three types: 81 [ASTint] for integers, [ASTptr] for pointers, and [ASTfloat] for floatingpoint 82 numbers. *) 80 (* We maintain some reasonable type information through the front end of the 81 compiler. *) 82 83 inductive signedness : Type[0] ≝ 84  Signed: signedness 85  Unsigned: signedness. 86 87 inductive intsize : Type[0] ≝ 88  I8: intsize 89  I16: intsize 90  I32: intsize. 91 92 (* * Float types come in two sizes: 32 bits (single precision) 93 and 64bit (double precision). *) 94 95 inductive floatsize : Type[0] ≝ 96  F32: floatsize 97  F64: floatsize. 83 98 84 99 inductive typ : Type[0] ≝ 85  ASTint : typ100  ASTint : intsize → signedness → typ 86 101  ASTptr : region → typ 87  ASTfloat : typ.102  ASTfloat : floatsize → typ. 88 103 89 104 (* XXX aliases *) 90 105 definition SigType ≝ typ. 91 definition SigType_Int ≝ ASTint .106 definition SigType_Int ≝ ASTint I32 Unsigned. 92 107 (* 93 108  SigType_Float: SigType … … 95 110 definition SigType_Ptr ≝ ASTptr Any. 96 111 97 98 (* FIXME: ASTint size is not 1 for Clight32 *) 112 definition size_intsize : intsize → nat ≝ 113 λsz. match sz with [ I8 ⇒ 1  I16 ⇒ 2  I32 ⇒ 4]. 114 115 definition size_floatsize : floatsize → nat ≝ 116 λsz. match sz with [ F32 ⇒ 4  F64 ⇒ 8 ]. 117 99 118 definition typesize : typ → nat ≝ λty. 100 match ty with [ ASTint ⇒ 1  ASTptr r ⇒ size_pointer r  ASTfloat ⇒ 8 ]. 119 match ty with 120 [ ASTint sz _ ⇒ size_intsize sz 121  ASTptr r ⇒ size_pointer r 122  ASTfloat sz ⇒ size_floatsize sz ]. 101 123 102 124 lemma typesize_pos: ∀ty. typesize ty > 0. 103 #ty cases ty [ 2: * ]/2/ qed.125 * *; try * /2/ qed. 104 126 105 127 lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2). 106 #t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct;qed.128 * * * *; try *; try *; try (%1 @refl) %2 @nmk #H destruct qed. 107 129 108 130 lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2). … … 132 154 definition proj_sig_res : signature → typ ≝ λs. 133 155 match sig_res s with 134 [ None ⇒ ASTint 156 [ None ⇒ ASTint I32 Unsigned 135 157  Some t ⇒ t 136 158 ].
Note: See TracChangeset
for help on using the changeset viewer.