 Timestamp:
 Mar 7, 2013, 2:51:40 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/TranslateUtils.ma
r2723 r2806 355 355 *) 356 356 357 definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝358 λX,Y,f.359 (∀x.opt_All … (λys.bool_to_Prop (uniqueb … ys)) (f x)) ∧360 (∀x1,x2.361 opt_All …362 (λys1.363 opt_All …364 (λys2.365 ∀y.y ∈ ys1 → y ∈ ys2 → x1 = x2)366 (f x2))367 (f x1)).368 369 357 lemma opt_All_intro : ∀X,P,o. 370 358 (∀x.o = Some ? x → P x) → opt_All X P o. #X #P * [//] #x #H @H % qed. … … 385 373 @hide_prf cases pt pt #pt whd in ⊢ (?%→?); #H % #G >G in H; * qed. 386 374 *) 375 376 let rec bind_new_P' R X (P : list R → X → Prop) (m : bind_new R X) on m : Prop ≝ 377 match m with 378 [ bret x ⇒ P [ ] x 379  bnew f ⇒ 380 ∀r.bind_new_P' R X (λl.P (l @ [r])) (f r) 381 ]. 382 383 definition step_registers : ∀p : uns_params.∀globals. 384 joint_step p globals → list register ≝ 385 λp,globals,s.get_used_registers_from_step … (functs … p) s. 386 387 definition step_forall_registers : ∀p : uns_params.∀globals. 388 (register → Prop) → joint_step p globals → Prop ≝ 389 λp,globals,P,s.All … P (step_registers … s). 390 391 definition fin_step_registers : ∀p : uns_params. 392 joint_fin_step p → list register ≝ 393 λp,s.match s with [ TAILCALL _ _ r ⇒ f_call_args … (functs … p) r  _ ⇒ [ ] ]. 394 395 definition fin_step_forall_registers : ∀p : uns_params. 396 (register → Prop) → joint_fin_step p → Prop ≝ 397 λp,P,s.All … P (fin_step_registers … s). 398 399 definition fin_step_forall_labels : ∀p : uns_params. 400 (label → Prop) → joint_fin_step p → Prop ≝ 401 λp,P,s.All … P (fin_step_labels … s). 402 403 definition step_labels_and_registers_in : ∀p : uns_params.∀globals. 404 list label → list register → joint_step p globals → Prop ≝ 405 λp,g,allowed_l,allowed_r,s. 406 step_forall_labels … (In ? allowed_l) s ∧ 407 step_forall_registers … (In ? allowed_r) s. 408 409 definition fin_step_labels_and_registers_in : ∀p : uns_params. 410 list label → list register → joint_fin_step p → Prop ≝ 411 λp,allowed_l,allowed_r,s. 412 fin_step_forall_labels … (In ? allowed_l) s ∧ 413 fin_step_forall_registers … (In ? allowed_r) s. 387 414 388 415 record b_graph_translate_data … … 393 420 ; init_stack_size : ℕ 394 421 ; added_prologue : list (joint_seq dst globals) 422 ; new_regs : list register (* new registers added globally *) 395 423 ; f_step : label → joint_step src globals → bind_step_block dst globals 396 424 ; f_fin : label → joint_fin_step src → bind_fin_block dst globals 397 ; good_f_step_good : 398 ∀l,s.bind_new_P ?? 399 (λblock.let 〈pref, op, post〉 ≝ block in 425 ; good_f_step : 426 ∀l,s.bind_new_P' ?? 427 (λlocal_new_regs,block.let 〈pref, op, post〉 ≝ block in 428 ∀l. 429 let allowed_labels ≝ l :: step_labels … s in 430 let allowed_registers ≝ new_regs @ local_new_regs @ step_registers … s in 400 431 All (label → joint_seq ??) 401 (λs'. ∀l.step_forall_labels … (In ? (l :: step_labels … s)) (s' l))432 (λs'.step_labels_and_registers_in … allowed_labels allowed_registers (step_seq dst globals (s' l))) 402 433 pref ∧ 403 (∀l.step_forall_labels … (In ? (l :: step_labels … s)) (op l)) ∧404 All (joint_seq ??) (step_ forall_labels … (In ? (step_labels … s))) post)434 step_labels_and_registers_in … allowed_labels allowed_registers (op l) ∧ 435 All (joint_seq ??) (step_labels_and_registers_in … allowed_labels allowed_registers) post) 405 436 (f_step l s) 406 437 ; good_f_fin : 407 ∀l,s.bind_new_P ?? 408 (λblock.let 〈pref, op〉 ≝ block in 409 All (joint_seq ??) (step_forall_labels … (In ? (fin_step_labels … s))) pref ∧ 410 All … (In ? (fin_step_labels … s)) (fin_step_labels … op)) 438 ∀l,s.bind_new_P' ?? 439 (λlocal_new_regs,block.let 〈pref, op〉 ≝ block in 440 let allowed_labels ≝ l :: fin_step_labels … s in 441 let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in 442 All (joint_seq ??) (λs.step_labels_and_registers_in … allowed_labels allowed_registers s) pref ∧ 443 fin_step_labels_and_registers_in … allowed_labels allowed_registers op) 411 444 (f_fin l s) 412 445 ; f_step_on_cost : 413 446 ∀l,c.f_step l (COST_LABEL … c) = 414 447 bret ? (step_block ??) 〈[ ], λ_.COST_LABEL dst globals c, [ ]〉 448 ; cost_in_f_step : 449 ∀l,s,c. 450 bind_new_P ?? 451 (λblock.∀l'.\snd (\fst block) l' = COST_LABEL dst globals c → 452 s = COST_LABEL … c) (f_step l s) 415 453 }. 454 455 definition bound_b_graph_translate_data ≝ 456 λsrc,dst,globals. 457 Σd : bind_new register (b_graph_translate_data src dst globals). 458 bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d. 459 460 unification hint 0 ≔ src,dst,globals ⊢ 461 bound_b_graph_translate_data src dst globals ≡ 462 Sig (bind_new register (b_graph_translate_data src dst globals)) (λd.bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d). 416 463 417 464 definition get_first_costlabel : ∀p,g. … … 436 483 qed. 437 484 485 definition partial_partition : ∀X.∀Y : DeqSet.(X → list Y) → Prop ≝ 486 λX,Y,f. 487 (∀x.bool_to_Prop (uniqueb … (f x))) ∧ 488 (∀x1,x2,y.y ∈ f x1 → y ∈ f x2 → x1 = x2). 489 438 490 record b_graph_translate_props 439 491 (src_g_pars, dst_g_pars : graph_params) 440 492 (globals: list ident) 441 493 (data : b_graph_translate_data src_g_pars dst_g_pars globals) 442 (data_regs : list register)443 494 (def_in : joint_closed_internal_function src_g_pars globals) 444 495 (def_out : joint_closed_internal_function dst_g_pars globals) 445 (f_lbls : label → option (list label))446 (f_regs : label → option (list register)) : Prop ≝496 (f_lbls : label → list label) 497 (f_regs : label → list register) : Prop ≝ 447 498 { res_def_out_eq : 448 499 joint_if_result … def_out = init_ret … data … … 456 507 ; partition_regs : partial_partition … f_regs 457 508 ; freshness_lbls : 458 (∀l. opt_All … (All …509 (∀l.All … 459 510 (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ 460 fresh_for_univ … lbl (joint_if_luniverse … def_out)) )(f_lbls l))511 fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls l)) 461 512 ; freshness_regs : 462 (∀l. opt_All … (All …513 (∀l.All … 463 514 (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 464 fresh_for_univ … reg (joint_if_runiverse … def_out)) )(f_regs l))515 fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs l)) 465 516 ; freshness_data_regs : 466 517 All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 467 fresh_for_univ … reg (joint_if_runiverse … def_out)) data_regs468 ; data_regs_disjoint : ∀l .opt_All … (λregs.∀r.r ∈ regs → r ∈ data_regs → False) (f_regs l)518 fresh_for_univ … reg (joint_if_runiverse … def_out)) (new_regs … data) 519 ; data_regs_disjoint : ∀l,r.r ∈ f_regs l → r ∈ new_regs … data → False 469 520 ; multi_fetch_ok : 470 521 ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s → 471 ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧522 let lbls ≝ f_lbls l in let regs ≝ f_regs l in 472 523 match s with 473 524 [ sequential s' nxt ⇒ … … 501 552 ∀globals: list ident. 502 553 (* initialization info *) 503 ∀data : b ind_new register (b_graph_translate_data src_g_pars dst_g_pars globals).554 ∀data : bound_b_graph_translate_data src_g_pars dst_g_pars globals. 504 555 (* source function *) 505 556 ∀def_in : joint_closed_internal_function src_g_pars globals. … … 507 558 Σdef_out : joint_closed_internal_function dst_g_pars globals. 508 559 ∃data',regs,f_lbls,f_regs. 509 bind_new_instantiates … data' data regs ∧510 b_graph_translate_props … data' regsdef_in def_out f_lbls f_regs560 bind_new_instantiates ?? data' data regs ∧ (* so new_regs … data = regs *) 561 b_graph_translate_props … data' def_in def_out f_lbls f_regs 511 562 ≝ 512 563 λsrc_g_pars,dst_g_pars,globals,data,def. … … 545 596 (* initialization *) 546 597 (∀globals.joint_closed_internal_function src_g_pars globals → 547 b ind_new register (b_graph_translate_data src_g_pars dst_g_pars globals)) →598 bound_b_graph_translate_data src_g_pars dst_g_pars globals) → 548 599 joint_program src_g_pars → 549 600 joint_program dst_g_pars ≝
Note: See TracChangeset
for help on using the changeset viewer.