Changeset 2391 for src/Clight/SimplifyCasts.ma
 Timestamp:
 Oct 9, 2012, 3:10:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SimplifyCasts.ma
r2353 r2391 1982 1982  Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2) 1983 1983  Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *) 1984  Swhile e s1 cl ⇒ Swhile (simplify_e e) (simplify_statement s1) cl(* TODO: try to reduce size of e *)1984  Swhile e s1 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *) 1985 1985  Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *) 1986 1986  Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *) … … 2015 2015  cc_stop : cont_cast Kstop Kstop 2016 2016  cc_seq : ∀s,k,k'. cont_cast k k' → cont_cast (Kseq s k) (Kseq (simplify_statement s) k') 2017  cc_while : ∀e,s, cl,k,k'.2017  cc_while : ∀e,s,k,k'. 2018 2018 cont_cast k k' → 2019 cont_cast (Kwhile e s cl k) (Kwhile (simplify_e e) (simplify_statement s) clk')2019 cont_cast (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') 2020 2020  cc_dowhile : ∀e,s,k,k'. 2021 2021 cont_cast k k' → … … 2424 2424  1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta // 2425 2425 ] ] 2426  6: #e #s # cl #Hind_s #k #k' #Hcont_cast2426  6: #e #s #Hind_s #k #k' #Hcont_cast 2427 2427 whd in match (find_label ???); 2428 2428 whd in match (find_label ? (simplify_statement ?) ?); 2429 elim (elim_IH_aux lab s (Kwhile e s cl k) (Kwhile (simplify_e e) (simplify_statement s) clk') ? Hind_s)2429 elim (elim_IH_aux lab s (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') ? Hind_s) 2430 2430 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2431 2431 normalize nodelta %{kst'} /2/ … … 2616 2616 [ 1: //  2: %1 // ] 2617 2617  3: (* Kwhile *) 2618 #cond #body # cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq2618 #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq 2619 2619 whd in match (ret ??) in Eq; destruct (Eq) 2620 %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body) cl) k0' en m)} @conj2620 %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} @conj 2621 2621 [ 1: //  2: %1 // ] 2622 2622  4: (* Kdowhile *) … … 2783 2783 [ 1: //  2: <e0 %1 // ] 2784 2784 ] ] ] ] 2785  6: # cl #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;2785  6: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2786 2786 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq 2787 2787 whd in match (exec_step ??) in Heq ⊢ %; … … 2798 2798  1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %; 2799 2799 [ 1: destruct skip (condtrace) 2800 %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) clk') en m)}2800 %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) k') en m)} 2801 2801 @conj 2802 2802 [ 1: //  2: <e0 %1 @cc_while // ] 2803 2803  2: destruct skip (condtrace) 2804 %{(State (simplify_function f) (optional_cost cl Sskip)k' en m)} @conj2805 [ 1: //  2: <e0 cases cl [2:#cl']%1 // ]2804 %{(State (simplify_function f) Sskip k' en m)} @conj 2805 [ 1: //  2: <e0 %1 // ] 2806 2806 ] ] ] ] 2807 2807  7: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; … … 2850 2850 [ 1: #Hk #Hk' #_ 2851 2851  2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 2852  3: #cond #body # cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_2852  3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 2853 2853  4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 2854 2854  5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ … … 2858 2858 destruct (H) 2859 2859 [ 1,4: %{(State (simplify_function f) Sbreak k0' en m)} @conj [ 1,3: //  2,4: %1 // ] 2860  %{(State (simplify_function f) (optional_cost cl Sskip) k0' en m)} @conj try // cases cl [2:#cl'] %1 // 2861  3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ] 2860  2,3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ] 2862 2861  10: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2863 2862 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq … … 2866 2865 [ 1: #Hk #Hk' #_ 2867 2866  2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 2868  3: #cond #body # cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_2867  3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 2869 2868  4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 2870 2869  5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ … … 2874 2873 destruct (H) 2875 2874 [ 1,4,6: %{(State (simplify_function f) Scontinue k0' en m)} @conj try // %1 // 2876  2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body) cl) k0' en m)}2875  2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} 2877 2876 @conj try // %1 // 2878 2877  3: elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq elim Hsim_cond in H; … … 3008 3007 [ 1: #Hk #Hk' #_ 3009 3008  2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 3010  3: #cond #body # cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_3009  3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 3011 3010  4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 3012 3011  5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
Note: See TracChangeset
for help on using the changeset viewer.