Changeset 1516 for src/Clight/toCminor.ma

Timestamp:

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

Author:

sacerdot

Message:

Ported to syntax of Matita 0.99.1.

File:

• src/Clight/toCminor.ma (modified) (14 diffs)

src/Clight/toCminor.ma

@@ -122 +122 @@
   local_id (add ?? vars id (Global r)) id' → local_id vars id'.
 #var #id #r #id'
-whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?)
+whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?);
 cases (identifier_eq ? id id')
-[ #E >E >lookup_add_hit whd in ⊢ (% → ?) *
+[ #E >E >lookup_add_hit whd in ⊢ (% → ?); *
 | #NE >lookup_add_miss /2/
 ] qed.
@@ -131 +131 @@
   id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.
 #vars #id #t #id' #NE
-whd in ⊢ (% → %)
-whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ])
+whd in ⊢ (% → %);
+whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]);
 >lookup_add_miss
 [ #H @H | /2/ ]
@@ -142 +142 @@
       Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).
 #globals #f
-whd in ⊢ (∀_.∀_.??%? → ?)
+whd in ⊢ (∀_.∀_.??%? → ?);
 elim (fn_params f @ fn_vars f)
-[ #vars #n whd in ⊢ (??%? → ?) #E destruct #i #H @False_ind
-  elim globals in H
+[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H @False_ind
+  elim globals in H;
   [ normalize //
-  | * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H)
+  | * #id #rg #t #IH whd in ⊢ (?%? → ?); #H @IH @(local_id_add_global ???? H)
   ]
-| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i
+| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i
   cases (identifier_eq ? id i)
   [ #E' <E' #H % @refl
   | #NE #H whd %2 >(contract_pair var_types nat ?) in E;
-    whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
-    cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
+    whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
+    cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
     @(IH m0 n0)
-    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ
+    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ
     | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE
     ]
@@ -348 +348 @@
   expr_vars ? e P.
 #P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
-whd in ⊢ (??%? → ?)
+whd in ⊢ (??%? → ?);
 [ cases (classify_add ty1 ty2)
-  [ 3,4: #z ] whd in ⊢ (??%? → ?)
-  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
+  [ 3,4: #z ] whd in ⊢ (??%? → ?);
+  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
     * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
     whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
-  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
+  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
     * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
     whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
@@ -360 +360 @@
   ]
 | cases (classify_sub ty1 ty2)
-  [ 3,4: #z] whd in ⊢ (??%? → ?)
-  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
+  [ 3,4: #z] whd in ⊢ (??%? → ?);
+  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
     * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
     whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
@@ -737 +737 @@
   〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'.
 #tmp #g #g' #vars #q
-whd in ⊢ (???% → ?) #E
+whd in ⊢ (???% → ?); #E
 #id #H
 cases (identifier_eq ? id tmp)
 destruct #E
-whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]
+whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ];
 [ >E >lookup_add_hit @I
 | cases E #NE >lookup_add_miss [ @H | /2/
@@ -765 +765 @@
 lemma local_id_add_local_oblivious : ∀vars,id,id'.
   local_id vars id → local_id (add ?? vars id' Local) id.
-#vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
+#vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
 cases (identifier_eq ? id id')
 [ #E >E >lookup_add_hit @I
@@ -791 +791 @@
   〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.
 #tmp #u #q #u0 #vars
-whd in ⊢ (???% → ?) #E
+whd in ⊢ (???% → ?); #E
 destruct
-whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] >lookup_add_hit
+whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
 @I
 qed.
@@ -987 +987 @@
 lemma lookup_label_add : ∀lbls,l,l'.
   lookup_label (add … lbls l l') l = OK ? l'.
-#lbls #l #l' whd in ⊢ (??%?) >lookup_add_hit @refl
+#lbls #l #l' whd in ⊢ (??%?); >lookup_add_hit @refl
 qed.
 
@@ -994 +994 @@
   lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
 #lbls #l #l' #l0 #NE
-whd in ⊢ (??%%)
+whd in ⊢ (??%%);
 >lookup_add_miss
 [ @refl | @NE ]
@@ -1012 +1012 @@
 ].
 [ #l #l' #H %2 @H
-| cases lbls1 #lbls' #I whd in ⊢ (??%?)
+| cases lbls1 #lbls' #I whd in ⊢ (??%?);
   #l1 #l1' #E1 @(eq_identifier_elim … l l1)
   [ #E %1 %1 @E
   | #NE cases (I l1 l1' E1)
     [ #H %1 %2 @H
-    | #LOOK' %2 >lookup_label_miss in LOOK' /2/ #H @H
+    | #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H
     ]
   ]
@@ -1027 +1027 @@
   OK ? «lbls, ?».
 #l #l' #E cases (H l l' E) //
-whd in ⊢ (??%? → ?) #H destruct
+whd in ⊢ (??%? → ?); #H destruct
 qed.
 
@@ -1034 +1034 @@
   local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen).
 #vars #tmpgen #i
-whd in ⊢ (?%? → ?)
+whd in ⊢ (?%? → ?);
 elim (tmp_env tmpgen)
 [ #H %1 @H
@@ -1086 +1086 @@
   #l * #l' #LOOKUP
   lapply (Ilbls l' l LOOKUP) #DEFINED
-  cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex)
+  cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP; #Ex destruct (Ex)
   #H @H
 ] qed.