include "utilities/lists.ma".
include "common/Globalenvs.ma".
include "Cminor/syntax.ma".
include "RTLabs/syntax.ma".

definition env ≝ identifier_map SymbolTag (register × typ).
definition label_env ≝ identifier_map Label label.
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.

definition  populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝
λen,gen. foldr ??
 (λid,engen.
   let 〈en,gen〉 ≝ engen in
   let 〈r,gen'〉 ≝ fresh … gen in
     〈add ?? en id r, gen'〉) 〈en, gen〉.

lemma populates_label_env : ∀ls,lbls,u,lbls',u'.
  populate_label_env lbls u ls = 〈lbls',u'〉 →
  ∀l. Exists ? (λl'.l' = l) ls → present ?? lbls' l.
#ls elim ls
[ #lbls #u #lbls' #u' #E #l *
| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
  lapply (refl ? (populate_label_env lbls u t))
  cases (populate_label_env lbls u t) in ⊢ (???% → %);
  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
  cases (fresh LabelTag u1) #lf #uf whd in ⊢ (??%? → ?);
  #E destruct
  #l *
  [ #El <El whd >lookup_add_hit % #Er destruct
  | #H @lookup_add_oblivious @(IH … E1 ? H)
  ]
] qed.

lemma label_env_contents : ∀ls,lbls,u,lbls',u'.
  populate_label_env lbls u ls = 〈lbls',u'〉 →
  ∀l. present ?? lbls' l → Exists ? (λl'.l = l') ls ∨ present ?? lbls l.
#ls elim ls
[ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
  lapply (refl ? (populate_label_env lbls u t))
  cases (populate_label_env lbls u t) in ⊢ (???% → %);
  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
  cases (fresh ? u1) #fi #fu whd in ⊢ (??%? → ?);
  #E destruct
  #l #H cases (identifier_eq ? l h)
  [ #El %1 %1 @El 
  | #NE cases (IH … E1 l ?)
    [ #H' %1 %2 @H' | #H' %2 @H' | whd in H; >lookup_add_miss in H; //  ]
  ]
] qed.

definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.

(* 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 ≝
λg1,g2. ∀l. present ?? g1 l → present ?? g2 l.

lemma graph_inc_trans : ∀g1,g2,g3.
  graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3.
#g1 #g2 #g3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed.

definition lpresent ≝ λlbls:label_env. λl. ∃l'. lookup ?? lbls l' = Some ? l.

definition partially_closed : label_env → graph statement → Prop ≝ 
 λe,g. forall_nodes ? (labels_P (λl. present ?? g l ∨ lpresent e l)) g.

(* Some data structures for the transformation that remain fixed throughout. *)
record fixed : Type[0] ≝ {
  fx_lenv   : label_env;
  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 ].

(* 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    : partially_closed (fx_lenv … fx) pf_graph
; 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).

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
}.

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
] 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 →
  partially_closed (fx_lenv … fx) (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 %1 @lookup_add_oblivious @H
| #NE @(labels_P_mp … (pf_closed … f l' s' ?))
  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @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) ? ?
                «pf_entry … f, ?» «pf_exit … f, ?».
[ @add_statement_inv @p
| @forall_nodes_add //
| 3,4: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ]
| % [ #l' @lookup_add_oblivious | // ] 
] 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
| @forall_nodes_add //
| whd >lookup_add_hit % #E destruct
| @lookup_add_oblivious @(pi2 … (pf_exit … f))
| % [ #l' @lookup_add_oblivious | // ]
] 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, ?»).
[ % [ #l' @lookup_add_oblivious | // ]
| @add_statement_inv @p @(pi2 … (pf_entry …))
| @forall_nodes_add //
| whd >lookup_add_hit % #E destruct
| @lookup_add_oblivious @(pi2 … (pf_exit …))
] qed.

(* Variants for labels which are (goto) labels *)

lemma add_statement_inv' : ∀fx,l,s.∀f.
  labels_P (λl. present ?? (pf_graph fx f) l ∨ lpresent (fx_lenv … fx) l) s →
  partially_closed (fx_lenv … fx) (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 %1 @lookup_add_oblivious @H | #H %2 @H ]
| #NE @(labels_P_mp … (pf_closed … f l' s' ?))
  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
  | >lookup_add_miss in H; /2/
  ]
] qed.

definition add_fresh_to_graph' : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx. 
  (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent (fx_lenv … fx) l) (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, ?»).
[ % [ #l' @lookup_add_oblivious | // ]
| @add_statement_inv' @p @(pi2 … (pf_entry …))
| @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 *
[ 3: #t' #r #cst #l #H %2 @H
| 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
| 5: #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /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_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 extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 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 @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) →
∃l'. lookup ?? (fx_lenv fx) l = Some ? l' ∧ present ?? (pf_graph 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,9: @(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 #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
| @(π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 ].

record stmt_inv (fx:fixed) (s:stmt) : Prop ≝ {
  si_vars : stmt_vars (Env_has (fx_env fx)) s;
  si_labels : stmt_labels (present ?? (fx_lenv 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/syntax/statement.con(0,1,0)".
(* If reenabling tailcalls, change 12 to 14. *)
alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,12,0)".

lemma lookup_label_rev : ∀lenv,l,l',p.
  lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
#lenv #l #l' #p
cut (∃lx. lookup ?? lenv l = Some ? lx)
[ whd in p; cases (lookup ?? lenv l) in p ⊢ %;
  [ * #H cases (H (refl ??))
  | #lx #_ %{lx} @refl
  ]
| * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl
] qed.

lemma lookup_label_rev' : ∀lenv,l,p.
  lookup ?? lenv l = Some ? (lookup_label lenv l p).
#lenv #l #p @lookup_label_rev [ @p | @refl ]
qed.

lemma lookup_label_lpresent : ∀lenv,l,p.
  lpresent lenv (lookup_label lenv l p).
#le #l #p whd %{l} @lookup_label_rev'
qed.

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 cases (ADDED l E) #l' * #L #P
%{l'} % [ @L | @(present_included … P) @INC ]
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
#l #E cases (H3 l E) #l' * #L #P
%{l'} % [ @L | @(present_included … P) @H1 ]
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 #H2
#l #E cases (H2 l E) #l' * #L #P
%{l'} % [ @L | @(present_included … P) @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/
| 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.


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 ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? 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
    let l' ≝ lookup_label (fx_lenv fx) l ? in
    «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
| St_goto l ⇒ λEnv.
    let l' ≝ lookup_label (fx_lenv fx) l ? in
    «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
| 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
| @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
| @(π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 #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
| @(pi2 … (pf_entry …))
| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
        | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f))
        ]
| @(si_labels … (π1 Env))
| #l1 #H whd %2 @lookup_label_lpresent
| @(si_labels … (π1 Env))
| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) ]
] 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 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
let 〈l,labgen〉 ≝ fresh … labgen1 in
let fixed ≝ mk_fixed label_env 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)
    ?
    ?
    l
    l in
let f ≝ add_stmt fixed (f_body f) ? emptyfn 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_typed … f)
    (pf_entry … f)
    (pf_exit … f)
  .
[ #l #s #E @(labels_P_mp … (pf_closed … f l s E))
  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ] 
  #P' @P'
  | cases (label_env_contents … (sym_eq ??? El) l ?)
    [ #H @H
    | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??))
    | whd >H % #E' destruct (E')
    ]
  ]
  ]
| -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 @(populates_label_env … (sym_eq … El)) @H
  | 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')
  ]
| #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
  [ * #E1 #E2 >E2 @I
  | whd in ⊢ (??%? → ?); #E' destruct (E')
  ]
| 6,7: 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 : Cminor_program → RTLabs_program ≝
λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.