Changeset 1631 for src/Cminor/toRTLabs.ma
 Timestamp:
 Dec 19, 2011, 2:48:37 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/toRTLabs.ma
r1626 r1631 13 13 let 〈r,gen'〉 ≝ fresh … gen in 14 14 〈〈r,ty〉::rs, add ?? en id 〈r,ty〉, gen'〉) 〈[ ], en, gen〉. 15 (* 15 16 definition Env_has : env → ident → typ → Prop ≝ 17 λe,i,t. match lookup ?? e i with [ Some x ⇒ \snd x = t  None ⇒ False ]. 18 19 lemma Env_has_present : ∀e,i,t. Env_has e i t → present … e i. 20 #e #i #t whd in ⊢ (% → %); cases (lookup ?? e i) 21 [ *  * #r #t' #E % #E' destruct ] 22 qed. 23 16 24 lemma populates_env : ∀l,e,u,l',e',u'. 25 distinct_env ?? l → 17 26 populate_env e u l = 〈l',e',u'〉 → 18 ∀i . Exists ? (λx.\fst x = i) l →19 present ?? e' i.27 ∀i,t. Exists ? (λx.x = 〈i,t〉) l → 28 Env_has e' i t. 20 29 #l elim l 21 [ #e #u #l' #e' #u' # E whd in E:(??%?); #idestruct (E) *22  * #id #t #tl #IH #e #u #l' #e' #u' #E #iwhd in E:(??%?) ⊢ (% → ?);23 * [ whd in ⊢ (??%? → ?); #E1 <E130 [ #e #u #l' #e' #u' #D #E whd in E:(??%?); #i #t destruct (E) * 31  * #id #ty #tl #IH #e #u #l' #e' #u' #D #E #i #t whd in E:(??%?) ⊢ (% → ?); 32 * [ #E1 destruct (E1) 24 33 generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ?; * * #x #y #z 25 whd in ⊢ (??%? → ?); elim (fresh RegisterTag z) #r #gen' #E 26 whd in E:(??%?); destruct; 27 whd >lookup_add_hit % #A destruct 34 whd in ⊢ (??%? → ?); 35 lapply (refl ? (fresh ? z)) elim (fresh ? z) in ⊢ (??%? → %); 36 #r #gen' #E1 #E2 37 whd in E2:(??%?); destruct; 38 whd >lookup_add_hit % 28 39  #H change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ? ])?); 29 40 lapply (refl ? (populate_env e u tl)) 30 41 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *) 31 * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?); cases (fresh RegisterTag u1) #r #u'' 42 * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?); 43 lapply (refl ? (fresh ? u1)) cases (fresh ? u1) in ⊢ (??%? → %); #r #u'' #E2 32 44 whd in ⊢ (??%? → ?); #E destruct 33 @lookup_add_oblivious 34 @(IH … E1 ? H) 45 whd >lookup_add_miss 46 [ @(IH … E1 ?? H) @(proj2 … D) 47  cases (Exists_All … H (proj1 … D)) #x * #E3 destruct #NE /2/ 48 ] 35 49 ] 36 50 ] qed. 37 51 52 lemma populates_env_distinct : ∀r,l,e,u,l',e',u'. 53 distinct_env ?? (l@r) → 54 populate_env e u l = 〈l',e',u'〉 → 55 All ? (λit. fresh_for_map … (\fst it) e) r → 56 All ? (λit. fresh_for_map … (\fst it) e') r. 57 #r #l elim l 58 [ #e #u #l' #e' #u' #D #E whd in E:(??%?); destruct (E) // 59  * #id #ty #tl #IH #e #u #l' #e' #u' #D #E whd in E:(??%?) ⊢ (% → ?); 60 change with (populate_env ???) in E:(??(match % with [ _ ⇒ ?])?); 61 lapply (refl ? (populate_env e u tl)) cases (populate_env e u tl) in (*E*) ⊢ (???% → ?); 62 * #x #y #z #E2 >E2 in E; 63 whd in ⊢ (??%? → ?); 64 elim (fresh ? z) 65 #rg #gen' #E 66 whd in E:(??%?); destruct 67 #F lapply (IH … E2 F) 68 [ @(proj2 … D) 69  lapply (All_append_r … (proj1 … D)) 70 elim r 71 [ // 72  * #i #t #tl' #IH * #D1 #D2 * #H1 #H2 % 73 [ @fresh_for_map_add /2/ 74  @IH // 75 ] 76 ] 77 ] 78 ] qed. 79 38 80 lemma populate_extends : ∀l,e,u,l',e',u'. 81 All ? (λit. fresh_for_map ?? (\fst it) e) l → 39 82 populate_env e u l = 〈l',e',u'〉 → 40 ∀i . present ?? e i → present ?? e' i.83 ∀i,t. Env_has e i t → Env_has e' i t. 41 84 #l elim l 42 [ #e #u #l' #e' #u' # E whd in E:(??%?); destruct //43  * #id #t #tl #IH #e #u #l' #e' #u' # E whd in E:(??%?);85 [ #e #u #l' #e' #u' #F #E whd in E:(??%?); destruct // 86  * #id #t #tl #IH #e #u #l' #e' #u' #F #E whd in E:(??%?); 44 87 change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?); 45 88 lapply (refl ? (populate_env e u tl)) 46 89 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0 47 >E0 in E; whd in ⊢ (??%? → ?); #E90 >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E 48 91 destruct 49 #i #H @lookup_add_oblivious @(IH … E0) @H 50 ] qed. 51 *) 92 #i #t #H whd >lookup_add_miss 93 [ @(IH … E0) [ @(proj2 … F)  @H ] 94  @(present_not_fresh ?? e) [ whd in H ⊢ %; % #E >E in H; *  @(proj1 … F) ] 95 ] qed. 96 97 definition lookup_reg : ∀e:env. ∀id,ty. Env_has e id ty → register ≝ λe,id,ty,H. \fst (lookup_present ?? e id ?). 98 /2/ qed. 99 100 lemma populate_env_list : ∀l,e,u,l',e',u'. 101 populate_env e u l = 〈l',e',u'〉 → 102 ∀i,r,t. ∀H:Env_has e' i t. lookup_reg e' i t H = r → 103 (∃H:Env_has e i t. lookup_reg e i t H = r) ∨ env_has l' r t. 104 #l elim l 105 [ #e #u #l' #e' #u' #E whd in E:(??%?); destruct #i #r #t #H #L %1 %{H} @L 106  * #id #ty #tl #IH #e #u #l' #e' #u' #E 107 whd in E:(??%?); 108 change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?); 109 lapply (refl ? (populate_env e u tl)) 110 cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0 111 >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E 112 destruct 113 #i #r #t cases (identifier_eq ? i id) 114 [ #E1 >E1 #H whd in ⊢ (??%? → %); whd in match (lookup_present ?????); 115 generalize in ⊢ (??(??? (?%))? → ?); 116 whd in H ⊢ (% → ?); >lookup_add_hit in H ⊢ %; normalize #E2 #NE #E3 destruct 117 %2 %1 % 118  #NE #H #L cases (IH … E0 i r t ??) 119 [ /2/ 120  #X %2 %2 @X 121  whd in H ⊢ %; >lookup_add_miss in H; // 122  whd in L:(??%?); whd in match (lookup_present ?????) in L; 123 lapply L L 124 generalize in ⊢ (??(???(?%))? → ?); whd in ⊢ (% → ?); 125 generalize in ⊢ (? → ? → ??(????%)?); 126 >lookup_add_miss // #H0 #p 127 change with (lookup_present SymbolTag (register×typ) e0 i ?) in ⊢ (??(???%)? → ?); 128 whd in ⊢ (? → ??%?); generalize in ⊢ (? → ??(???(?????%))?); 129 #p' #X @X 130 ] 131 ] 132 ] qed. 133 52 134 definition populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝ 53 135 λen,gen. foldr ?? … … 67 149 cases (populate_label_env lbls u t) in ⊢ (???% → %); 68 150 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?); 151 cases (fresh LabelTag u1) #lf #uf whd in ⊢ (??%? → ?); 69 152 #E destruct 70 153 #l * … … 84 167 cases (populate_label_env lbls u t) in ⊢ (???% → %); 85 168 #lbls1 #u1 #E1 whd in ⊢ (??%? → ?); 169 cases (fresh ? u1) #fi #fu whd in ⊢ (??%? → ?); 86 170 #E destruct 87 171 #l #H cases (identifier_eq ? l h) … … 92 176 ] qed. 93 177 94 definition Env_has : env → ident → typ → Prop ≝95 λe,i,t. match lookup ?? e i with [ Some x ⇒ \snd x = t  None ⇒ False ].96 97 lemma Env_has_present : ∀e,i,t. Env_has e i t → present … e i.98 #e #i #t whd in ⊢ (% → %); cases (lookup ?? e i)99 [ *  * #r #t' #E % #E' destruct ]100 qed.101 102 definition lookup_reg : ∀e:env. ∀id,ty. Env_has e id ty → register ≝ λe,id,ty,H. \fst (lookup_present ?? e id ?).103 /2/ qed.104 178 definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??. 105 179 … … 754 828 ] qed. 755 829 830 notation > "hvbox('let' ❬ident x,ident y❭ 'as' ident E ≝ t 'in' s)" 831 with precedence 10 832 for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒ 833 λ${ident E}.$s ] (refl ? $t) }. 756 834 757 835 definition c2ra_function (*: internal_function → internal_function*) ≝ … … 762 840 let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in 763 841 let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in 764 let ❬locals_reggen, result❭ ≝842 let ❬locals_reggen, result❭ as E3 ≝ 765 843 match f_return f return λ_.𝚺lr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt)) with 766 844 [ None ⇒ ❬〈locals0, reggen2〉, None ?❭ … … 807 885 [ @(stmt_vars_mp … V) 808 886 #i #t #H cases (Exists_append … H) 809 cases daemon (* XXX needs populates_env 810 [ #H1 @(populate_extends ?????? (sym_eq … E2)) 811 @(populates_env … (sym_eq … E1)) @H1 812  #H1 @(populates_env … (sym_eq … E2)) @H1 813 ]*) 887 [ #H1 @(populate_extends … (sym_eq … E2)) 888 [ @(populates_env_distinct … (sym_eq … E1)) // 889 @All_alt // 890  @(populates_env … (sym_eq … E1)) [ @distinct_env_append_l //  @H1 ] 891 ] 892  #H1 @(populates_env … (sym_eq … E2)) /2/ @H1 893 ] 814 894  @(stmt_labels_mp … L) 815 895 #l #H @(populates_label_env … (sym_eq … El)) @H … … 826 906 ] 827 907 ] 828  cases daemon (* XXX need information about env *) 908  #id #ty #r #H #L cases (populate_env_list … (sym_eq … E2) … H L) 909 [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1) 910 [ * *  normalize @Exists_append_r ] 911  cases (f_return f) in E3; 912 [ whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct 913 @Exists_append_l 914  #rt cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct 915 #H' @Exists_append_l %2 @H' 916 ] 917 ] 829 918  #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP) 830 919 [ * #E1 #E2 >E2 @I
Note: See TracChangeset
for help on using the changeset viewer.