Changeset 1515 for src/Cminor
 Timestamp:
 Nov 18, 2011, 1:03:14 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/toRTLabs.ma
r1464 r1515 47 47 lapply (refl ? (populate_env e u tl)) 48 48 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) * #l0 #e0 #u0 #E0 49 >E0 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u0) #i1 #u1 #E 50 whd in E:(??%?) 51 >(?:e' = add ?? e0 id i1) [ 2: destruct (E) @refl ] 49 >E0 in E; whd in ⊢ (??%? → ?) #E 50 destruct 52 51 #i #H @lookup_add_oblivious @(IH … E0) @H 53 52 ] qed. … … 69 68 lapply (refl ? (populate_label_env lbls u t)) 70 69 cases (populate_label_env lbls u t) in ⊢ (???% → %) 71 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?)72 #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ]70 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) 71 #E destruct 73 72 #l * 74 73 [ #El <El whd >lookup_add_hit % #Er destruct … … 86 85 lapply (refl ? (populate_label_env lbls u t)) 87 86 cases (populate_label_env lbls u t) in ⊢ (???% → %) 88 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?)89 #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ]87 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) 88 #E destruct 90 89 #l #H cases (identifier_eq ? l h) 91 90 [ #El %1 %1 @El 92 91  #NE cases (IH … E1 l ?) 93 [ #H' %1 %2 @H'  #H' %2 @H'  whd in H >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/]92 [ #H' %1 %2 @H'  #H' %2 @H'  whd in H >lookup_add_miss in H // ] 94 93 ] 95 94 ] qed. … … 154 153  #NE @(labels_P_mp … (pf_closed ? f l' s' ?)) 155 154 [ #lx * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ] 156  >lookup_add_miss in H / / @eq_identifier_elim // #E cases NE /2/155  >lookup_add_miss in H /2/ 157 156 ] 158 157 ] qed. … … 210 209  #NE @(labels_P_mp … (pf_closed ? f l' s' ?)) 211 210 [ #lx * [ #H %1 @lookup_add_oblivious @H  #H %2 @H ] 212  >lookup_add_miss in H / / @eq_identifier_elim // #E cases NE /2/211  >lookup_add_miss in H /2/ 213 212 ] 214 213 ] qed. … … 680 679 l in 681 680 do f ← add_stmt env label_env (f_body f) ? emptyfn [ ]; 682 do u1 ← check_universe_ok ? (pf_labgen ? f);683 do u2 ← check_universe_ok ? (pf_reggen ? f);684 681 OK ? (mk_internal_function 685 682 (pf_labgen ? f)
Note: See TracChangeset
for help on using the changeset viewer.