include "joint/Joint_paolo.ma".
include "utilities/bindLists.ma".

(* general type of functions generating fresh things *)
(* type T is the syntactic type of the generated things *)
(* (sig for RTLabs registers, unit in others ) *)
definition freshT ≝ λg.λpars : params.λX,T : Type[0].
   T → state_monad (joint_internal_function … g pars) X.

definition rtl_ertl_fresh_reg: 
 ∀inst_pars,funct_pars,globals.
  freshT globals (rtl_ertl_params inst_pars funct_pars) register unit ≝
  λinst_pars,var_pars,globals,it,def.
    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.

let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n :
  freshT globals (rtl_ertl_params inst_pars funct_pars) (list register) unit ≝
  match n with
  [ O ⇒ λ_. return [ ]
  | S n' ⇒ λ_.
    ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n' it;
    ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals it;
    return (reg :: regs')
  ].

lemma rtl_ertl_fresh_regs_length:
 ∀i_pars,f_pars,globals.∀def: joint_internal_function … globals
  (rtl_ertl_params i_pars f_pars). ∀n: nat.
  |(\snd (rtl_ertl_fresh_regs … n it def))| = n.
 #ipars#fpars #globals #def #n elim n
  [ %
  | #m whd in ⊢ (? → ??(??(???%))?); @pair_elim
    #def' #regs #EQ>EQ
    whd in ⊢ (? → ??(??(???%))?); @pair_elim #def'' #reg #_ normalize // ]
qed.

definition rtl_ertl_fresh_regs_strong:
 ∀i_pars,f_pars,globals. joint_internal_function … globals (rtl_ertl_params i_pars f_pars) →
  ∀n: nat. Σregs: (joint_internal_function … globals (rtl_ertl_params i_pars f_pars)) × (list register). |\snd regs| = n ≝
 λi_pars,f_pars,globals,def,n.rtl_ertl_fresh_regs i_pars f_pars globals n it def. //
qed.

definition fresh_label:
 ∀g_pars,globals.freshT globals g_pars label unit ≝
  λg_pars,globals,it,def.
    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
     〈set_luniverse … def luniverse, r〉.

(* insert into a graph a block of instructions *)
let rec adds_graph
  (g_pars: graph_params)
  (globals: list ident)
  (insts: list (joint_instruction g_pars globals))
  (src : label)
  (dest : label)
  (def: joint_internal_function … g_pars) on insts ≝
  match insts with
  [ nil ⇒ add_graph … src (GOTO … dest) def
  | cons instr others ⇒
    match others with
    [ nil ⇒ (* only one instruction *)
      add_graph … src (sequential … instr dest) def
    | _ ⇒ (* need to generate label *)
      let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
      adds_graph g_pars globals others tmp_lbl dest
        (add_graph … src (sequential … instr tmp_lbl) def)
    ]
  ].

definition b_adds_graph :
  ∀g_pars: graph_params.
  ∀globals: list ident.
  (* type of allocatable registers and of their types (unit if not in RTLabs) *)
  ∀R,T : Type[0].
  (* fresh register creation *)
  freshT globals g_pars R T →
  ∀insts: bind_list R T (joint_instruction g_pars globals).
  ∀src : label.
  ∀dest : label.
  joint_internal_function globals g_pars →
  joint_internal_function globals g_pars ≝
  λg_pars,globals,T,R,fresh_r,insts,src,dest,def.
  let 〈def', stmts〉 ≝ bcompile … fresh_r insts def in
  adds_graph … stmts src dest def'.

(* translation with inline fresh register allocation *)
definition b_graph_translate :
  ∀src_g_pars,dst_g_pars : graph_params.
  ∀globals: list ident.
  (* type of allocatable registers (unit if not in RTLabs) *)
  ∀T : Type[0].
  (* fresh register creation *)
  freshT globals dst_g_pars (localsT dst_g_pars) T →
  (* function dictating the translation *)
  (label → joint_instruction src_g_pars globals →
    bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
    (* this can be added to allow redirections: × label *)) →
  (* initialized function definition with empty graph *)
  joint_internal_function globals dst_g_pars →
  (* source function *)
  joint_internal_function globals src_g_pars →
  (* destination function *)
  joint_internal_function globals dst_g_pars ≝ 
  λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,empty,def.
  let f : label → joint_statement src_g_pars globals →
    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝ 
    λlbl,stmt,def.
    match stmt with
    [ sequential inst next ⇒ b_adds_graph … fresh_reg (trans lbl inst) lbl next def
    | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    | RETURN ⇒ add_graph … lbl (RETURN …) def
    ] in
  foldi … f (joint_if_code … def) empty.
  
(* translation without register allocation *)
definition graph_translate :
  ∀src_g_pars,dst_g_pars : graph_params.
  ∀globals: list ident.
  (* function dictating the translation *)
  (label → joint_instruction src_g_pars globals →
    list (joint_instruction dst_g_pars globals)) →
  (* initialized function definition with empty graph *)
  joint_internal_function … dst_g_pars →
  (* source function *)
  joint_internal_function … src_g_pars →
  (* destination function *)
  joint_internal_function … dst_g_pars ≝ 
  λsrc_g_pars,dst_g_pars,globals,trans,empty,def.
  let f : label → joint_statement src_g_pars globals →
    joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝ 
    λlbl,stmt,def.
    match stmt with
    [ sequential inst next ⇒
      adds_graph dst_g_pars globals (trans lbl inst) lbl next def
    | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    | RETURN ⇒ add_graph … lbl (RETURN …) def
    ] in
  foldi ??? f (joint_if_code ?? def) empty.
      
(* 
let rec add_translates
  (pars1: params1) (globals: list ident)
  (translate_list: list ?) (start_lbl: label) (dest_lbl: label) 
  (def: joint_internal_function … (graph_params pars1 globals))
    on translate_list ≝
  match translate_list with
  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
  | cons trans translate_list ⇒
    match translate_list with
    [ nil ⇒ trans start_lbl dest_lbl def
    | _ ⇒
      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
      let def ≝ trans start_lbl tmp_lbl def in
        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].

definition adds_graph ≝
 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
  *)