Changeset 3044 for src/Clight/switchRemoval.ma

Timestamp:

Mar 29, 2013, 8:16:50 PM (7 years ago)

Author:

campbell

Message:

Start showing combination of switch removal and labelling is OK.
Fix typo in switch removal statement.

File:

• src/Clight/switchRemoval.ma (modified) (17 diffs)

src/Clight/switchRemoval.ma

@@ -2755 +2755 @@
   exec_step ge s1 = Value … 〈tr,s2〉 →  
   ∃n. after_n_steps (S n) … clight_exec ge' s1' (λ_. true)
-  (λtr',s2'. tr = tr' ∧ switch_state_sim ge' s2 s2').
+  (λtr',s2'. tr = tr' ∧ switch_state_sim ge s2 s2').
 #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state
 inversion Hsim_state
@@ -2798 +2798 @@
          <sss_func_hyp 
          lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
-         %1{u (refl ? (switch_removal s u))} try assumption try @refl         
-         #id #Hmem lapply (Hext_fresh_for_ge id Hmem) #Hfind <(rg_find_symbol … Hrelated id) @Hfind
+         %1{u (refl ? (switch_removal s u))} assumption
     | 3: #cond #body #k #k' #fgen #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
          lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
@@ -2810 +2809 @@
          | 3: whd in match (switch_removal ??); 
               cases (switch_removal body fgen) in Hincl; * #body' #fvs' #fgen' normalize nodelta #H @H
-         | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+         ]
     | 4: #cond #body #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
          lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')    
@@ -2825 +2824 @@
               | 2: whd in match (switch_removal ??); 
                    cases (switch_removal body u) in Hincl; * #body' #fvs' #u' normalize nodelta #H @H
-              | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+              ]
          | 2: %{u … (switch_removal Sskip u) } try assumption try //
-              [ 1: @(fresh_for_Sskip … Hfresh)
-              | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ]
+              @(fresh_for_Sskip … Hfresh)
+         ]
     | 5: #cond #stmt1 #stmt2 #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_
          #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
@@ -2834 +2833 @@
          #Hexec_step %{0} whd whd in Hresult:(??%?) Hexec_step:(??%?); destruct (Hexec_step)
          @conj try @refl
-         %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try // try assumption
-         #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
+         %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try // assumption
     | 6: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars
          #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
@@ -2847 +2845 @@
               whd in match (ret_vars ??); /2 by All_append_l/
          | 3: @(swc_for3 … u) //
-         | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+         ]
     | 7: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars
          #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
@@ -2854 +2852 @@
          %1{u … new_vars … sss_writeable … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)}
          try // try assumption
-         [ 1: whd in match (switch_removal ??) in ⊢ (??%%); destruct normalize
-              cases (switch_removal stmt1 u) * #stmt1' #fvs1' #u' normalize
-              cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' @refl
-         | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+         whd in match (switch_removal ??) in ⊢ (??%%); destruct normalize
+         cases (switch_removal stmt1 u) * #stmt1' #fvs1' #u' normalize
+         cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' @refl
     | 8: #k #k' #new_vars #Hsimcont #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
          lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
          #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl
          %1{sss_lu … new_vars … sss_writeable} try // try assumption
-         [ 1: destruct (sss_result_hyp) @refl
-         | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+         destruct (sss_result_hyp) @refl
     | 9: #en #en' #r #f #k #k' #old_vars #new_vars #Hsimcont #Hnew_vars_eq #Hdisjoint_k #_
          #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
@@ -2898 +2894 @@
        try // try assumption
        [ 1: @(fresh_for_Sskip … sss_lu_fresh)
-       | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
        | 2: #v #Hmem #vb #Hlookup lapply (sss_new_alloc v Hmem vb Hlookup) * * #Hvb #Hlow #Hhigh            
             cut (store_value_of_type' (typeof lhs) sss_m (\fst  xl) (\fst  xr) = Some ? m')
@@ -2962 +2957 @@
        | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
             /2 by All_append_l/
-       | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+       ]
        @(swc_seq … u') try //
        [ 2: >HeqB @refl
@@ -2985 +2980 @@
              | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
                   /2 by All_append_l/
-             | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
+             ]
        | 2: %1{u' … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqB} try assumption try //
              [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize #_
@@ -2991 +2986 @@
              | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
                   /2 by All_append_r/                   
-             | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ]
+             ] ]
   | 6: (* While loop *)
        #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp
@@ -3005 +3000 @@
              [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize //
              | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H
-             | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
              | 3: @(swc_while … sss_lu) try // 
                   [ 1: >HeqA @refl
@@ -3011 +3005 @@
              ]
        | 2: %{… sss_func_hyp … (switch_removal Sskip u')} try assumption try //
-            [ 1: lapply (switch_removal_fte body sss_lu) >HeqA #Hfte whd in match (ret_u ??) in Hfte;
-                 @(fresher_for_univ … Hfte) @(fresh_for_Sskip … sss_lu_fresh)
-            | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ]
+            lapply (switch_removal_fte body sss_lu) >HeqA #Hfte whd in match (ret_u ??) in Hfte;
+            @(fresher_for_univ … Hfte) @(fresh_for_Sskip … sss_lu_fresh)
+       ]
   | 7: (* do while loop *)
        #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp
@@ -3024 +3018 @@
        | 2: >HeqA @refl
        | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H
-       | 5: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
        | 4: @(swc_dowhile … sss_lu) try assumption try //
             [ 1: >HeqA @refl
@@ -3091 +3084 @@
                  ]
             | 2: %1{u' … sss_func_hyp … (switch_removal Sskip u')} try assumption try //
-                 [ 1: @(fresh_for_Sskip … sss_lu_fresh) ] ] ]
-        #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
+                 @(fresh_for_Sskip … sss_lu_fresh) ] ]
   | 9: (* break *)
        (* sss_enclosing_label TODO : switch case *)
@@ -3122 +3114 @@
             #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?));
             #Heq destruct (Heq) ]
-       #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
   | 10: (* continue *)
        #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta
@@ -3175 +3166 @@
              #_ #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?));
             #Heq destruct (Heq) ]
-       #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
   | 11: (* return *)
         #Hexec %{0} whd whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec