Changeset 1100 for Deliverables/D3.3/id-lookup-branch
- Timestamp:
- Aug 3, 2011, 5:18:15 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma
r1097 r1100 744 744 definition lenv ≝ identifier_map SymbolTag (identifier Label). 745 745 746 definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup ?? lbls l' = Some ? l. 746 axiom MissingLabel : String. 747 748 definition lookup_label ≝ 749 λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l). 750 751 definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l. 747 752 748 753 let rec labels_defined (s:statement) : list ident ≝ … … 766 771 definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s). 767 772 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 773 definition labels_translated : lenv → statement → stmt → Prop ≝ 774 774 λlbls,s,s'. ∀l. … … 827 827 lookup_label lbls l = OK ? l' → 828 828 lpresent lbls l'. 829 #lbls #l #l' whd in ⊢ (??%? → %) #E %{l} cases (lookup ??? l) in E ⊢ % 830 normalize #x try #y destruct /2/ 829 #lbls #l #l' #E whd %{l} @E 831 830 qed. 832 831 … … 1082 1081 ] qed. 1083 1082 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 1083 axiom DuplicateLabel : String. 1093 (*1094 (* We only record labels from Slabel, not Sgoto, so that we detect badly formed1095 programs. The gratutitous let-in expansion is so that Russell generated1096 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) with1099 [ Ssequence s1 s2 ⇒1100 do lu1 ← extend_label_env s1 lu0;1101 do lu2 ← extend_label_env s2 lu1; OK ? «eject … lu2, ?»1102 | Sifthenelse _ s1 s2 ⇒1103 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, ?»1107 | Sfor s1 _ s2 s3 ⇒1108 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, ?»1112 | Slabel l s ⇒1113 let 〈lbls, u〉 ≝ lu0 in1114 match lookup_label lbls l with1115 [ OK _ ⇒ Error ? (msg DuplicateLabel)1116 | Error _ ⇒1117 let 〈l',u〉 ≝ fresh ? u in1118 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, ?»1122 ]1123 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) with1125 [ LSdefault s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»1126 | LScase _ _ s ls ⇒1127 do lu1 ← extend_label_env s lu0;1128 do lu2 ← extend_label_env' ls lu1; OK ? «eject … lu2, ?»1129 ]. @conj1130 [ 1,3,5,17,19,21,27: #l *1131 | 2,4,6,18,20,22,28: #l #l' #H @H1132 | 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 @L11135 | #H2 cases (I2 l H2) #l' #L2 %{l'} @L21136 ]1137 1138 definition build_label_env ≝ λbody. extend_label_env body (empty_map ??) (new_universe ?).1139 *)1140 1084 1141 1085 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'. 1086 λlbls0,lbls,ls. 1087 ∀l,l'. lookup_label lbls l = OK ? l' → 1088 Exists ? (λl'. l' = l) ls ∨ lookup_label lbls0 l = OK ? l'. 1144 1089 1145 1090 lemma lookup_label_add : ∀lbls,l,l'. … … 1148 1093 qed. 1149 1094 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 1095 lemma lookup_label_miss : ∀lbls,l,l',l0. 1096 l0 ≠ l → 1097 lookup_label (add … lbls l l') l0 = lookup_label lbls l0. 1098 #lbls #l #l' #l0 * #NE 1155 1099 whd in ⊢ (??%%) 1156 1100 >lookup_add_miss 1157 [ @E2 | @(eq_identifier_elim ?? l0 l) // #E >E in E2 >E1 #X destruct ] 1101 [ @refl | @(eq_identifier_elim ?? l0 l) 1102 [ #E cases (NE E) 1103 | #_ @I 1104 ] 1105 ] 1158 1106 qed. 1159 1107 … … 1169 1117 OK ? «eject … lbls1, ?» 1170 1118 ] (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. 1119 ]. 1120 [ #l #l' #H %2 @H 1121 | cases lbls1 #lbls' #I whd in ⊢ (??%?) 1122 #l1 #l1' #E1 @(eq_identifier_elim … l l1) 1123 [ #E %1 %1 @E 1124 | #NE cases (I l1 l1' E1) 1125 [ #H %1 %2 @H 1126 | #LOOK' %2 >lookup_label_miss in LOOK' /2/ #H @H 1127 ] 1128 ] 1129 ] qed. 1188 1130 1189 1131 notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40 1190 1132 for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }. 1133 1134 definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) ≝ 1135 λbody. 1136 do «lbls, H» ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?); 1137 OK ? «lbls, ?». 1138 #l #l' #E cases (H l l' E) // 1139 whd in ⊢ (??%? → ?) #H destruct 1140 qed. 1191 1141 1192 1142 (* FIXME: the temporary handling is nonsense, I'm afraid. *) … … 1226 1176 | @(stmt_labels_mp … H2) 1227 1177 #l * #l' #LOOKUP 1228 1229 generalize in ⊢ (???(?(???(????%)))) 1230 * #S #L 1178 lapply (Ilbls l' l LOOKUP) #DEFINED 1179 cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex) 1180 #H @H 1181 ] 1182 | whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ] 1231 1183 | whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_hit % 1232 | whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ]1233 1234 1184 ] qed. 1235 1185
Note: See TracChangeset
for help on using the changeset viewer.