include "ASM/ASM.ma".

let rec pre_erase
  (the_program: list labelled_instruction) (labels: list Identifier)
    on the_program: ((identifier_map ASMTag Identifier) × (list labelled_instruction)) ≝
  match the_program with
  [ nil        ⇒
    match labels with
    [ nil ⇒ 〈empty_map ??, [ ]〉 (* XXX: labels should be empty *)
    | _   ⇒ ⊥
    ]
  | cons hd tl ⇒
    let 〈label, instruction〉 ≝ hd in
      match label with
      [ None ⇒
        let 〈maps, the_program〉 ≝ pre_erase tl labels in
        match instruction with
        [ Cost cost ⇒ 〈maps, the_program〉
        | _ ⇒ 〈maps, 〈None …, instruction〉 :: the_program〉
        ]
      | Some label ⇒
        match instruction with
        [ Cost cost ⇒ pre_erase tl (label :: labels)
        | _ ⇒
          let 〈maps, the_program〉 ≝ pre_erase tl [ ] in
          let maps ≝ foldr ?? (λl. λmap. add … map l label) maps (label::labels) in
            〈maps, the_program〉
        ]
      ]
  ].
  @daemon
qed.

definition relabel_instruction: preinstruction Identifier → identifier_map ASMTag Identifier → preinstruction Identifier ≝
  λpre.
  λmap.
  match pre with
  [ JC ident ⇒
    let located ≝ lookup_def … map ident ident in
      JC … located
  | JNC ident ⇒
    let located ≝ lookup_def … map ident ident in
      JNC … located
  | JB bit ident ⇒
    let located ≝ lookup_def … map ident ident in
      JB … bit located
  | JNB bit ident ⇒
    let located ≝ lookup_def … map ident ident in
      JNB … bit located
  | JBC bit ident ⇒
    let located ≝ lookup_def … map ident ident in
      JBC … bit located
  | JZ ident ⇒
    let located ≝ lookup_def … map ident ident in
      JZ … located
  | JNZ ident ⇒
    let located ≝ lookup_def … map ident ident in
      JNZ … located
  | CJNE src ident ⇒
    let located ≝ lookup_def … map ident ident in
      CJNE … src located
  | DJNZ src ident ⇒
    let located ≝ lookup_def … map ident ident in
      DJNZ … src located
  (* XXX: no identifiers in rest of instructions *)
  | _ ⇒ pre
  ].

definition relabel_pseudo_instruction: pseudo_instruction → identifier_map ASMTag Identifier → pseudo_instruction ≝
  λpseudo.
  λmap.
  match pseudo with
  [ Instruction instr ⇒ Instruction (relabel_instruction instr map)
  | Cost cost ⇒ Cost cost
  | Comment comment ⇒ Comment comment
  | Jmp ident ⇒
    let located ≝ lookup_def … map ident ident in
      Jmp located
  | Call ident ⇒
    let located ≝ lookup_def … map ident ident in
      Call located
  | Mov dptr ident ⇒
    let located ≝ lookup_def … map ident ident in
      Mov dptr located
  ].
      
let rec relabel
  (the_program: list labelled_instruction) (map: identifier_map ASMTag Identifier)
    on the_program: list labelled_instruction ≝
  match the_program with
  [ nil        ⇒ [ ]
  | cons hd tl ⇒
    let 〈label, instruction〉 ≝ hd in
    let relabelled ≝ relabel_pseudo_instruction instruction map in
    let label ≝
      match label with
      [ None ⇒ None …
      | Some label ⇒ Some … (lookup_def … map ident ident)
      ]
    in
      〈label, relabelled〉 :: relabel tl map
  ].

definition erase: pseudo_assembly_program → pseudo_assembly_program ≝
  λprogram.
  let 〈preamble, instructions〉 ≝ program in
  let 〈maps, instructions〉 ≝ pre_erase instructions [ ] in
  let relabelled ≝ relabel instructions maps in
    〈preamble, relabelled〉.