Ignore:
Timestamp:
Mar 30, 2013, 1:11:01 AM (8 years ago)
Author:
campbell
Message:

Main part of combined switch removal and labelling proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r3044 r3046  
    20002000 ∀ssc_writeable.
    20012001 ∀ssc_mem_hyp : sr_memext ssc_m ssc_m_ext ssc_writeable.
    2002  (match ssc_fd with
     2002 switch_cont_sim (match ssc_fd with
    20032003  [ CL_Internal ssc_f ⇒
    2004     switch_cont_sim (\snd (function_switch_removal ssc_f)) ssc_k ssc_k_ext
    2005   | _ ⇒ True ])
     2004    (\snd (function_switch_removal ssc_f))
     2005  | _ ⇒ [ ] ]) ssc_k ssc_k_ext
    20062006    switch_state_sim ge (Callstate ssc_vf ssc_fd ssc_args ssc_k ssc_m)
    20072007                        (Callstate ssc_vf (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext)
     
    29212921       [ 1: whd in ⊢ ((??%%) → (??%%)); #Heq whd destruct (Heq) @conj try @refl
    29222922            %2{sss_writeable … sss_mem_hyp}
    2923             cases called_fundef
    2924             [ 2: #id #tl #ty @I
    2925             | 1: #called_function whd
    2926                  cut (sss_func_tr = \fst (function_switch_removal sss_func))
    2927                  [ 1: <sss_func_hyp @refl ] #H >H -H
    2928                  cut (sss_new_vars = \snd (function_switch_removal sss_func))
    2929                  [ 1: <sss_func_hyp @refl ] #H >H -H
    2930                  @(swc_call … sss_k_hyp) try assumption
    2931                  <sss_func_hyp @refl ]
     2923            cut (sss_func_tr = \fst (function_switch_removal sss_func))
     2924            [ 1: <sss_func_hyp @refl ] #H >H -H
     2925            cut (sss_new_vars = \snd (function_switch_removal sss_func))
     2926            [ 1: <sss_func_hyp @refl ] #H >H -H
     2927            @(swc_call … sss_k_hyp) try assumption
     2928            <sss_func_hyp @refl
    29322929       | 2: #ret_expr #Hexec_ret_expr
    29332930            cases (bindIO_inversion ??????? Hexec_ret_expr) #xret * #Heq_ret
     
    29382935            [ 1: <sss_func_hyp @refl ] #H >H -H
    29392936            @(sws_callstate … sss_writeable … sss_mem_hyp)
    2940             cases called_fundef
    2941             [ 2: #id #tl #ty @I
    2942             | 1: #called_function whd
    2943                  cut (sss_func_tr = \fst (function_switch_removal sss_func))
    2944                  [ 1: <sss_func_hyp @refl ] #H >H -H
    2945                  cut (sss_new_vars = \snd (function_switch_removal sss_func))
    2946                  [ 1: <sss_func_hyp @refl ] #H >H -H
    2947                  @(swc_call … sss_k_hyp) try assumption
    2948                  <sss_func_hyp @refl ] ]
     2937            cut (sss_func_tr = \fst (function_switch_removal sss_func))
     2938            [ 1: <sss_func_hyp @refl ] #H >H -H
     2939            cut (sss_new_vars = \snd (function_switch_removal sss_func))
     2940            [ 1: <sss_func_hyp @refl ] #H >H -H
     2941            @(swc_call … sss_k_hyp) try assumption
     2942            <sss_func_hyp @refl ]
    29492943  | 4: (* Sequence statement *)
    29502944       #Hexec %{0} whd in sss_result_hyp:(??%?); whd whd in Hexec:(??%?) ⊢ (??%?); destruct (Hexec)
Note: See TracChangeset for help on using the changeset viewer.