Changeset 1515 for src/ASM/Status.ma


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (9 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r1459 r1515  
    702702  λr: BitVector 3.
    703703    let address ≝ bit_address_of_register ? s r in
    704       lookup address (low_internal_ram ? s) (zero 8).
     704      lookup ?? address (low_internal_ram ? s) (zero 8).
    705705     
    706706definition set_register ≝
     
    717717  λM: Type[0].
    718718  λs: PreStatus M.
    719     let 〈 nu, nl 〉 ≝ split 4 4 (get_8051_sfr ? s SFR_SP) in
     719    let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_SP) in
    720720    let m ≝ get_index_v … nu O ? in
    721721    let r1 ≝ get_index_v … nu 1 ? in
     
    804804        λext_indirect_dptr: True.
    805805          let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    806             lookup 16 address (external_ram ? s) (zero 8)
     806            lookup ? 16 address (external_ram ? s) (zero 8)
    807807      | EXT_INDIRECT e ⇒
    808808        λext_indirect: True.
    809809          let address ≝ get_register ? s [[ false; false; e ]]  in
    810810          let padded_address ≝ pad 8 8 address in
    811             lookup 16 padded_address (external_ram ? s) (zero 8)
     811            lookup ? 16 padded_address (external_ram ? s) (zero 8)
    812812      | ACC_DPTR ⇒
    813813        λacc_dptr: True.
     
    815815          let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in
    816816          let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
    817             lookup 16 address (external_ram ? s) (zero 8)
     817            lookup ? 16 address (external_ram ? s) (zero 8)
    818818      | ACC_PC ⇒
    819819        λacc_pc: True.
    820820          let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in
    821821          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ? s) padded_acc in
    822             lookup 16 address (external_ram ? s) (zero 8)
     822            lookup ? 16 address (external_ram ? s) (zero 8)
    823823      | DIRECT d ⇒
    824824        λdirect: True.
    825           let 〈 nu, nl 〉 ≝ split 4 4 d in
     825          let 〈 nu, nl 〉 ≝ split ? 4 4 d in
    826826          let bit_one ≝ get_index_v ? ? nu 0 ? in
    827827          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
     
    836836          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ? s [[ false; false; i]]) in
    837837          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
    838           let bit_1 ≝ get_index_v bit_one_v O ? in
     838          let bit_1 ≝ get_index_v ?? bit_one_v O ? in
    839839          match  bit_1 with
    840840            [ false ⇒
     
    10021002                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    10031003                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1004                 let trans ≝ lookup 7 address' (low_internal_ram ? s) (zero 8) in
     1004                let trans ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
    10051005                  ¬(get_index_v … trans (modulus address 8) ?)
    10061006              ]
     
    10381038                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    10391039                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1040                 let t ≝ lookup 7 address' (low_internal_ram ? s) (zero 8) in
     1040                let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
    10411041                let n_bit ≝ set_index … t (modulus address 8) v ? in
    10421042                let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in
     
    10961096    match \fst x with
    10971097    [ None ⇒ false
    1098     | Some x ⇒ eq_bv ? x y
     1098    | Some x ⇒ eq_identifier ? x y
    10991099    ].
    11001100
     
    11141114lemma does_not_occur_Some:
    11151115 ∀id,id',i,list_instr.
    1116   eq_bv ? id' id = false →
     1116  eq_identifier ? id' id = false →
    11171117   does_not_occur id (list_instr@[〈Some ? id',i〉]) =
    11181118    does_not_occur id list_instr.
     
    11261126  does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
    11271127 #id #i #list_instr elim list_instr
    1128   [ normalize change with (if (if eq_bv ??? then ? else ?) then ? else ? = ?)
    1129     >eq_bv_refl %
     1128  [ normalize change with (if (if eq_identifier ??? then ? else ?) then ? else ? = ?)
     1129    >eq_identifier_refl %
    11301130  | * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %]
    11311131qed.
     
    11511151lemma occurs_exactly_once_Some:
    11521152 ∀id,id',i,prefix.
    1153   occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_bv ? id' id ∨ occurs_exactly_once id prefix.
     1153  occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once id prefix.
    11541154 #id #id' #i #prefix elim prefix
    1155   [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
    1156     change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/
     1155  [ whd in ⊢ (?% → ?)
     1156    change in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) with (eq_identifier ? id' id)
     1157    @eq_identifier_elim normalize nodelta; /2/
    11571158  | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
    11581159    cases he; normalize nodelta
    11591160     [ #H @ (IH H)
    1160      | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
    1161        change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta;
    1162        [generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
    1163         /2/ #H >does_not_occur_Some //
     1161     | #x whd in ⊢ (? → ?(??%)) change in match (instruction_matches_identifier ??) with (eq_identifier ? x id)
     1162       @eq_identifier_elim #E normalize nodelta
     1163       [ destruct @eq_identifier_elim normalize nodelta;
     1164        /2/ #H >does_not_occur_Some /2/
    11641165       | #H @IH @H]]]
    11651166qed.
     
    11681169  ∀id,id',i,prefix.
    11691170    occurs_exactly_once id (prefix@[〈Some ? id',i〉]) →
    1170     (eq_bv ? id' id ∧ does_not_occur id prefix) ∨
    1171     (¬eq_bv ? id' id ∧ occurs_exactly_once id prefix).
     1171    (eq_identifier ? id' id ∧ does_not_occur id prefix) ∨
     1172    (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix).
    11721173 #id #id' #i #prefix elim prefix
    1173  [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?)
    1174   change with (? → eq_v ?? eq_b id' id∧?∨?) cases (eq_v ?????)
     1174 [ whd in ⊢ (?% → ?) change in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?) with (eq_identifier ???)
     1175   @eq_identifier_elim #E
    11751176  [ normalize //
    11761177  | normalize #H @⊥ @H 
     
    11791180   cases he; normalize nodelta
    11801181   [ #H @ (IH H)
    1181    | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
    1182      generalize in match (refl ? (eq_bv 16 x id)) change in match (eq_v ???x id) with (eq_bv ? x id)
    1183      cases (eq_bv ???) in ⊢ (???% → %) #Heq
    1184      [ generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta
    1185        [ #H >(eq_bv_eq … (sym_eq … H)) >does_not_occur_absurd #Hf @⊥ @Hf
     1182   | #x @eq_identifier_elim #Heq
     1183     [ @eq_identifier_elim normalize nodelta
     1184       [ #H >H >does_not_occur_absurd #Hf @⊥ @Hf
    11861185       | #H >(does_not_occur_Some)
    1187          [ #H2 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
    1188            change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
    1189            @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) whd in match (instruction_matches_identifier ??)
    1190            change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta @H2 
    1191          | @(sym_eq … H)
     1186         [ #H2 whd in match (does_not_occur ??)
     1187           change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1188           >Heq >eq_identifier_refl normalize nodelta
     1189           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??)
     1190           change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1191           >eq_identifier_refl
     1192           normalize nodelta @H2 
     1193         | /2/
    11921194         ]
    11931195       ]
    1194      | normalize nodelta #H lapply (IH H) -IH -H; #Hor @orb_elim
    1195        generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %)
    1196        #Heq2
    1197        [ normalize nodelta <Heq2 in Hor; #Hor normalize in Hor;
    1198          whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
    1199          change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
    1200          cases (does_not_occur id tl) in Hor; normalize nodelta //
     1196     | normalize nodelta #H lapply (IH H) -IH -H;
     1197       @eq_identifier_elim #Heq2
     1198       #Hor @orb_elim
     1199       [ <Heq2 in Hor; #Hor normalize in Hor;
     1200         whd in match (does_not_occur ??) change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1201         >eq_identifier_false // normalize nodelta
     1202         cases (does_not_occur id' tl) in Hor; normalize nodelta //
    12011203       | normalize nodelta whd in match (occurs_exactly_once ??)
    1202          whd in match (instruction_matches_identifier ??) change in match (eq_v ???x id) with (eq_bv ? x id)
    1203          >Heq normalize nodelta <Heq2 in Hor; normalize //
     1204         change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1205         >eq_identifier_false //
    12041206       ]
    12051207     ] 
     
    12411243
    12421244lemma index_of_internal_Some_miss: ∀i,id,id'.
    1243  eq_bv ? id' id = false →
     1245 eq_identifier ? id' id = false →
    12441246 ∀instr_list,n.
    12451247 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
     
    12591261  = |instr_list| + n.
    12601262 #i #id #instr_list elim instr_list
    1261   [ #n #_ whd in ⊢ (??%%) change with (if eq_bv … id id then ? else ? = ?) >eq_bv_refl %
     1263  [ #n #_ whd in ⊢ (??%%) change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
    12621264  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
    1263     [ >does_not_occur_absurd #abs cases abs | #H applyS (IH (S n)) //]]
     1265    [ >does_not_occur_absurd #abs cases abs | #H >plus_n_Sm applyS (IH (S n)) //]]
    12641266qed.
    12651267
     
    12781280
    12791281lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
    1280  eq_bv ? id' id = false →
     1282 eq_identifier ? id' id = false →
    12811283  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
    12821284   address_of_word_labels_code_mem instr_list id =
    12831285   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
    12841286 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
    1285  >(index_of_internal_Some_miss … H) //
     1287 >(index_of_internal_Some_miss … H) [ @refl | // ]
    12861288qed.
    12871289
     
    12911293   = bitvector_of_nat … (|instr_list|).
    12921294 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)
    1293  >(index_of_internal_Some_hit … H) //
     1295 >(index_of_internal_Some_hit … H) <plus_n_O @refl
    12941296qed.
    12951297
     
    13011303definition construct_datalabels ≝
    13021304  λpreamble.
    1303     \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
     1305    \fst (foldl ((identifier_map ASMTag Word) × nat) ? (
    13041306    λt. λpreamble.
    13051307      let 〈datalabels, addr〉 ≝ t in
    13061308      let 〈name, size〉 ≝ preamble in
    13071309      let addr_16 ≝ bitvector_of_nat 16 addr in
    1308         〈insert ? ? name addr_16 datalabels, addr + size〉)
    1309           〈(Stub ? ?), 0〉 preamble).
     1310        〈add ? ? datalabels name addr_16, addr + size〉)
     1311          〈empty_map …, 0〉 preamble).
Note: See TracChangeset for help on using the changeset viewer.