Changeset 1872 for src/common/AST.ma
 Timestamp:
 Apr 4, 2012, 6:48:23 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/AST.ma
r1640 r1872 90 90 #r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed. 91 91 92 (* Carefully defined to be convertably nonzero *) 92 93 definition size_pointer : region → nat ≝ 93 λsp. match sp with [ Data ⇒ 1  IData ⇒ 1  PData ⇒ 1  XData ⇒ 2  Code ⇒ 2  Any ⇒ 3].94 λsp. S match sp with [ Data ⇒ 0  IData ⇒ 0  PData ⇒ 0  XData ⇒ 1  Code ⇒ 1  Any ⇒ 2 ]. 94 95 95 96 (* We maintain some reasonable type information through the front end of the … … 155 156 * * * #NE try @refl @False_ind @NE @refl 156 157 qed. 158 159 definition signedness_check : ∀sg1,sg2:signedness. ∀P:signedness → signedness → Type[0]. 160 P sg1 sg1 → P sg1 sg2 → P sg1 sg2 ≝ 161 λsg1,sg2,P. 162 match sg1 return λsg1. P sg1 sg1 → P sg1 sg2 → P sg1 sg2 with 163 [ Signed ⇒ λx. match sg2 return λsg2. P ? sg2 → P Signed sg2 with [ Signed ⇒ λd. x  _ ⇒ λd. d ] 164  Unsigned ⇒ λx. match sg2 return λsg2. P ? sg2 → P Unsigned sg2 with [ Unsigned ⇒ λd. x  _ ⇒ λd. d ] 165 ]. 166 167 let rec inttyp_eq_elim' (sz1,sz2:intsize) (sg1,sg2:signedness) (P:intsize → signedness → intsize → signedness → Type[0]) on sz1 : 168 P sz1 sg1 sz1 sg1 → P sz1 sg1 sz2 sg2 → P sz1 sg1 sz2 sg2 ≝ 169 match sz1 return λsz. P sz sg1 sz sg1 → P sz sg1 sz2 sg2 → P sz sg1 sz2 sg2 with 170 [ I8 ⇒ λx. match sz2 return λsz. P ?? sz ? → P I8 ? sz ? with [ I8 ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x  _ ⇒ λd. d ] 171  I16 ⇒ λx. match sz2 return λsz. P I16 sg1 sz sg2 → P I16 sg1 sz sg2 with [ I16 ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x  _ ⇒ λd. d ] 172  I32 ⇒ λx. match sz2 return λsz. P I32 sg1 sz sg2 → P I32 sg1 sz sg2 with [ I32 ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x  _ ⇒ λd. d ] 173 ]. 174 175 let rec intsize_eq_elim' (sz1,sz2:intsize) (P:intsize → intsize → Type[0]) on sz1 : 176 P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝ 177 match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with 178 [ I8 ⇒ λx. match sz2 return λsz. P ? sz → P I8 sz with [ I8 ⇒ λd. x  _ ⇒ λd. d ] 179  I16 ⇒ λx. match sz2 return λsz. P ? sz → P I16 sz with [ I16 ⇒ λd. x  _ ⇒ λd. d ] 180  I32 ⇒ λx. match sz2 return λsz. P ? sz → P I32 sz with [ I32 ⇒ λd. x  _ ⇒ λd. d ] 181 ]. 157 182 158 183 (* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and … … 189 214 λsz. S match sz with [ F32 ⇒ 3  F64 ⇒ 7 ]. 190 215 216 let rec floatsize_eq_elim (sz1,sz2:floatsize) (P:floatsize → floatsize → Type[0]) on sz1 : 217 P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝ 218 match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with 219 [ F32 ⇒ λx. match sz2 return λsz. P ? sz → P F32 sz with [ F32 ⇒ λd. x  _ ⇒ λd. d ] 220  F64 ⇒ λx. match sz2 return λsz. P ? sz → P F64 sz with [ F64 ⇒ λd. x  _ ⇒ λd. d ] 221 ]. 222 223 191 224 definition typesize : typ → nat ≝ λty. 192 225 match ty with … … 231 264  Some t ⇒ t 232 265 ]. 233 234 (* * Memory accesses (load and store instructions) are annotated by235 a ``memory chunk'' indicating the type, size and signedness of the236 chunk of memory being accessed. *)237 238 inductive memory_chunk : Type[0] ≝239  Mint8signed : memory_chunk (*r 8bit signed integer *)240  Mint8unsigned : memory_chunk (*r 8bit unsigned integer *)241  Mint16signed : memory_chunk (*r 16bit signed integer *)242  Mint16unsigned : memory_chunk (*r 16bit unsigned integer *)243  Mint32 : memory_chunk (*r 32bit integer, or pointer *)244  Mfloat32 : memory_chunk (*r 32bit singleprecision float *)245  Mfloat64 : memory_chunk (*r 64bit doubleprecision float *)246  Mpointer : region → memory_chunk. (* pointer addressing given region *)247 248 definition typ_of_memory_chunk : memory_chunk → typ ≝249 λc. match c with250 [ Mint8signed ⇒ ASTint I8 Signed251  Mint8unsigned ⇒ ASTint I8 Unsigned252  Mint16signed ⇒ ASTint I16 Signed253  Mint16unsigned ⇒ ASTint I16 Unsigned254  Mint32 ⇒ ASTint I32 Unsigned (* XXX signed? *)255  Mfloat32 ⇒ ASTfloat F32256  Mfloat64 ⇒ ASTfloat F64257  Mpointer r ⇒ ASTptr r258 ].259 266 260 267 (* * Initialization data for global variables. *)
Note: See TracChangeset
for help on using the changeset viewer.