Changeset 1627 for src/Clight
 Timestamp:
 Dec 19, 2011, 2:48:34 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r1626 r1627 720 720 qed. 721 721 722 record tmpgen : Type[0] ≝ { 722 definition add_tmps : var_types → list (ident × type) → var_types ≝ 723 λvs,tmpenv. 724 foldr ?? (λidty,vs. add ?? vs (\fst idty) 〈Local, \snd idty〉) vs tmpenv. 725 726 record tmpgen (vars:var_types) : Type[0] ≝ { 723 727 tmp_universe : universe SymbolTag; 724 tmp_env : list (ident × type) 728 tmp_env : list (ident × type); 729 tmp_ok : fresh_map_for_univ … (add_tmps vars tmp_env) tmp_universe; 730 tmp_preserved : 731 ∀id,ty. local_id vars id ty → local_id (add_tmps vars tmp_env) id ty 725 732 }. 726 733 727 definition alloc_tmp : type → tmpgen → ident × tmpgen ≝ 728 λty,g. 729 let 〈tmp,u〉 ≝ fresh ? (tmp_universe g) in 730 〈tmp, mk_tmpgen u (〈tmp, ty〉::(tmp_env g))〉. 734 definition alloc_tmp : ∀vars. type → tmpgen vars → ident × (tmpgen vars) ≝ 735 λvars,ty,g. 736 let 〈tmp,u〉 as E ≝ fresh ? (tmp_universe ? g) in 737 〈tmp, mk_tmpgen ? u (〈tmp, ty〉::(tmp_env ? g)) ??〉. 738 [ #id #ty' 739 whd in ⊢ (? → ?%??); 740 whd in ⊢ (% → %); 741 whd in ⊢ (? → match % with [_ ⇒ ?  _ ⇒ ?]); #H 742 >lookup_add_miss 743 [ @(tmp_preserved … g) @H 744  @(fresh_distinct … E) @(tmp_ok … g) 745 lapply (tmp_preserved … g id ty' H) 746 whd in ⊢ (% → %); 747 whd in ⊢ (match % with [_ ⇒ ?  _ ⇒ ?] → ?); 748 cases (lookup ??? id) 749 [ *  #x #_ % #E destruct ] 750 ] 751  @fresh_map_add 752 [ @(fresh_map_preserved … E) @(tmp_ok … g) 753  @(fresh_is_fresh … E) 754 ] 755 ] qed. 731 756 732 757 lemma lookup_label_hit : ∀lbls,l,l'. … … 736 761 qed. 737 762 738 definition add_tmps : var_types → tmpgen → var_types ≝ 739 λvs,g. 740 foldr ?? (λidty,vs. add ?? vs (\fst idty) 〈Local, \snd idty〉) vs (tmp_env g). 741 742 definition tmps_preserved : var_types → tmpgen → tmpgen → Prop ≝ 763 (* TODO: is this really needed now? *) 764 definition tmps_preserved : ∀vars:var_types. tmpgen vars → tmpgen vars → Prop ≝ 743 765 λvars,u1,u2. 744 ∀id,ty. local_id (add_tmps vars u1) id ty → local_id (add_tmps vars u2) id ty. 745 746 lemma alloc_tmp_preserves : ∀tmp,u,u',vars,q. 747 〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'. 748 cases daemon (* XXX freshness 749 #tmp #g #g' #vars #q 750 whd in ⊢ (???% → ?); #E 751 #id #H 752 cases (identifier_eq ? id tmp) 753 destruct #E 754 whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ?  _ ⇒ ? ]; 755 [ >E >lookup_add_hit @I 756  cases E #NE >lookup_add_miss [ @H  /2/ 757 ] *) qed. 758 759 definition trans_inv : var_types → lenv → statement → tmpgen → (stmt×tmpgen) → Prop ≝ 766 ∀id,ty. local_id (add_tmps vars (tmp_env … u1)) id ty → local_id (add_tmps vars (tmp_env … u2)) id ty. 767 768 lemma alloc_tmp_preserves : ∀vars,tmp,u,u',q. 769 〈tmp,u'〉 = alloc_tmp ? q u → tmps_preserved vars u u'. 770 #vars #tmp * #u1 #e1 #F1 #P1 * #u2 #e2 #F2 #P2 #q 771 whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?); 772 cases (fresh SymbolTag u1) in ⊢ (??%? → ???(match % with [ _ ⇒ ? ]?) → ?); 773 #tmp' #u' #E1 #E2 whd in E2:(???%); destruct 774 #id #ty #H whd in ⊢ (?%??); whd in H ⊢ %; 775 whd in ⊢ match % with [ _ ⇒ ?  _ ⇒ ? ]; 776 >lookup_add_miss // @(fresh_distinct … E1) @F1 777 whd in H:(match % with [_ ⇒ ?_ ⇒ ?]) ⊢ %; 778 cases (lookup ??? id) in H ⊢ %; 779 [ *  #x #_ % #E destruct ] 780 qed. 781 782 definition trans_inv : ∀vars:var_types. lenv → statement → tmpgen vars → (stmt×(tmpgen vars)) → Prop ≝ 760 783 λvars,lbls,s,u,su'. 761 784 let 〈s',u'〉 ≝ su' in 762 stmt_inv (add_tmps vars u') lbls s' ∧785 stmt_inv (add_tmps vars (tmp_env … u')) lbls s' ∧ 763 786 labels_translated lbls s s' ∧ 764 787 tmps_preserved vars u u'. 765 788 766 789 lemma trans_inv_stmt_inv : ∀vars,lbls,s,u,su. 767 trans_inv vars lbls s u su → stmt_inv (add_tmps vars ( \snd su)) lbls (\fst su).790 trans_inv vars lbls s u su → stmt_inv (add_tmps vars (tmp_env … (\snd su))) lbls (\fst su). 768 791 #var #lbls #s #u * #s' #u' * * #H1 #H2 #H3 @H1 769 792 qed. … … 774 797 qed. 775 798 776 (* XXX Not true without fresh id' XXX799 (* TODO: still needed? *) 777 800 lemma local_id_add_local_oblivious : ∀vars,id,ty,id',ty'. 801 fresh_for_map ?? id' vars → 778 802 local_id vars id ty → local_id (add ?? vars id' 〈Local, ty'〉) id ty. 779 #vars #id #ty #id' #ty' # H whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ])803 #vars #id #ty #id' #ty' #F #H whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 780 804 cases (identifier_eq ? id id') 781 [ #E >E >lookup_add_hit @I 782  #NE >lookup_add_miss [ @H  /2/ 805 [ #E @False_ind >E in H; whd in ⊢ (% → ?); 806 whd in ⊢ (match % with [_⇒ ?_⇒ ?] → ?); cases id' in F ⊢ %; #id' 807 #F whd in F; >F * 808  #NE >lookup_add_miss [ @H  // ] 809 ] qed. 810 811 (* 812 lemma local_id_add_tmps_oblivious : ∀vars,id,ty,u. 813 local_id vars id ty → local_id (add_tmps vars (tmp_env vars u)) id ty. 814 #vars #id #ty * #u #l #F #H elim l 815 [ // 816  * #id' #ty' #tl @local_id_add_local_oblivious @F 783 817 ] qed. 784 818 *) 785 819 786 (* XXX freshness XXX *)787 axiom local_id_add_tmps_oblivious : ∀vars,id,ty,u.788 local_id vars id ty → local_id (add_tmps vars u) id ty.789 (*790 #vars #id * #u #l #H elim l791 [ //792  * #id' #ty #tl @local_id_add_local_oblivious793 ] qed.794 *)795 796 820 lemma add_tmps_oblivious : ∀vars,lbls,s,u. 797 stmt_inv vars lbls s → stmt_inv (add_tmps vars u) lbls s.821 stmt_inv vars lbls s → stmt_inv (add_tmps vars (tmp_env vars u)) lbls s. 798 822 #vars #lbls #s #u #H 799 823 @(stmt_P_mp … H) 800 824 #s' * #H1 #H2 % 801 825 [ @(stmt_vars_mp … H1) 802 #id #t @ local_id_add_tmps_oblivious826 #id #t @(tmp_preserved ? u) 803 827  @H2 804 828 ] qed. 805 829 806 lemma local_id_fresh_tmp : ∀tmp,u,ty,u0,vars. 807 〈tmp,u〉 = alloc_tmp ty u0 → local_id (add_tmps vars u) tmp (typ_of_type ty). 808 #tmp #u #ty #u0 #vars 809 whd in ⊢ (???% → ?); #E 830 lemma local_id_fresh_tmp : ∀vars,tmp,u,ty,u0. 831 〈tmp,u〉 = alloc_tmp vars ty u0 → local_id (add_tmps vars (tmp_env … u)) tmp (typ_of_type ty). 832 #vars #tmp #u #ty #u0 833 whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?); 834 cases (fresh SymbolTag (tmp_universe vars u0)) in ⊢ (??%? → ???(match % with [_⇒?]?) → ?); 835 * #tmp' #u' #e #E whd in E:(???%); 810 836 destruct 811 837 whd in ⊢ (?%??); whd whd in ⊢ match % with [ _ ⇒ ?  _ ⇒ ? ]; >lookup_add_hit … … 813 839 qed. 814 840 815 let rec translate_statement (vars:var_types) (lbls:lenv) (u:tmpgen ) (s:statement) on s : res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) ≝816 match s return λs.res (Σsu:stmt× tmpgen.trans_inv vars lbls s u su) with841 let rec translate_statement (vars:var_types) (lbls:lenv) (u:tmpgen vars) (s:statement) on s : res (Σsu:stmt×(tmpgen vars).trans_inv vars lbls s u su) ≝ 842 match s return λs.res (Σsu:stmt×(tmpgen vars).trans_inv vars lbls s u su) with 817 843 [ Sskip ⇒ OK ? «〈St_skip, u〉, ?» 818 844  Sassign e1 e2 ⇒ … … 830 856 [ IdDest id ty p ⇒ OK ? «〈St_call (Some ? 〈id,typ_of_type ty〉) ef' args', u〉, ?» 831 857  MemDest r q e1' ⇒ 832 let 〈tmp, u〉 as Etmp ≝ alloc_tmp (typeof e1) u in858 let 〈tmp, u〉 as Etmp ≝ alloc_tmp ? (typeof e1) u in 833 859 OK ? «〈St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r q e1' (Id ? tmp)), u〉, ?» 834 860 ] … … 909 935 try (#id #ty #H @H) 910 936 [ @add_tmps_oblivious @(pi2 ?? s') 911  @ local_id_add_tmps_oblivious@p937  @(tmp_preserved … u) @p 912 938 ] 913 try (@sub_pi2 #x @expr_vars_mp #i #ty @ local_id_add_tmps_oblivious)914 [ 1,3,6: @sub_pi2 #x @All_mp * #ty #e @expr_vars_mp #i #ty' @ local_id_add_tmps_oblivious939 try (@sub_pi2 #x @expr_vars_mp #i #ty @(tmp_preserved … u)) 940 [ 1,3,6: @sub_pi2 #x @All_mp * #ty #e @expr_vars_mp #i #ty' @(tmp_preserved … u) 915 941  2,4: @(local_id_fresh_tmp … Etmp) 916 942  @(alloc_tmp_preserves … Etmp) … … 960 986 961 987 (* ls and s0 aren't real parameters, they're just there for giving the invariant. *) 962 definition alloc_params : ∀vars:var_types.∀ls,s0,u. list (ident×type) → (Σsu:stmt× tmpgen. trans_inv vars ls s0 u su) → res (Σsu:stmt×tmpgen.trans_inv vars ls s0 u su) ≝988 definition alloc_params : ∀vars:var_types.∀ls,s0,u. list (ident×type) → (Σsu:stmt×(tmpgen vars). trans_inv vars ls s0 u su) → res (Σsu:stmt×(tmpgen vars).trans_inv vars ls s0 u su) ≝ 963 989 λvars,ls,s0,u,params,s. foldl ?? (λsu,it. 964 990 let 〈id,ty〉 ≝ it in … … 966 992 do 〈t,ty'〉 as E ← lookup' vars id; 967 993 match t return λx.? → ? with 968 [ Local ⇒ λE. OK (Σs:stmt× tmpgen.?) «〈s,u〉,Is»994 [ Local ⇒ λE. OK (Σs:stmt×(tmpgen vars).?) «〈s,u〉,Is» 969 995  Stack n ⇒ λE. 970 996 do q ← match access_mode ty with … … 978 1004 try @conj try @conj try @conj try @conj try @conj try @conj 979 1005 try @I 980 [ @(expr_vars_mp … ( λid,ty. local_id_add_tmps_oblivious vars id tyu)) whd >E @refl1006 [ @(expr_vars_mp … (tmp_preserved … u)) whd >E @refl 981 1007  @(π1 (π1 Is)) 982 1008  @(π2 (π1 Is)) … … 1047 1073 1048 1074 lemma local_id_split : ∀vars,tmpgen,i,t. 1049 local_id (add_tmps vars tmpgen) i t →1050 local_id vars i t ∨ Exists ? (λx. \fst x = i ∧ typ_of_type (\snd x) = t) (tmp_env tmpgen).1075 local_id (add_tmps vars (tmp_env vars tmpgen)) i t → 1076 local_id vars i t ∨ Exists ? (λx. \fst x = i ∧ typ_of_type (\snd x) = t) (tmp_env … tmpgen). 1051 1077 #vars #tmpgen #i #t 1052 1078 whd in ⊢ (?%?? → ?); 1053 elim (tmp_env tmpgen)1079 elim (tmp_env vars tmpgen) 1054 1080 [ #H %1 @H 1055 1081  * #id #ty #tl #IH … … 1077 1103 do «lbls, Ilbls» ← build_label_env (fn_body f); 1078 1104 let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in 1079 let tmp ≝ mk_tmpgen tmpuniverse [ ]in1105 let tmp ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in 1080 1106 do s ← translate_statement vartypes lbls tmp (fn_body f); 1081 1107 do «s,tmp, Is» ← alloc_params vartypes lbls ?? (fn_params f) s; … … 1083 1109 (opttyp_of_type (fn_return f)) 1084 1110 (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f)) 1085 ((map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env tmp @ fn_vars f)))1111 ((map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? tmp @ fn_vars f))) 1086 1112 stacksize 1087 1113 s ?). 1088 cases Is * #S #L #TP 1089 @(stmt_P_mp ???? S) 1090 #s1 * #H1 #H2 % 1091 [ @(stmt_vars_mp … H1) 1092 #i #t #H 1093 cases (local_id_split … H) 1094 [ #H' >map_append 1095 @Exists_map [ 2: @Exists_squeeze @(characterise_vars_all … (sym_eq ??? E) i t) @H' 1096  skip 1097  * #id #ty * #E1 #E2 <E1 <E2 @refl 1098 ] 1099  #EX @Exists_append_r <map_append @Exists_append_l @Exists_map [2: @EX  skip  * #id #ty * #E1 #E2 <E1 <E2 % @refl ] 1100 ] 1101  @(stmt_labels_mp … H2) 1102 #l * #l' #LOOKUP 1103 lapply (Ilbls l' l LOOKUP) #DEFINED 1104 cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP; #Ex destruct (Ex) 1105 #H @H 1114 [ // 1115  (* FIXME *) cases daemon 1116  cases Is * #S #L #TP 1117 @(stmt_P_mp ???? S) 1118 #s1 * #H1 #H2 % 1119 [ @(stmt_vars_mp … H1) 1120 #i #t #H 1121 cases (local_id_split … H) 1122 [ #H' >map_append 1123 @Exists_map [ 2: @Exists_squeeze @(characterise_vars_all … (sym_eq ??? E) i t) @H' 1124  skip 1125  * #id #ty * #E1 #E2 <E1 <E2 @refl 1126 ] 1127  #EX @Exists_append_r <map_append @Exists_append_l @Exists_map [2: @EX  skip  * #id #ty * #E1 #E2 <E1 <E2 % @refl ] 1128 ] 1129  @(stmt_labels_mp … H2) 1130 #l * #l' #LOOKUP 1131 lapply (Ilbls l' l LOOKUP) #DEFINED 1132 cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP; #Ex destruct (Ex) 1133 #H @H 1134 ] 1106 1135 ] qed. 1107 1136
Note: See TracChangeset
for help on using the changeset viewer.