Changeset 2011 for src/Clight/SimplifyCasts.ma
 Timestamp:
 May 31, 2012, 4:41:33 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SimplifyCasts.ma
r2009 r2011 23 23 24 24 This might be too conservative  if we're going to cast it anyway, can't 25 I just ignore the fact that the integer doesn't fit? let (++)25 I just ignore the fact that the integer doesn't fit? 26 26 *) 27 27 … … 99 99 100 100 101 (* /!\ This lemma uses the "uniqueness of identity proofs" K axiom. I've tried doing a proper102 * induction on t but it turns out to be a nonwellfounded pandora box. /!\ *)103 (* Finally useless104 lemma type_eq_dec_identity : ∀t. type_eq_dec t t = inl ?? (refl ? t).105 #t elim (type_eq_dec t t)106 [ 1: @streicherK //107  2: #H elim H #Hcontr elim (Hcontr (refl ? t)) ] qed.108 *)109 110 (* Useless111 lemma sign_eq_dec : ∀s1,s2:signedness. (s1 = s2) ∨ (s1 ≠ s2).112 * * /2/ %2 % #H destruct113 qed.114 *)115 116 101 lemma eq_intsize_identity : ∀id. eq_intsize id id = true. 117 102 * normalize // … … 131 116 [ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2)) 132 117  2: #Hneq' normalize // ] qed. 133 134 (* Useless135 lemma type_eq_eq : ∀t1, t2. type_eq t1 t2 = true → t1 = t2.136 #t1 #t2 whd in match (type_eq ??); cases (type_eq_dec t1 t2) normalize137 [ 1: //  2: #_ #H destruct ] qed.138 *)139 118 140 119 definition size_le ≝ λsz1,sz2. … … 192 171 ]. 193 172 194 (* Used to inject boolean functions in invariants. *)195 (* Useless196 definition is_true : bool → Prop ≝ λb.197 match b with198 [ true ⇒ True199  false ⇒ False ].200 *)201 202 (* An useful lemma to cull out recursive calls: the guard forces the target type to be different from the origin type. *)203 204 (* aux lemma *)205 (* Useless206 lemma size_lt_dec_not_refl : ∀sz. ∃H. size_lt_dec sz sz = inr ??H.207 * normalize @(ex_intro … (nmk False (λauto:False.auto))) // qed.208 *)209 210 173 (* Inversion on necessary_conditions *) 211 174 lemma necessary_conditions_spec : … … 228 191 (* Compare the results [r1,r2] of the evaluation of two expressions. If [r1] is an 229 192 * integer value smaller but containing the same stuff than [r2] then all is well. 230 * If the two evaluations are erroneous, all is well too. *)193 * If the first evaluation is erroneous, we don't care about anything else. *) 231 194 definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res (val×trace). 232 195 match r1 with … … 847 810 * * // qed. 848 811 849 (* This ought to be somewhere else. Lemma used in proving the correctness of the Binop case. *)850 812 lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true. 851 813 * * normalize #H @conj // qed. … … 871 833 ] (refl ? $t) 872 834 }. 873 874 notation > "hvbox('do' «ident x, ident y» 'as' ident E ← t; break s)" 875 with precedence 48 876 for @{ match $t with 877 [ Some ${fresh res} ⇒ 878 match ${fresh res} return λx.x = ${fresh res} → ? with 879 [ mk_Sig ${ident x} ${ident y} ⇒ λ${ident E}. $s 880 ] (refl ? ${fresh res}) 881  None ⇒ None ? 882 ] }. 883 835 884 836 885 837 (* This function will make your eyes bleed. You've been warned. … … 2060 2012 cont_cast k k' → 2061 2013 cont_cast (Kcall r f en k) (Kcall r (simplify_function f) en k'). 2062 (* wtf2063  cc_seqls : ∀ls,k,k'. cont_cast k k' →2064 cont_cast (Kseq (seq_of_labeled_statement ls) k) (Kseq (seq_of_labeled_statement (simplify_ls ls)) k').2065 *)2066 2014 2067 2015 lemma call_cont_cast : ∀k,k'. … … 2378 2326 ] qed. 2379 2327 2380 lemma invoke_cthulhu:2328 lemma elim_IH_aux : 2381 2329 ∀lab. ∀s:statement.∀k,k'. cont_cast k k' → 2382 2330 ∀Hind:(∀k:cont.∀k':cont. … … 2432 2380 whd in match (find_label ? (Ssequence s1 s2) ?); 2433 2381 whd in match (find_label ? (simplify_statement (Ssequence s1 s2)) ?); 2434 elim ( invoke_cthulhulab s1 (Kseq s2 k) (Kseq (simplify_statement s2) k') ? Hind_s1)2382 elim (elim_IH_aux lab s1 (Kseq s2 k) (Kseq (simplify_statement s2) k') ? Hind_s1) 2435 2383 [ 3: try ( @cc_seq // ) 2436 2384  2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2437 2385 normalize nodelta %{kst'} /2/ 2438 2386  1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta 2439 elim ( invoke_cthulhulab s2 k k' Hcont_cast Hind_s2)2387 elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2) 2440 2388 [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast' 2441 2389 normalize nodelta %{kst'} /2/ … … 2445 2393 whd in match (find_label ???); 2446 2394 whd in match (find_label ? (simplify_statement ?) ?); 2447 elim ( invoke_cthulhulab s1 k k' Hcont_cast Hind_s1)2395 elim (elim_IH_aux lab s1 k k' Hcont_cast Hind_s1) 2448 2396 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2449 2397 normalize nodelta %{kst'} /2/ 2450 2398  1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta 2451 elim ( invoke_cthulhulab s2 k k' Hcont_cast Hind_s2)2399 elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2) 2452 2400 [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast' 2453 2401 normalize nodelta %{kst'} /2/ … … 2457 2405 whd in match (find_label ???); 2458 2406 whd in match (find_label ? (simplify_statement ?) ?); 2459 elim ( invoke_cthulhulab s (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') ? Hind_s)2407 elim (elim_IH_aux lab s (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') ? Hind_s) 2460 2408 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2461 2409 normalize nodelta %{kst'} /2/ … … 2465 2413 whd in match (find_label ???); 2466 2414 whd in match (find_label ? (simplify_statement ?) ?); 2467 elim ( invoke_cthulhulab s (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') ? Hind_s)2415 elim (elim_IH_aux lab s (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') ? Hind_s) 2468 2416 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2469 2417 normalize nodelta %{kst'} /2/ … … 2473 2421 whd in match (find_label ???); 2474 2422 whd in match (find_label ? (simplify_statement ?) ?); 2475 elim ( invoke_cthulhulab s12423 elim (elim_IH_aux lab s1 2476 2424 (Kseq (Sfor Sskip cond s2 s3) k) 2477 2425 (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) (simplify_statement s3)) k') … … 2481 2429  3: @cc_for1 // 2482 2430  1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta 2483 elim ( invoke_cthulhulab s32431 elim (elim_IH_aux lab s3 2484 2432 (Kfor2 cond s2 s3 k) 2485 2433 (Kfor2 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k') … … 2489 2437  3: @cc_for2 // 2490 2438  1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta 2491 elim ( invoke_cthulhulab s22439 elim (elim_IH_aux lab s2 2492 2440 (Kfor3 cond s2 s3 k) 2493 2441 (Kfor3 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k') … … 2503 2451 whd in match (find_label ???); 2504 2452 whd in match (find_label ? (simplify_statement ?) ?); 2505 (* We can't invoke Cthulhuon a list of labeled statements. We must proceed more manually. *)2453 (* We can't elim the Hind on a list of labeled statements. We must proceed more manually. *) 2506 2454 lapply (Hind (Kswitch k) (Kswitch k') ?) 2507 2455 [ 1: @cc_switch // … … 2514 2462 cases (ident_eq lab lab') normalize nodelta 2515 2463 [ 1: #_ %{k'} /2/ 2516  2: #_ elim ( invoke_cthulhulab s0 k k' Hcont_cast Hind)2464  2: #_ elim (elim_IH_aux lab s0 k k' Hcont_cast Hind) 2517 2465 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2518 2466 normalize nodelta %{kst'} /2/ … … 2523 2471 whd in match (find_label ???); 2524 2472 whd in match (find_label ? (simplify_statement ?) ?); 2525 elim ( invoke_cthulhulab s0 k k' Hcont_cast Hind)2473 elim (elim_IH_aux lab s0 k k' Hcont_cast Hind) 2526 2474 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2527 2475 normalize nodelta %{kst'} /2/ … … 2530 2478 whd in match (find_label ???); 2531 2479 whd in match (find_label ? (simplify_statement ?) ?); 2532 elim ( invoke_cthulhulab s0 k k' Hcont_cast Hind)2480 elim (elim_IH_aux lab s0 k k' Hcont_cast Hind) 2533 2481 [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast' 2534 2482 normalize nodelta %{kst'} /2/ … … 2540 2488 @(labeled_statements_ind … t) 2541 2489 [ 1: #default_case #Hind_ls whd in match (seq_of_labeled_statement ?); 2542 elim ( invoke_cthulhulab s02490 elim (elim_IH_aux lab s0 2543 2491 (Kseq default_case k) 2544 2492 (Kseq (simplify_statement default_case) k') ? Hind_s0) … … 2568 2516 2569 2517 whd in match (seq_of_labeled_statement ?); 2570 elim ( invoke_cthulhulab s02518 elim (elim_IH_aux lab s0 2571 2519 (Kseq (Ssequence s' (seq_of_labeled_statement tl')) k) 2572 2520 (Kseq (simplify_statement (Ssequence s' (seq_of_labeled_statement tl'))) k')
Note: See TracChangeset
for help on using the changeset viewer.