include "utilities/lists.ma".
include "common/Globalenvs.ma".
include "Cminor/Cminor_syntax.ma".
include "RTLabs/RTLabs_syntax.ma".

definition env ≝ identifier_map SymbolTag (register × typ).
definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
λen,gen. foldr ??
 (λidt,rsengen.
   let 〈id,ty〉 ≝ idt in
   let 〈rs,en,gen〉 ≝ rsengen in
   let 〈r,gen'〉 ≝ fresh … gen in
     〈〈r,ty〉::rs, add ?? en id 〈r,ty〉, gen'〉) 〈[ ], en, gen〉.

definition Env_has : env → ident → typ → Prop ≝
λe,i,t. match lookup ?? e i with [ Some x ⇒ \snd x = t | None ⇒ False ].

lemma Env_has_present : ∀e,i,t. Env_has e i t → present … e i.
#e #i #t whd in ⊢ (% → %); cases (lookup ?? e i)
[ * | * #r #t' #E % #E' destruct ]
qed.

lemma populates_env : ∀l,e,u,l',e',u'.
  distinct_env ?? l →
  populate_env e u l = 〈l',e',u'〉 →
  ∀i,t. Exists ? (λx.x = 〈i,t〉) l →
      Env_has e' i t.
#l elim l
[ #e #u #l' #e' #u' #D #E whd in E:(??%?); #i #t destruct (E) *
| * #id #ty #tl #IH #e #u #l' #e' #u' #D #E #i #t whd in E:(??%?) ⊢ (% → ?);
  * [ #E1 destruct (E1)
      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ?; * * #x #y #z
      whd in ⊢ (??%? → ?);
      lapply (refl ? (fresh ? z)) elim (fresh ? z) in ⊢ (??%? → %);
      #r #gen' #E1 #E2
      whd in E2:(??%?); destruct;
      whd >lookup_add_hit %
    | #H change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ? ])?);
      lapply (refl ? (populate_env e u tl))
      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *)
      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?);
      lapply (refl ? (fresh ? u1)) cases (fresh ? u1) in ⊢ (??%? → %); #r #u'' #E2
      whd in ⊢ (??%? → ?); #E destruct
      whd >lookup_add_miss
      [ @(IH … E1 ?? H) @(proj2 … D)
      | cases (Exists_All … H (proj1 … D)) #x * #E3 destruct #NE /2/
      ]
    ]
] qed.

lemma populates_env_distinct : ∀r,l,e,u,l',e',u'.
  distinct_env ?? (l@r) →
  populate_env e u l = 〈l',e',u'〉 →
  All ? (λit. fresh_for_map … (\fst it) e) r →
  All ? (λit. fresh_for_map … (\fst it) e') r.
#r #l elim l
[ #e #u #l' #e' #u' #D #E whd in E:(??%?); destruct (E) //
| * #id #ty #tl #IH #e #u #l' #e' #u' #D #E whd in E:(??%?) ⊢ (% → ?);
  change with (populate_env ???) in E:(??(match % with [ _ ⇒ ?])?);
  lapply (refl ? (populate_env e u tl)) cases (populate_env e u tl) in (*E*) ⊢ (???% → ?);
  * #x #y #z #E2 >E2 in E;
  whd in ⊢ (??%? → ?);
  elim (fresh ? z)
  #rg #gen' #E
  whd in E:(??%?); destruct
  #F lapply (IH … E2 F)
  [ @(proj2 … D)
  | lapply (All_append_r … (proj1 … D))
    elim r
    [ //
    | * #i #t #tl' #IH * #D1 #D2 * #H1 #H2 %
      [ @fresh_for_map_add /2/
      | @IH //
      ]
    ]
  ]
] qed.

lemma populate_extends : ∀l,e,u,l',e',u'.
  All ? (λit. fresh_for_map ?? (\fst it) e) l →
  populate_env e u l = 〈l',e',u'〉 →
  ∀i,t. Env_has e i t → Env_has e' i t.
#l elim l 
[ #e #u #l' #e' #u' #F #E whd in E:(??%?); destruct //
| * #id #t #tl #IH #e #u #l' #e' #u' #F #E whd in E:(??%?);
  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
  lapply (refl ? (populate_env e u tl))
  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
  >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E
  destruct
  #i #t #H whd >lookup_add_miss
  [ @(IH … E0) [ @(proj2 … F) | @H ]
  | @(present_not_fresh ?? e) [ whd in H ⊢ %; % #E >E in H; * | @(proj1 … F) ]
] qed.

definition lookup_reg : ∀e:env. ∀id,ty. Env_has e id ty → register ≝ λe,id,ty,H. \fst (lookup_present ?? e id ?).
/2/ qed.

lemma populate_env_list : ∀l,e,u,l',e',u'.
  populate_env e u l = 〈l',e',u'〉 →
  ∀i,r,t. ∀H:Env_has e' i t. lookup_reg e' i t H = r →
    (∃H:Env_has e i t. lookup_reg e i t H = r) ∨ env_has l' r t.
#l elim l
[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct #i #r #t #H #L %1 %{H} @L
| * #id #ty #tl #IH #e #u #l' #e' #u' #E
  whd in E:(??%?);
  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
  lapply (refl ? (populate_env e u tl))
  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
  >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E
  destruct
  #i #r #t cases (identifier_eq ? i id)
  [ #E1 >E1 #H whd in ⊢ (??%? → %); whd in match (lookup_present ?????);
    generalize in ⊢ (??(??? (?%))? → ?);
    whd in H ⊢ (% → ?); >lookup_add_hit in H ⊢ %; normalize #E2 #NE #E3 destruct
    %2 %1 %
  | #NE #H #L cases (IH … E0 i r t ??)
    [ /2/
    | #X %2 %2 @X
    | whd in H ⊢ %; >lookup_add_miss in H; //
    | whd in L:(??%?); whd in match (lookup_present ?????) in L;
      lapply L -L
      generalize in ⊢ (??(???(?%))? → ?); whd in ⊢ (% → ?);
      generalize in ⊢ (? → ? → ??(????%)?);
      >lookup_add_miss // #H0 #p 
      change with (lookup_present SymbolTag (register×typ) e0 i ?) in ⊢ (??(???%)? → ?);
      whd in ⊢ (? → ??%?); generalize in ⊢ (? → ??(???(?????%))?);
      #p' #X @X
    ]
  ]
] qed.

(* Check that the domain of one graph is included in another, for monotonicity
   properties.  Note that we don't say anything about the statements. *)
definition graph_included : graph statement → graph statement → Prop ≝
extends_domain ??.

lemma graph_inc_trans : ∀g1,g2,g3.
  graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3.
@extends_dom_trans
qed.


(* Some data structures for the transformation that remain fixed throughout. *)
record fixed : Type[0] ≝ {
  fx_gotos  : identifier_set Label;
  fx_env    : env;
  fx_rettyp : option typ
}.

definition resultok : option typ → list (register × typ) → Type[0] ≝ 
λty,env.
  match ty with [ Some t ⇒ Σr:register. env_has env r t | _ ⇒ True ].

(* We put in dummy statements for gotos, then change them afterwards once we
   know their true destinations.  So first we need a mapping between the dummy
   CFG nodes and the Cminor destination.  (We'll also keep a mapping of goto
   labels to their RTLabs statements.) *)

record goto_map (fx:fixed) (g:graph statement) : Type[0] ≝ {
  gm_map :> identifier_map LabelTag (identifier Label);
  gm_dom : ∀id. present ?? gm_map id → present ?? g id;
  gm_img : ∀id,l. lookup … gm_map id = Some ? l → present ?? (fx_gotos fx) l
}.

(* I'd use a single parametrised definition along with internal_function, but
   it's a pain without implicit parameters. *)
record partial_fn (fx:fixed) : Type[0] ≝
{ pf_labgen    : universe LabelTag
; pf_reggen    : universe RegisterTag
; pf_params    : list (register × typ)
; pf_locals    : list (register × typ)
; pf_result    : resultok (fx_rettyp … fx) (pf_locals @ pf_params)
; pf_envok     : ∀id,ty,r,H. lookup_reg (fx_env … fx) id ty H = r → env_has (pf_locals @ pf_params) r ty
; pf_stacksize : nat
; pf_graph     : graph statement
; pf_closed    : graph_closed pf_graph
; pf_gotos     : goto_map fx pf_graph
; pf_labels    : Σm:identifier_map Label (identifier LabelTag). ∀l,l'. lookup … m l = Some ? l' → present ?? pf_graph l'
; pf_typed     : graph_typed (pf_locals @ pf_params) pf_graph
; pf_entry     : Σl:label. present ?? pf_graph l
; pf_exit      : Σl:label. present ?? pf_graph l
}.

definition fn_env_has ≝
  λfx,f. env_has (pf_locals fx f @ pf_params fx f).

(* TODO: move or use another definition if there's already one *)
definition map_extends : ∀tag,A. identifier_map tag A → identifier_map tag A → Prop ≝
λtag,A,m1,m2. ∀id,a. lookup tag A m1 id = Some A a → lookup tag A m2 id = Some A a.

lemma map_extends_trans : ∀tag,A,m1,m2,m3.
  map_extends tag A m1 m2 →
  map_extends tag A m2 m3 →
  map_extends tag A m1 m3.
/3/
qed.

record fn_contains (fx:fixed) (f1:partial_fn fx) (f2:partial_fn fx) : Prop ≝
{ fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2)
; fn_con_env : ∀r,ty. fn_env_has … f1 r ty → fn_env_has … f2 r ty
; fn_con_labels : extends_domain … (pf_labels … f1) (pf_labels … f2)
}.

lemma fn_con_trans : ∀fx,f1,f2,f3.
  fn_contains fx f1 f2 → fn_contains … f2 f3 → fn_contains … f1 f3.
#fx #f1 #f2 #f3 #H1 #H2 %
[ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2))
| #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H
| @(extends_dom_trans … (fn_con_labels … H1) (fn_con_labels … H2))
] qed.

lemma fn_con_refl : ∀fx,f.
  fn_contains fx f f.
#fx #f % #l // qed.

lemma fn_con_sig : ∀fx,f,f0.
  ∀f':Σf':partial_fn fx. fn_contains … f0 f'.
  fn_contains fx f f0 →
  fn_contains fx f f'.
#fx #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1)
qed.

lemma add_statement_inv : ∀fx,l,s.∀f.
  labels_present (pf_graph fx f) s →
  graph_closed (add … (pf_graph … f) l s).
#fx #l #s #f #p
#l' #s' #H cases (identifier_eq … l l')
[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
  @(labels_P_mp … p) #l0 #H @lookup_add_oblivious @H
| #NE @(labels_P_mp … (pf_closed … f l' s' ?))
  [ #lx #H @lookup_add_oblivious @H
  | >lookup_add_miss in H; /2/
  ]
] qed.

definition statement_typed_in ≝
λfx,f,s. statement_typed (pf_locals fx f @ pf_params fx f) s.

lemma forall_nodes_add : ∀A,P,l,a,g.
  forall_nodes A P g → P a → forall_nodes A P (add ?? g l a).
#A #P #l #a #g #ALL #NEW
#l' #a'
cases (identifier_eq … l' l)
[ #E destruct >lookup_add_hit #E destruct @NEW
| #ne >lookup_add_miss /2/
] qed.

(* Add a statement to the graph, *without* updating the entry label. *)
definition fill_in_statement : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
  labels_present (pf_graph … f) s →
  statement_typed_in … f s →
  Σf':partial_fn fx. fn_contains … f f' ≝
λfx,l,s,f,p,tp.
  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ?
                (mk_goto_map … (pf_gotos … f) ??) «pf_labels … f, ?» ?
                «pf_entry … f, ?» «pf_exit … f, ?».
[ @add_statement_inv @p
| @gm_img
| #id #PR @lookup_add_oblivious @(gm_dom … PR)
| #l1 #l2 #L @lookup_add_oblivious @(pi2 … (pf_labels … f) … L)
| @forall_nodes_add //
| 6,7: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ]
| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ] 
] qed.

(* Add a statement to the graph, making it the entry label. *)
definition add_to_graph : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
  labels_present (pf_graph … f) s →
  statement_typed_in … f s →
  Σf':partial_fn fx. fn_contains … f f' ≝
λfx,l,s,f,p,tl.
  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ????
                «l, ?» «pf_exit … f, ?».
[ @add_statement_inv @p
| cases (pf_gotos … f) #m #dom #img %
  [ @m | #id #P @lookup_add_oblivious @dom @P | @img ]
| cases (pf_labels … f) #m #PR %{m} #l1 #l2 #L @lookup_add_oblivious @(PR … L)
| @forall_nodes_add //
| whd >lookup_add_hit % #E destruct
| @lookup_add_oblivious @(pi2 … (pf_exit … f))
| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
] qed.

(* Change the entry point to the function (i.e., the successor for any new
   instructions that we add). *)
definition change_entry : ∀fx. ∀f:partial_fn fx.
  ∀l. present ?? (pf_graph … f) l →
  Σf':partial_fn fx. fn_contains … f f' ≝
λfx,f,l,PR.
  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
                (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f)
                (pf_labels … f) (pf_typed … f)
                «l, PR» (pf_exit … f).
% //
qed.

(* Add a statement with a fresh label to the start of the function.  The
   statement is parametrised by the *next* instruction's label. *)
definition add_fresh_to_graph : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx.
  (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
  (∀l. statement_typed_in … f (s l)) →
  Σf':partial_fn fx. fn_contains … f f' ≝
λfx,s,f,p,tp.
  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
  let s' ≝ s (pf_entry … f) in
    (mk_partial_fn fx g (pf_reggen … f)
                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ????
                   «l, ?» «pf_exit … f, ?»).
[ 4: cases (pf_labels … f) #m #PR %{m} #l1 #l2 #L @lookup_add_oblivious @(PR … L)
| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
| @add_statement_inv @p @(pi2 … (pf_entry …))
| cases (pf_gotos … f) #m #dom #img %
  [ @m | #id #P @lookup_add_oblivious @dom @P | @img ]
| @forall_nodes_add //
| whd >lookup_add_hit % #E destruct
| @lookup_add_oblivious @(pi2 … (pf_exit …))
] qed.

lemma extend_typ_env : ∀te,r,t,r',t'.
  env_has te r t → env_has (〈r',t'〉::te) r t.
#tw #r #t #r' #t' #H %2 @H
qed.

lemma stmt_extend_typ_env : ∀te,r,t,s.
  statement_typed te s → statement_typed (〈r,t〉::te) s.
#tw #r #t *
[ 1,2: //
| #t' #r #cst #l #H %2 @H
| #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
| #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/
| 6,7: #t' #r1 #r2 #l * /3/
| #id #rs * [ 2: #dst ] #l * #RS [ * #td ] #DST % [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ | // ]
| #fnptr #rs * [ 2: #dst ] #l * * #FNPTR #RS [ * #td ] #DST % try @conj /2/ [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ ]
| #r' #l1 #l2 * #t' #E /3/
| //
] qed.

(* A little more nesting in the result type than I'd like, but it keeps the 
   function closely paired with the proof that it contains f. *)
definition fresh_reg : ∀fx. ∀f:partial_fn fx. ∀ty:typ.
  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
λfx,f,ty.
  let 〈r,g〉 ≝ fresh … (pf_reggen … f) in
  let f' ≝
    «mk_partial_fn fx
       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) ? ?
       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f) (pf_labels … f) ? (pf_entry … f) (pf_exit … f), ?»
  in
    ❬f' , ?(*«r, ?»*)❭.
[ @(«r, ?») % @refl
| #l #s #L @stmt_extend_typ_env @(pf_typed … L)
| #i #t #r1 #H #L %2 @(pf_envok … f … L)
| lapply (pf_result fx f) cases (fx_rettyp fx) // #t * #r' #H %{r'} @extend_typ_env //
| % [ #l // | #r' #ty' #H @extend_typ_env @H | // ]
] qed.

definition choose_reg : ∀fx.∀ty.∀e:expr ty. ∀f:partial_fn fx. expr_vars ty e (Env_has (fx_env fx)) →
  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
λfx,ty,e,f.
  match e return λty,e. expr_vars ty e (Env_has (fx_env fx)) → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) with
  [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg (fx_env fx) i t Env, ?»❭
  | _ ⇒ λ_.fresh_reg … f ?
  ].
[ % //
| @(pf_envok … Env) @refl
] qed.
  
let rec foldr_all (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → B → B) (b:B) (l:list A) (H:All ? P l) on l :B ≝  
 match l return λx.All ? P x → B with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) (foldr_all A B P f b l (proj2 … H))] H.
  
let rec foldr_all' (A:Type[0]) (P:A → Prop) (B:list A → Type[0]) (f:∀a:A. P a → ∀l. B l → B (a::l)) (b:B [ ]) (l:list A) (H:All ? P l) on l :B l ≝  
 match l return λx.All ? P x → B x with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) l (foldr_all' A P B f b l (proj2 … H))] H.

definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (Env_has env) ].

definition eject' : ∀A. ∀P:A → Type[0]. (𝚺a.P a) → A ≝
λA,P,x. match x with [ mk_DPair a _ ⇒ a].

definition choose_regs : ∀fx. ∀es:list (𝚺t:typ.expr t).
                         ∀f:partial_fn fx. All ? (exprtyp_present (fx_env fx)) es →
                         𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es) ≝
λfx,es,f,Env.
  foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es))
    (λe,p,tl,acc.
      match acc return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒
        match e return λe.exprtyp_present (fx_env fx) e → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp.
          match choose_reg fx t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (❬t,e❭::tl)) with [ mk_DPair f' r ⇒
            ❬«pi1 … f', ?»,«(pi1 … r)::(pi1 … rs), ?»❭
          ]
        ] p
      ]) ❬«f, ?», «[ ], I»❭ es Env.
[ @p
| cases r #r' #Hr' cases rs #rs' #Hrs'
  % [ whd in ⊢ (??%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]
| @fn_con_trans [ 3: @(pi2 … f') | skip | @(pi2 … f1) ]
| @fn_con_refl
]  qed.

lemma choose_regs_length : ∀fx,es,f,p,f',rs.
  choose_regs fx es f p = ❬f',rs❭ → |es| = length … rs.
#fx #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
qed.

lemma present_included : ∀fx,f,f',l.
  fn_contains fx f f' →
  present ?? (pf_graph … f) l →
  present ?? (pf_graph … f') l.
#fx #f #f' #l * #H1 #H2 #H3 @H1 qed.

(* Some definitions for the add_stmt function later, which we introduce now so
   that we can build the whole fn_graph_included machinery at once. *)

(* We need to show that the graph only grows, and that Cminor labels will end
   up in the graph. *)
definition Cminor_labels_added ≝ λfx,s,f'.
∀l. Exists ? (λl'.l=l') (labels_of s) → present ?? (pf_labels fx f') l.

record add_stmt_inv (fx:fixed) (s:stmt) (f:partial_fn fx) (f':partial_fn fx) : Prop ≝
{ stmt_graph_con : fn_contains … f f'
; stmt_labels_added : Cminor_labels_added … s f'
}.

(* Build some machinery to solve fn_contains goals. *)

(* A datatype saying how we intend to prove a step. *)
inductive fn_con_because (fx:fixed) : partial_fn fx → Type[0] ≝
| fn_con_eq : ∀f. fn_con_because fx f
| fn_con_sig : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
    ∀f3:(Σf3:partial_fn fx.fn_contains … f2 f3). fn_con_because fx f3
| fn_con_addinv : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
    ∀s.∀f3:(Σf3:partial_fn fx.add_stmt_inv … s f2 f3). fn_con_because fx f3
.

(* Extract the starting function for a step. *)
let rec fn_con_because_left fx f0  (b:fn_con_because ? f0) on b : partial_fn fx ≝
  match b with [ fn_con_eq f ⇒ f | fn_con_sig f _ _ _ ⇒ f | fn_con_addinv f _ _ _ _ ⇒ f ].

(* Some unification hints to pick the right step to apply.  The dummy variable
   is there to provide goal that the lemma can't apply to, which causes an error
   and forces the "repeat" tactical to stop.  The first hint recognises that we
   have reached the desired starting point. *)

unification hint 0 ≔ fx:fixed, f:partial_fn fx, dummy:True;
  f' ≟ f,
  b  ≟ fn_con_eq fx f
⊢
  fn_contains fx f f' ≡ fn_contains fx (fn_con_because_left fx f' b) f'
.

unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, f3:(Σf3:partial_fn fx. fn_contains fx f2 f3);
  b ≟ fn_con_sig fx f1 f2 H12 f3
⊢
  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
.

unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, s:stmt, f3:(Σf3:partial_fn fx. add_stmt_inv fx s f2 f3);
  b ≟ fn_con_addinv fx f1 f2 H12 s f3
⊢
  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
.

(* A lemma to perform a step of the proof.  We can repeat this to do the whole
   proof. *)  
lemma fn_contains_step : ∀fx,f. ∀b:fn_con_because fx f. fn_contains … (fn_con_because_left … f b) f.
#fx #f *
[ #f @fn_con_refl
| #f1 #f2 #H12 * #f3 #H23 @(fn_con_trans … H12 H23)
| #f1 #f2 #H12 #s * #f3 * #H23 #X @(fn_con_trans … H12 H23)
] qed.


let rec add_expr (fx:fixed) (ty:typ) (e:expr ty)
  (Env:expr_vars ty e (Env_has (fx_env fx))) (f:partial_fn fx)
  (dst:Σdst. fn_env_has … f dst ty)
  on e: Σf':partial_fn fx. fn_contains … f f' ≝
match e return λty,e.expr_vars ty e (Env_has ?) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn fx. fn_contains … f f' with
[ Id t i ⇒ λEnv,dst.
    let r ≝ lookup_reg (fx_env fx) i t Env in
    match register_eq r dst with
    [ inl _ ⇒ «f, ?»
    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
    ]
| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const ? dst c) f ??, ?»
| Op1 t t' op e' ⇒ λEnv,dst.
    let ❬f,r❭ ≝ choose_reg … e' f Env in
    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
    let f ≝ add_expr … ? e' Env f «r, ?» in
      «pi1 … f, ?»
| Op2 _ _ _ op e1 e2 ⇒ λEnv,dst.
    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
    let f ≝ add_expr … ? e2 (proj2 … Env) f «r2, ?» in
    let f ≝ add_expr … ? e1 (proj1 … Env) f «r1, ?» in
      «pi1 … f, ?»
| Mem t e' ⇒ λEnv,dst.
    let ❬f,r❭ ≝ choose_reg … e' f Env in
    let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
    let f ≝ add_expr … ? e' Env f «r,?» in
      «pi1 … f, ?»
| Cond _ _ _ e' e1 e2 ⇒ λEnv,dst.
    let resume_at ≝ pf_entry … f in
    let f ≝ add_expr … ? e2 (proj2 … Env) f dst in
    let lfalse ≝ pf_entry … f in
    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
    let f ≝ add_expr … ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
    let ❬f,r❭ ≝ choose_reg … e' f ? in
    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
    let f ≝ add_expr … ? e' (proj1 … (proj1 … Env)) f «r, ?» in
      «pi1 … f, ?»
| Ecost _ l e' ⇒ λEnv,dst.
    let f ≝ add_expr … ? e' Env f dst in
    let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
      «f, ?»
] Env dst.
(* For new labels, we need to step back through the definitions of f until we
   hit the point that it was added. *)
try (repeat @fn_contains_step @I)
try (#l #H @H)
try (#l @I)
[ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ]
| #l @(pi2 … dst)
| 3,8,10: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
| #l % [ % [ @(fn_con_env … (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I 
| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
| #l % [2: @(pi2 ?? r) | skip ]
| @(π1 (π1 Env))
| @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I
| #l #H @(fn_con_graph … (pi2 ?? resume_at)) repeat @fn_contains_step @I
] qed.

let rec add_exprs (fx:fixed) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present (fx_env fx)) es)
                  (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn fx)
                  (Hdsts:All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn fx. fn_contains … f f' ≝
match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn fx. fn_contains … f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
| cons e et ⇒ λEnv.
    match dsts return λx. All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
    [ nil ⇒ λ_.λpf.⊥
    | cons r rt ⇒ λHdsts,pf.
        let f' ≝ add_exprs … et ? rt ? f ? in
        match e return λe.exprtyp_present ? e → fn_env_has … f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr.
          let f'' ≝ add_expr … ty e ? f' r in
            «pi1 … f'', ?»
        ] (proj1 ?? Env) (π1 Hdsts)
    ]
] Env Hdsts pf.
try (repeat @fn_contains_step @I)
[ 1,2: normalize in pf; destruct
| @Env
| @(fn_con_env … Hr) repeat @fn_contains_step @I
| @(proj2 … Env)
| normalize in pf; destruct @e0
| @(π2 Hdsts)
] qed.

definition return_ok ≝
λt,s. match s with [ St_return oe ⇒ rettyp_match t oe | _ ⇒ True ].

(* Invariants about Cminor statements that we'll need *)

record stmt_inv (fx:fixed) (s:stmt) : Prop ≝ {
  si_vars : stmt_vars (Env_has (fx_env fx)) s;
  si_labels : stmt_labels (present ?? (fx_gotos fx)) s;
  si_return : return_ok (fx_rettyp fx) s
}.

definition stmts_inv : fixed → stmt → Prop ≝
λfx. stmt_P (stmt_inv fx).

(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
definition expr_is_Id : ∀t. expr t → option ident ≝
λt,e. match e with
[ Id _ id ⇒ Some ? id
| _ ⇒ None ?
].

(* XXX Work around odd disambiguation errors. *)
alias id "R_skip" = "cic:/matita/cerco/RTLabs/RTLabs_syntax/statement.con(0,1,0)".
(* If reenabling tailcalls, change 12 to 14. *)
alias id "R_return" = "cic:/matita/cerco/RTLabs/RTLabs_syntax/statement.con(0,11,0)".

lemma empty_Cminor_labels_added : ∀fx,s,f'.
  labels_of s = [ ] → Cminor_labels_added fx s f'.
#fx #s #f' #E whd >E #l *;
qed.

lemma equal_Cminor_labels_added : ∀fx,s,s',f.
  labels_of s = labels_of s' → Cminor_labels_added … s' f →
  Cminor_labels_added fx s f.
#fx #s #s' #f #E whd in ⊢ (% → %); > E #H @H
qed.

lemma Cminor_labels_con : ∀fx,s,f,f'.
  fn_contains fx f f' →
  Cminor_labels_added … s f →
  Cminor_labels_added … s f'.
#fx #s #f #f' #INC #ADDED
#l #E
@(fn_con_labels … INC l (ADDED l E))
qed.

lemma Cminor_labels_inv : ∀fx,s,s',f.
  ∀f':Σf':partial_fn fx. add_stmt_inv fx s' f f'.
  Cminor_labels_added fx s f →
  Cminor_labels_added fx s f'.
#fx #s #s' #f * #f' * #H1 #H2 #H3
@(Cminor_labels_con … H1) assumption
qed.

lemma Cminor_labels_sig : ∀fx,s,f.
  ∀f':Σf':partial_fn fx. fn_contains … f f'.
  Cminor_labels_added … s f →
  Cminor_labels_added … s f'.
#fx #s #f * #f' #H1 @(Cminor_labels_con … H1)
qed.

discriminator option.
discriminator DPair.

(* Return statements need a little careful treatment to avoid errors using the
   invariant about the return type. *)

definition add_return : ∀fx,opt_e. ∀f:partial_fn fx. ∀Env:stmts_inv fx (St_return opt_e).
  Σf':partial_fn fx. add_stmt_inv fx (St_return opt_e) f f' ≝
λfx,opt_e,f.
  let f0 ≝ f in
  let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
  match opt_e return λo. stmts_inv ? (St_return o) → Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f' with
  [ None ⇒ λEnv. «pi1 … f, ?»
  | Some et ⇒
    match et return λe.stmts_inv fx (St_return (Some ? e)) → Σf':partial_fn fx.add_stmt_inv … (St_return (Some ? e)) f0 f' with
    [ mk_DPair ty e ⇒ λEnv.
      match fx_rettyp fx return λX. rettyp_match X ? → match X with [ Some t ⇒ Σr:register. env_has ?? t | None ⇒ ? ] → ? with
      [ None ⇒ λH. ⊥
      | Some t ⇒ λH,R.
        match R with
        [ mk_Sig r Hr ⇒ 
            let f ≝ add_expr fx ty e ? f «r, ?» in
            «pi1 … f, ?»
        ]
      ] (si_return … (π1 Env)) (pf_result fx f)
    ]
  ].
[ @mk_add_stmt_inv /2 by refl, empty_Cminor_labels_added, fn_con_sig/
| inversion H #A #B #C destruct
| @mk_add_stmt_inv
  [ repeat @fn_contains_step @I
  | @empty_Cminor_labels_added //
  ]
| @(si_vars … (π1 Env))
| inversion H [ #E destruct ] #ty' #e' #E1 #E2 #_ destruct @Hr
| #l #H @I
| #l //
] qed.

(* Record the mapping for a Cminor goto label so that we can put it in the skips
   for the goto statements later. *)

definition record_goto_label : ∀fx. partial_fn fx → identifier Label → partial_fn fx ≝
λfx,f,l. mk_partial_fn fx
  (pf_labgen … f) (pf_reggen … f) (pf_params … f) (pf_locals … f)
  (pf_result … f) (pf_envok … f) (pf_stacksize … f) (pf_graph … f)
  (pf_closed … f) (pf_gotos …  f) «add … (pf_labels … f) l (pf_entry … f), ?»
  (pf_typed … f) (pf_entry … f) (pf_exit … f).
#l1 #l2 cases (identifier_eq … l2 (pf_entry … f))
[ #E destruct #L @(pi2 … (pf_entry … f))
| #NE cases (identifier_eq … l l1)
  [ #E destruct >lookup_add_hit #E destruct /2/
  | #NE' >lookup_add_miss [ @(pi2 … (pf_labels … f)) | /2/ ]
  ]
] qed.

(* Add a dummy statement for each goto so that we can put the real destination
   in at the end once we've recorded them all. *)

definition add_goto_dummy : ∀fx. ∀f:partial_fn fx. ∀l. present … (fx_gotos fx) l → Σf':partial_fn fx. fn_contains … f f' ≝
λfx,f,dest,PR.
  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
    (mk_partial_fn fx g (pf_reggen … f)
                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
                   (pf_stacksize … f) (add ?? (pf_graph … f) l St_return) ?
                   (mk_goto_map … (add … (pf_gotos … f) l dest) ??)
                   «pf_labels … f, ?» ?
                   «l, ?» «pf_exit … f, ?»).
[ % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
| @add_statement_inv @I
| #l1 #l2 cases (identifier_eq … l1 l)
  [ #E destruct >lookup_add_hit #E destruct @PR
  | #NE >lookup_add_miss [ @(gm_img … (pf_gotos … f)) | // ]
  ]
| #id cases (identifier_eq … id l)
  [ #E destruct //
  | #NE whd in ⊢ (% → %); >lookup_add_miss [ >lookup_add_miss [ @(gm_dom … (pf_gotos … f)) | // ] | // ]
  ]
| cases (pf_labels … f) #m #PR #l1 #l2 #L @lookup_add_oblivious @(PR … L)
| @forall_nodes_add //
| whd >lookup_add_hit % #E destruct
| @lookup_add_oblivious @(pi2 … (pf_exit …))
] qed.

(* It's important for correctness that recursive calls to add_stmt happen in
   reverse order.  This is because Cminor and Clight programs allow goto labels
   to occur multiple times, but only use the first one to appear in the
   function.  It would be nice to rule these programs out entirely, but that
   means establishing and maintaining another invariant on Cminor programs,
   which I'd like to avoid. *)

let rec add_stmt (fx:fixed) (s:stmt) (Env:stmts_inv fx s) (f:partial_fn fx) on s : Σf':partial_fn fx. add_stmt_inv fx s f f' ≝
match s return λs.stmts_inv fx s → Σf':partial_fn fx. add_stmt_inv … s f f' with
[ St_skip ⇒ λ_. «f, ?»
| St_assign t x e ⇒ λEnv.
    let dst ≝ lookup_reg (fx_env fx) x t (π1 (si_vars … (π1 Env))) in
    «pi1 … (add_expr … e (π2 (si_vars … (π1 Env))) f dst), ?»
| St_store t e1 e2 ⇒ λEnv.
    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (si_vars … (π1 Env))) in
    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (si_vars … (π1 Env))) in
    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
    let f ≝ add_expr … e1 (π1 (si_vars … (π1 Env))) f «addr_reg, ?» in
    «pi1 … (add_expr … ? e2 (π2 (si_vars … (π1 Env))) f «val_reg, ?»), ?»
| St_call return_opt_id e args ⇒ λEnv.
    let return_opt_reg ≝
      match return_opt_id return λo. ? → ? with
      [ None ⇒ λ_. None ?
      | Some idty ⇒ λEnv. Some ? (lookup_reg (fx_env fx) (\fst idty) (\snd idty) ?)
      ] Env in
    let ❬f, args_regs❭ ≝ choose_regs ? args f (π2 (si_vars ?? (π1 Env))) in
    let f ≝
      match expr_is_Id ? e with
      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
      | None ⇒ 
        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (si_vars … (π1 Env)))) in
        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
        «pi1 … (add_expr … ? e (π2 (π1 (si_vars … (π1 Env)))) f «fnr, ?»), ?»
      ] in
    «pi1 … (add_exprs … args (π2 (si_vars … (π1 Env))) args_regs ? f ?), ?»
| St_seq s1 s2 ⇒ λEnv.
    let f2 ≝ add_stmt … s2 ? f in
    let f1 ≝ add_stmt … s1 ? f2 in
      «pi1 … f1, ?»
| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
    let l_next ≝ pf_entry … f in
    let f2 ≝ add_stmt … s2 (π2 (π2 Env)) f in
    let l2 ≝ pf_entry … f2 in
    let f ≝ change_entry … f2 l_next ? in
    let f1 ≝ add_stmt … s1 (π1 (π2 Env)) f in
    let ❬f,r❭ ≝ choose_reg … e f1 (si_vars … (π1 Env)) in
    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
    «pi1 … (add_expr … ? e (si_vars … (π1 Env)) f «r, ?»), ?»
| St_return opt_e ⇒ λEnv. add_return fx opt_e f Env
| St_label l s' ⇒ λEnv.
    let f ≝ add_stmt … s' (π2 Env) f in
    «record_goto_label … f l, ?»
| St_goto l ⇒ λEnv.
    «add_goto_dummy … f l ?, ?»
| St_cost l s' ⇒ λEnv.
    let f ≝ add_stmt … s' (π2 Env) f in
    «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
] Env.
try @(π2 Env)
try @(π1 (π2 Env))
try @(π2 (π2 Env))
try @mk_add_stmt_inv
try (repeat @fn_contains_step @I)
try (@empty_Cminor_labels_added @refl)
try (#l #H @I)
try (#l #H @H)
try (#l @I)
[ @(pf_envok … (π1 (si_vars … (π1 Env)))) @refl
| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
| #l % [ @(fn_con_env … (pi2 ?? val_reg)) | @(pi2 ?? addr_reg) ] repeat @fn_contains_step @I
| @sym_eq @(All2_length … (pi2 ?? args_regs))
| @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
| @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
| #l % try @conj
  [ @(pi2 ?? fnr)
  | @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I
  | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %;
    [ #Env @I
    | * #retid #retty * #Env #moo %{retty} /2/
    ]
  ]
| #l %
  [ @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I
  | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %;
    [ #Env @I
    | * #retid #retty * #Env #moo %{retty} /2/
    ]
  ]
| @(π1 (π1 (si_vars … (π1 Env))))
| #l #H cases (Exists_append … H)
  [ #H1 @(stmt_labels_added ???? (pi2 ?? f1) ? H1)
  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (pi2 ?? f2))
  ]
| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
| #l #H cases (Exists_append … H)
  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f1)) 
  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f2)) 
  ]
| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
| #l whd % [2: @(pi2 ?? r) | skip ] 
| @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
| cases (pi2 … f) * #INC #ENV #LBLE #LBLA %
  [ @INC | @ENV | @(extends_dom_trans … LBLE) #l1 #PR whd in ⊢ (???%?); @lookup_add_oblivious @PR ]
| #l1 * [ #E >E //
        | @(Cminor_labels_con … (stmt_labels_added ???? (pi2 … f)))
          % [ // | // | #x #PR @lookup_add_oblivious @PR ]
        ]
| @(si_labels … (π1 Env))
| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) ]
] qed.



definition patch_gotos : ∀fx. ∀f:partial_fn fx.
 (∀l,l'. lookup ?? (pf_gotos … f) l = Some ? l' → present ?? (pf_labels … f) l') →
 Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l ≝
λfx,f,PR.
fold_inf ? (Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l) ? (pf_gotos … f)
  (λl,l',H,f'. «fill_in_statement fx l (St_skip (lookup_present ?? (pf_labels … f') l' ?)) f' ??, ?»)
  «f, λx,H.H».
[ #l #PR' @(pi2 … f') @PR'
| @(pi2 … f') @(PR … H)
| @(pi2 … (pf_labels … f')) [ @l' | @lookup_lookup_present ]
| %
] qed.

definition c2ra_function (*: internal_function → internal_function*) ≝
λf.
let labgen0 ≝ new_universe LabelTag in
let reggen0 ≝ new_universe RegisterTag in
let cminor_labels ≝ labels_of (f_body f) in
let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
let ❬locals_reggen, result❭ as E3 ≝
  match f_return f return λt.𝚺lr. resultok t ((\fst lr)@params) with
  [ None ⇒ ❬〈locals0, reggen2〉, I❭
  | Some ty ⇒
      let 〈r,gen〉 ≝ fresh … reggen2 in
        mk_DPair ? (λlr.Σr. env_has ((\fst lr)@params) r ty) 〈〈r,ty〉::locals0, gen〉 «r, ?» ] in
let locals ≝ \fst locals_reggen in
let reggen ≝ \snd locals_reggen in
let 〈l,labgen〉 ≝ fresh … labgen0 in
let fixed ≝ mk_fixed (set_of_list … (labels_of (f_body f))) env (f_return f) in
let emptyfn ≝
  mk_partial_fn fixed
    labgen
    reggen
    params
    locals
    result
    ?
    (f_stacksize f)
    (add ?? (empty_map …) l St_return)
    ?
    (mk_goto_map ?? (empty_map …) ??)
    «empty_map …, ?»
    ?
    l
    l in
let f ≝ add_stmt fixed (f_body f) ? emptyfn in
let f ≝ patch_gotos … f ? in
  mk_internal_function
    (pf_labgen … f)
    (pf_reggen … f)
    (match fx_rettyp fixed return λt. match t with [ Some t ⇒ Σr:register. env_has ? r t | _ ⇒ True ] → ? with [ None ⇒ λ_. None ? | Some t ⇒ λR. Some ? 〈(pi1 … R),t〉 ] (pf_result … f))
    (pf_params … f)
    (pf_locals … f)
    (pf_stacksize … f)
    (pf_graph … f)
    (pf_closed … f)
    (pf_typed … f)
    (pf_entry … f)
    (pf_exit … f)
  .
[ #l1 #l2 #L
  lapply (gm_img … (pf_gotos … f) … L)
  whd in match fixed;
  #PR
  lapply (in_set_of_list' … PR)
  @(stmt_labels_added … (pi2 … f))
| -emptyfn @(stmt_P_mp … (f_inv f))
  #s * #V #L #R %
  [ @(stmt_vars_mp … V)
    #i #t #H cases (Exists_append … H)
    [ #H1 @(populate_extends … (sym_eq … E2))
      [ @(populates_env_distinct … (sym_eq … E1)) //
        @All_alt //
      | @(populates_env … (sym_eq … E1)) [ @distinct_env_append_l // | @H1 ]
      ]
    | #H1 @(populates_env … (sym_eq … E2)) /2/ @H1
    ]
  | @(stmt_labels_mp … L)
    #l #H whd in match fixed; @in_set_of_list assumption
  | cases s in R ⊢ %; //
  ]
| #id #ty #r #H #L cases (populate_env_list … (sym_eq … E2) … H L)
  [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1)
    [ * * | normalize @Exists_append_r ]
  | (* gave up with     cases (f_return f) in result E3; *)
    @(match f_return f return λx.∀R:resultok x ((\fst locals_reggen)@params). ❬locals_reggen,R❭ = match x with [None ⇒ ?|Some _ ⇒ ?] → ? with [ None ⇒ λres1.? | Some rty ⇒ λres1.?] result E3)
    [ whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
      @Exists_append_l
    | cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
      #H' @Exists_append_l %2 @H'
    ]
  ]
| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
  [ * #E1 #E2 >E2 @I
  | whd in ⊢ (??%? → ?); #E' destruct (E')
  ]
| #id #l #E normalize in E; destruct
| #id normalize * #H cases (H (refl ??))
| #l #l' normalize #E destruct
| #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
  [ * #E1 #E2 >E2 @I
  | whd in ⊢ (??%? → ?); #E' destruct (E')
  ]
| 9,10: whd >lookup_add_hit % #E destruct
| % @refl
]
qed.

definition cminor_noinit_to_rtlabs : Cminor_noinit_program → RTLabs_program ≝
λp.transform_program … p (λ_. transf_fundef … c2ra_function).

include "Cminor/initialisation.ma".

definition cminor_to_rtlabs : costlabel → Cminor_program → RTLabs_program ≝
λinit_cost,p. let p' ≝ replace_init init_cost p in cminor_noinit_to_rtlabs p'.