Changeset 2806 for src/joint


Ignore:
Timestamp:
Mar 7, 2013, 2:51:40 PM (7 years ago)
Author:
tranquil
Message:

new b_graph_translate obligations

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r2723 r2806  
    355355*)
    356356
    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 
    369357lemma opt_All_intro : ∀X,P,o.
    370358(∀x.o = Some ? x → P x) → opt_All X P o. #X #P * [//] #x #H @H % qed.
     
    385373@hide_prf cases pt -pt #pt whd in ⊢ (?%→?); #H % #G >G in H; * qed.
    386374*)
     375
     376let rec bind_new_P' R X (P : list R → X → Prop) (m : bind_new R X) on m : Prop ≝
     377match 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
     383definition 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
     387definition 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
     391definition 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
     395definition 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
     399definition 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
     403definition 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
     409definition 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.
    387414
    388415record b_graph_translate_data
     
    393420; init_stack_size : ℕ
    394421; added_prologue : list (joint_seq dst globals)
     422; new_regs : list register (* new registers added globally *)
    395423; f_step : label → joint_step src globals → bind_step_block dst globals
    396424; 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
    400431       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)))
    402433         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)
    405436    (f_step l s)
    406437; 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)
    411444    (f_fin l s)
    412445; f_step_on_cost :
    413446  ∀l,c.f_step l (COST_LABEL … c) =
    414447    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)
    415453}.
     454
     455definition bound_b_graph_translate_data ≝
     456λsrc,dst,globals.
     457Σd : bind_new register (b_graph_translate_data src dst globals).
     458bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d.
     459
     460unification hint 0 ≔ src,dst,globals ⊢
     461bound_b_graph_translate_data src dst globals ≡
     462Sig (bind_new register (b_graph_translate_data src dst globals)) (λd.bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d).
    416463
    417464definition get_first_costlabel : ∀p,g.
     
    436483qed.
    437484
     485definition 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
    438490record b_graph_translate_props
    439491  (src_g_pars, dst_g_pars : graph_params)
    440492  (globals: list ident)
    441493  (data : b_graph_translate_data src_g_pars dst_g_pars globals)
    442   (data_regs : list register)
    443494  (def_in : joint_closed_internal_function src_g_pars globals)
    444495  (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 ≝
    447498{ res_def_out_eq :
    448499           joint_if_result … def_out = init_ret … data
     
    456507; partition_regs : partial_partition … f_regs
    457508; freshness_lbls :
    458   (∀l.opt_All … (All …
     509  (∀l.All …
    459510    (λ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))
    461512; freshness_regs :
    462   (∀l.opt_All … (All …
     513  (∀l.All …
    463514    (λ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))
    465516; freshness_data_regs :
    466517  All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
    467                fresh_for_univ … reg (joint_if_runiverse … def_out)) data_regs
    468 ; 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
    469520; multi_fetch_ok :
    470521  ∀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
    472523  match s with
    473524  [ sequential s' nxt ⇒
     
    501552  ∀globals: list ident.
    502553  (* initialization info *)
    503   ∀data : bind_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.
    504555  (* source function *)
    505556  ∀def_in : joint_closed_internal_function src_g_pars globals.
     
    507558  Σdef_out : joint_closed_internal_function dst_g_pars globals.
    508559  ∃data',regs,f_lbls,f_regs.
    509     bind_new_instantiates … data' data regs ∧
    510     b_graph_translate_props … data' regs def_in def_out f_lbls f_regs
     560    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
    511562   ≝
    512563  λsrc_g_pars,dst_g_pars,globals,data,def.
     
    545596  (* initialization *)
    546597  (∀globals.joint_closed_internal_function src_g_pars globals →
    547     bind_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) →
    548599  joint_program src_g_pars →
    549600  joint_program dst_g_pars ≝
Note: See TracChangeset for help on using the changeset viewer.