Changeset 2011


Ignore:
Timestamp:
May 31, 2012, 4:41:33 PM (5 years ago)
Author:
garnier
Message:

Minor cleanup.

Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r2009 r2011  
    2323
    2424   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?
    2626*)
    2727
     
    9999
    100100
    101 (* /!\ This lemma uses the "uniqueness of identity proofs" K axiom. I've tried doing a proper
    102  * induction on t but it turns out to be a non-well-founded pandora box. /!\ *)
    103 (* Finally useless
    104 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 (* Useless
    111 lemma sign_eq_dec : ∀s1,s2:signedness. (s1 = s2) ∨ (s1 ≠ s2).
    112 * * /2/ %2 % #H destruct
    113 qed.
    114 *)
    115 
    116101lemma eq_intsize_identity : ∀id. eq_intsize id id = true.
    117102* normalize //
     
    131116[ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2))
    132117| 2: #Hneq' normalize // ] qed.
    133 
    134 (* Useless
    135 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) normalize
    137 [ 1: // | 2: #_ #H destruct ] qed.
    138 *)
    139118
    140119definition size_le ≝ λsz1,sz2.
     
    192171].
    193172
    194 (* Used to inject boolean functions in invariants. *)
    195 (* Useless
    196 definition is_true : bool → Prop ≝ λb.
    197 match b with
    198 [ true ⇒ True
    199 | 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 (* Useless
    206 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 
    210173(* Inversion on necessary_conditions *)
    211174lemma necessary_conditions_spec :
     
    228191(* Compare the results [r1,r2] of the evaluation of two expressions. If [r1] is an
    229192 * 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. *)
    231194definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res (val×trace).
    232195match r1 with
     
    847810* * // qed.
    848811
    849 (* This ought to be somewhere else. Lemma used in proving the correctness of the Binop case. *)
    850812lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true.
    851813* * normalize #H @conj // qed.
     
    871833       ] (refl ? $t)
    872834      }.
    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                 
    884836                       
    885837(* This function will make your eyes bleed. You've been warned.
     
    20602012    cont_cast k k' →
    20612013    cont_cast (Kcall r f en k) (Kcall r (simplify_function f) en k').
    2062 (* wtf
    2063 | 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 *)
    20662014
    20672015lemma call_cont_cast : ∀k,k'.
     
    23782326] qed.
    23792327
    2380 lemma invoke_cthulhu :
     2328lemma elim_IH_aux :
    23812329  ∀lab. ∀s:statement.∀k,k'. cont_cast k k' →
    23822330  ∀Hind:(∀k:cont.∀k':cont.
     
    24322380     whd in match (find_label ? (Ssequence s1 s2) ?);
    24332381     whd in match (find_label ? (simplify_statement (Ssequence s1 s2)) ?);
    2434      elim (invoke_cthulhu lab 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)
    24352383     [ 3: try ( @cc_seq // )
    24362384     | 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    24372385          normalize nodelta %{kst'} /2/
    24382386     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
    2439           elim (invoke_cthulhu lab s2 k k' Hcont_cast Hind_s2)
     2387          elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2)
    24402388          [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast'
    24412389               normalize nodelta %{kst'} /2/
     
    24452393     whd in match (find_label ???);
    24462394     whd in match (find_label ? (simplify_statement ?) ?);
    2447      elim (invoke_cthulhu lab s1 k k' Hcont_cast Hind_s1)
     2395     elim (elim_IH_aux lab s1 k k' Hcont_cast Hind_s1)
    24482396     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    24492397          normalize nodelta %{kst'} /2/
    24502398     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
    2451           elim (invoke_cthulhu lab s2 k k' Hcont_cast Hind_s2)
     2399          elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2)
    24522400          [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast'
    24532401               normalize nodelta %{kst'} /2/
     
    24572405     whd in match (find_label ???);
    24582406     whd in match (find_label ? (simplify_statement ?) ?);
    2459      elim (invoke_cthulhu lab 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)
    24602408     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    24612409          normalize nodelta %{kst'} /2/
     
    24652413     whd in match (find_label ???);
    24662414     whd in match (find_label ? (simplify_statement ?) ?);
    2467      elim (invoke_cthulhu lab 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)
    24682416     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    24692417          normalize nodelta %{kst'} /2/
     
    24732421     whd in match (find_label ???);
    24742422     whd in match (find_label ? (simplify_statement ?) ?);
    2475      elim (invoke_cthulhu lab s1
     2423     elim (elim_IH_aux lab s1
    24762424               (Kseq (Sfor Sskip cond s2 s3) k)
    24772425               (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) (simplify_statement s3)) k')
     
    24812429     | 3: @cc_for1 //
    24822430     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
    2483           elim (invoke_cthulhu lab s3
     2431          elim (elim_IH_aux lab s3
    24842432                    (Kfor2 cond s2 s3 k)
    24852433                    (Kfor2 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
     
    24892437          | 3: @cc_for2 //
    24902438          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
    2491                elim (invoke_cthulhu lab s2
     2439               elim (elim_IH_aux lab s2
    24922440                         (Kfor3 cond s2 s3 k)
    24932441                         (Kfor3 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
     
    25032451     whd in match (find_label ???);
    25042452     whd in match (find_label ? (simplify_statement ?) ?);
    2505      (* We can't invoke Cthulhu on 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. *)
    25062454     lapply (Hind (Kswitch k) (Kswitch k') ?)
    25072455     [ 1: @cc_switch //
     
    25142462     cases (ident_eq lab lab') normalize nodelta
    25152463     [ 1: #_ %{k'} /2/
    2516      | 2: #_ elim (invoke_cthulhu lab s0 k k' Hcont_cast Hind)
     2464     | 2: #_ elim (elim_IH_aux lab s0 k k' Hcont_cast Hind)
    25172465          [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    25182466                normalize nodelta %{kst'} /2/
     
    25232471     whd in match (find_label ???);
    25242472     whd in match (find_label ? (simplify_statement ?) ?);
    2525      elim (invoke_cthulhu lab s0 k k' Hcont_cast Hind)
     2473     elim (elim_IH_aux lab s0 k k' Hcont_cast Hind)
    25262474     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    25272475          normalize nodelta %{kst'} /2/
     
    25302478     whd in match (find_label ???);
    25312479     whd in match (find_label ? (simplify_statement ?) ?);
    2532      elim (invoke_cthulhu lab s0 k k' Hcont_cast Hind)
     2480     elim (elim_IH_aux lab s0 k k' Hcont_cast Hind)
    25332481     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    25342482          normalize nodelta %{kst'} /2/
     
    25402488     @(labeled_statements_ind … t)
    25412489     [ 1: #default_case #Hind_ls whd in match (seq_of_labeled_statement ?);
    2542           elim (invoke_cthulhu lab s0
     2490          elim (elim_IH_aux lab s0
    25432491                  (Kseq default_case k)
    25442492                  (Kseq (simplify_statement default_case) k') ? Hind_s0)
     
    25682516     
    25692517          whd in match (seq_of_labeled_statement ?);
    2570           elim (invoke_cthulhu lab s0
     2518          elim (elim_IH_aux lab s0
    25712519                   (Kseq (Ssequence s' (seq_of_labeled_statement tl')) k)
    25722520                   (Kseq (simplify_statement (Ssequence s' (seq_of_labeled_statement tl'))) k')
  • src/Clight/labelSimulation.ma

    r2000 r2011  
    344344| swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m)
    345345| swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r)
    346 . 
     346.
    347347
    348348(* ... and add the states where the cases from switch statements are expanded.
Note: See TracChangeset for help on using the changeset viewer.