Changeset 2973


Ignore:
Timestamp:
Mar 27, 2013, 1:11:13 PM (4 years ago)
Author:
tranquil
Message:

semanticUtils adapted to changes in TranslateUtils?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2954 r2973  
    515515   let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
    516516  ∀bl,def_in.
    517   block_id … bl ≠ -1 →
    518517  find_funct_ptr … src_genv bl = return (Internal ? def_in) →
    519518  ∃init_data,def_out.
     
    653652 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
    654653 ∀bl : Σbl.block_region … bl = Code.∀id,def_in.
    655  block_id … bl ≠ -1 →
    656  fetch_internal_function … src_genv bl = return 〈id, def_in〉 →
    657  ∃init_data,def_out.
    658  fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
    659  bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
    660  b_graph_translate_props src dst ? init_data
    661     def_in def_out (f_lbls bl) (f_regs bl).
     654 if eqZb (block_id … bl) (-1) then
     655   (fetch_internal_function … dst_genv bl =
     656     return 〈pre_main_id, pre_main_generator … dst prog_out〉)
     657 else
     658   (fetch_internal_function … src_genv bl = return 〈id, def_in〉 →
     659   ∃init_data,def_out.
     660   fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
     661   bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
     662   b_graph_translate_props src dst ? init_data
     663      def_in def_out (f_lbls bl) (f_regs bl)).
    662664#src #dst #stacksizes #data #prog_in
    663665#init_regs #f_lbls #f_regs #props
    664 #bl #id #def_in #NEQ
     666#bl #id #def_in
     667@if_elim' #Hbl
     668[ whd in match fetch_internal_function; whd in match fetch_function;
     669  normalize nodelta >Hbl % ]
    665670#H @('bind_inversion H) * #id' * #def_in' -H
    666671normalize nodelta [2: #_ whd in ⊢ (??%%→?); #ABS destruct ]
    667672whd in match fetch_function; normalize nodelta
    668 >(eqZb_false … NEQ) normalize nodelta
     673>Hbl normalize nodelta
    669674#H @('bind_inversion (opt_eq_from_res … H)) -H #id'' #EQ1
    670675#H @('bind_inversion H) -H #def_in'' #H
    671676whd in ⊢ (??%%→??%%→?); #EQ2 #EQ3 destruct
    672 cases (props … NEQ H)
     677cases (props … H)
    673678#loc_data * #def_out ** #H1 #H2 #H3
    674679%{loc_data} %{def_out}
     
    676681whd in match fetch_internal_function;
    677682whd in match fetch_function; normalize nodelta
    678 >(eqZb_false … NEQ) normalize nodelta
     683>Hbl normalize nodelta
    679684>symbol_for_block_transf >EQ1 >m_return_bind
    680685>H1 %
     
    694699 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
    695700 ∀pc,id,def_in,s.
    696  block_id … (pc_block … pc) ≠ -1 →
    697  fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
    698  ∃init_data,def_out.
    699  let bl ≝ pc_block pc in
    700  fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
    701  bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
    702  let l ≝ point_of_pc dst pc in
    703  ∃lbls,regs.
    704  f_lbls bl l = lbls ∧
    705  f_regs bl l = regs ∧
    706   match s with
    707   [ sequential s' nxt ⇒
    708     let block ≝
    709       if eq_identifier … (joint_if_entry … def_in) l then
    710         append_seq_list … (f_step … init_data l s') (added_prologue … init_data)
    711       else
    712         f_step … init_data l s' in
    713     l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
    714   | final s' ⇒
    715     l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
    716   | FCOND abs _ _ _ ⇒ Ⓧabs
    717   ].
     701 if eqZb (block_id … (pc_block … pc)) (-1) then
     702   (fetch_internal_function … dst_genv (pc_block … pc) =
     703     return 〈pre_main_id, pre_main_generator … dst prog_out〉)
     704 else
     705   (fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
     706   ∃init_data,def_out.
     707   let bl ≝ pc_block pc in
     708   fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
     709   bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
     710   let l ≝ point_of_pc dst pc in
     711    let lbls ≝ f_lbls bl l in let regs ≝ f_regs bl l in
     712    match s with
     713    [ sequential s' nxt ⇒
     714      let block ≝
     715        if not_emptyb … (added_prologue … init_data) ∧
     716           eq_identifier … (joint_if_entry … def_in) l then
     717          bret … [ ]
     718        else
     719          f_step … init_data l s' in
     720      l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
     721    | final s' ⇒
     722      l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
     723    | FCOND abs _ _ _ ⇒ Ⓧabs
     724    ]).
    718725#src #dst #stacksizes #data #prog_in
    719726#init_regs #f_lbls #f_regs #props
    720 #pc #id #def_in #s #NEQ
     727#pc #id #def_in #s
     728lapply (b_graph_transform_program_fetch_internal_function … props
     729  (pc_block … pc) id def_in)
     730@if_elim' #Hbl >Hbl normalize nodelta [ #H @H ] #G
    721731#H @('bind_inversion H) * #id' #def_in' -H
    722732#EQfif
     
    724734#H lapply (opt_eq_from_res ???? H) -H
    725735#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
    726 cases (b_graph_transform_program_fetch_internal_function … props … NEQ EQfif)
     736cases (G … EQfif)
    727737#a * #b ** #H1 #H2 #H3 %{a} %{b} %
    728738[ %{H1 H2}
    729 | % [2: % [2: % [% %]] | skip] @(multi_fetch_ok … H3 … EQstmt_at) ]
     739| @(multi_fetch_ok … H3 … EQstmt_at)
     740]
    730741qed.
    731742
     
    743754 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
    744755 ∀pc,id,def_in,s.
    745  block_id … (pc_block … pc) ≠ -1 →
    746  fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
    747  ∃init_data,def_out.
    748  let bl ≝ pc_block pc in
    749  fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
    750  bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
    751  let l ≝ point_of_pc dst pc in
    752  ∃lbls,regs.
    753  f_lbls bl l = lbls ∧
    754  f_regs bl l = regs ∧
    755  joint_if_entry … def_out = joint_if_entry … def_in ∧
    756  partial_partition … (f_lbls bl) ∧
    757  partial_partition … (f_regs bl) ∧
    758  (∀l.All …
    759     (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
    760            fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls bl l)) ∧
    761   (∀l.All …
    762     (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
    763            fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs bl l)) ∧
    764   match s with
    765   [ sequential s' nxt ⇒
    766     let block ≝
    767       if eq_identifier … (joint_if_entry … def_in) l then
    768         append_seq_list … (f_step … init_data l s') (added_prologue … init_data)
    769       else
    770         f_step … init_data l s' in
    771     l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
    772   | final s' ⇒
    773     l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
    774   | FCOND abs _ _ _ ⇒ Ⓧabs
    775   ].
     756 if eqZb (block_id … (pc_block … pc)) (-1) then
     757   (fetch_internal_function … dst_genv (pc_block … pc) =
     758     return 〈pre_main_id, pre_main_generator … dst prog_out〉)
     759 else
     760   (fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
     761   ∃init_data,def_out.
     762   let bl ≝ pc_block pc in
     763   fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
     764   bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
     765   let l ≝ point_of_pc dst pc in
     766   let lbls ≝ f_lbls bl l in
     767   let regs ≝ f_regs bl l in
     768   partial_partition … (f_lbls bl) ∧
     769   partial_partition … (f_regs bl) ∧
     770   (∀l.All …
     771      (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
     772             fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls bl l)) ∧
     773    (∀l.All …
     774      (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
     775             fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs bl l)) ∧
     776   match s with
     777    [ sequential s' nxt ⇒
     778      let block ≝
     779        if not_emptyb … (added_prologue … init_data) ∧
     780           eq_identifier … (joint_if_entry … def_in) l then
     781          bret … [ ]
     782        else
     783          f_step … init_data l s' in
     784      l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
     785    | final s' ⇒
     786      l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
     787    | FCOND abs _ _ _ ⇒ Ⓧabs
     788    ]).
    776789#src #dst #stacksizes #data #prog_in
    777790#init_regs #f_lbls #f_regs #props
    778 #pc #id #def_in #s #NEQ
     791#pc #id #def_in #s
     792lapply (b_graph_transform_program_fetch_internal_function … props … (pc_block … pc) id def_in)
     793@if_elim' #Hbl >Hbl normalize nodelta
     794[ #H @H ] #G
    779795#H @('bind_inversion H) * #id' #def_in' -H
    780796#EQfif
     
    782798#H lapply (opt_eq_from_res ???? H) -H
    783799#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
    784 cases (b_graph_transform_program_fetch_internal_function … props … NEQ EQfif)
     800cases (G … EQfif)
    785801#a * #b ** #H1 #H2 #H3 %{a} %{b} %
    786802[ %{H1 H2}
    787 | %
    788    [2:
    789       %
    790         [2: %
    791             [%
    792                [%
    793                   [%
    794                      [%
    795                         [%
    796                            [%
    797                               %
    798                             | @(entry_eq … H3)
    799                             ]
    800                         | @(partition_lbls … H3)
    801                         ]
    802                      |  @(partition_regs … H3)
    803                      ]
    804                   | @(freshness_lbls … H3)
    805                   ]
    806                |  @(freshness_regs … H3)
    807                ]
    808             |  @(multi_fetch_ok … H3 … EQstmt_at)
    809             ]
    810         |
    811         ]
    812    |
    813    ]
     803| %{(multi_fetch_ok … H3 … EQstmt_at)}
     804  %{(freshness_regs … H3)}
     805  %{(freshness_lbls … H3)}
     806  %{(partition_regs … H3)}
     807  @(partition_lbls … H3)
    814808]         
    815809qed.
Note: See TracChangeset for help on using the changeset viewer.