Changeset 2681 for src/joint/TranslateUtils.ma
 Timestamp:
 Feb 19, 2013, 6:48:32 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/TranslateUtils.ma
r2675 r2681 93 93 (* ignoring register allocation for now *) 94 94 95 (* 95 96 definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝ 96 97 λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def). 97 98 *) 98 99 (* 99 100 lemma All_fresh_not_memb : ∀tag,u,l,id,u'. … … 111 112 ] 112 113 qed. 113 *) 114 114 115 115 116 lemma fresh_was_fresh : ∀tag,id,id',u,u'. … … 132 133 #tag * #id * #u * #u' normalize #EQ destruct // 133 134 qed. 134 135 *) 135 136 (* 136 137 lemma adds_graph_list_fresh_preserve : … … 242 243 qed. 243 244 *) 244 245 (* 245 246 axiom adds_graph_ok : 246 247 ∀g_pars,globals,B,src,dst,def. … … 270 271 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ 271 272 src ~❨B,src::l❩~> it in joint_if_code … def'. 272 273 (* preserves first statement if a cost label (should be an invariant) *) 274 definition insert_prologue ≝ 275 λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals). 276 λdef : joint_internal_function g_pars globals. 277 let entry ≝ joint_if_entry … def in 278 match stmt_at … entry 279 return λx.match x with [None ⇒ false  Some _ ⇒ true] → ? 280 with 281 [ Some s ⇒ λ_. 282 let default_add ≝ λ_ : unit. 283 let 〈def', lbl〉 ≝ fresh_label … def in 284 let def'' ≝ add_graph … lbl s def' in 285 adds_graph … insts entry lbl def'' in 286 match s with 287 [ sequential s' next ⇒ 288 match s' with 289 [ step_seq s'' ⇒ 290 match s'' with 291 [ COST_LABEL _ ⇒ 292 adds_graph ?? (s'' :: insts) entry next def 293  _ ⇒ 294 default_add it 295 ] 296  _ ⇒ 297 default_add it 298 ] 299  _ ⇒ 300 default_add it 301 ] 302  None ⇒ Ⓧ 303 ] (pi2 … entry). 273 *) 274 275 definition append_seq_list : 276 ∀p,g.bind_step_block p g → bind_new register (list (joint_seq p g)) → 277 bind_step_block p g ≝ 278 λp,g,bbl,bl. 279 ! 〈pref, op, post〉 ← bbl ; ! l ← bl ; return 〈pref, op, post @ l〉. 304 280 305 281 (* … … 332 308 adds_graph … stmts src dst def. 333 309 310 (* 334 311 axiom b_adds_graph_ok : 335 312 ∀g_pars,globals,B,src,dst,def. … … 349 326 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧ 350 327 src ~❨B,src::l,r❩~> dst in joint_if_code … def'. 351 328 *) 352 329 definition b_fin_adds_graph : 353 330 ∀g_pars: graph_params. … … 361 338 fin_adds_graph … stmts src def. 362 339 340 (* 363 341 axiom b_fin_adds_graph_ok : 364 342 ∀g_pars,globals,B,src,def. … … 378 356 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧ 379 357 src ~❨B,src::l,r❩~> it in joint_if_code … def'. 380 381 (* translation with inline fresh register allocation *) 382 definition b_graph_translate : 383 ∀src_g_pars,dst_g_pars : graph_params. 384 ∀globals: list ident. 385 (* initialization info *) 386 call_dest dst_g_pars → (* joint_if_result *) 387 paramsT dst_g_pars → (* joint_if_params *) 388 ℕ → (* joint_if_stacksize *) 389 (* functions dictating the translation *) 390 (label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) → 391 (label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) → 392 (* source function *) 393 joint_closed_internal_function src_g_pars globals → 394 (* destination function *) 395 joint_closed_internal_function dst_g_pars globals ≝ 396 λsrc_g_pars,dst_g_pars,globals, 397 init_ret,init_params,init_stack_size,trans_step,trans_fin_step,def. 398 let init ≝ 399 mk_joint_internal_function dst_g_pars globals 400 (joint_if_luniverse … def) 401 (joint_if_runiverse … def) 402 init_ret init_params init_stack_size 403 (add ?? (empty_map ? (joint_statement ??)) (joint_if_entry … def) (RETURN …)) 404 (pi1 … (joint_if_entry … def)) in 405 let f : label → joint_statement (src_g_pars : params) globals → 406 joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 407 λlbl,stmt,def. 408 match stmt with 409 [ sequential inst next ⇒ 410 b_adds_graph … (trans_step lbl inst) lbl next def 411  final inst ⇒ 412 b_fin_adds_graph … (trans_fin_step lbl inst) lbl def 413  FCOND abs _ _ _ ⇒ Ⓧabs 414 ] in 415 foldi … f (joint_if_code … def) init. 416 @hide_prf [ cases daemon (* TODO *)  >graph_code_has_point @mem_set_add_id ] qed. 358 *) 417 359 418 360 definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝ … … 447 389 *) 448 390 449 450 axiom b_graph_translate_ok : 451 ∀src_g_pars,dst_g_pars : graph_params. 452 ∀globals: list ident. 453 ∀init_ret,init_params,init_stack_size. 454 ∀f_step,f_fin,def_in. 455 let def_out ≝ 456 b_graph_translate src_g_pars dst_g_pars globals 457 init_ret init_params init_stack_size f_step f_fin def_in in 458 luniverse_ok ?? def_in → 459 luniverse_ok … def_out ∧ 460 joint_if_result … def_out = init_ret ∧ 461 joint_if_params … def_out = init_params ∧ 462 joint_if_stacksize … def_out = init_stack_size ∧ 463 pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in) ∧ 464 ∃f_lbls : label → option (list label). 465 ∃f_regs : label → option (list register). 466 partial_partition … f_lbls ∧ 467 partial_partition … f_regs ∧ 391 record b_graph_translate_data 392 (src, dst : graph_params) 393 (globals : list ident) : Type[0] ≝ 394 { init_ret : call_dest dst 395 ; init_params : paramsT dst 396 ; init_stack_size : ℕ 397 ; added_prologue : list (joint_seq dst globals) 398 ; f_step : label → joint_step src globals → bind_step_block dst globals 399 ; f_fin : label → joint_fin_step src → bind_fin_block dst globals 400 ; good_f_step_good : 401 ∀l,s.bind_new_P ?? 402 (λblock.let 〈pref, op, post〉 ≝ block in 403 All (label → joint_seq ??) 404 (λs'.∀l.step_forall_labels … (In ? (l :: step_labels … s)) (s' l)) 405 pref ∧ 406 (∀l.step_forall_labels … (In ? (l :: step_labels … s)) (op l)) ∧ 407 All (joint_seq ??) (step_forall_labels … (In ? (step_labels … s))) post) 408 (f_step l s) 409 ; good_f_fin : 410 ∀l,s.bind_new_P ?? 411 (λblock.let 〈pref, op〉 ≝ block in 412 All (joint_seq ??) (step_forall_labels … (In ? (fin_step_labels … s))) pref ∧ 413 All … (In ? (fin_step_labels … s)) (fin_step_labels … op)) 414 (f_fin l s) 415 ; f_step_on_cost : 416 ∀l,c.f_step l (COST_LABEL … c) = bret … [ COST_LABEL … c ] 417 }. 418 419 definition get_first_costlabel : ∀p,g. 420 joint_closed_internal_function p g → costlabel × (succ p) ≝ 421 λp,g,def. 422 match stmt_at … (joint_if_code … def) (joint_if_entry … def) 423 return λx.stmt_at ???? = x → ? with 424 [ Some s ⇒ 425 match s return λx.stmt_at ???? = Some ? x → ? with 426 [ sequential s' nxt ⇒ 427 match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with 428 [ step_seq s'' ⇒ 429 match s'' return λx.stmt_at ???? = Some ? (sequential … (step_seq … x) nxt) → ? with 430 [ COST_LABEL c ⇒ λ_.〈c, nxt〉 431  _ ⇒ λabs.⊥ 432 ] 433  _ ⇒ λabs.⊥ 434 ] 435  _ ⇒ λabs.⊥ 436 ] 437  _ ⇒ λabs.⊥ 438 ] (refl …). 439 @hide_prf 440 cases def in abs; def #def #good_def 441 cases (entry_costed … good_def) #c * #nxt' #EQ >EQ #ABS destruct 442 qed. 443 444 record b_graph_translate_props 445 (src_g_pars, dst_g_pars : graph_params) 446 (globals: list ident) 447 (data : b_graph_translate_data src_g_pars dst_g_pars globals) 448 (data_regs : list register) 449 (def_in : joint_closed_internal_function src_g_pars globals) 450 (def_out : joint_closed_internal_function dst_g_pars globals) 451 (f_lbls : label → option (list label)) 452 (f_regs : label → option (list register)) : Prop ≝ 453 { res_def_out_eq : 454 joint_if_result … def_out = init_ret … data 455 ; pars_def_out_eq : 456 joint_if_params … def_out = init_params … data 457 ; ss_def_out_eq : 458 joint_if_stacksize … def_out = init_stack_size … data 459 ; entry_eq : 460 pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in) 461 ; partition_lbls : partial_partition … f_lbls 462 ; partition_regs : partial_partition … f_regs 463 ; freshness_lbls : 468 464 (∀l.opt_All … (All … 469 465 (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ 470 fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l)) ∧ 466 fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l)) 467 ; freshness_regs : 471 468 (∀l.opt_All … (All … 472 469 (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 473 fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l)) ∧ 470 fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l)) 471 ; freshness_data_regs : 472 All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 473 fresh_for_univ … reg (joint_if_runiverse … def_out)) data_regs 474 ; data_regs_disjoint : ∀l.opt_All … (λregs.∀r.r ∈ regs → r ∈ data_regs → False) (f_regs l) 475 ; multi_fetch_ok : 474 476 ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s → 475 477 ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧ 476 478 match s with 477 479 [ sequential s' nxt ⇒ 478 l ~❨f_step l s', l::lbls, regs❩~> nxt in joint_if_code … def_out 480 let block ≝ 481 if eq_identifier … (joint_if_entry … def_in) l then 482 append_seq_list … (f_step … data l s') (added_prologue … data) 483 else 484 f_step … data l s' in 485 l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out 479 486  final s' ⇒ 480 l ~❨f_fin l s', l::lbls, regs❩~> it in joint_if_code … def_out487 l ~❨f_fin … data l s', l::lbls, regs❩~> it in joint_if_code … def_out 481 488  FCOND abs _ _ _ ⇒ Ⓧabs 482 ]. 489 ] 490 }. 491 492 lemma if_merge_right : ∀A.∀b.∀x,y : A.x = y → if b then x else y = y. 493 #A * #x #y #EQ >EQ % qed. 494 495 lemma append_seq_list_nil : ∀p,g,b.append_seq_list p g b [ ] = b. 496 #p #g #b elim b b 497 [ ** #a #b #c normalize >append_nil % 498  #f #IH @bnew_proper #r @IH 499 ] 500 qed. 501 502 definition pair_swap : ∀A,B.(A × B) → B × A ≝ λA,B,pr.〈\snd pr, \fst pr〉. 503 504 (* translation with inline fresh register allocation *) 505 definition b_graph_translate : 506 ∀src_g_pars,dst_g_pars : graph_params. 507 ∀globals: list ident. 508 (* initialization info *) 509 ∀data : bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals). 510 (* source function *) 511 ∀def_in : joint_closed_internal_function src_g_pars globals. 512 (* destination function *) 513 Σdef_out : joint_closed_internal_function dst_g_pars globals. 514 ∃data',regs,f_lbls,f_regs. 515 bind_new_instantiates … data' data regs ∧ 516 b_graph_translate_props … data' regs def_in def_out f_lbls f_regs 517 ≝ 518 λsrc_g_pars,dst_g_pars,globals,data,def. 519 let runiv_data ≝ bcompile … (pair_swap ?? ∘ fresh RegisterTag) data (joint_if_runiverse … def) in 520 let runiv ≝ \fst runiv_data in 521 let data ≝ \snd runiv_data in 522 let entry ≝ joint_if_entry … def in 523 let init ≝ 524 mk_joint_internal_function dst_g_pars globals 525 (joint_if_luniverse … def) 526 runiv 527 (init_ret … data) (init_params … data) (init_stack_size … data) 528 (add ?? (empty_map ? (joint_statement ??)) entry (RETURN …)) 529 («pi1 … entry, mem_set_add_id …») in 530 let f : label → joint_statement (src_g_pars : params) globals → 531 joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 532 λlbl,stmt,def. 533 match stmt with 534 [ sequential inst next ⇒ 535 b_adds_graph … (f_step … data lbl inst) lbl next def 536  final inst ⇒ 537 b_fin_adds_graph … (f_fin … data lbl inst) lbl def 538  FCOND abs _ _ _ ⇒ Ⓧabs 539 ] in 540 let def_out ≝ foldi ??? f (joint_if_code … def) init in 541 let init_c_nxt ≝ get_first_costlabel … def in 542 let def_out_nxt ≝ adds_graph_post … (added_prologue … data) (\snd (init_c_nxt)) def_out in 543 ««add_graph … entry (sequential … (COST_LABEL … (\fst init_c_nxt)) (\snd def_out_nxt)) (\fst def_out_nxt), ?», ?». 544 @hide_prf 545 [ cases daemon 546  cases daemon (* TODO *) 547 ] qed. 483 548 484 549 definition b_graph_transform_program : 485 550 ∀src_g_pars,dst_g_pars : graph_params. 486 ∀X : list ident → Type[0].487 551 (* initialization *) 488 552 (∀globals.joint_closed_internal_function src_g_pars globals → 489 (call_dest dst_g_pars) × (paramsT dst_g_pars) × ℕ × (X globals)) → 490 (* functions dictating the translation *) 491 (∀globals.X globals → label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) → 492 (∀globals.X globals → label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) → 493 joint_program src_g_pars → joint_program dst_g_pars ≝ 494 λsrc,dst,X,init,f_step,f_fin,p. 553 bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals)) → 554 joint_program src_g_pars → 555 joint_program dst_g_pars ≝ 556 λsrc,dst,init,p. 495 557 transform_program ??? p 496 558 (λvarnames.transf_fundef ?? (λdef_in. 497 let 〈fields, init_data〉 ≝ init varnames def_in in 498 let 〈init_ret, init_params, init_stack_size〉 ≝ fields in 499 b_graph_translate … init_ret init_params init_stack_size 500 (f_step ? init_data) (f_fin ? init_data) def_in)). 559 b_graph_translate … (init varnames def_in) def_in)). 501 560 502 561 definition added_registers : … … 513 572 opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l). 514 573 515 (* translation without register allocation (more or less an alias) *)574 (*(* translation without register allocation (more or less an alias) *) 516 575 definition graph_translate : 517 576 ∀src_g_pars,dst_g_pars : graph_params. … … 532 591 (λl,s.return trans_step l s) 533 592 (λl,s.return trans_fin_step l s). 534 593 *) 535 594 (* 536 595 let rec add_translates
Note: See TracChangeset
for help on using the changeset viewer.