Changeset 2232 for src/Cminor

Timestamp:

Jul 23, 2012, 2:05:10 PM (9 years ago)

Author:

campbell

Message:

Remove unused block structure in Cminor.

Location:

src/Cminor

Files:

• initialisation.ma (modified) (1 diff)
• semantics.ma (modified) (6 diffs)
• syntax.ma (modified) (7 diffs)
• toRTLabs.ma (modified) (10 diffs)

src/Cminor/initialisation.ma

@@ -68 +68 @@
 | #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
   >(IH1 H1) >(IH2 H2) @refl
-| #s #IH * * #_ #_ #H @(IH H)
-| #s #IH * * #_ #_ #H @(IH H)
 | #l #s #IH * * #_ *
 | #l #s #IH * * #_ #_ #H @(IH H)

src/Cminor/semantics.ma

@@ -159 +159 @@
     | Some sk ⇒ Some ? sk
     ]
-| St_loop s' ⇒ λInv. find_label l s' (Kseq (St_loop s') k) f en ??
-| St_block s' ⇒ λInv. find_label l s' (Kblock k) f en ??
 | St_label l' s' ⇒ λInv.
     match identifier_eq ? l l' with
@@ -173 +171 @@
 try @(π2 (π1 Inv))
 [ % [ @(π2 Inv) | @kInv ]
-| % [ @Inv | @kInv ]
 | % [ @(π2 Inv) | @kInv ]
 ] qed. 
@@ -208 +205 @@
   | #sk #_ #E whd in E:(??%?); destruct
   ]
-| #s1 #IH #k #f #en #Inv #kInv @IH
-| #s1 #IH #k #f #en #Inv #kInv @IH
 | #E whd in i:(??%?); cases (identifier_eq Label l a) in i;
   whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ]
@@ -286 +281 @@
 axiom FailedStore : String.
 axiom BadFunctionValue : String.
-axiom BadSwitchValue : String.
-axiom UnknownLabel : String.
 axiom ReturnMismatch : String.
 
@@ -329 +322 @@
         ! b ← eval_bool_of_val v;
         return 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉
-    | St_loop s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st〉
-    | St_block s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kblock k) ? st〉
-    | St_exit n ⇒ λInv.
-        ! k' ← k_exit n k ?? kInv;
-        return 〈E0, State f St_skip en fInv ? m sp k' ? st〉
-    | St_switch sz _ e cs default ⇒ λInv.
-        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
-        match v with
-        [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
-            ! k' ← k_exit (find_case ?? i cs default) k ?? kInv;
-            return 〈tr, State f St_skip en fInv ? m sp k' ? st〉)
-            (Error ? (msg BadSwitchValue))
-        | _ ⇒ Error ? (msg BadSwitchValue)
-        ]
     | St_return eo ⇒
         match eo return λeo. stmt_inv f en (St_return eo) → ? with
@@ -411 +390 @@
 | @(π2 Inv')
 | @(π1 Inv')
-| @(pi2 … k')
-| @(pi2 … k')
-| % [ @Inv | @kInv ]
 | cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
 | % [ @(π2 Inv) | @kInv ]
 | @stmt_inv_update @fInv
-| 10,11:
+| 7,8:
   @(stmt_P_mp … (f_inv f))
   #s * #V #L %

src/Cminor/syntax.ma

@@ -46 +46 @@
 | St_seq : stmt → stmt → stmt
 | St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
-| St_loop : stmt → stmt
-| St_block : stmt → stmt
-| St_exit : nat → stmt
-(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
-| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
 | St_return : option (𝚺t. expr t) → stmt
 | St_label : identifier Label → stmt → stmt
@@ -60 +55 @@
 [ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
 | St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
-| St_loop s' ⇒ P s ∧ stmt_P P s'
-| St_block s' ⇒ P s ∧ stmt_P P s'
 | St_label _ s' ⇒ P s ∧ stmt_P P s'
 | St_cost _ s' ⇒ P s ∧ stmt_P P s'
@@ -71 +64 @@
 [ #s1 #s2 * * /2/
 | #sz #sg #e #s1 #s2 * * /2/ 
-| 3,4: #s * /2/
-| 5,6: #i #s normalize * /2/
+| *: #i #s normalize * /2/
 ] qed.
 
@@ -86 +78 @@
 *)
 | St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
-| St_switch _ _ e _ _ ⇒ expr_vars ? e P
 | St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ]
 | _ ⇒ True
@@ -103 +94 @@
 [ #s1 #s2 #H1 #H2 normalize * * /4/
 | #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
-| #s #H * /5/
-| #s #H * /5/
 | #l #s #H * /5/
 | #l #s #H * /5/
@@ -120 +109 @@
 | #s1 #s2 #H1 #H2 * /3/
 | #sz #sg #e #s1 #s2 #H1 #H2 /5/
-| 7,8: #s #H1 #H2 /2/
-| //
-| /5/
 | * normalize [ // | *; normalize /3/ ]
 | /2/
@@ -137 +123 @@
 [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
 | St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
-| St_loop s ⇒ labels_of s
-| St_block s ⇒ labels_of s
 | St_label l s ⇒ l::(labels_of s)
 | St_cost _ s ⇒ labels_of s

src/Cminor/toRTLabs.ma

@@ -610 +610 @@
 alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,12,0)".
 
-definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝
-λA,P,m,l,n.
-  match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with
-  [ None ⇒ λ_. Error ? m
-  | Some a ⇒ λH'. OK ? «a, ?»
-  ] (All_nth A P n l (pi2 … l)).
-@H' @refl qed.
-
 lemma lookup_label_rev : ∀lenv,l,l',p.
   lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
@@ -677 +669 @@
 qed.
 
-let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) (exits:Σls:list label. All ? (present ?? (pf_graph … f)) ls) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝
+let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝
 match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with
 [ St_skip ⇒ λ_. OK ? «f, ?»
@@ -719 +711 @@
 *)
 | St_seq s1 s2 ⇒ λEnv.
-    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
-    do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»;
+    do f2 ← add_stmt env label_env s2 ? f;
+    do f1 ← add_stmt env label_env s1 ? f2;
       OK ? «pi1 … f1, ?»
 | St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
     let l_next ≝ pf_entry … f in
-    do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;
+    do f2 ← add_stmt env label_env s2 (π2 Env) f;
     let l2 ≝ pf_entry … f2 in
     let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
-    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;
+    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f;
     let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in
     let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
     OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?»
-| St_loop s ⇒ λEnv.
-    let f ≝ add_fresh_to_graph … R_skip f ?? in (* dummy statement, fill in afterwards *)
-    let l_loop ≝ pf_entry … f in
-    do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
-    OK ? «pi1 … (fill_in_statement … l_loop (R_skip (pf_entry … f)) f ??), ?»
-| St_block s ⇒ λEnv.
-    do f ← add_stmt env label_env s (π2 Env) f («pf_entry … f::exits, ?»);
-    OK ? «pi1 … f, ?»
-| St_exit n ⇒ λEnv.
-    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
-    OK ? «pi1 … (add_fresh_to_graph … (λ_. R_skip l) f ??), ?»
-| St_switch sz sg e tab n ⇒ λEnv.
-    let ❬f,r❭ ≝ choose_reg … e f ? in
-    do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;
-    let f ≝ add_fresh_to_graph … (λ_. R_skip l_default) f ?? in
-    do f ← foldr ? (res (Σf':partial_fn ??. ?)) (λcs,f.
-      do f ← f;
-      let 〈i,n〉 ≝ cs in
-      let ❬f,cr❭ ≝ fresh_reg … f (ASTint sz sg) in
-      let ❬f,br❭ ≝ fresh_reg … f (ASTint I8 Unsigned) in
-      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
-      let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in
-      let f ≝ add_fresh_to_graph … (St_op2 … (Ocmp sz sg Unsigned Ceq) br r cr) f ?? in
-      let f ≝ add_fresh_to_graph … (St_const ? cr (Ointconst sz sg i)) f ?? in
-        OK ? «pi1 … f, ?») (OK ? f) tab;
-    OK ? «pi1 … (add_expr ? env ? e (π1 Env) f «r, ?»), ?»
 | St_return opt_e ⇒ let f0 ≝ f in
     let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
@@ -776 +742 @@
     ]
 | St_label l s' ⇒ λEnv.
-    do f ← add_stmt env label_env s' (π2 Env) f exits;
+    do f ← add_stmt env label_env s' (π2 Env) f;
     let l' ≝ lookup_label label_env l ? in
     OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
@@ -783 +749 @@
     OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
 | St_cost l s' ⇒ λEnv.
-    do f ← add_stmt env label_env s' (π2 Env) f exits;
+    do f ← add_stmt env label_env s' (π2 Env) f;
     OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
 ] Env.
@@ -799 +765 @@
 | @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
 | @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
-| (*4,8:*) @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
-| (*5,9:*) @sym_eq @(All2_length … (pi2 ?? args_regs))
-| (*6,10:*) @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
+| @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
+| @sym_eq @(All2_length … (pi2 ?? args_regs))
+| @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
 | @(π1 (π1 (π1 Env)))
-| 8,10,11,16,17: (*11,13,14,19,20:*) (@(All_mp … (pi2 ?? exits))) #i #H @(fn_con_graph … H) repeat @fn_contains_step @I
 | #l #H cases (Exists_append … H)
   [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1)
@@ -815 +780 @@
 | @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
 | #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
-| @(pi2 … (pf_entry …))
-| @Cminor_labels_sig @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
-| % [ @pi2 | @(pi2 ?? exits) ]
-| @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
-| #l' #H @(pi2 … l)
-| #l #H @(fn_con_graph … (pi2 ?? l_default)) repeat @fn_contains_step @I
-| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
-| #l #H % [ @(fn_con_graph … (pi2 ?? l_case)) repeat @fn_contains_step @I | @H ]
-| #l % [ % [ @(fn_con_env … (pi2 ?? r)) | @(fn_con_env … (pi2 ?? cr)) ] | @(fn_con_env … (pi2 ?? br)) ] repeat @fn_contains_step @I
-| #l @(fn_con_env … (pi2 ?? cr)) repeat @fn_contains_step @I
 | #_ (* see above *) <E @(pi2 ?? r)
 | @(pi2 … (pf_entry …))
@@ -867 +822 @@
     l
     l in
-do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
+do f ← add_stmt env label_env (f_body f) ? emptyfn;
 OK ? (mk_internal_function
     (pf_labgen … f)
@@ -881 +836 @@
     (pf_exit … f)
   ).
-[ @I
-| -emptyfn @(stmt_P_mp … (f_inv f))
+[ -emptyfn @(stmt_P_mp … (f_inv f))
   #s * #V #L %
   [ @(stmt_vars_mp … V)
@@ -925 +879 @@
   | whd in ⊢ (??%? → ?); #E' destruct (E')
   ]
-| 7,8: whd >lookup_add_hit % #E destruct
+| 6,7: whd >lookup_add_hit % #E destruct
 | % @refl
 ]