Changeset 1053 for src/RTLabs
 Timestamp:
 Jul 4, 2011, 6:20:23 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1052 r1053 102 102 〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉. 103 103 104 definition float_free_p≝104 definition size_of_sig_type ≝ 105 105 λsig. 106 106 match sig with 107 [ ASTfloat _ ⇒ False108  _ ⇒ True109 ].110 111 definition size_of_sig_type ≝112 λsig.113 λprf: float_free_p sig.114 match sig return λx. float_free_p x → nat with115 107 [ ASTint isize sign ⇒ 116 λast_int_prf. 117 let isize' ≝ match isize with [ I8 ⇒ 8  I16 ⇒ 16  I32 ⇒ 32 ] in 118 isize' ÷ (nat_of_bitvector ? int_size) 119  ASTfloat _ ⇒ 120 λast_float_prf. ? 121  ASToffset ⇒ 122 λast_offset_prf. 123 nat_of_bitvector ? int_size 124  ASTptr rgn ⇒ 125 λast_ptr_prf. 126 nat_of_bitvector ? ptr_size 127 ]. 128 normalize in ast_float_prf; 129 cases ast_float_prf; 108 let isize' ≝ match isize with [ I8 ⇒ 8  I16 ⇒ 16  I32 ⇒ 32 ] in 109 isize' ÷ (nat_of_bitvector ? int_size) 110  ASTfloat _ ⇒ ? (* dpm: not implemented *) 111  ASTptr rgn ⇒ nat_of_bitvector ? ptr_size 112 ]. 113 cases not_implemented; 130 114 qed. 131 115 … … 158 142 λruniverse. 159 143 λlenv. 160 λr. 161 λt. 162 match size_of_sig_type t with 163 [ None ⇒ None ? 164  Some size ⇒ 165 let rs ≝ register_freshes runiverse size in 166 Some ? (add_local_env r rs lenv) 167 ]. 144 λr_sig. 145 let 〈r, sig〉 ≝ r_sig in 146 let size ≝ size_of_sig_type sig in 147 let rs ≝ register_freshes runiverse size in 148 add_local_env r rs lenv. 168 149 169 150 definition initialize_local_env ≝ 170 151 λruniverse. 171 λptrs.172 152 λregisters. 153 λresult. 173 154 let registers ≝ registers @ 174 155 match result with … … 177 158 ] 178 159 in 179 foldl ? ? ( 180 λbvt. λr. 181 match bvt with 182 [ None ⇒ None ? 183  Some bvt' ⇒ initialize_local_env_internal runiverse bvt' r typ 184 ]) ? ?. 185 186 let initialize_local_env runiverse registers result = 187 let registers = 188 registers @ (match result with None → [ ]  Some (r, t) → [(r, t)]) in 189 let f lenv (r, t) = 190 let rs = register_freshes runiverse (size_of_sig_type t) in 191 add_local_env r rs lenv in 192 List.fold_left f Register.Map.empty registers 160 foldl ? ? (initialize_local_env_internal runiverse) (Stub …) registers. 193 161 194 162 definition map_list_local_env_internal ≝ … … 201 169 λlenv. 202 170 λregs. 203 204 205 let map_list_local_env lenv regs = 206 let f res r = res @ (find_local_env r lenv) in 207 List.fold_left f [] regs 208 209 definition filter_and_to_list_local_env_internal ≝ 210 λlenv. 211 λl. 212 λr. 213 match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with 214 [ Some entry ⇒ 215 match entry with 216 [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ]) 217  register_int r ⇒ (l @ [ r ]) 218 ] 219  None ⇒ [ ] (* dpm: should this be none? *) 220 ]. 221 222 definition filter_and_to_list_local_env ≝ 223 λlenv. 224 λregisters. 225 foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers. 226 227 definition list_of_register_type ≝ 228 λrt. 229 match rt with 230 [ register_ptr r1 r2 ⇒ [ r1; r2 ] 231  register_int r ⇒ [ r ] 232 ]. 233 234 definition find_and_list ≝ 235 λr. 236 λlenv. 237 match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with 238 [ None ⇒ [ ] (* dpm: should this be none? *) 239  Some lkup ⇒ list_of_register_type lkup 240 ]. 241 242 definition find_and_list_args ≝ 243 λargs. 244 λlenv. 245 map ? ? (λr. find_and_list r lenv) args. 171 foldl ? ? (map_list_local_env_internal lenv) [ ] regs. 172 173 definition make_addr ≝ 174 λA. 175 λlst: list A. 176 λprf: length A lst = 2. (* do not use on arguments other than those of length 2 *) 177 match lst return λx. length A x = 2 → A × A with 178 [ nil ⇒ λlst_nil_prf. ? 179  cons hd tl ⇒ λprf. 180 match tl return λx. length A x = 1 → A × A with 181 [ nil ⇒ λtl_nil_prf. ? 182  cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉 183 ] ? 184 ] prf. 185 [1: normalize in lst_nil_prf; 186 destruct(lst_nil_prf); 187 2: normalize in prf; 188 destruct(prf) 189 @e0 190 3: normalize in tl_nil_prf; 191 destruct(tl_nil_prf); 192 ] 193 qed. 246 194 247 195 definition find_and_addr ≝ 248 196 λr. 249 197 λlenv. 250 match find_and_list r lenv with 251 [ cons hd tl ⇒ 252 match tl with 253 [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉 254  nil ⇒ None ? 255 ] 256  nil ⇒ None ? (* dpm: was assert false *) 257 ]. 198 make_addr ? (find_local_env r lenv). 258 199 259 200 definition rtl_args ≝ 260 201 λregs_list. 261 202 λlenv. 262 flatten ? (find_and_list_args regs_list lenv). 203 flatten ? (map ? ? ( 204 λr. find_local_env r lenv) regs_list). 263 205 264 206 definition change_label ≝ … … 284 226  rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2 285 227  rtl_st_return r ⇒ rtl_st_return r 286  _ ⇒ ? 287 ]. 288 228 ]. 229 230 (* Ack! Should generating a fresh label ever fail? This seems to be a sideeffect 231 of implementing everything as a bitvector, which is bounded. If we implemented 232 labels as unbounded nats then this function will never fail. 233 *) 289 234 let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝ 290 235 match stmt_list with … … 304 249 ] 305 250 ]. 306 251 307 252 (* dpm: had to lift this into option *) 308 253 let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label) … … 321 266 [ None ⇒ None ? 322 267  Some def ⇒ add_translates tl tmp_lbl dest_lbl def 323 ]324 ]325 ]326 ].327 328 329 (* dpm: horrendous, use dependent types.330 length destr = length srcrs *)331 let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label)332 (dest_lbl: label) (def: ?) ≝333 match destrs with334 [ nil ⇒335 match srcrs with336 [ nil ⇒ Some ? def337  cons hd tl ⇒ None ?338 ]339  cons hd tl ⇒340 match srcrs with341 [ nil ⇒ None ?342  cons hd' tl' ⇒343 match tl with344 [ nil ⇒345 match tl' with346 (* one element lists *)347 [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def)348  cons hd'' tl'' ⇒ None ?349 ]350  cons hd'' tl'' ⇒351 match tl' with352 [ nil ⇒ None ?353 (* multielement lists *)354  cons hd''' tl''' ⇒355 let tmp_lbl ≝ fresh_label def in356 match tmp_lbl with357 [ None ⇒ None ?358  Some tmp_lbl ⇒359 let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in360 translate_move tl tl' tmp_lbl dest_lbl def361 ]362 268 ] 363 269 ] … … 411 317  cast_sizeof size ⇒ ? 412 318 (*  cast_float f ⇒ None ? *) (* what are we doing with floats? *) 319 ]. 320 321 definition filter_and_to_list_local_env_internal ≝ 322 λlenv. 323 λl. 324 λr. 325 match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with 326 [ Some entry ⇒ 327 match entry with 328 [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ]) 329  register_int r ⇒ (l @ [ r ]) 330 ] 331  None ⇒ [ ] (* dpm: should this be none? *) 332 ]. 333 334 definition filter_and_to_list_local_env ≝ 335 λlenv. 336 λregisters. 337 foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers. 338 339 definition list_of_register_type ≝ 340 λrt. 341 match rt with 342 [ register_ptr r1 r2 ⇒ [ r1; r2 ] 343  register_int r ⇒ [ r ] 344 ]. 345 346 definition find_and_list ≝ 347 λr. 348 λlenv. 349 match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with 350 [ None ⇒ [ ] (* dpm: should this be none? *) 351  Some lkup ⇒ list_of_register_type lkup 352 ]. 353 354 definition find_and_list_args ≝ 355 λargs. 356 λlenv. 357 map ? ? (λr. find_and_list r lenv) args. 358 359 (* dpm: horrendous, use dependent types. 360 length destr = length srcrs *) 361 let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label) 362 (dest_lbl: label) (def: ?) ≝ 363 match destrs with 364 [ nil ⇒ 365 match srcrs with 366 [ nil ⇒ Some ? def 367  cons hd tl ⇒ None ? 368 ] 369  cons hd tl ⇒ 370 match srcrs with 371 [ nil ⇒ None ? 372  cons hd' tl' ⇒ 373 match tl with 374 [ nil ⇒ 375 match tl' with 376 (* one element lists *) 377 [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def) 378  cons hd'' tl'' ⇒ None ? 379 ] 380  cons hd'' tl'' ⇒ 381 match tl' with 382 [ nil ⇒ None ? 383 (* multielement lists *) 384  cons hd''' tl''' ⇒ 385 let tmp_lbl ≝ fresh_label def in 386 match tmp_lbl with 387 [ None ⇒ None ? 388  Some tmp_lbl ⇒ 389 let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in 390 translate_move tl tl' tmp_lbl dest_lbl def 391 ] 392 ] 393 ] 394 ] 413 395 ]. 414 396
Note: See TracChangeset
for help on using the changeset viewer.