Changeset 1515 for src/ASM/Erase.ma


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (8 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/Erase.ma

    r1463 r1515  
    11include "ASM/ASM.ma".
    2 include "ASM/BitVectorTrie.ma".
    3      
     2
    43let rec pre_erase
    54  (the_program: list labelled_instruction) (labels: list Identifier)
    6     on the_program: ((BitVectorTrie Identifier 16) × (list labelled_instruction)) ≝
     5    on the_program: ((identifier_map ASMTag Identifier) × (list labelled_instruction)) ≝
    76  match the_program with
    87  [ nil        ⇒
    98    match labels with
    10     [ nil ⇒ 〈Stub Identifier 16, [ ]〉 (* XXX: labels should be empty *)
     9    [ nil ⇒ 〈empty_map ??, [ ]〉 (* XXX: labels should be empty *)
    1110    | _   ⇒ ⊥
    1211    ]
     
    2524        | _ ⇒
    2625          let 〈maps, the_program〉 ≝ pre_erase tl [ ] in
    27           let maps ≝ foldr … (λl. λmap. insert … l label map) maps (label::labels) in
     26          let maps ≝ foldr ?? (λl. λmap. add … map l label) maps (label::labels) in
    2827            〈maps, the_program〉
    2928        ]
     
    3332qed.
    3433
    35 definition relabel_instruction: preinstruction Identifier → BitVectorTrie Identifier 16 → preinstruction Identifier ≝
     34definition relabel_instruction: preinstruction Identifier → identifier_map ASMTag Identifier → preinstruction Identifier ≝
    3635  λpre.
    3736  λmap.
    3837  match pre with
    3938  [ JC ident ⇒
    40     let located ≝ lookup … ident map ident in
     39    let located ≝ lookup_def … map ident ident in
    4140      JC … located
    4241  | JNC ident ⇒
    43     let located ≝ lookup … ident map ident in
     42    let located ≝ lookup_def … map ident ident in
    4443      JNC … located
    4544  | JB bit ident ⇒
    46     let located ≝ lookup … ident map ident in
     45    let located ≝ lookup_def … map ident ident in
    4746      JB … bit located
    4847  | JNB bit ident ⇒
    49     let located ≝ lookup … ident map ident in
     48    let located ≝ lookup_def … map ident ident in
    5049      JNB … bit located
    5150  | JBC bit ident ⇒
    52     let located ≝ lookup … ident map ident in
     51    let located ≝ lookup_def … map ident ident in
    5352      JBC … bit located
    5453  | JZ ident ⇒
    55     let located ≝ lookup … ident map ident in
     54    let located ≝ lookup_def … map ident ident in
    5655      JZ … located
    5756  | JNZ ident ⇒
    58     let located ≝ lookup … ident map ident in
     57    let located ≝ lookup_def … map ident ident in
    5958      JNZ … located
    6059  | CJNE src ident ⇒
    61     let located ≝ lookup … ident map ident in
     60    let located ≝ lookup_def … map ident ident in
    6261      CJNE … src located
    6362  | DJNZ src ident ⇒
    64     let located ≝ lookup … ident map ident in
     63    let located ≝ lookup_def … map ident ident in
    6564      DJNZ … src located
    6665  (* XXX: no identifiers in rest of instructions *)
     
    6867  ].
    6968
    70 definition relabel_pseudo_instruction: pseudo_instruction → BitVectorTrie Identifier 16 → pseudo_instruction ≝
     69definition relabel_pseudo_instruction: pseudo_instruction → identifier_map ASMTag Identifier → pseudo_instruction ≝
    7170  λpseudo.
    7271  λmap.
     
    7675  | Comment comment ⇒ Comment comment
    7776  | Jmp ident ⇒
    78     let located ≝ lookup … ident map ident in
     77    let located ≝ lookup_def … map ident ident in
    7978      Jmp located
    8079  | Call ident ⇒
    81     let located ≝ lookup … ident map ident in
     80    let located ≝ lookup_def … map ident ident in
    8281      Call located
    8382  | Mov dptr ident ⇒
    84     let located ≝ lookup … ident map ident in
     83    let located ≝ lookup_def … map ident ident in
    8584      Mov dptr located
    8685  ].
    8786     
    8887let rec relabel
    89   (the_program: list labelled_instruction) (map: BitVectorTrie Identifier 16)
     88  (the_program: list labelled_instruction) (map: identifier_map ASMTag Identifier)
    9089    on the_program: list labelled_instruction ≝
    9190  match the_program with
     
    9796      match label with
    9897      [ None ⇒ None …
    99       | Some label ⇒ Some … (lookup … ident map ident)
     98      | Some label ⇒ Some … (lookup_def … map ident ident)
    10099      ]
    101100    in
Note: See TracChangeset for help on using the changeset viewer.