include "ASM/Util.ma".
include "utilities/BitVectorTrieSet.ma".
include "LIN/LIN.ma".
include "ASM/ASM.ma".

definition register_address: Register → [[ acc_a; direct; registr ]] ≝
  λr: Register.
    match r with
    [ Register00 ⇒ REGISTER [[ false; false; false ]]
    | Register01 ⇒ REGISTER [[ false; false; true ]]
    | Register02 ⇒ REGISTER [[ false; true; false ]]
    | Register03 ⇒ REGISTER [[ false; true; true ]]
    | Register04 ⇒ REGISTER [[ true; false; false ]]
    | Register05 ⇒ REGISTER [[ true; false; true ]]
    | Register06 ⇒ REGISTER [[ true; true; false ]]
    | Register07 ⇒ REGISTER [[ true; true; true ]]
    | RegisterA ⇒ ACC_A
    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r)) 
    ]. @I qed.

(* TODO:
  this should translate back end immediates (which rely on beval) to ASM
  byte immediates. How should it work? surely needs arguments for instantiation
  of blocks. If it's too much a fuss, we can go back to byte immediates in the
  back end. *)
definition asm_byte_of_beval : beval → Byte ≝
  λb.match b with
    [ BVByte b ⇒ b
    | BVundef ⇒ (* any will do *) zero_byte
    | BVnonzero ⇒ (* any will do *) maximum 7 @@ [[ true ]]
    | BVnull _ ⇒ zero_byte (* is it correct? *)
    | BVptr b p o ⇒ ?
    ].
  cases daemon qed.

definition arg_address : hdw_argument → [[ acc_a ; direct ; registr ; data ]] ≝
  λa.match a with
  [ Reg r ⇒ register_address r
  | Imm bv ⇒ DATA (asm_byte_of_beval bv)
  ].
  cases a #x [2: normalize //] normalize nodelta
  elim (register_address ?) #rslt @is_in_subvector_is_in_supervector @I
qed.

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 lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
 
definition statement_labels ≝
  λg: list ident.
  λs: lin_statement g.
  let 〈label, instr〉 ≝ s in
  let generated ≝
    match instr with
    [ sequential instr' _ ⇒
      match instr' with
      [ step_seq instr'' ⇒
        match instr'' with
        [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
        | _ ⇒ ∅
        ]
      | COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }
      ]
    | final instr' ⇒
      match instr' with
      [ GOTO lbl ⇒ {(toASM_ident ? lbl)}
      | _ ⇒ ∅
      ]
    ]
  in
  match label with
  [ None ⇒ generated
  | Some lbl ⇒ add_set ? generated (toASM_ident ? lbl)
  ].

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

(* dpm: A = Identifier *)
definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝
  λA: Type[0].
  λglobals: list ident.
  λf: A × (joint_function LIN globals).
  let 〈ignore, fun_def〉 ≝ f in
  match fun_def return λ_. identifier_set ? with
  [ Internal stmts ⇒
      foldl ? ? (function_labels_internal globals) ∅ (joint_if_code ?? stmts)
  | External _ ⇒ ∅
  ].
  
definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝
  λA: Type[0].
  λglobals: list ident.
  λlabels: identifier_set ?.
  λfunct: A × (joint_function LIN globals).
    labels ∪ (function_labels ? globals funct).

(* CSC: here we are silently throwing away the region information *)
definition program_labels ≝
 λprogram: lin_program.
    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
              ∅ (prog_funct … 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).

(* TODO: check and change to free bit *)
definition asm_other_bit ≝ BIT_ADDR (zero_byte).

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: joint_statement LIN globals_old.
  match statement with
  [ final instr ⇒
    match instr with
    [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
    | RETURN ⇒ Instruction (RET ?)
    | tailcall abs ⇒ match abs in void with [ ]
    ]
  | sequential instr _ ⇒
      match instr with
      [ step_seq instr' ⇒
        match instr' with
        [ extension_seq ext ⇒
          match ext with
          [ SAVE_CARRY ⇒
            Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
          | RESTORE_CARRY ⇒
            Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
          ]
        | COMMENT comment ⇒ Comment comment
        | COST_LABEL lbl ⇒ Cost lbl
        | POP _ ⇒ Instruction (POP ? accumulator_address)
        | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
        | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
        | CALL_ID f _ _ ⇒ Call (toASM_ident ? f)
        | extension_call abs ⇒ match abs in void with [ ]
        | OPACCS accs _ _ _ _ ⇒
          match accs with
          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
          ]
        | OP1 op1 _ _ ⇒
          match op1 with
          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
          | Inc ⇒ Instruction (INC ? ACC_A)
          | Rl ⇒ Instruction (RL ? ACC_A)
          ]
        | OP2 op2 _ _ reg ⇒
          match op2 with
          [ Add ⇒
            let reg' ≝ arg_address reg in
            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                           direct;
                                                           registr;
                                                           data ]] 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))
            | DATA b ⇒ λdata : True.
              Instruction (ADD ? ACC_A (DATA b))
            | _ ⇒ Ⓧ
            ] (subaddressing_modein … reg')
          | Addc ⇒
            let reg' ≝ arg_address reg in
            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                           direct;
                                                           registr;
                                                           data ]] 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))
            | DATA b ⇒ λdata : True.
              Instruction (ADDC ? ACC_A (DATA b))
            | _ ⇒ Ⓧ
            ] (subaddressing_modein … reg')
          | Sub ⇒
            let reg' ≝ arg_address reg in
            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                           direct;
                                                           registr;
                                                           data ]] 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))
            | DATA b ⇒ λdata : True.
              Instruction (SUBB ? ACC_A (DATA b))
            | _ ⇒ Ⓧ
            ] (subaddressing_modein … reg')
          | And ⇒
            let reg' ≝ arg_address reg in
            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                           direct;
                                                           registr;
                                                           data ]] 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〉)))
            | DATA b ⇒ λdata : True.
              Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
            | _ ⇒ Ⓧ
            ] (subaddressing_modein … reg')
          | Or ⇒
            let reg' ≝ arg_address reg in
            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                           direct;
                                                           registr ; data ]] 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〉)))
            | DATA b ⇒ λdata : True.
              Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
            | _ ⇒ Ⓧ
            ] (subaddressing_modein … reg')
          | Xor ⇒
            let reg' ≝ arg_address reg in
            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
                                                           direct;
                                                           registr ; data ]] 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〉))
            | DATA b ⇒ λdata : True.
              Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
            | _ ⇒ Ⓧ
            ] (subaddressing_modein … reg')
          ]
        | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
        | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
        | ADDRESS addr proof _ _ ⇒
          let look ≝ association addr globals (prf ? proof) in
            Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
        | SET_CARRY ⇒
          Instruction (SETB ? CARRY)
        | MOVE regs ⇒
          match regs with
          [ to_acc _ reg ⇒
             let reg' ≝ register_address 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')
          | from_acc reg _ ⇒
             let reg' ≝ register_address 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')
          | int_to_reg reg bv ⇒
            let b ≝ asm_byte_of_beval bv in
            let reg' ≝ register_address 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 b〉))))))
              | ACC_A ⇒ λacc: True.
                Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
              | DIRECT d ⇒ λdirect7: True.
                Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
              | _ ⇒ λother: False. ⊥
              ] (subaddressing_modein … reg')
          | int_to_acc _ bv ⇒
            let b ≝ asm_byte_of_beval bv in
            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
          ]
        ]
      | COND _ lbl ⇒
        (* dpm: this should be handled in translate_code! *)
        Instruction (JNZ ? (toASM_ident ? lbl))
      ]
    ].
  try assumption
  try @ I
qed.

(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
definition ident_of_label: label → Identifier ≝
 toASM_ident LabelTag.

definition build_translated_statement ≝
  λglobals.
  λglobals_old.
  λprf.
  λstatement: lin_statement globals_old.
    〈option_map … ident_of_label (\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.

definition translate_fun_def ≝
  λglobals: list (ident × nat).
  λglobals_old.
  λprf.
  λid_def.
    let 〈id, def〉 ≝ id_def in
    match def with
    [ Internal int ⇒
      let code ≝ joint_if_code LIN globals_old int in
      match translate_code globals globals_old prf code with
      [ nil ⇒ ⊥
      | cons hd tl ⇒
        let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in
          map ? ? (
            λr.
            match fst ? ? r with
            [ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉
            | None ⇒ 〈None ?, \snd r〉
            ]) rest
      ]
    | External _ ⇒ [ ]
    ].
cases daemon (*CSC: XXX will be fixed by an invariant later *)
qed.

include "common/Identifiers.ma".

let rec flatten_fun_defs
  (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat)
    (the_list: list ((identifier SymbolTag) × (fundef (joint_internal_function LIN globals_old))))
      on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝
  match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with
  [ cons hd tl ⇒
    let fun_def ≝ \snd hd in
    let fun_id ≝ \fst hd in
    let translated ≝ translate_fun_def globals globals_old prf hd in
    let size_translated ≝ | translated | in
    let 〈tail_trans, tail_map〉 ≝ flatten_fun_defs globals globals_old prf (initial_pc + size_translated) tl in
    let new_hd ≝ translated @ tail_trans in
    let new_map ≝ add ? ? tail_map fun_id initial_pc in
      〈new_hd, new_map〉
  | nil ⇒ 〈[ ], empty_map …〉
  ].

definition translate_functs ≝
  λglobals.
  λglobals_old.
  λprf.
  λexit_label.
  λmain.
  λfuncts.
  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
  let 〈flattened, map〉 ≝ flatten_fun_defs globals globals_old prf 6 (* Size of preamble above *) functs in
   〈preamble @ flattened, map〉.

(*CSC: region silently thrown away here *)
definition globals_addr ≝
 λl.
  let globals_addr_internal ≝
   λres_offset.
   λx_size: ident × region × nat.
    let 〈res, offset〉 ≝ res_offset in
    let 〈x, region, size〉 ≝ x_size in
      〈〈x, offset〉 :: res, offset + size〉
  in
    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).

(* dpm: plays the role of the string "_exit" in the O'caml source *)
axiom identifier_prefix: Identifier.
(*CSC: XXXXXXX wrong anyway since labels from different functions can now
  clash with each other and with names of functions *)
axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier.

(* dpm: fresh prefix stuff needs unifying with brian *)
definition lin_to_asm : lin_program → pseudo_assembly_program ≝
  λp.
  let prog_lbls ≝ program_labels … p in
  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
  let global_addr ≝ globals_addr (prog_vars … p) in
  let global_addr' ≝ map … (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x, bitvector_of_nat 16 off〉) global_addr in
  let 〈translated, funct_map〉 ≝ translate_functs global_addr (prog_var_names … p) ? exit_label (toASM_ident … (prog_main … p)) (prog_funct … p) in
    〈〈funct_map, global_addr'〉, translated〉.
 #i normalize nodelta -global_addr' -global_addr -exit_label -prog_lbls;
 normalize in match prog_var_names; normalize nodelta
 elim (prog_vars … p) //
 #hd #tl #IH whd in ⊢ (% → %);
 whd in match globals_addr; normalize nodelta
 whd in match (foldl ???? (hd::tl)); normalize nodelta
 cases hd * #id #reg #size normalize nodelta
 cases daemon (*CSC: provable using a pair of lemmas over foldl *)
qed.