Changeset 2816 for src


Ignore:
Timestamp:
Mar 7, 2013, 10:20:26 PM (7 years ago)
Author:
sacerdot
Message:

Repaired after Paolo's commit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2796 r2816  
    449449  λdata,prog_in.
    450450  λinit_regs : block → list register.
    451   λf_lbls : block → label → option (list label).
    452   λf_regs : block → label → option (list register).
     451  λf_lbls : block → label → list label.
     452  λf_regs : block → label → list register.
    453453   let prog_out ≝ b_graph_transform_program src dst data prog_in in
    454454   let src_genv ≝ globalenv_noinit ? prog_in in
     
    459459  find_funct_ptr … dst_genv bl = return (Internal ? def_out) ∧
    460460  bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
    461   b_graph_translate_props src dst ? init_data (init_regs bl)
     461  b_graph_translate_props src dst ? init_data
    462462    def_in def_out (f_lbls bl) (f_regs bl).
    463  
     463
    464464lemma make_b_graph_transform_program_props :
    465465 ∀src,dst:sem_graph_params.
    466466 ∀data : ∀globals.joint_closed_internal_function src globals →
    467   bind_new register (b_graph_translate_data src dst globals).
     467  bound_b_graph_translate_data src dst globals.
    468468 ∀prog_in : joint_program src.
    469469 let prog_out ≝ b_graph_transform_program … data prog_in in
     
    471471 let dst_genv ≝ globalenv_noinit ? prog_out in
    472472 ∃init_regs : block → list register.
    473  ∃f_lbls : block → label → option (list label).
    474  ∃f_regs : block → label → option (list register).
     473 ∃f_lbls : block → label → list label.
     474 ∃f_regs : block → label → list register.
    475475 b_graph_transform_program_props src dst data prog_in init_regs f_lbls f_regs.
    476476#src #dst #data #prog_in
     
    489489[ #functs1_empty | #p #f #IH #p_not_in ]
    490490#functs2 #H1 #H2 #transf
    491 [ %{(λ_.[ ])} %{(λ_.λ_.None ?)} %{(λ_.λ_.None ?)}
     491[ %{(λ_.[ ])} %{(λ_.λ_.[])} %{(λ_.λ_.[])}
    492492  #bl #def_in #ABS @⊥ lapply ABS -ABS
    493493  whd in match find_funct_ptr;
     
    552552 ∀src,dst:sem_graph_params.
    553553 ∀data : ∀globals.joint_closed_internal_function src globals →
    554   bind_new register (b_graph_translate_data src dst globals).
     554  bound_b_graph_translate_data src dst globals.
    555555 ∀prog_in : joint_program src.
    556556 ∀init_regs : block → list register.
    557  ∀f_lbls : block → label → option (list label).
    558  ∀f_regs : block → label → option (list register).
     557 ∀f_lbls : block → label → list label.
     558 ∀f_regs : block → label → list register.
    559559 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
    560560 let prog_out ≝ b_graph_transform_program … data prog_in in
     
    566566 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
    567567 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
    568  b_graph_translate_props src dst ? init_data (init_regs bl)
     568 b_graph_translate_props src dst ? init_data
    569569    def_in def_out (f_lbls bl) (f_regs bl).
    570570#src #dst #data #prog_in
     
    589589 ∀src,dst:sem_graph_params.
    590590 ∀data : ∀globals.joint_closed_internal_function src globals →
    591   bind_new register (b_graph_translate_data src dst globals).
     591  bound_b_graph_translate_data src dst globals.
    592592 ∀prog_in : joint_program src.
    593593 ∀init_regs : block → list register.
    594  ∀f_lbls : block → label → option (list label).
    595  ∀f_regs : block → label → option (list register).
     594 ∀f_lbls : block → label → list label.
     595 ∀f_regs : block → label → list register.
    596596 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
    597597 let prog_out ≝ b_graph_transform_program … data prog_in in
     
    606606 let l ≝ point_of_pc dst pc in
    607607 ∃lbls,regs.
    608  f_lbls bl l = Some ? lbls ∧
    609  f_regs bl l = Some ? regs ∧
     608 f_lbls bl l = lbls ∧
     609 f_regs bl l = regs ∧
    610610  match s with
    611611  [ sequential s' nxt ⇒
     
    630630cases (b_graph_transform_program_fetch_internal_function … props … EQfif)
    631631#a * #b ** #H1 #H2 #H3 %{a} %{b} %
    632 [ %{H1 H2} | @(multi_fetch_ok … H3 … EQstmt_at) ]
    633 qed.
     632[ %{H1 H2}
     633| % [2: % [2: % [% %]] | skip] @(multi_fetch_ok … H3 … EQstmt_at) ]
     634qed.
Note: See TracChangeset for help on using the changeset viewer.