Changeset 2391 for src/Clight/switchRemoval.ma

Timestamp:

Oct 9, 2012, 3:10:07 PM (8 years ago)

Author:

campbell

Message:

Revert "Put the post-loop cost label into the Clight while statement ..."
Rely on the Cminor to RTLabs stage ignoring Cminor skips instead.
This reverts commit 2353.

File:

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

src/Clight/switchRemoval.ma

@@ -78 +78 @@
 | Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2
 | Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2
-| Swhile e body _ ⇒ switch_free body
+| Swhile e body ⇒ switch_free body
 | Sdowhile e body ⇒ switch_free body
 | Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
@@ -249 +249 @@
   do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
   ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉
-| Swhile e body cl ⇒
+| Swhile e body ⇒
   do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
-  ret 〈Swhile e body' cl, acc, fvs', u'〉
+  ret 〈Swhile e body', acc, fvs', u'〉
 | Sdowhile e body ⇒
   do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
@@ -318 +318 @@
   let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
   〈fvs @ fvs', u''〉
-| Swhile e body cl ⇒
+| Swhile e body ⇒
   mk_fresh_variables body u
 | Sdowhile e body ⇒
@@ -367 +367 @@
   (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
   (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
-  (Swh:∀e,s,cl. P s → P (Swhile e s cl))
+  (Swh:∀e,s. P s → P (Swhile e s))
   (Sdo:∀e,s. P s → P (Sdowhile e s))
   (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
@@ -390 +390 @@
     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
-| Swhile e s cl ⇒ Swh e s cl
+| Swhile e s ⇒ Swh e s
     (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
 | Sdowhile e s ⇒ Sdo e s
@@ -416 +416 @@
   (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
   (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
-  (Swh:∀e,s,cl. P s → P (Swhile e s cl))
+  (Swh:∀e,s. P s → P (Swhile e s))
   (Sdo:∀e,s. P s → P (Sdowhile e s))
   (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
@@ -472 +472 @@
          (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
          (ret_u statement s2')))} % try //
-| 6: #e #s #cl #H #u0 #u1 #post normalize
+| 6: #e #s #H #u0 #u1 #post normalize
      elim (H u0 u1 post) #s1' * normalize
      cases (mk_fresh_variables s u0) #fvs #u'
      #Heq1 #Heq1_fvs >Heq1 normalize nodelta
-     %{(mk_swret statement (Swhile e (ret_st statement s1') cl) (ret_acc statement s1')
+     %{(mk_swret statement (Swhile e (ret_st statement s1')) (ret_acc statement s1')
         (ret_fvs statement s1') (ret_u statement s1'))} % try //
 | 7: #e #s #H #u0 #u1 #post normalize
@@ -628 +628 @@
 | Sifthenelse e s1 s2 ⇒
   max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2))
-| Swhile e body _ ⇒
+| Swhile e body ⇒
   max_id (max_of_expr e) (max_of_statement body)
 | Sdowhile e body ⇒
@@ -712 +712 @@
 | Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2
 | Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2
-| Swhile e sub _ ⇒ Q e ∧ P sub
+| Swhile e sub ⇒ Q e ∧ P sub
 | Sdowhile e sub ⇒ Q e ∧ P sub
 | Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
@@ -2194 +2194 @@
     switch_removal s fvs u = Some ? result →
     switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
-| swc_while : ∀fvs,e,s,optlab,k,k',u,result.
-    fresh_for_statement (Swhile e s optlab) u →
+| swc_while : ∀fvs,e,s,k,k',u,result.
+    fresh_for_statement (Swhile e s) u →
     switch_cont_sim fvs k k' →
     switch_removal s fvs u = Some ? result →
-    switch_cont_sim fvs (Kwhile e s optlab k) (Kwhile e (ret_st ? result) optlab k')
+    switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) k')
 | swc_dowhile : ∀fvs,e,s,k,k',u,result.
     fresh_for_statement (Sdowhile e s) u →
@@ -2801 +2801 @@
 qed. *)
 
-lemma while_fresh_lift : ∀e,s,cl,u.
-   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s cl) u.
-#e #s #cl * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ???));
+lemma while_fresh_lift : ∀e,s,u.
+   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u.
+#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??));
 cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
 cases (leb e s) try /2/