Changeset 1516 for src/Cminor/toRTLabs.ma
 Timestamp:
 Nov 19, 2011, 12:38:20 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/toRTLabs.ma
r1515 r1516 23 23 [ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) * 24 24  * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?); 25 * [ whd in ⊢ (??%? → ?) #E1 <E126 generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z27 whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E25 * [ whd in ⊢ (??%? → ?); #E1 <E1 26 generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ?; * * #x #y #z 27 whd in ⊢ (??%? → ?); elim (fresh RegisterTag z) #r #gen' #E 28 28 whd in E:(??%?); destruct; 29 29 whd >lookup_add_hit % #A destruct 30  #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl)30  #H change in E:(??(match % with [ _ ⇒ ? ])?); with (populate_env e u tl) 31 31 lapply (refl ? (populate_env e u tl)) 32 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *)33 * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u''34 whd in ⊢ (??%? → ?) #E destruct32 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *) 33 * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?); cases (fresh RegisterTag u1) #r #u'' 34 whd in ⊢ (??%? → ?); #E destruct 35 35 @lookup_add_oblivious 36 36 @(IH … E1 ? H) … … 44 44 [ #e #u #l' #e' #u' #E whd in E:(??%?); destruct // 45 45  * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?); 46 change in E:(??(match % with [ _ ⇒ ?])?) with (populate_env e u tl)46 change in E:(??(match % with [ _ ⇒ ?])?); with (populate_env e u tl) 47 47 lapply (refl ? (populate_env e u tl)) 48 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) * #l0 #e0 #u0 #E049 >E0 in E; whd in ⊢ (??%? → ?) #E48 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0 49 >E0 in E; whd in ⊢ (??%? → ?); #E 50 50 destruct 51 51 #i #H @lookup_add_oblivious @(IH … E0) @H … … 64 64 #ls elim ls 65 65 [ #lbls #u #lbls' #u' #E #l * 66  #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?) 67 change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)66  #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?); 67 change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???) 68 68 lapply (refl ? (populate_label_env lbls u t)) 69 cases (populate_label_env lbls u t) in ⊢ (???% → %) 70 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) 69 cases (populate_label_env lbls u t) in ⊢ (???% → %); 70 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?); 71 71 #E destruct 72 72 #l * … … 81 81 #ls elim ls 82 82 [ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H 83  #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?) 84 change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)83  #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?); 84 change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???) 85 85 lapply (refl ? (populate_label_env lbls u t)) 86 cases (populate_label_env lbls u t) in ⊢ (???% → %) 87 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) 86 cases (populate_label_env lbls u t) in ⊢ (???% → %); 87 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?); 88 88 #E destruct 89 89 #l #H cases (identifier_eq ? l h) 90 90 [ #El %1 %1 @El 91 91  #NE cases (IH … E1 l ?) 92 [ #H' %1 %2 @H'  #H' %2 @H'  whd in H >lookup_add_miss in H// ]92 [ #H' %1 %2 @H'  #H' %2 @H'  whd in H; >lookup_add_miss in H; // ] 93 93 ] 94 94 ] qed. … … 149 149 #le #l #s #f #p 150 150 #l' #s' #H cases (identifier_eq … l l') 151 [ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //]151 [ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //] 152 152 @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H 153 153  #NE @(labels_P_mp … (pf_closed ? f l' s' ?)) 154 154 [ #lx * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ] 155  >lookup_add_miss in H /2/155  >lookup_add_miss in H; /2/ 156 156 ] 157 157 ] qed. … … 205 205 #le #l #s #f #p 206 206 #l' #s' #H cases (identifier_eq … l l') 207 [ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //]207 [ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //] 208 208 @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ] 209 209  #NE @(labels_P_mp … (pf_closed ? f l' s' ?)) 210 210 [ #lx * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ] 211  >lookup_add_miss in H /2/211  >lookup_add_miss in H; /2/ 212 212 ] 213 213 ] qed. … … 273 273 #le #env #es #f elim es 274 274 [ #p #rs #f normalize #E destruct @refl 275  * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E275  * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?); #E 276 276 cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 E; 277 277 cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 E2; … … 453 453 #lenv #l #l' #p 454 454 cut (∃lx. lookup ?? lenv l = Some ? lx) 455 [ whd in p; cases (lookup ?? lenv l) in p ⊢ % 455 [ whd in p; cases (lookup ?? lenv l) in p ⊢ %; 456 456 [ * #H cases (H (refl ??)) 457 457  #lx #_ %{lx} @refl 458 458 ] 459  * #lx #E whd in ⊢ (??%? → ?) cases p >E #q whd in ⊢ (??%? → ?)#E' >E' @refl459  * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl 460 460 ] qed. 461 461 … … 478 478 labels_of s = labels_of s' → Cminor_labels_added le s' f → 479 479 Cminor_labels_added le s f. 480 #le #s #s' #f #E whd in ⊢ (% → %) > E #H @H480 #le #s #s' #f #E whd in ⊢ (% → %); > E #H @H 481 481 qed. 482 482 … … 621 621 try (#l #H @H) 622 622 [ f @(choose_regs_length … (sym_eq … Eregs)) 623  whd in Env @(π1 (π1 (π1 Env)))623  whd in Env; @(π1 (π1 (π1 Env))) 624 624  f @(choose_regs_length … (sym_eq … Eregs)) 625 625  #l #H cases (Exists_append … H) … … 709 709  cases (label_env_contents … (sym_eq ??? El) l ?) 710 710 [ #H @H 711  whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)* #H cases (H (refl ??))711  whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??)) 712 712  whd >H % #E' destruct (E') 713 713 ] … … 716 716  #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP) 717 717 [ * #E1 #E2 >E2 @I 718  whd in ⊢ (??%? → ?) #E' destruct (E')718  whd in ⊢ (??%? → ?); #E' destruct (E') 719 719 ] 720 720  *: whd >lookup_add_hit % #E destruct
Note: See TracChangeset
for help on using the changeset viewer.