include "joint/Joint.ma".
include "joint/blocks.ma".
include "utilities/hide.ma".
include "utilities/deqsets_extra.ma".

(*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.state_monad (joint_internal_function g_pars globals) label ≝
  λg_pars,globals,def.
    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
     〈set_luniverse … def luniverse, r〉.

definition fresh_register:
 ∀g_pars,globals.state_monad (joint_internal_function g_pars globals) register ≝
  λg_pars,globals,def.
    let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
     〈set_runiverse … def runiverse, r〉.

(* insert into a graph a list of instructions *)
let rec adds_graph_pre
  X
  (g_pars: graph_params)
  (globals: list ident)
  (* for ERTLptr: the label parameter is filled by the last label *)
  (pre_process : label → X → joint_seq g_pars globals)
  (insts: list X)
  (src : label) on insts :
  state_monad (joint_internal_function g_pars globals) label ≝
  match insts with
  [ nil ⇒ return src
  | cons i rest ⇒
    ! mid ← fresh_label … ;
    ! dst ← adds_graph_pre … pre_process rest mid ;
    !_ state_update … (add_graph … src (sequential … (pre_process dst i) mid)) ;
    return dst
  ].

let rec adds_graph_post
  (g_pars: graph_params)
  (globals: list ident)
  (insts: list (joint_seq g_pars globals))
  (dst : label) on insts :
  state_monad (joint_internal_function g_pars globals) label ≝
  match insts with
  [ nil ⇒ return dst
  | cons i rest ⇒
    ! src ← fresh_label … ;
    ! mid ← adds_graph_post … rest dst ;
    !_ state_update … (add_graph … src (sequential … i mid)) ;
    return src
  ].

definition adds_graph :
  ∀g_pars : graph_params.
  ∀globals: list ident.
  ∀b : step_block g_pars globals.
  label → label →
  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
  λg_pars,globals,insts,src,dst,def.
  let pref ≝ \fst (\fst insts) in
  let op ≝ \snd (\fst insts) in
  let post ≝ \snd insts in
  let 〈def, mid〉 ≝ adds_graph_pre … (λlbl,inst.inst lbl) pref src def in
  let 〈def, mid'〉 ≝ adds_graph_post … post dst def in
  add_graph … mid (sequential … (op mid) mid') def.

definition fin_adds_graph :
  ∀g_pars : graph_params.
  ∀globals: list ident.
  ∀b : fin_block g_pars globals.
  label →
  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
  λg_pars,globals,insts,src,def.
  let pref ≝ \fst insts in
  let last ≝ \snd insts in
  let 〈def, mid〉 ≝ adds_graph_pre … (λ_.λi.i) pref src def in
  add_graph … mid (final … last) 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 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.

lemma fresh_not_in_univ : ∀tag,id,u,u'.
〈id, u'〉 = fresh tag u →
¬fresh_for_univ tag id u.
#tag * #id * #u * #u' normalize #EQ destruct //
qed.
*)
(*
lemma adds_graph_list_fresh_preserve :
  ∀g_pars,globals,b,src,dst,def.
  let def' ≝ adds_graph_list g_pars globals b src dst def in
  ∀lbl.fresh_for_univ … lbl (joint_if_luniverse … def) →
       fresh_for_univ … lbl (joint_if_luniverse … def').
#g_pars #globals #l elim l -l
[ #src #dst #def whd #lbl #H @H ]
#hd1 * [ #_ #src #dst #def whd #lbl #H @H ] #hd2 #tl #IH #src #dst #def whd #lbl #H
whd in match (adds_graph_list ??????);
whd in match fresh_label; normalize nodelta
inversion (fresh ??) #mid #luniv' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh
normalize nodelta 
@IH whd in match (joint_if_luniverse ???);
@(fresh_remains_fresh … EQfresh) @H
qed.

lemma with_last_not_empty : ∀X,pref,last.not_empty X (pref @ [last]).
#X * [2: #hd #tl ] #last % qed.

lemma split_on_last_ne_elim : ∀X,l.∀P : ((list X) × X) → Prop.
(∀pref,last.pi1 ?? l = pref @ [last] → P 〈pref, last〉) →
P (split_on_last_ne X l).
#X * @list_elim_left [ * ] #last #pref #_ #prf #P #H
>split_on_last_ne_def @H % qed.

(* use Russell? *)
lemma adds_graph_list_ok :
  ∀g_pars,globals,b,src,dst,def.
  fresh_for_univ … src (joint_if_luniverse … def) →
  luniverse_ok ?? def →
  let def' ≝ adds_graph_list g_pars globals b src dst def in
  luniverse_ok ?? def' ∧
  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
                      stmt_at … (joint_if_code … def') lbl =
                      stmt_at … (joint_if_code … def) lbl) ∧
  let B ≝ ensure_step_block … b in
  ∃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 [2: #hd1 * [ #_ | #hd2 #tl #IH ]]
#src #dst #def #Hsrc #Hdef
[1,3: %
  [1,3: %
    [1,3: #lbl @(eq_identifier_elim … lbl src) #H destruct [1,3: #_ @Hsrc ]
      whd in ⊢ (%→?); whd in match (adds_graph_list ??????);
      >(lookup_add_miss ?????? H) @Hdef
    |*: #lbl #H #G @lookup_add_miss @H
    ]
  |*: %{[]} % [1,3: %% ] %{src} % [1,3:%] %{dst} % [1,3: @lookup_add_hit ] %
  ]
]
whd in match (adds_graph_list ??????);
whd in match (fresh_label ???);
inversion (fresh ??) normalize nodelta
#mid #luniverse' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh
letin def' ≝ (add_graph p g src (sequential … hd1 mid) (set_luniverse … def luniverse'))
lapply (IH mid dst def' ??)
[ #lbl @(eq_identifier_elim … lbl src) #H destruct
  [2: whd in ⊢ (%→?); whd in match (adds_graph_list ??????);
    >(lookup_add_miss ?????? H) ]
  #Hpres @(fresh_remains_fresh … EQfresh) [ @Hdef ] assumption
| whd in match def';
  @(fresh_is_fresh … EQfresh)
]
whd in match (joint_if_luniverse ???);
whd in match (joint_if_code ???);
** #Hdef'' #stmt_preserved * #l ** #Hl1 #Hl2 
whd in ⊢ (%→?); @split_on_last_ne_elim #pref #last #EQ * #mid' * #Hl3 #Hl4
%
[ %{Hdef''} #lbl #NEQ
  @(eq_identifier_elim ?? lbl mid)
  [ #EQ destruct #ABS cases (absurd ? ABS ?) @(fresh_not_in_univ … EQfresh)
  | #NEQ' #H >(stmt_preserved … NEQ')
    [ whd in match (joint_if_code ???);
      whd in match (stmt_at ????); >lookup_add_miss [2: @NEQ ] %
    | @(fresh_remains_fresh … EQfresh) @H
    ]
  ]
]
%{(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 … EQfresh)
  | #H >H assumption
  ]
| %
  [ %{(fresh_not_in_univ … EQfresh)}
    @adds_graph_list_fresh_preserve @(fresh_is_fresh … EQfresh)
  | @(All_mp … Hl2) #lbl * * #H1 #H2 %{H2} % #H3 @H1
    @(fresh_remains_fresh … EQfresh) assumption
  ]
| whd in match (ensure_step_block ???) in EQ ⊢ %;
  whd in match (map ??? (hd2 :: ?)); >EQ whd
  change with ((?::?)@?) in match (?::?@?); >split_on_last_ne_def
  %{mid'} % [2: @Hl4 ]
  %{Hl3} %{mid} >stmt_preserved
  [ % [2: % ] @lookup_add_hit
  | @(fresh_remains_fresh … EQfresh) assumption
  | % #ABS destruct @(absurd ? Hsrc) @(fresh_not_in_univ … EQfresh)
  ]
]
qed.
*)
(*
axiom adds_graph_ok :
  ∀g_pars,globals,B,src,dst,def.
  fresh_for_univ … src (joint_if_luniverse … def) →
  luniverse_ok ?? def →
  let def' ≝ adds_graph g_pars globals B src dst def in
  luniverse_ok ?? def' ∧
  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
                      stmt_at … (joint_if_code … def') lbl =
                      stmt_at … (joint_if_code … def) lbl) ∧
  ∃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,src::l❩~> dst in joint_if_code … def'.
 
axiom fin_adds_graph_ok :
  ∀g_pars,globals,B,src,def.
  fresh_for_univ … src (joint_if_luniverse … def) →
  luniverse_ok ?? def →
  let def' ≝ fin_adds_graph g_pars globals B src def in
  luniverse_ok ?? def' ∧
  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
                      stmt_at … (joint_if_code … def') lbl =
                      stmt_at … (joint_if_code … def) lbl) ∧
  ∃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,src::l❩~> it in joint_if_code … def'.
*)

definition append_seq_list :
∀p,g.bind_step_block p g → bind_new register (list (joint_seq p g)) →
  bind_step_block p g ≝
λp,g,bbl,bl.
! 〈pref, op, post〉 ← bbl ; ! l ← bl ; return 〈pref, op, post @ l〉.

(*
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.
  ∀b : bind_step_block g_pars globals.
  label → label →
  joint_internal_function g_pars globals→
  joint_internal_function g_pars globals ≝
  λg_pars,globals,insts,src,dst,def.
  let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in
  adds_graph … stmts src dst def.

(*
axiom b_adds_graph_ok :
  ∀g_pars,globals,B,src,dst,def.
  fresh_for_univ … src (joint_if_luniverse … def) →
  luniverse_ok ?? def →
  let def' ≝ b_adds_graph g_pars globals B src dst def in
  luniverse_ok ?? def' ∧
  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
                      stmt_at … (joint_if_code … def') lbl =
                      stmt_at … (joint_if_code … def) lbl) ∧
  ∃l,r.
    bool_to_Prop (uniqueb … l) ∧
    bool_to_Prop (uniqueb … r) ∧
    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
    src ~❨B,src::l,r❩~> dst in joint_if_code … def'.
*)
definition b_fin_adds_graph :
  ∀g_pars: graph_params.
  ∀globals: list ident.
  ∀b : bind_fin_block g_pars globals.
  label →
  joint_internal_function g_pars globals→
  joint_internal_function g_pars globals ≝
  λg_pars,globals,insts,src,def.
  let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in
  fin_adds_graph … stmts src def.

(*
axiom b_fin_adds_graph_ok :
  ∀g_pars,globals,B,src,def.
  fresh_for_univ … src (joint_if_luniverse … def) →
  luniverse_ok ?? def →
  let def' ≝ b_fin_adds_graph g_pars globals B src def in
  luniverse_ok ?? def' ∧
  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
                      stmt_at … (joint_if_code … def') lbl =
                      stmt_at … (joint_if_code … def) lbl) ∧
  ∃l,r.
    bool_to_Prop (uniqueb … l) ∧
    bool_to_Prop (uniqueb … r) ∧
    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
    src ~❨B,src::l,r❩~> it in joint_if_code … def'.
*)

lemma opt_All_intro : ∀X,P,o.
(∀x.o = Some ? x → P x) → opt_All X P o. #X #P * [//] #x #H @H % qed.
 
(*
definition points_of : ∀p,g.joint_internal_function p g → Type[0] ≝
λp,g,def.Σl.bool_to_Prop (code_has_point … (joint_if_code … def) l).

unification hint 0 ≔ p, g, def;
points ≟ code_point p,
code ≟ joint_if_code p g def,
P ≟ λl : points.bool_to_Prop (code_has_point p g code l)
⊢
points_of p g def ≡ Sig points P.

definition stmt_at_safe : ∀p,g,def.points_of p g def → joint_statement p g ≝
  λp,g,def,pt.opt_safe ? (stmt_at ?? (joint_if_code ?? def) (pi1 … pt)) ?.
@hide_prf cases pt -pt #pt whd in ⊢ (?%→?); #H % #G >G in H; * qed.
*)

let rec bind_new_P' R X (P : list R → X → Prop) (m : bind_new R X) on m : Prop ≝
match m with
[ bret x ⇒ P [ ] x
| bnew f ⇒
  ∀r.bind_new_P' R X (λl.P (l @ [r])) (f r)
].

definition step_registers :  ∀p : uns_params.∀globals.
  joint_step p globals → list register ≝
λp,globals,s.get_used_registers_from_step … (functs … p) s.

definition step_forall_registers : ∀p : uns_params.∀globals.
  (register → Prop) → joint_step p globals → Prop ≝
λp,globals,P,s.All … P (step_registers … s).

definition fin_step_registers :  ∀p : uns_params.
  joint_fin_step p → list register ≝
λp,s.match s with [ TAILCALL _ _ r ⇒ f_call_args … (functs … p) r | _ ⇒ [ ] ].

definition fin_step_forall_registers : ∀p : uns_params.
  (register → Prop) → joint_fin_step p → Prop ≝
λp,P,s.All … P (fin_step_registers … s).

definition fin_step_forall_labels : ∀p : uns_params.
  (label → Prop) → joint_fin_step p → Prop ≝
λp,P,s.All … P (fin_step_labels … s).

definition step_labels_and_registers_in : ∀p : uns_params.∀globals.
  list label → list register → joint_step p globals → Prop ≝
λp,g,allowed_l,allowed_r,s.
  step_forall_labels … (In ? allowed_l) s ∧
  step_forall_registers … (In ? allowed_r) s.

definition fin_step_labels_and_registers_in : ∀p : uns_params.
  list label → list register → joint_fin_step p → Prop ≝
λp,allowed_l,allowed_r,s.
  fin_step_forall_labels … (In ? allowed_l) s ∧
  fin_step_forall_registers … (In ? allowed_r) s.

record b_graph_translate_data
  (src, dst : graph_params)
  (globals : list ident) : Type[0] ≝
{ init_ret : call_dest dst
; init_params : paramsT dst
; init_stack_size : ℕ
; added_prologue : list (joint_seq dst globals)
; new_regs : list register (* new registers added globally *)
; f_step : label → joint_step src globals → bind_step_block dst globals
; f_fin : label → joint_fin_step src → bind_fin_block dst globals
; good_f_step :
  ∀l,s.bind_new_P' ??
    (λlocal_new_regs,block.let 〈pref, op, post〉 ≝ block in
       ∀l.
       let allowed_labels ≝ l :: step_labels … s in
       let allowed_registers ≝ new_regs @ local_new_regs @ step_registers … s in
       All (label → joint_seq ??)
         (λs'.step_labels_and_registers_in … allowed_labels allowed_registers (step_seq dst globals (s' l)))
         pref ∧
       step_labels_and_registers_in … allowed_labels allowed_registers (op l) ∧
       All (joint_seq ??) (step_labels_and_registers_in … allowed_labels allowed_registers) post)
    (f_step l s)
; good_f_fin :
  ∀l,s.bind_new_P' ??
    (λlocal_new_regs,block.let 〈pref, op〉 ≝ block in
       let allowed_labels ≝ l :: fin_step_labels … s in
       let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in
       All (joint_seq ??) (λs.step_labels_and_registers_in … allowed_labels allowed_registers s) pref ∧
       fin_step_labels_and_registers_in … allowed_labels allowed_registers op)
    (f_fin l s)
; f_step_on_cost :
  ∀l,c.f_step l (COST_LABEL … c) =
    bret ? (step_block ??) 〈[ ], λ_.COST_LABEL dst globals c, [ ]〉
; cost_in_f_step :
  ∀l,s,c.
  bind_new_P ??
    (λblock.∀l'.\snd (\fst block) l' = COST_LABEL dst globals c →
       s = COST_LABEL … c) (f_step l s)
}.

definition bound_b_graph_translate_data ≝
λsrc,dst,globals.
Σd : bind_new register (b_graph_translate_data src dst globals).
bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d.

unification hint 0 ≔ src,dst,globals ⊢
bound_b_graph_translate_data src dst globals ≡
Sig (bind_new register (b_graph_translate_data src dst globals)) (λd.bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d).

definition get_first_costlabel : ∀p,g.
  joint_closed_internal_function p g → costlabel × (succ p) ≝
  λp,g,def.
  match stmt_at … (joint_if_code … def) (joint_if_entry … def)
  return λx.stmt_at ???? = x → ? with
  [ Some s ⇒
    match s return λx.stmt_at ???? = Some ? x → ? with
    [ sequential s' nxt ⇒
      match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with
      [ COST_LABEL c ⇒ λ_.〈c, nxt〉
      | _ ⇒ λabs.⊥
      ]
    | _ ⇒ λabs.⊥
    ]
  | _ ⇒ λabs.⊥
  ] (refl …).
@hide_prf
cases def in abs; -def #def #good_def
cases (entry_costed … good_def) #c * #nxt' #EQ >EQ #ABS destruct
qed.

definition partial_partition : ∀X.∀Y : DeqSet.(X → list Y) → Prop ≝
λX,Y,f.
(∀x.bool_to_Prop (uniqueb … (f x))) ∧
(∀x1,x2,y.y ∈ f x1 → y ∈ f x2 → x1 = x2).

record b_graph_translate_props 
  (src_g_pars, dst_g_pars : graph_params)
  (globals: list ident)
  (data : b_graph_translate_data src_g_pars dst_g_pars globals)
  (def_in : joint_closed_internal_function src_g_pars globals)
  (def_out : joint_closed_internal_function dst_g_pars globals)
  (f_lbls : label → list label)
  (f_regs : label → list register) : Prop ≝
{ res_def_out_eq :
           joint_if_result … def_out = init_ret … data
; pars_def_out_eq :
           joint_if_params … def_out = init_params … data
; ss_def_out_eq :
           joint_if_stacksize … def_out = init_stack_size … data
; entry_eq : joint_if_entry … def_out = joint_if_entry … def_in
; partition_lbls : partial_partition … f_lbls
; partition_regs : partial_partition … f_regs
; freshness_lbls :
  (∀l.All …
    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
           fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls l))
; freshness_regs :
  (∀l.All …
    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
           fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs l))
; freshness_data_regs :
  All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
               fresh_for_univ … reg (joint_if_runiverse … def_out)) (new_regs … data)
; data_regs_disjoint : ∀l,r.r ∈ f_regs l → r ∈ new_regs … data → False
; multi_fetch_ok :
  ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s →
  let lbls ≝ f_lbls l in let regs ≝ f_regs l in
  match s with
  [ sequential s' nxt ⇒
    let block ≝
      if eq_identifier … (joint_if_entry … def_in) l then
        append_seq_list … (f_step … data l s') (added_prologue … data)
      else
        f_step … data l s' in
    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
  | final s' ⇒
    l ~❨f_fin … data l s', l::lbls, regs❩~> it in joint_if_code … def_out
  | FCOND abs _ _ _ ⇒ Ⓧabs
  ]
}.

lemma if_merge_right : ∀A.∀b.∀x,y : A.x = y → if b then x else y = y.
#A * #x #y #EQ >EQ % qed.

lemma append_seq_list_nil : ∀p,g,b.append_seq_list p g b [ ] = b.
#p #g #b elim b -b
[ ** #a #b #c normalize >append_nil %
| #f #IH @bnew_proper #r @IH
]
qed.

definition pair_swap : ∀A,B.(A × B) → B × A ≝ λA,B,pr.〈\snd pr, \fst pr〉.

(* translation with inline fresh register allocation *)
definition b_graph_translate :
  ∀src_g_pars,dst_g_pars : graph_params.
  ∀globals: list ident.
  (* initialization info *)
  ∀data : bound_b_graph_translate_data src_g_pars dst_g_pars globals.
  (* source function *)
  ∀def_in : joint_closed_internal_function src_g_pars globals.
  (* destination function *)
  Σdef_out : joint_closed_internal_function dst_g_pars globals.
  ∃data',regs,f_lbls,f_regs.
    bind_new_instantiates ?? data' data regs ∧ (* so new_regs … data = regs *)
    b_graph_translate_props … data' def_in def_out f_lbls f_regs
   ≝
  λsrc_g_pars,dst_g_pars,globals,data,def.
  let runiv_data ≝ bcompile … (pair_swap ?? ∘ fresh RegisterTag) data (joint_if_runiverse … def) in
  let runiv ≝ \fst runiv_data in
  let data ≝ \snd runiv_data in
  let entry ≝ joint_if_entry … def in
  let init ≝
    mk_joint_internal_function dst_g_pars globals
    (joint_if_luniverse … def)
    runiv
    (init_ret … data) (init_params … data) (init_stack_size … data)
    (joint_if_local_stacksize … def)
    (add ?? (empty_map ? (joint_statement ??)) entry (RETURN …))
    entry in
  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 … (f_step … data lbl inst) lbl next def
    | final inst ⇒
      b_fin_adds_graph … (f_fin … data lbl inst) lbl def
    | FCOND abs _ _ _ ⇒ Ⓧabs
    ] in
  let def_out ≝ foldi ??? f (joint_if_code … def) init in
  let init_c_nxt ≝ get_first_costlabel … def in
  let def_out_nxt ≝ adds_graph_post … (added_prologue … data) (\snd (init_c_nxt)) def_out in
  ««add_graph … entry (sequential … (COST_LABEL … (\fst init_c_nxt)) (\snd def_out_nxt)) (\fst def_out_nxt), ?», ?».
@hide_prf
[ cases daemon
| cases daemon (* TODO *)
] qed.

definition b_graph_transform_program :
  ∀src_g_pars,dst_g_pars : graph_params.
  (* initialization *)
  (∀globals.joint_closed_internal_function src_g_pars globals →
    bound_b_graph_translate_data src_g_pars dst_g_pars globals) →
  joint_program src_g_pars →
  joint_program dst_g_pars ≝
  λsrc,dst,init,p.
  transform_program ??? p
    (λvarnames.transf_fundef ?? (λdef_in.
      b_graph_translate … (init varnames def_in) def_in)).

definition added_registers :
  ∀p : graph_params.∀g.
  joint_internal_function p g → (label → option (list register)) → list register ≝
  λp,g,def,f_regs.
  let f ≝ λlbl : label.λ_.λacc.
    match f_regs lbl with [ None ⇒ acc | Some regs ⇒ regs@acc ] in
  foldi … f (joint_if_code p g def) [ ].

axiom added_registers_ok :
  ∀p,g,def,f_regs.
  ∀l,s.stmt_at … (joint_if_code … def) l = Some ? s →
  opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l).

(*(* translation without register allocation (more or less an alias) *)
definition graph_translate :
  ∀src_g_pars,dst_g_pars : graph_params.
  ∀globals: list ident.
  (* initialization info *)
  call_dest dst_g_pars → (* joint_if_result *)
  paramsT dst_g_pars → (* joint_if_params *)
  ℕ → (* joint_if_stacksize *)
  (* functions dictating the translation *)
  (label → joint_step src_g_pars globals → step_block dst_g_pars globals) →
  (label → joint_fin_step src_g_pars → fin_block dst_g_pars globals) →
  (* 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,init1,init2,init3,trans_step,trans_fin_step.
  b_graph_translate … init1 init2 init3
    (λl,s.return trans_step l s)
    (λl,s.return trans_fin_step l s).
*)
(* 
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).
  *)