Changeset 1516 for src/Clight/toCminor.ma
- Timestamp:
- Nov 19, 2011, 12:38:20 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/toCminor.ma
r1515 r1516 122 122 local_id (add ?? vars id (Global r)) id' → local_id vars id'. 123 123 #var #id #r #id' 124 whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?)124 whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?); 125 125 cases (identifier_eq ? id id') 126 [ #E >E >lookup_add_hit whd in ⊢ (% → ?) *126 [ #E >E >lookup_add_hit whd in ⊢ (% → ?); * 127 127 | #NE >lookup_add_miss /2/ 128 128 ] qed. … … 131 131 id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'. 132 132 #vars #id #t #id' #NE 133 whd in ⊢ (% → %) 134 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]) 133 whd in ⊢ (% → %); 134 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]); 135 135 >lookup_add_miss 136 136 [ #H @H | /2/ ] … … 142 142 Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f). 143 143 #globals #f 144 whd in ⊢ (∀_.∀_.??%? → ?) 144 whd in ⊢ (∀_.∀_.??%? → ?); 145 145 elim (fn_params f @ fn_vars f) 146 [ #vars #n whd in ⊢ (??%? → ?) #E destruct #i #H @False_ind147 elim globals in H 146 [ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H @False_ind 147 elim globals in H; 148 148 [ normalize // 149 | * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H)149 | * #id #rg #t #IH whd in ⊢ (?%? → ?); #H @IH @(local_id_add_global ???? H) 150 150 ] 151 | * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i151 | * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i 152 152 cases (identifier_eq ? id i) 153 153 [ #E' <E' #H % @refl 154 154 | #NE #H whd %2 >(contract_pair var_types nat ?) in E; 155 whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?) 156 cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?) 155 whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); 156 cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); 157 157 #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2 158 158 @(IH m0 n0) 159 [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ159 [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ 160 160 | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE 161 161 ] … … 348 348 expr_vars ? e P. 349 349 #P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2 350 whd in ⊢ (??%? → ?) 350 whd in ⊢ (??%? → ?); 351 351 [ cases (classify_add ty1 ty2) 352 [ 3,4: #z ] whd in ⊢ (??%? → ?) 353 [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?) 352 [ 3,4: #z ] whd in ⊢ (??%? → ?); 353 [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?); 354 354 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 355 355 whd in c:(??%?); destruct % [ @H1 | % // @H2 ] 356 | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?) 356 | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?); 357 357 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 358 358 whd in c:(??%?); destruct % [ @H2 | % // @H1 ] … … 360 360 ] 361 361 | cases (classify_sub ty1 ty2) 362 [ 3,4: #z] whd in ⊢ (??%? → ?) 363 [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?) 362 [ 3,4: #z] whd in ⊢ (??%? → ?); 363 [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?); 364 364 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 365 365 whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I … … 737 737 〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'. 738 738 #tmp #g #g' #vars #q 739 whd in ⊢ (???% → ?) #E739 whd in ⊢ (???% → ?); #E 740 740 #id #H 741 741 cases (identifier_eq ? id tmp) 742 742 destruct #E 743 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]743 whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; 744 744 [ >E >lookup_add_hit @I 745 745 | cases E #NE >lookup_add_miss [ @H | /2/ … … 765 765 lemma local_id_add_local_oblivious : ∀vars,id,id'. 766 766 local_id vars id → local_id (add ?? vars id' Local) id. 767 #vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) 767 #vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); 768 768 cases (identifier_eq ? id id') 769 769 [ #E >E >lookup_add_hit @I … … 791 791 〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp. 792 792 #tmp #u #q #u0 #vars 793 whd in ⊢ (???% → ?) #E793 whd in ⊢ (???% → ?); #E 794 794 destruct 795 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]>lookup_add_hit795 whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit 796 796 @I 797 797 qed. … … 987 987 lemma lookup_label_add : ∀lbls,l,l'. 988 988 lookup_label (add … lbls l l') l = OK ? l'. 989 #lbls #l #l' whd in ⊢ (??%?) >lookup_add_hit @refl989 #lbls #l #l' whd in ⊢ (??%?); >lookup_add_hit @refl 990 990 qed. 991 991 … … 994 994 lookup_label (add … lbls l l') l0 = lookup_label lbls l0. 995 995 #lbls #l #l' #l0 #NE 996 whd in ⊢ (??%%) 996 whd in ⊢ (??%%); 997 997 >lookup_add_miss 998 998 [ @refl | @NE ] … … 1012 1012 ]. 1013 1013 [ #l #l' #H %2 @H 1014 | cases lbls1 #lbls' #I whd in ⊢ (??%?) 1014 | cases lbls1 #lbls' #I whd in ⊢ (??%?); 1015 1015 #l1 #l1' #E1 @(eq_identifier_elim … l l1) 1016 1016 [ #E %1 %1 @E 1017 1017 | #NE cases (I l1 l1' E1) 1018 1018 [ #H %1 %2 @H 1019 | #LOOK' %2 >lookup_label_miss in LOOK' /2/ #H @H1019 | #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H 1020 1020 ] 1021 1021 ] … … 1027 1027 OK ? «lbls, ?». 1028 1028 #l #l' #E cases (H l l' E) // 1029 whd in ⊢ (??%? → ?) #H destruct1029 whd in ⊢ (??%? → ?); #H destruct 1030 1030 qed. 1031 1031 … … 1034 1034 local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen). 1035 1035 #vars #tmpgen #i 1036 whd in ⊢ (?%? → ?) 1036 whd in ⊢ (?%? → ?); 1037 1037 elim (tmp_env tmpgen) 1038 1038 [ #H %1 @H … … 1086 1086 #l * #l' #LOOKUP 1087 1087 lapply (Ilbls l' l LOOKUP) #DEFINED 1088 cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex)1088 cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP; #Ex destruct (Ex) 1089 1089 #H @H 1090 1090 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.