include "ASM/Util.ma".
include "utilities/BitVectorTrieSet.ma".
include "utilities/IdentifierTools.ma".
include "LIN/LIN.ma".
  
let rec association (i: ident) (l: list (ident × nat))
                    on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝
  match l return λl. member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat with
  [ nil ⇒ λabsd. ?
  | cons hd tl ⇒
    λprf: member i (eq_identifier ?) (map ? ? (fst ? ?) (cons ? hd tl)).
      (match eq_identifier ? (\fst hd) i return λb. eq_identifier ? (\fst hd) i = b → nat with
      [ true ⇒ λeq_prf. \snd hd
      | false ⇒ λeq_prf. association i tl ?
      ]) (refl ? (eq_identifier ? (\fst hd) i))
  ].
  [ cases absd
  | cases prf
    [ > eq_prf
      # H
      cases H
    | # H
      assumption
    ]
  ]
qed.

definition statement_labels ≝
  λg: list ident.
  λs: lin_statement g.
  let 〈label, instr〉 ≝ s in
  let generated ≝
    match instr with
    [ joint_st_sequential instr' _ ⇒
        match instr' with
        [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
        | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
        | _ ⇒ set_empty ?
        ]
    | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    | joint_st_return ⇒ set_empty ?
    ] in
  match label with
  [ None ⇒ generated
  | Some lbl ⇒ set_insert ? (word_of_identifier ? lbl) generated
  ].

definition function_labels_internal ≝
  λglobals: list ident.
  λlabels: BitVectorTrieSet ?.
  λstatement: lin_statement globals.
    set_union ? labels (statement_labels globals statement).

(* dpm: A = Identifier *)
definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
  λA: Type[0].
  λglobals: list ident.
  λf: A × (lin_function_definition globals).
  let 〈ignore, fun_def〉 ≝ f in
  match fun_def return λ_. BitVectorTrieSet ? with
  [ lin_fu_internal stmts proof ⇒
      foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
  | lin_fu_external _ ⇒ set_empty ?
  ].
  
definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet ? ≝
  λA: Type[0].
  λglobals: list ident.
  λlabels: BitVectorTrieSet ?.
  λfunct: A × (lin_function_definition globals).
    set_union ? labels (function_labels ? globals funct).
    
definition program_labels ≝
  λprogram.
    foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_vars program)))
              (set_empty ?) (lin_pr_funcs program).
    
definition data_of_int ≝ λbv. DATA bv.
definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).

axiom ImplementedInRuntime: False.

definition translate_statements ≝
  λglobals: list (ident × nat).
  λglobals_old: list ident.
  λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
  λstatement: pre_lin_statement globals_old.
  match statement with
  [ joint_st_return ⇒ Instruction (RET ?)
  | joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
  | joint_st_sequential instr _ ⇒
    match instr with
    [ joint_instr_comment comment ⇒ Comment comment
    | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
    | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
    | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
    | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
    | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
    | joint_instr_opaccs accs ⇒
      match accs with
      [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
      | Divu ⇒ Instruction (DIV ? ACC_A ACC_B)
      | Modu ⇒ ?
      ]
    | joint_instr_op1 op1 ⇒
      match op1 with
      [ Cmpl ⇒ Instruction (CPL ? ACC_A)
      | Inc ⇒ Instruction (INC ? ACC_A)
      ]
    | joint_instr_op2 op2 reg ⇒
      match op2 with
      [ Add ⇒
        let reg' ≝ register_address (Register_of_register reg) in
        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                       direct;
                                                       registr ]] x) → ? with
        [ ACC_A ⇒ λacc_a: True.
          Instruction (ADD ? ACC_A accumulator_address)
        | DIRECT d ⇒ λdirect1: True.
          Instruction (ADD ? ACC_A (DIRECT d))
        | REGISTER r ⇒ λregister1: True.
          Instruction (ADD ? ACC_A (REGISTER r))
        | _ ⇒ λother: False. ⊥
        ] (subaddressing_modein … reg')
      | Addc ⇒
        let reg' ≝ register_address (Register_of_register reg) in
        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                       direct;
                                                       registr ]] x) → ? with
        [ ACC_A ⇒ λacc_a: True.
          Instruction (ADDC ? ACC_A accumulator_address)
        | DIRECT d ⇒ λdirect2: True.
          Instruction (ADDC ? ACC_A (DIRECT d))
        | REGISTER r ⇒ λregister2: True.
          Instruction (ADDC ? ACC_A (REGISTER r))
        | _ ⇒ λother: False. ⊥
        ] (subaddressing_modein … reg')
      | Sub ⇒
        let reg' ≝ register_address (Register_of_register reg) in
        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                       direct;
                                                       registr ]] x) → ? with
        [ ACC_A ⇒ λacc_a: True.
          Instruction (SUBB ? ACC_A accumulator_address)
        | DIRECT d ⇒ λdirect3: True.
          Instruction (SUBB ? ACC_A (DIRECT d))
        | REGISTER r ⇒ λregister3: True.
          Instruction (SUBB ? ACC_A (REGISTER r))
        | _ ⇒ λother: False. ⊥
        ] (subaddressing_modein … reg')
      | And ⇒
        let reg' ≝ register_address (Register_of_register reg) in
        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                       direct;
                                                       registr ]] x) → ? with
        [ ACC_A ⇒ λacc_a: True.
          Instruction (NOP ?)
        | DIRECT d ⇒ λdirect4: True.
          Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
        | REGISTER r ⇒ λregister4: True.
          Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
        | _ ⇒ λother: False. ⊥
        ] (subaddressing_modein … reg')
      | Or ⇒
        let reg' ≝ register_address (Register_of_register reg) in
        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                       direct;
                                                       registr ]] x) → ? with
        [ ACC_A ⇒ λacc_a: True.
          Instruction (NOP ?)
        | DIRECT d ⇒ λdirect5: True.
          Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
        | REGISTER r ⇒ λregister5: True.
          Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
        | _ ⇒ λother: False. ⊥
        ] (subaddressing_modein … reg')
      | Xor ⇒
        let reg' ≝ register_address (Register_of_register reg) in
        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                       direct;
                                                       registr ]] x) → ? with
        [ ACC_A ⇒ λacc_a: True.
          Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
        | DIRECT d ⇒ λdirect6: True.
          Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
        | REGISTER r ⇒ λregister6: True.
          Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
        | _ ⇒ λother: False. ⊥
        ] (subaddressing_modein … reg')
      ]
    | joint_instr_int reg byte ⇒
      let reg' ≝ register_address (Register_of_register reg) in
        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                       direct;
                                                       registr ]] x) → ? with
        [ REGISTER r ⇒ λregister7: True.
          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
        | ACC_A ⇒ λacc: True.
          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
        | DIRECT d ⇒ λdirect7: True.
          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
        | _ ⇒ λother: False. ⊥
        ] (subaddressing_modein … reg')
    | joint_instr_from_acc reg ⇒
      let reg' ≝ register_address (Register_of_register reg) in
        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                       direct;
                                                       registr ]] x) → ? with
        [ REGISTER r ⇒ λregister8: True.
          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
        | ACC_A ⇒ λacc: True.
          Instruction (NOP ?)
        | DIRECT d ⇒ λdirect8: True.
          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
        | _ ⇒ λother: False. ⊥
        ] (subaddressing_modein … reg')
    | joint_instr_to_acc reg ⇒
      let reg' ≝ register_address (Register_of_register reg) in
        match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                       direct;
                                                       registr ]] x) → ? with
        [ REGISTER r ⇒ λregister9: True.
          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
        | DIRECT d ⇒ λdirect9: True.
          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
        | ACC_A ⇒ λacc_a: True.
          Instruction (NOP ?)
        | _ ⇒ λother: False. ⊥
        ] (subaddressing_modein … reg')
    | joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    | joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    | joint_instr_address addr proof ⇒
      let look ≝ association addr globals (prf ? proof) in
        Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    | joint_instr_cond_acc lbl ⇒
      (* dpm: this should be handled in translate_code! *)
      WithLabel (JNZ ? (word_of_identifier ? lbl))
    ]
  ].
  try assumption
  try @ I
  cases ImplementedInRuntime
qed.

definition build_translated_statement ≝
  λglobals.
  λglobals_old.
  λprf.
  λstatement: lin_statement globals_old.
    〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.

definition translate_code ≝
  λglobals: list (ident × nat).
  λglobals_old: list ident.
  λprf.
  λcode: list (lin_statement globals_old).
    map ? ? (build_translated_statement globals globals_old prf) code.
    
lemma translate_code_preserves_WellFormedP:
  ∀globals, globals_old, prf, code.
    well_formed_P ? ? code → well_formed_P ? ? (translate_code globals globals_old prf code).
  #G #GO #P #C
  elim C
  [ normalize
    //
  | #G2 #G02 #IH (* CSC: understand here *)
    whd in ⊢ (% → %)
    normalize in ⊢ (% → %)
    //
  ]
qed.

definition translate_fun_def ≝
  λglobals.
  λglobals_old.
  λprf.
  λid_def.
    let 〈id, def〉 ≝ id_def in
    match def with
    [ lin_fu_internal code proof ⇒
      match translate_code globals globals_old prf code return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
      [ nil ⇒ λprf2. ⊥
      | cons hd tl ⇒ λ_.
        let rest ≝ 〈Some ? id, \snd hd〉 :: tl in
          map ? ? (
            λr.
            match fst ? ? r with
            [ Some id' ⇒ 〈Some ? (word_of_identifier ? id'), snd ? ? r〉
            | None ⇒ 〈None ?, \snd r〉
            ]) rest
      ] (translate_code_preserves_WellFormedP globals globals_old prf code proof)
    | _ ⇒ [ ]
    ].
    @ prf2
qed.
    
definition translate_functs ≝
  λglobals.
  λglobals_old.
  λprf.
  λexit_label.
  λmain.
  λfuncts.
  let preamble ≝
    match main with
    [ None ⇒ [ ]
    | Some main' ⇒ [ 〈None ?, Call main'〉 ; 〈Some ? exit_label, Jmp exit_label〉 ]
    ] in
      preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).

definition globals_addr_internal ≝
  λres_offset.
  λx_size: Identifier × nat.
    let 〈res, offset〉 ≝ res_offset in
    let 〈x, size〉 ≝ x_size in
      〈〈x, offset〉 :: res, offset + size〉.

definition globals_addr ≝
  λl.
    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
     
(* dpm: plays the role of the string "_exit" in the O'caml source *)
axiom identifier_prefix: Identifier.

(* dpm: fresh prefix stuff needs unifying with brian *)

(*
definition translate ≝
  λp.
  let prog_lbls ≝ program_labels p in
  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
  let global_addr ≝ globals_addr (LIN_Pr_vars p) in
    〈global_addr, translate_functs global_addr (map ? ? (fst ? ?) (LIN_Pr_vars p)) ? exit_label (LIN_Pr_main p) (LIN_Pr_funs p)〉.
*)