Changeset 1516 for src/Clight/CexecSound.ma

Timestamp:

Nov 19, 2011, 12:38:20 AM (8 years ago)

Author:

sacerdot

Message:

Ported to syntax of Matita 0.99.1.

File:

• src/Clight/CexecSound.ma (modified) (19 diffs)

src/Clight/CexecSound.ma

@@ -6 +6 @@
 cases v; [ | #sz #i | #f | #r1 | #r' #b #pc #of ]
 cases ty; [ 2,11,20,29,38: #sz' #sg | 3,12,21,30,39: #sz' | 4,13,22,31,40: #rg #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
-whd in ⊢ (??%? → ?)
+whd in ⊢ (??%? → ?);
 [ 2: @intsize_eq_elim_elim
   [ #NE #H destruct
@@ -15 +15 @@
   ]
 | 8: #H cases (eq_dec f Fzero)
-  [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
-  | #ne >Feq_zero_false in H // #E destruct @bool_of_val_true @is_true_float @ne
+  [ #e >e in H ⊢ %; >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
+  | #ne >Feq_zero_false in H; // #E destruct @bool_of_val_true @is_true_float @ne
   ]
 | 14: #H destruct @bool_of_val_false @is_false_pointer
@@ -35 +35 @@
 lemma try_cast_null_sound: ∀m,sz,i,ty,ty',v'. try_cast_null m sz i ty ty' = OK ? v' → cast m (Vint sz i) ty ty' v'.
 #m #sz #i #ty #ty' #v'
-whd in ⊢ (??%? → ?)
+whd in ⊢ (??%? → ?);
 @eq_bv_elim
 [ #e >e
@@ -55 +55 @@
   | 7,8,9: #a #b #H whd in H:(??%?); destruct;
   | #sz1 #si1 cases ty';
-    [ whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
+    [ whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
       [ #NE #H destruct
       | *; whd #H whd in H:(??%?); destruct;
       ]
-    | 3: #a whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
+    | 3: #a whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
       [ #E #H whd in H:(??%?); destruct
       | *; whd #H whd in H:(??%?); destruct; @cast_if
       ]
-    | 2,7,8,9: #a #b whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
+    | 2,7,8,9: #a #b whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
       [ 1,3,5,7: #NE #H destruct
       | *: *; whd #H whd in H:(??%?); destruct; //
@@ -70 +70 @@
                  | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
                  | #args #rty letin t ≝ (Tfunction args rty) ]
-        whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
+        whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
         [ 1,3,5: #NE #H destruct
         | *: *; whd
@@ -100 +100 @@
     cases ty' in H2; normalize; try #a try #b try #c try #d destruct;
     @cast_pp_z //;
-| #r #b #pc #of whd in ⊢ (??%? → ?) #e
+| #r #b #pc #of whd in ⊢ (??%? → ?); #e
     elim (bind_inversion ????? e) #s * #es #e'
     elim (bind_inversion ????? e') #u * #eu #e'' -e';
@@ -113 +113 @@
         | #Hty'
             cut (s = r). elim (eq_region_dec r s) in eu; //; normalize; #_ #e destruct.
-            #e >e in Hty #Hty
-            cases (pointer_compat_dec b s') in e'''
+            #e >e in Hty; #Hty
+            cases (pointer_compat_dec b s') in e''';
             #Hcompat #e''' whd in e''':(??%?); destruct (e'''); /2/
         ]
@@ -190 +190 @@
 (P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
 #ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
-[ #sz #ty #c whd in ⊢ (???%) cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%)
+[ #sz #ty #c whd in ⊢ (???%); cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%);
   @eq_intsize_elim #E try @I <E whd % 
 | #ty #c whd //
@@ -197 +197 @@
     @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
     @opt_bind_OK #vl #evl whd in evl:(??%?); @(eval_Elvalue … evl)
-    >H in He' #He' @He'
+    >H in He'; #He' @He'
 | #v #ty
     whd in ⊢ (???%);
     lapply (refl ? (lookup SymbolTag block en v))
-    cases (lookup SymbolTag block en v) in ⊢ (???% → %)
+    cases (lookup SymbolTag block en v) in ⊢ (???% → %);
     [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind
         whd; @(eval_Evar_global … eget efind)
     | #loc #eget @(eval_Evar_local … eget)
     ]
-| #ty #e #He whd in ⊢ (???%)
+| #ty #e #He whd in ⊢ (???%);
     @bind2_OK #v cases v // #r #l #pc #ofs #tr #Hv whd
-    >Hv in He #He
+    >Hv in He; #He
     @eval_Ederef [ 3: @He | *: skip ]
 | #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H
   cases ty // * #pty
-  cases loc in H ⊢ % * #loc' #H
+  cases loc in H ⊢ %; * #loc' #H
   whd try @I
-  @eval_Eaddrof whd in H:(??%?) >H in He'' #He'' @He''
+  @eval_Eaddrof whd in H:(??%?); >H in He''; #He'' @He''
 | #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
     @opt_bind_OK #v #ev
     @(eval_Eunop … ev)
-    >Hv1 in He1 #He1 @He1
+    >Hv1 in He1; #He1 @He1
 | #ty #op #e1 #e2 #He1 #He2
-    @bind2_OK #v1 #tr1 #ev1 >ev1 in He1 #He1
-    @bind2_OK #v2 #tr2 #ev2 >ev2 in He2 #He2
+    @bind2_OK #v1 #tr1 #ev1 >ev1 in He1; #He1
+    @bind2_OK #v2 #tr2 #ev2 >ev2 in He2; #He2
     @opt_bind_OK #v #ev whd in He1 He2; whd;
     @(eval_Ebinop … He1 He2 ev)
 | #ty #ty' #e' #He'
-    @bind2_OK #v #tr #Hv >Hv in He' #He'
+    @bind2_OK #v #tr #Hv >Hv in He'; #He'
     @bind_OK #v' #ev'
     @(eval_Ecast … He' ?)
@@ -231 +231 @@
     @(exec_cast_sound … ev')
 | #ty #e1 #e2 #e3 #He1 #He2 #He3
-    @bind2_OK #vb #tr1 #Hvb >Hvb in He1 #He1
+    @bind2_OK #vb #tr1 #Hvb >Hvb in He1; #He1
     @bind_OK #b
     cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
-    @bind2_OK #v #tr #Hv whd in Hv:(??%?)
-    [ >Hv in He2 #He2 whd in He2 Hv:(??%?) ⊢%;
+    @bind2_OK #v #tr #Hv whd in Hv:(??%?);
+    [ >Hv in He2; #He2 whd in He2 Hv:(??%?) ⊢%;
         @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb)
-    | >Hv in He3 #He3 whd in He3 Hv:(??%?) ⊢%;
+    | >Hv in He3; #He3 whd in He3 Hv:(??%?) ⊢%;
         @(eval_Econdition_false … He1 ? He3) @(bool_of ??? Hb)
     ]
 | #ty #e1 #e2 #He1 #He2
-    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
+    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
     @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
-    [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
+    [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
         @bind_OK #b2 #eb2
         @(eval_Eandbool_2 … He1 … He2)
@@ -250 +250 @@
     ]
 | #ty #e1 #e2 #He1 #He2
-    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
+    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
     @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
     [ @(eval_Eorbool_1 … He1) @(bool_of … Hb1)
-    | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
+    | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
         @bind_OK #b2 #eb2
         @(eval_Eorbool_2 … He1 … He2)
@@ -261 +261 @@
 | #ty #e' #ty' #i cases ty'; //;
     [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
-        @bind_OK #delta #Hdelta whd in H:(??%?) >H in He' #He'
+        @bind_OK #delta #Hdelta whd in H:(??%?); >H in He'; #He'
         @(eval_Efield_struct …  He' (refl ??) Hdelta)
-    | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?)
-        >H in He' #He'
+    | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?);
+        >H in He'; #He'
         @(eval_Efield_union … He' (refl ??))
     ]
-| #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He' #He'
+| #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He'; #He'
     @(eval_Ecost … He')
 (* exec_lvalue fails on non-lvalues. *)
@@ -280 +280 @@
 #ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H;
 [ 1,2,5: #a #b #c #H @False_ind destruct (H);
-| #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1 #H1 @False_ind
+| #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1; #H1 @False_ind
     @(eval_lvalue_inv_ind … H1)
     [ #a #b #c #d #bad destruct (bad);
@@ -304 +304 @@
 exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 →
 exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr r (mk_block r loc) (same_compat ??) off, tr〉.
-#ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?)
->H whd in ⊢ (??%?) cases r @refl
+#ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?);
+>H whd in ⊢ (??%?); cases r @refl
 qed.
 
@@ -312 +312 @@
 #ge #en #m #e lapply (refl ? (exec_lvalue ge en m e));
 cases (exec_lvalue ge en m e) in ⊢ (???% → %);
-[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ % #locr #loci #H
+[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #locr #loci #H
     @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ @same_compat ]
     lapply (addrof_exec_lvalue … H) #H'
@@ -350 +350 @@
 | * #id #ty #t #IH #en #m #en' #m'
   lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC
-  whd in EXEC:(??%?) ALLOC:(???%)
+  whd in EXEC:(??%?) ALLOC:(???%);
  @(alloc_variables_cons … ALLOC)
  @IH @EXEC
@@ -365 +365 @@
       @opt_bind_OK #m' #STORE
       lapply (refl ? (exec_bind_parameters en m' ps' vs))
-      cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %) [2: #msg #_ %]
+      cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %); [2: #msg #_ %]
       #m'' #BIND
       @(bind_parameters_cons … GET STORE)
-      lapply (IH vs en m') whd in ⊢ (% → ?) >BIND //
+      lapply (IH vs en m') whd in ⊢ (% → ?); >BIND //
     ]
 ] qed.
@@ -378 +378 @@
 | #v #vs #IH *
   [ //
-  | #ty #tys whd in ⊢ (???%)
+  | #ty #tys whd in ⊢ (???%);
     cases ty [ #sz #sg | #sz | #r ] cases v //
-    [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?)
+    [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?);
       @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct 
     | #v ] @bind_OK #evs #CHECKevs
@@ -498 +498 @@
   ]
 | #f0 #vargs #k #m whd in ⊢ (?????%); cases f0;
-  [ #fn whd in ⊢ (?????%)
+  [ #fn whd in ⊢ (?????%);
     lapply (refl ? (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)))
-    cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %)
-    #en' #m' #ALLOC whd in ⊢ (?????%)
+    cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %);
+    #en' #m' #ALLOC whd in ⊢ (?????%);
     @res_bindIO_OK #m2 #BIND
     whd; @(step_internal_function … (exec_alloc_variables_sound … ALLOC))