Changeset 985 for src/ASM/Status.ma
 Timestamp:
 Jun 16, 2011, 4:50:23 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r949 r985 1085 1085 cases not_implemented. 1086 1086 qed. 1087 1088 definition instruction_matches_identifier ≝ 1089 λy: Identifier. 1090 λx: labelled_instruction. 1091 match \fst x with 1092 [ None ⇒ false 1093  Some x ⇒ eq_bv ? x y 1094 ]. 1095 1096 let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝ 1097 match l with 1098 [ nil ⇒ true 1099  cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl]. 1100 1101 lemma does_not_occur_None: 1102 ∀id,i,list_instr. 1103 does_not_occur id (list_instr@[〈None …,i〉]) = 1104 does_not_occur id list_instr. 1105 #id #i #list_instr elim list_instr 1106 [ %  #hd #tl #IH whd in ⊢ (??%%) >IH %] 1107 qed. 1108 1109 lemma does_not_occur_Some: 1110 ∀id,id',i,list_instr. 1111 eq_bv ? id' id = false → 1112 does_not_occur id (list_instr@[〈Some ? id',i〉]) = 1113 does_not_occur id list_instr. 1114 #id #id' #i #list_instr elim list_instr 1115 [ #H normalize in H ⊢ %; >H % 1116  * #x #i' #tl #IH #H whd in ⊢ (??%%) >(IH H) %] 1117 qed. 1118 1119 lemma does_not_occur_absurd: 1120 ∀id,i,list_instr. 1121 does_not_occur id (list_instr@[〈Some ? id,i〉]) = false. 1122 #id #i #list_instr elim list_instr 1123 [ normalize change with (if (if eq_bv ??? then ? else ?) then ? else ? = ?) 1124 >eq_bv_refl % 1125  * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %] 1126 qed. 1127 1128 1129 let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝ 1130 match l with 1131 [ nil ⇒ false 1132  cons hd tl ⇒ 1133 if instruction_matches_identifier id hd then 1134 does_not_occur id tl 1135 else 1136 occurs_exactly_once id tl ]. 1137 1138 lemma occurs_exactly_once_None: 1139 ∀id,i,list_instr. 1140 occurs_exactly_once id (list_instr@[〈None …,i〉]) = 1141 occurs_exactly_once id list_instr. 1142 #id #i #list_instr elim list_instr 1143 [ %  #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %] 1144 qed. 1145 1146 lemma occurs_exactly_once_Some: 1147 ∀id,id',i,prefix. 1148 occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_bv ? id' id ∨ occurs_exactly_once id prefix. 1149 #id #id' #i #prefix elim prefix 1150 [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) 1151 change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/ 1152  *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) 1153 cases he; normalize nodelta 1154 [ #H @ (IH H) 1155  #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??) 1156 change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta; 1157 [generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; 1158 /2/ #H >does_not_occur_Some // 1159  #H @IH @H]]] 1160 qed. 1161 1162 let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝ 1163 match l with 1164 [ nil ⇒ ? 1165  cons hd tl ⇒ 1166 if pred hd then 1167 acc 1168 else 1169 index_of_internal A pred tl (S acc) 1170 ]. 1171 cases not_implemented. 1172 qed. 1173 1174 1175 definition index_of ≝ 1176 λA. 1177 λeq. 1178 λl. 1179 index_of_internal A eq l 0. 1180 1181 lemma index_of_internal_None: ∀i,id,instr_list,n. 1182 occurs_exactly_once id (instr_list@[〈None …,i〉]) → 1183 index_of_internal ? (instruction_matches_identifier id) instr_list n = 1184 index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n. 1185 #i #id #instr_list elim instr_list 1186 [ #n #abs whd in abs; cases abs 1187  #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ?  _ ⇒ ?] → ?) 1188 cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ?  _ ⇒ ?] → ??%%) 1189 [ #H % 1190  #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ % 1191 [ #_ %  #abs cases abs ]]] 1192 qed. 1193 1194 lemma index_of_internal_Some_miss: ∀i,id,id'. 1195 eq_bv ? id' id = false → 1196 ∀instr_list,n. 1197 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) → 1198 index_of_internal ? (instruction_matches_identifier id) instr_list n = 1199 index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n. 1200 #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ 1201 change with (occurs_exactly_once ?? → ?) generalize in match n; n H; elim instr_list 1202 [ #n #abs cases abs 1203  #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta; 1204 [ //  #K @IH //]] 1205 qed. 1206 1207 lemma index_of_internal_Some_hit: ∀i,id. 1208 ∀instr_list,n. 1209 occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) → 1210 index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n 1211 = instr_list + n. 1212 #i #id #instr_list elim instr_list 1213 [ #n #_ whd in ⊢ (??%%) change with (if eq_bv … id id then ? else ? = ?) >eq_bv_refl % 1214  #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta; 1215 [ >does_not_occur_absurd #abs cases abs  #H applyS (IH (S n)) //]] 1216 qed. 1217 1218 definition address_of_word_labels_code_mem ≝ 1219 λcode_mem. 1220 λid: Identifier. 1221 bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem). 1222 1223 lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list. 1224 occurs_exactly_once id (instr_list@[〈None …,i〉]) → 1225 address_of_word_labels_code_mem instr_list id = 1226 address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id. 1227 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?)) 1228 >(index_of_internal_None … H) % 1229 qed. 1230 1231 lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list. 1232 eq_bv ? id' id = false → 1233 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) → 1234 address_of_word_labels_code_mem instr_list id = 1235 address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id. 1236 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?)) 1237 >(index_of_internal_Some_miss … H) // 1238 qed. 1239 1240 lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list. 1241 occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) → 1242 address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id 1243 = bitvector_of_nat … (instr_list). 1244 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?) 1245 >(index_of_internal_Some_hit … H) // 1246 qed. 1247 1248 definition address_of_word_labels ≝ 1249 λps: PseudoStatus. 1250 λid: Identifier. 1251 address_of_word_labels_code_mem (\snd (code_memory ? ps)) id. 1252 1253 definition construct_datalabels ≝ 1254 λpreamble. 1255 \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? ( 1256 λt. λpreamble. 1257 let 〈datalabels, addr〉 ≝ t in 1258 let 〈name, size〉 ≝ preamble in 1259 let addr_16 ≝ bitvector_of_nat 16 addr in 1260 〈insert ? ? name addr_16 datalabels, addr + size〉) 1261 〈(Stub ? ?), 0〉 preamble).
Note: See TracChangeset
for help on using the changeset viewer.