Changeset 985 for src/ASM/Status.ma


Ignore:
Timestamp:
Jun 16, 2011, 4:50:23 PM (9 years ago)
Author:
sacerdot
Message:

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r949 r985  
    10851085    cases not_implemented.
    10861086qed.
     1087
     1088definition 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
     1096let 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
     1101lemma 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 %]
     1107qed.
     1108
     1109lemma 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) %]
     1117qed.
     1118
     1119lemma 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 ?) %]
     1126qed.
     1127
     1128
     1129let 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
     1138lemma 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 %]
     1144qed.
     1145
     1146lemma 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]]]
     1160qed.
     1161
     1162let 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.
     1172qed.
     1173
     1174
     1175definition index_of ≝
     1176  λA.
     1177  λeq.
     1178  λl.
     1179    index_of_internal A eq l 0.
     1180
     1181lemma 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 ]]]
     1192qed.
     1193
     1194lemma 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 //]]
     1205qed.
     1206
     1207lemma 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)) //]]
     1216qed.
     1217
     1218definition 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
     1223lemma 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) %
     1229qed.
     1230
     1231lemma 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) //
     1238qed.
     1239
     1240lemma 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) //
     1246qed.
     1247
     1248definition address_of_word_labels ≝
     1249  λps: PseudoStatus.
     1250  λid: Identifier.
     1251    address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
     1252
     1253definition 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.