include "joint/Joint.ma".
include "joint/blocks.ma".
include "utilities/hide.ma".
include "utilities/deqsets.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
  ].

(* ignoring register allocation for now *)

definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).

lemma present_to_memb : ∀tag,A,l,m.present tag A m l → bool_to_Prop (l∈m).
#tag #A * #l * #m whd in ⊢ (%→?%);
elim (lookup tag ???)
[ * #ABS elim (ABS ?) %
| #a #_ %
] qed.

lemma memb_to_present : ∀tag,A,l,m.l∈m → present tag A m l.
#tag #A * #l * #m whd in ⊢ (?%→%);
elim (lookup tag ???)
[ * | #a * % #ABS destruct(ABS) ] qed.

(*
lemma All_fresh_not_memb : ∀tag,u,l,id,u'.
  All (identifier tag) (λid'.¬fresh_for_univ tag id' u) l →
  〈id, u'〉 = fresh tag u →
  ¬id ∈ l.
#tag #u #l elim l [2: #hd #tl #IH] #id #u' *
[ #hd_fresh #tl_fresh #EQfresh
  whd in ⊢ (?(?%));
  change with (eq_identifier ???) in match (?==?);
  >eq_identifier_sym
  >(eq_identifier_false … (fresh_distinct … hd_fresh EQfresh))
  normalize nodelta @(IH … tl_fresh EQfresh)
| #_ %
]
qed.
*)

lemma fresh_was_fresh : ∀tag,id,id',u,u'.
〈id,u'〉 = fresh tag u →
fresh_for_univ tag id' u' →
id' ≠ id →
fresh_for_univ tag id' u.
#tag * #id * #id' * #u * #u'
normalize #EQfresh destruct
#H #NEQ
elim (le_to_or_lt_eq … H)
[ (* not recompiling... /2 by monotonic_pred/ *) /2/ ]
#H >(succ_injective … H) in NEQ;
* #G elim (G (refl …))
qed.

(* use Russell? *)
axiom adds_graph_list_ok :
  ∀g_pars,globals,b,src,def.
  fresh_for_univ … src (joint_if_luniverse … def) →
  luniverse_ok ?? def →
  let 〈def', dst〉 ≝ adds_graph_list g_pars globals b src def in
  luniverse_ok ?? def' ∧
  ∃l.bool_to_Prop (uniqueb … l) ∧
     All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
                  fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
     src ~❨b,l❩~> dst in joint_if_code … def'.
(*
#p #g #l elim l -l
[ #src #def #_ #Hdef whd
  %{Hdef} %{[ ]} %%% ]
#hd #tl #IH #src #def #src_fresh #Hdef
whd in match (adds_graph_list ?????);
whd in match (fresh_label ???);
@(pair_elim … (fresh ??)) normalize nodelta
#mid #luniverse' #EQfresh
whd in ⊢ (match % with [ _ ⇒ ?]);
letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse'))
cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def)
  [ % ] #EQ_aux
  lapply (IH mid def' ??)
  [ #l whd in match def'; #Hpres
    lapply (present_to_memb … Hpres) -Hpres
    >mem_set_add @eq_identifier_elim
    [ #EQ destruct(EQ) *
    | #NEQ change with (? ∈ joint_if_code p ??) in ⊢ (?%→?); >EQ_aux
      #l_in
    ]
    @(fresh_remains_fresh … (sym_eq … EQfresh))
    [2: @Hdef @memb_to_present ] assumption
  | whd in match def';
    cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
    whd in match (set_luniverse ????);
    @(fresh_is_fresh … (sym_eq … EQfresh))
  ]
  elim (adds_graph_list ?????) #def'' #mid' normalize nodelta
  * #Hdef'' * #l ** #Hl1 #Hl2 #Hl3 %{Hdef''} %{(mid::l)}
  % [ % ]
  [ whd in ⊢ (?%);
    cut (Not (bool_to_Prop (mid∈l)))
    [ % #H elim (All_memb … Hl2 H)
      whd in match (joint_if_luniverse ???);
      #G #_ @(absurd ?? G)
      @ (fresh_is_fresh … (sym_eq … EQfresh))
    | #H >H assumption
    ]
  | %
    [ %
      [ 
      normalize #H10 #H11
      
    >(All_fresh_not_memb … (sym_eq … EQfresh))
    [ assumption ]
    @(All_mp … Hl2) #lbl *
    cases def in EQfresh; #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19
    normalize #EQfresh #H #lbl_not_mid
    lapply(fresh_remains_fresh … H (sym_eq … EQfresh))
    
    elim (true_or_false_Prop (mid∈l)) #mid_l >mid_l
    [ normalize
*)

(* 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
    | FCOND abs _ _ _ ⇒ Ⓧabs
    ] 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
    | FCOND abs _ _ _ ⇒ Ⓧabs
    ] in
  foldi … f (joint_if_code … def) empty.

definition init_graph_if ≝ 
  λg_pars : graph_params.λglobals.
  λluniverse,runiverse,ret,params,locals,stack_size,entry,exit.
  let graph ≝ add ? ? (empty_map ? (joint_statement ??)) entry (GOTO … exit) in
  let graph ≝ add ? ? graph exit (RETURN …) in
  mk_joint_internal_function g_pars globals
    luniverse runiverse ret params locals stack_size
    graph entry exit.
>graph_code_has_point @map_mem_prop
[@graph_add_lookup] @graph_add
qed.


(* 
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).
  *)