Ignore:
Timestamp:
Mar 11, 2013, 1:02:02 PM (7 years ago)
Author:
piccolo
Message:

1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2816 r2843  
    633633| % [2: % [2: % [% %]] | skip] @(multi_fetch_ok … H3 … EQstmt_at) ]
    634634qed.
     635
     636lemma b_graph_transform_program_fetch_statement_plus :
     637 ∀src,dst:sem_graph_params.
     638 ∀data : ∀globals.joint_closed_internal_function src globals →
     639  bound_b_graph_translate_data src dst globals.
     640 ∀prog_in : joint_program src.
     641 ∀init_regs : block → list register.
     642 ∀f_lbls : block → label → list label.
     643 ∀f_regs : block → label → list register.
     644 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
     645 let prog_out ≝ b_graph_transform_program … data prog_in in
     646 let src_genv ≝ globalenv_noinit ? prog_in in
     647 let dst_genv ≝ globalenv_noinit ? prog_out in
     648 ∀pc,id,def_in,s.
     649 fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
     650 ∃init_data,def_out.
     651 let bl ≝ pc_block pc in
     652 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
     653 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
     654 let l ≝ point_of_pc dst pc in
     655 ∃lbls,regs.
     656 f_lbls bl l = lbls ∧
     657 f_regs bl l = regs ∧
     658 joint_if_entry … def_out = joint_if_entry … def_in ∧
     659 partial_partition … (f_lbls bl) ∧
     660 partial_partition … (f_regs bl) ∧
     661 (∀l.All …
     662    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
     663           fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls bl l)) ∧
     664  (∀l.All …
     665    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
     666           fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs bl l)) ∧
     667  match s with
     668  [ sequential s' nxt ⇒
     669    let block ≝
     670      if eq_identifier … (joint_if_entry … def_in) l then
     671        append_seq_list … (f_step … init_data l s') (added_prologue … init_data)
     672      else
     673        f_step … init_data l s' in
     674    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
     675  | final s' ⇒
     676    l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
     677  | FCOND abs _ _ _ ⇒ Ⓧabs
     678  ].
     679#src #dst #data #prog_in
     680#init_regs #f_lbls #f_regs #props
     681#pc #id #def_in #s
     682#H @('bind_inversion H) * #id' #def_in' -H
     683#EQfif
     684#H @('bind_inversion H) -H #s
     685#H lapply (opt_eq_from_res ???? H) -H
     686#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
     687cases (b_graph_transform_program_fetch_internal_function … props … EQfif)
     688#a * #b ** #H1 #H2 #H3 %{a} %{b} %
     689[ %{H1 H2}
     690| %
     691   [2:
     692      %
     693        [2: %
     694            [%
     695               [%
     696                  [%
     697                     [%
     698                        [%
     699                           [%
     700                              %
     701                            | @(entry_eq … H3)
     702                            ]
     703                        | @(partition_lbls … H3)
     704                        ]
     705                     |  @(partition_regs … H3)
     706                     ]
     707                  | @(freshness_lbls … H3)
     708                  ]
     709               |  @(freshness_regs … H3)
     710               ]
     711            |  @(multi_fetch_ok … H3 … EQstmt_at)
     712            ]
     713        |
     714        ]
     715   |
     716   ]
     717]         
     718qed.
Note: See TracChangeset for help on using the changeset viewer.