Changeset 1097 for Deliverables/D3.3/idlookupbranch
 Timestamp:
 Aug 3, 2011, 1:04:49 PM (9 years ago)
 Location:
 Deliverables/D3.3/idlookupbranch
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/Clight/toCminor.ma
r1096 r1097 746 746 definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup ?? lbls l' = Some ? l. 747 747 748 let rec labels_defined (s:statement) : list ident ≝ 749 match s with 750 [ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2 751  Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2 752  Swhile _ s ⇒ labels_defined s 753  Sdowhile _ s ⇒ labels_defined s 754  Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3 755  Sswitch _ ls ⇒ labels_defined_switch ls 756  Slabel l s ⇒ l::(labels_defined s) 757  Scost _ s ⇒ labels_defined s 758  _ ⇒ [ ] 759 ] 760 and labels_defined_switch (ls:labeled_statements) : list ident ≝ 761 match ls with 762 [ LSdefault s ⇒ labels_defined s 763  LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls 764 ]. 765 766 definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s). 767 768 axiom MissingLabel : String. 769 770 definition lookup_label ≝ 771 λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l). 772 773 definition labels_translated : lenv → statement → stmt → Prop ≝ 774 λlbls,s,s'. ∀l. 775 (Exists ? (λl'.l' = l) (labels_defined s)) → 776 ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'. 777 748 778 definition stmt_inv ≝ 749 779 λvars. λlbls:lenv. … … 794 824 ] qed. 795 825 796 axiom MissingLabel : String.797 798 definition lookup_label ≝799 λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).800 801 826 lemma lookup_label_hit : ∀lbls,l,l'. 802 827 lookup_label lbls l = OK ? l' → … … 806 831 qed. 807 832 808 let rec translate_statement (vars:var_types) (lbls:lenv) (tmp:Σi:ident.local_id vars i) (tmpp:Σi:ident.local_id vars i) (s:statement) on s : res (Σs:stmt.stmt_inv vars lbls s) ≝ 809 match s with 833 definition trans_inv : var_types → lenv → statement → stmt → Prop ≝ 834 λvars,lbls,s,s'. stmt_inv vars lbls s' ∧ labels_translated lbls s s'. 835 836 lemma trans_inv_stmt_inv : ∀vars,lbls,s,s'. 837 trans_inv vars lbls s s' → stmt_inv vars lbls s'. 838 #var #lbls #s #s' * // 839 qed. 840 841 lemma trans_inv_labels : ∀vars,lbls,s,s'. 842 trans_inv vars lbls s s' → labels_translated lbls s s'. 843 #vars #lbls #s #s' @proj2 844 qed. 845 846 lemma Exists_append : ∀A,P,l1,l2. 847 Exists A P (l1@l2) → 848 Exists A P l1 ∨ Exists A P l2. 849 #A #P #l1 elim l1 850 [ #l2 #H %2 @H 851  #h #t #IH #l2 whd in ⊢ (% → ?) * 852 [ #H %1 %1 @H 853  #H cases (IH l2 H) /4/ 854 ] 855 ] qed. 856 857 lemma Exists_append_l : ∀A,P,l1,l2. 858 Exists A P l1 → Exists A P (l1@l2). 859 #A #P #l1 #l2 elim l1 860 [ * 861  #h #t #IH * 862 [ #H %1 @H 863  #H %2 @IH @H 864 ] 865 ] qed. 866 867 lemma Exists_append_r : ∀A,P,l1,l2. 868 Exists A P l2 → Exists A P (l1@l2). 869 #A #P #l1 #l2 elim l1 870 [ #H @H 871  #h #t #IH #H %2 @IH @H 872 ] qed. 873 874 875 let rec translate_statement (vars:var_types) (lbls:lenv) (tmp:Σi:ident.local_id vars i) (tmpp:Σi:ident.local_id vars i) (s:statement) on s : res (Σs':stmt.trans_inv vars lbls s s') ≝ 876 match s return λs.res (Σs':stmt.trans_inv vars lbls s s') with 810 877 [ Sskip ⇒ OK ? «St_skip, ?» 811 878  Sassign e1 e2 ⇒ … … 897 964 OK ? «St_cost l s1', ?» 898 965 ]. 899 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj 966 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj 900 967 try @I 968 try @(trans_inv_stmt_inv ???? (sig_ok ? (λs.trans_inv ??? s) …)) 901 969 try @(sig_ok ? (λs.stmt_inv ?? s)) 902 970 try @(sig_ok ? (λe.expr_vars ? e ?)) … … 906 974 try @(sig_ok ? (local_id vars)) 907 975 try @(lookup_label_hit … E) 908 [ @(sig_ok ?? s') 976 [ 1,3,5,6,7,13,14,15,16,18: whd #l * 977  @(sig_ok ?? s') 909 978  @p 910 ] qed. 911 912 let rec labels_defined (s:statement) : list ident ≝ 913 match s with 914 [ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2 915  Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2 916  Swhile _ s ⇒ labels_defined s 917  Sdowhile _ s ⇒ labels_defined s 918  Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3 919  Sswitch _ ls ⇒ labels_defined_switch ls 920  Slabel l s ⇒ l::(labels_defined s) 921  Scost _ s ⇒ labels_defined s 922  _ ⇒ [ ] 923 ] 924 and labels_defined_switch (ls:labeled_statements) : list ident ≝ 925 match ls with 926 [ LSdefault s ⇒ labels_defined s 927  LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls 928 ]. 929 930 lemma OK_sig_eq : ∀A,P,x,xp,y,yp. OK (Σx:A.P x) «x,xp» = OK (Σx:A.P x) «y,yp» → x = y. 931 #A #P #x #xp #y #yp #E destruct @refl 932 qed. 933 934 definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s). 935 936 lemma Exists_append : ∀A,P,l1,l2. 937 Exists A P (l1@l2) → 938 Exists A P l1 ∨ Exists A P l2. 939 #A #P #l1 elim l1 940 [ #l2 #H %2 @H 941  #h #t #IH #l2 whd in ⊢ (% → ?) * 942 [ #H %1 %1 @H 943  #H cases (IH l2 H) /4/ 944 ] 945 ] qed. 946 947 lemma Exists_append_l : ∀A,P,l1,l2. 948 Exists A P l1 → Exists A P (l1@l2). 949 #A #P #l1 #l2 elim l1 950 [ * 951  #h #t #IH * 952 [ #H %1 @H 953  #H %2 @IH @H 954 ] 955 ] qed. 956 957 lemma Exists_append_r : ∀A,P,l1,l2. 958 Exists A P l2 → Exists A P (l1@l2). 959 #A #P #l1 #l2 elim l1 960 [ #H @H 961  #h #t #IH #H %2 @IH @H 962 ] qed. 963 964 lemma reflmatch : ∀A,B,e.∀P:∀v:A. e = OK ? v → res B.∀x. 965 match e return λx.e = x → ? with [ OK v ⇒ P v  Error m ⇒ λ_.Error ? m ] (refl ? e) = OK ? x → 966 ∃v,p. P v p = OK ? x. 967 #A #B * 968 [ #v #P #x normalize #H %{v} % [ @refl  @H ] 969  #m #P #x normalize #H destruct 970 ] qed. 971 972 lemma labels_translated : ∀vars,lbls,tmp,tmpp,s,l,s',p. 973 (Exists ? (λl'.l' = l) (labels_defined s)) → 974 translate_statement vars lbls tmp tmpp s = OK ? «s', p» → 975 ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'. 976 #vars #lbls #tmp #tmpp #s #l @(statement_ind … s) (* FIXME: once switch is done we'll need something else here *) 977 [ #s' #p * 978  #e1 #e2 #s' #p * 979  #eo #e #args #s' #p * 980  #s1 #s2 #IH1 #IH2 #s' #p #H #E 981 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 982 cases (bind_inversion ????? E) * #s2' #I2 * #E2 E #E 983 <(OK_sig_eq ?????? E) E; 984 cases (Exists_append ???? H) 985 [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_l @L2 ] 986  #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_r @L2 ] 987 ] 988  #e #s1 #s2 #IH1 #IH2 #s' #p #H #E 989 (* Carefully get rid of the equality that will screw up the case analysis *) 990 cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ % 991 [ #sz #sg #e' #E 992 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 993 cases (bind_inversion ????? E) * #s2' #I2 * #E2 E #E 994 <(OK_sig_eq ?????? E) E; 995 cases (Exists_append ???? H) 996 [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_l @L2 ] 997  #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_r @L2 ] 998 ] 999  *: #x #e' normalize #E destruct 1000 ] 1001  #e #s #IH #s' #p #H #E 1002 (* Carefully get rid of the equality that will screw up the case analysis *) 1003 cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ % 1004 [ #sz #sg #e' #E 1005 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 1006 <(OK_sig_eq ?????? E) E; 1007 cases (IH s1' I1 H E1) #l' * #La #Lb %{l'} % [ @La  whd; normalize in ⊢ (???%) >append_nil @Lb ] 1008  *: #x #e' normalize #E destruct 1009 ] 1010  #e #s #IH #s' #p #H #E 1011 (* Carefully get rid of the equality that will screw up the case analysis *) 1012 cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ % 1013 [ #sz #sg #e' #E 1014 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 1015 <(OK_sig_eq ?????? E) E; 1016 cases (IH s1' I1 H E1) #l' * #La #Lb %{l'} % [ @La  whd; normalize in ⊢ (???%) >append_nil @Lb ] 1017  *: #x #e' normalize #E destruct 1018 ] 1019  #s1 #e #s1 #s2 #IH1 #IH2 #IH3 #s' #p #H #E 1020 (* Carefully get rid of the equality that will screw up the case analysis *) 1021 cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ % 1022 [ #sz #sg #e' #E 1023 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 1024 cases (bind_inversion ????? E) * #s2' #I2 * #E2 E #E 1025 cases (bind_inversion ????? E) * #s3' #I3 * #E3 E #E 1026 <(OK_sig_eq ?????? E) E; 1027 cases (Exists_append ???? H) 1028 [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_l @L2 ] 1029  H #H cases (Exists_append ???? H) 1030 [ #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_r @Exists_append_l @Exists_append_r @L2 ] 1031  #H3 cases (IH3 s3' I3 H3 E3) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_r @Exists_append_l @Exists_append_l @L2 ] 1032 ] 1033 ] 1034  *: #x #e' normalize #E destruct 1035 ] 1036  #s' #p * 1037  #s' #p * 1038  #eo #s' #p * 1039  #e #ls #IH #s' #p #H #E whd in E:(??%?); destruct (* FIXME once switch is implemented ... *) 1040  #l0 #s0 #IH #s' #p #H 1041 whd in ⊢ (??%? → ?) #E cases (reflmatch ????? E) E #l1 * #El #E 1042 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 1043 <(OK_sig_eq ?????? E) E; 1044 cases H 1045 [ #El' %{l1} <El' % [ @El  %1 @refl ] 1046  #H1 cases (IH s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1  %2 @L2 ] 1047 ] 1048  #l0 #s' #p * 1049  #l0 #s0 #IH #s' #p #H #E 1050 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 1051 <(OK_sig_eq ?????? E) E; 1052 @(IH s1' I1 H E1) 1053 ] qed. 979  #l #H cases (Exists_append … H) 980 [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1 981 %{l'} % [ @E1  @Exists_append_l @D1 ] 982  #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2 983 %{l'} % [ @E2  @Exists_append_r @D2 ] 984 ] 985  #l #H cases (Exists_append … H) 986 [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1 987 %{l'} % [ @E1  @Exists_append_l @D1 ] 988  #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2 989 %{l'} % [ @E2  @Exists_append_r @D2 ] 990 ] 991  cases s1' #s1' * #S1 #L1 #l #H cases (L1 l H) #l' * #E1 #D1 992 %{l'} % [ @E1  @Exists_append_l @D1 ] 993  cases s1' #s1' * #S1 #L1 #l #H cases (L1 l H) #l' * #E1 #D1 994 %{l'} % [ @E1  @Exists_append_l @D1 ] 995  #l #H cases (Exists_append … H) 996 [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1 997 %{l'} % [ @E1  @Exists_append_l @D1 ] 998  #H cases (Exists_append … H) 999 [ #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2 1000 %{l'} % [ @E2  @Exists_append_r @Exists_append_l @Exists_append_r @D2 ] 1001  #H3 cases s3' #s3' * #S3 #L3 cases (L3 l H3) #l' * #E3 #D3 1002 %{l'} % [ @E3  @Exists_append_r @Exists_append_l @Exists_append_l @D3 ] 1003 ] 1004 ] 1005  cases s1' #s1' * #S1 #L1 #l0 * 1006 [ #El <El %{l'} >E % [ @refl  %1 @refl ] 1007  #H cases (L1 l0 H) #l0' * #E1 #D1 1008 %{l0'} % [ @E1  %2 @D1 ] 1009 ] 1010  cases s1' #s1' * #S1 #L1 @L1 1011 ] qed. 1012 1054 1013 1055 1014 axiom ParamGlobalMixup : String. 1056 1015 1057 definition alloc_params : ∀vars:var_types.∀ls. list (ident×type) → (Σs:stmt. stmt_inv vars ls s) → res (Σs:stmt.stmt_inv vars ls s) ≝ 1058 λvars,ls,params,s. foldl ?? (λs,it. 1016 (* ls and s0 aren't real parameters, they're just there for giving the invariant. *) 1017 definition alloc_params : ∀vars:var_types.∀ls,s0. list (ident×type) → (Σs:stmt. trans_inv vars ls s0 s) → res (Σs:stmt.trans_inv vars ls s0 s) ≝ 1018 λvars,ls,s0,params,s. foldl ?? (λs,it. 1059 1019 let 〈id,ty〉 ≝ it in 1060 1020 do s ← s; … … 1074 1034 try @I 1075 1035 [ whd >E @I 1076  @(sig_ok … s) 1036  @(trans_inv_stmt_inv … s0) @(sig_ok … s) 1037  cases s #s * #S #L @L 1077 1038 ] qed. 1078 1039 … … 1121 1082 ] qed. 1122 1083 1084 definition lenv_inv : lenv → lenv → statement → Prop ≝ 1085 λlbls0,lbls,s. (∀l. Exists ? (λl'. l' = l) (labels_defined s) → ∃lm. lookup_label lbls l = OK ? lm) ∧ 1086 ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'. 1087 1088 definition lenv_inv_switch : lenv → lenv → labeled_statements → Prop ≝ 1089 λlbls0,lbls,ls. (∀l. Exists ? (λl'. l' = l) (labels_defined_switch ls) → ∃lm. lookup_label lbls l = OK ? lm) ∧ 1090 ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'. 1091 1092 axiom DuplicateLabel : String. 1093 (* 1123 1094 (* We only record labels from Slabel, not Sgoto, so that we detect badly formed 1124 programs. *) 1125 let rec extend_label_env (s:statement) (lbls:lenv) (u:universe ?) : lenv × (universe ?) ≝ 1126 match s with 1127 [ Ssequence s1 s2 ⇒ 1128 let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in 1129 extend_label_env s2 lbls u 1095 programs. The gratutitous letin expansion is so that Russell generated 1096 nice hypotheses for us. *) 1097 let rec extend_label_env (s:statement) (lu0:lenv×(universe ?)) : res (Σx:lenv × (universe ?). lenv_inv (\fst lu0) (\fst x) s) ≝ 1098 match s return λs.res (Σx:lenv × (universe ?). lenv_inv (\fst lu0) (\fst x) s) with 1099 [ Ssequence s1 s2 ⇒ 1100 do lu1 ← extend_label_env s1 lu0; 1101 do lu2 ← extend_label_env s2 lu1; OK ? «eject … lu2, ?» 1130 1102  Sifthenelse _ s1 s2 ⇒ 1131 let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in1132 extend_label_env s2 lbls u1133  Swhile _ s ⇒ extend_label_env s lbls u1134  Sdowhile _ s ⇒ extend_label_env s lbls u1103 do lu1 ← extend_label_env s1 lu0; 1104 do lu2 ← extend_label_env s2 lu1; OK ? «eject … lu2, ?» 1105  Swhile _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?» 1106  Sdowhile _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?» 1135 1107  Sfor s1 _ s2 s3 ⇒ 1136 let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in1137 let 〈lbls,u〉 ≝ extend_label_env s2 lbls u in1138 extend_label_env s3 lbls u1139  Sswitch _ ls ⇒ extend_label_env' ls lbls u1108 do lu1 ← extend_label_env s1 lu0; 1109 do lu2 ← extend_label_env s2 lu1; 1110 do lu3 ← extend_label_env s3 lu2; OK ? «eject … lu3, ?» 1111  Sswitch _ ls ⇒ do lu ← extend_label_env' ls lu0; OK ? «eject … lu, ?» 1140 1112  Slabel l s ⇒ 1141 let 〈l',u〉 ≝ fresh ? u in 1142 extend_label_env s (add … lbls l l') u 1143  Scost _ s ⇒ extend_label_env s lbls u 1144  _ ⇒ 〈lbls,u〉 1113 let 〈lbls, u〉 ≝ lu0 in 1114 match lookup_label lbls l with 1115 [ OK _ ⇒ Error ? (msg DuplicateLabel) 1116  Error _ ⇒ 1117 let 〈l',u〉 ≝ fresh ? u in 1118 do lu ← extend_label_env s 〈add … lbls l l', u〉; OK ? «eject … lu, ?» 1119 ] 1120  Scost _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?» 1121  _ ⇒ OK ? «lu0, ?» 1145 1122 ] 1146 and extend_label_env' (ls:labeled_statements) (l bls:lenv) (u:universe ?) : lenv × (universe ?) ≝1147 match ls with1148 [ LSdefault s ⇒ extend_label_env s lbls u1123 and extend_label_env' (ls:labeled_statements) (lu0:lenv×(universe ?)) : res (Σx:lenv × (universe ?). lenv_inv_switch (\fst lu0) (\fst x) ls) ≝ 1124 match ls return λls.res (Σx:lenv × (universe ?). lenv_inv_switch (\fst lu0) (\fst x) ls) with 1125 [ LSdefault s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?» 1149 1126  LScase _ _ s ls ⇒ 1150 let 〈lbls,u〉 ≝ extend_label_env s lbls u in 1151 extend_label_env' ls lbls u 1152 ]. 1127 do lu1 ← extend_label_env s lu0; 1128 do lu2 ← extend_label_env' ls lu1; OK ? «eject … lu2, ?» 1129 ]. @conj 1130 [ 1,3,5,17,19,21,27: #l * 1131  2,4,6,18,20,22,28: #l #l' #H @H 1132  cases lu1 in lu2 ⊢ % * #lbls1 #u1 * #I1 #E1 * * #lbls2 #u2 * #I2 #E2 whd in E2:(∀_.∀_.??(?%?)? → ?) ⊢ (∀_.? → ??(λ_.??(?%?)?)) 1133 #l #H cases (Exists_append … H) 1134 [ #H1 cases (I1 l H1) #l' #L1 %{l'} @E2 @L1 1135  #H2 cases (I2 l H2) #l' #L2 %{l'} @L2 1136 ] 1153 1137 1154 1138 definition build_label_env ≝ λbody. extend_label_env body (empty_map ??) (new_universe ?). 1139 *) 1140 1141 definition lenv_list_inv : lenv → lenv → list ident → Prop ≝ 1142 λlbls0,lbls,ls. (∀l. Exists ? (λl'. l' = l) ls → ∃lm. lookup_label lbls l = OK ? lm) ∧ 1143 ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'. 1144 1145 lemma lookup_label_add : ∀lbls,l,l'. 1146 lookup_label (add … lbls l l') l = OK ? l'. 1147 #lbls #l #l' whd in ⊢ (??%?) >lookup_add_hit @refl 1148 qed. 1149 1150 lemma lookup_label_new : ∀lbls,l,l',msg,l0,l0'. 1151 lookup_label lbls l = Error ? msg → 1152 lookup_label lbls l0 = OK ? l0' → 1153 lookup_label (add … lbls l l') l0 = OK ? l0'. 1154 #lbls #l #l' #msg #l0 #l0' #E1 #E2 1155 whd in ⊢ (??%%) 1156 >lookup_add_miss 1157 [ @E2  @(eq_identifier_elim ?? l0 l) // #E >E in E2 >E1 #X destruct ] 1158 qed. 1159 1160 let rec populate_lenv (ls:list ident) (lbls:lenv) (u:universe ?) : res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) ≝ 1161 match ls return λls. res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) with 1162 [ nil ⇒ OK ? «lbls, ?» 1163  cons l t ⇒ 1164 match lookup_label lbls l return λx.lookup_label lbls l = x → ? with 1165 [ OK _ ⇒ λ_. Error ? (msg DuplicateLabel) 1166  Error _ ⇒ λLOOK. 1167 let 〈l',u1〉 ≝ fresh … u in 1168 do lbls1 ← populate_lenv t (add … lbls l l') u1; 1169 OK ? «eject … lbls1, ?» 1170 ] (refl ? (lookup_label lbls l)) 1171 ]. @conj 1172 [ #l * 1173  #l #l' #H @H 1174  cases lbls1 #lbls' * #E1 #E2 whd in ⊢ (∀_.?→??(λ_.??(?%?)?)) #l0 * 1175 [ #E <E %{l'} @E2 @lookup_label_add 1176  @E1 1177 ] 1178  cases lbls1 #lbls' * #E1 #E2 #l1 #l2 #L whd in ⊢ (??(?%?)?) 1179 @E2 @(lookup_label_new … LOOK L) 1180 ] qed. 1181 1182 definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l.Exists ? (λl'.l' = l) (labels_defined body) → ∃l'.lookup_label lbls l = OK ? l') ≝ 1183 λbody. 1184 do lbls ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?); 1185 OK ? «eject … lbls, ?». 1186 cases lbls #lbls * #E1 #E2 @E1 1187 qed. 1188 1189 notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40 1190 for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }. 1155 1191 1156 1192 (* FIXME: the temporary handling is nonsense, I'm afraid. *) 1157 1193 definition translate_function : list (ident×region) → function → res internal_function ≝ 1158 1194 λglobals, f. 1159 let 〈lbls, label_universe〉 ≝ build_label_env (fn_body f) in1195 do «lbls, Ilbls» ← build_label_env (fn_body f); 1160 1196 let 〈vartypes0, stacksize〉 as E ≝ characterise_vars globals f in 1161 1197 let tmp ≝ bigid1 in (* FIXME *) 1162 1198 let tmpp ≝ bigid2 in (* FIXME *) 1163 1199 let vartypes ≝ add … (add … vartypes0 tmp Local) tmpp Local in 1164 do s as E1← translate_statement vartypes lbls tmp tmpp (fn_body f);1165 do s as E2 ← alloc_params vartypes lbls(fn_params f) s;1200 do s ← translate_statement vartypes lbls tmp tmpp (fn_body f); 1201 do «s,Is» ← alloc_params vartypes lbls ? (fn_params f) s; 1166 1202 OK ? (mk_internal_function 1167 1203 (opttyp_of_type (fn_return f)) … … 1170 1206 stacksize 1171 1207 s ?). 1172 [ whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]) >lookup_add_hit % 1208 [ cases Is #S #L 1209 @(stmt_P_mp ???? S) 1210 #s1 * #H1 #H2 % 1211 [ @(stmt_vars_mp … H1) 1212 #i #H cases (identifier_eq ? tmp i) 1213 [ #E <E @Exists_mid @refl 1214  #NE1 @Exists_rm cases (identifier_eq ? tmpp i) 1215 [ #E <E @Exists_mid @refl 1216  #NE2 @Exists_rm 1217 >map_append 1218 @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i) 1219 @(local_id_add_miss ?? Local ? NE1) 1220 @(local_id_add_miss ?? Local ? NE2) @H 1221  skip 1222  * #id #ty #E1 <E1 @refl 1223 ] 1224 ] 1225 ] 1226  @(stmt_labels_mp … H2) 1227 #l * #l' #LOOKUP 1228 1229 generalize in ⊢ (???(?(???(????%)))) 1230 * #S #L 1231  whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]) >lookup_add_hit % 1173 1232  whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit % % ] 1174  @(stmt_P_mp ???? (sig_ok ?? s)) 1175 #s1 * #H1 #H2 % [ 2: @H2 ] 1176 @stmt_vars_mp [ 3: @sig_ok  skip ] 1177 #i #H cases (identifier_eq ? tmp i) 1178 [ #E <E @Exists_mid @refl 1179  #NE1 @Exists_rm cases (identifier_eq ? tmpp i) 1180 [ #E <E @Exists_mid @refl 1181  #NE2 @Exists_rm 1182 >map_append 1183 @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i) 1184 @(local_id_add_miss ?? Local ? NE1) 1185 @(local_id_add_miss ?? Local ? NE2) @H 1186  skip 1187  * #id #ty #E1 <E1 @refl 1188 ] 1189 ] 1190 ] 1233 1191 1234 ] qed. 1192 1235 
Deliverables/D3.3/idlookupbranch/Cminor/syntax.ma
r1096 r1097 129 129 ] qed. 130 130 131 lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s. 132 #P #Q #H #s elim s normalize /2/ qed. 133 131 134 (* Get labels from a Cminor statement. *) 132 135 let rec labels_of (s:stmt) : list (identifier Label) ≝
Note: See TracChangeset
for help on using the changeset viewer.