include "joint/Joint_paolo.ma".
include "joint/blocks.ma".
include "utilities/hide.ma".

(* general type of functions generating fresh things *)
definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g).

include alias "basics/lists/list.ma".
let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ)
  on n :
  freshT pars globals (Σl : list A. |l| = n) ≝
  match n  return λx.freshT … (Σl.|l| = x) with
  [ O ⇒ return «[ ], ?»
  | S n' ⇒
    ! regs' ← repeat_fresh … fresh n';
    ! reg ← fresh ;
    return «reg::regs',?»
  ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.

definition fresh_label:
 ∀g_pars,globals.freshT globals g_pars label ≝
  λg_pars,globals,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_list
  (g_pars: graph_params)
  (globals: list ident)
  (insts: list (joint_seq g_pars globals))
  (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝
  match insts with
  [ nil ⇒ return src
  | cons instr others ⇒
    ! mid ← fresh_label … ;
    ! def ← state_get … ;
    !_ state_set … (add_graph … src (sequential … instr mid) def) ;
    adds_graph_list g_pars globals others mid
  ].

definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
  [ inl _ ⇒ true
  | inr _ ⇒ false
  ].
definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
  [ inl _ ⇒ true
  | inr _ ⇒ false
  ].

definition adds_graph :
  ∀g_pars : graph_params.
  ∀globals: list ident.
  ∀b : seq_block g_pars globals (joint_step g_pars globals) +
       seq_block g_pars globals (joint_fin_step g_pars).
  label → if is_inl … b then label else unit →
  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
  λg_pars,globals,insts,src.
  match insts return λx.if is_inl … x then ? else ? → ? → ? with
  [ inl b ⇒ λdst,def.
    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
    add_graph … mid (sequential … (\snd b) dst) def
  | inr b ⇒ λdst,def.
    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
    add_graph … mid (final … (\snd b)) def
  ].

(* preserves first statement if a cost label (should be an invariant) *)
definition insert_prologue ≝
  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
  λdef : joint_internal_function g_pars globals.
  let entry ≝ joint_if_entry … def in
  match stmt_at … entry
  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
  with
  [ Some s ⇒ λ_.
    match s with
    [ sequential s' next ⇒
      match s' with
      [ step_seq s'' ⇒
        match s'' with
        [ COST_LABEL _ ⇒
          adds_graph ?? (inl … (s'' :: insts)) entry next def
        | _ ⇒
          let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
          add_graph … tmp s def'
        ]
      | _ ⇒
        let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
        add_graph … tmp s def'
      ]
    | _ ⇒
      let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
      add_graph … tmp s def'
    ]
  | None ⇒ Ⓧ
  ] (pi2 … entry).

definition insert_epilogue ≝
  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
  λdef : joint_internal_function g_pars globals.
  let exit ≝ joint_if_exit … def in
  match stmt_at … exit
  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
  with
  [ Some s ⇒ λ_.
    let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in
    let def'' ≝ add_graph … tmp s def' in
    set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp
  | None ⇒ Ⓧ
  ] (pi2 … exit).
whd in match def''; >graph_code_has_point //
qed.

definition b_adds_graph :
  ∀g_pars: graph_params.
  ∀globals: list ident.
  (* fresh register creation *)
  freshT g_pars globals (localsT … g_pars) →
  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
       bind_seq_block g_pars globals (joint_fin_step g_pars).
  label → if is_inl … b then label else unit →
  joint_internal_function g_pars globals→
  joint_internal_function g_pars globals ≝
  λg_pars,globals,fresh_r,insts,src.
  match insts return λx.if is_inl … x then ? else ? → ? → ? with
  [ inl b ⇒ λdst,def.
    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
    adds_graph … (inl … stmts) src dst def
  | inr b ⇒ λdst,def.
    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
    adds_graph … (inr … stmts) src dst def
  ].

(* translation with inline fresh register allocation *)
definition b_graph_translate :
  ∀src_g_pars,dst_g_pars : graph_params.
  ∀globals: list ident.
  (* fresh register creation *)
  freshT dst_g_pars globals (localsT dst_g_pars) →
  (* initialized function definition with empty graph *)
  joint_internal_function dst_g_pars globals →
  (* functions dictating the translation *)
  (label → joint_step src_g_pars globals →
    bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
  (label → joint_fin_step src_g_pars →
    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
  (* source function *)
  joint_internal_function src_g_pars globals →
  (* destination function *)
  joint_internal_function dst_g_pars globals ≝
  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
  let f : label → joint_statement (src_g_pars : params) globals →
    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 
    λlbl,stmt,def.
    match stmt with
    [ sequential inst next ⇒
      b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def
    | final inst ⇒
      b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it 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.
  (* initialized function definition with empty graph *)
  joint_internal_function dst_g_pars globals →
  (* functions dictating the translation *)
  (label → joint_step src_g_pars globals →
    seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
  (label → joint_fin_step src_g_pars →
    seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
  (* source function *)
  joint_internal_function src_g_pars globals →
  (* destination function *)
  joint_internal_function dst_g_pars globals ≝ 
  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
  let f : label → joint_statement (src_g_pars : params) globals →
    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 
    λlbl,stmt,def.
    match stmt with
    [ sequential inst next ⇒
      adds_graph … (inl … (trans_step lbl inst)) lbl next def
    | final inst ⇒
      adds_graph … (inr … (trans_fin_step lbl inst)) lbl it 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).
  *)