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.

(* I'd use a single parametrised definition along with internal_function, but
   it's a pain without implicit parameters. *)
record partial_fn (lenv:label_env) (env:env) : Type[0] ≝
{ pf_labgen    : universe LabelTag
; pf_reggen    : universe RegisterTag
; pf_params    : list (register × typ)
; pf_locals    : list (register × typ)
; pf_result    : option (Σrt:register × typ. env_has (pf_locals @ pf_params) (\fst rt) (\snd rt))
; pf_envok     : ∀id,ty,r,H. lookup_reg env id ty H = r → env_has (pf_locals @ pf_params) r ty
; pf_stacksize : nat
; pf_graph     : graph statement
; pf_closed    : partially_closed lenv 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 ≝
  λle,env,f. env_has (pf_locals le env f @ pf_params le env f).

record fn_contains (le:label_env) (env:env) (f1:partial_fn le env) (f2:partial_fn le env) : Prop ≝
{ fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2)
; fn_con_env : ∀r,ty. fn_env_has le env f1 r ty → fn_env_has le env f2 r ty
}.

lemma fn_con_trans : ∀le,env,f1,f2,f3.
  fn_contains le env f1 f2 → fn_contains le env f2 f3 → fn_contains le env f1 f3.
#le #env #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 : ∀label_env,env,f.
  fn_contains label_env env f f.
#le #env #f % #l // qed.

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

lemma add_statement_inv : ∀le,env,l,s.∀f.
  labels_present (pf_graph le env f) s →
  partially_closed le (add … (pf_graph … f) l s).
#le #env #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 ≝
λle,env,f,s. statement_typed (pf_locals le env f @ pf_params le env 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 : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
  labels_present (pf_graph … f) s →
  statement_typed_in le env f s →
  Σf':partial_fn le env. fn_contains … f f' ≝
λle,env,l,s,f,p,tp.
  mk_partial_fn le env (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 : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
  labels_present (pf_graph … f) s →
  statement_typed_in … f s →
  Σf':partial_fn le env. fn_contains … f f' ≝
λle,env,l,s,f,p,tl.
  mk_partial_fn le env (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 : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env.
  (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
  (∀l. statement_typed_in … f (s l)) →
  Σf':partial_fn le env. fn_contains … f f' ≝
λle,env,s,f,p,tp.
  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
  let s' ≝ s (pf_entry … f) in
    (mk_partial_fn le env 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' : ∀le,env,l,s.∀f.
  labels_P (λl. present ?? (pf_graph le env f) l ∨ lpresent le l) s →
  partially_closed le (add … (pf_graph … f) l s).
#le #env #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' : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env. 
  (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent le l) (s l)) →
  (∀l. statement_typed_in … f (s l)) →
  Σf':partial_fn le env. fn_contains … f f' ≝
λle,env,s,f,p,tp.
  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
  let s' ≝ s (pf_entry … f) in
    (mk_partial_fn le env 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 : ∀le,env. ∀f:partial_fn le env. ∀ty:typ.
  𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
λle,env,f,ty.
  let 〈r,g〉 ≝ fresh … (pf_reggen … f) in
  let f' ≝
    «mk_partial_fn le env
       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f))
       (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? «pi1 … rt, ?»]) ?
       (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)
| %2 @(pi2 … rt)
| % [ #l // | #r' #ty' #H @extend_typ_env @H ]
] qed.

axiom UnknownVariable : String.

definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le env. expr_vars ty e (Env_has env) →
  𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
λle,env,ty,e,f.
  match e return λty,e. expr_vars ty e (Env_has env) → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) with
  [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg env i t Env, ?»❭
  | _ ⇒ λ_.fresh_reg le env 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 : ∀le. ∀env:env. ∀es:list (𝚺t:typ.expr t).
                         ∀f:partial_fn le env. All ? (exprtyp_present env) es →
                         𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs es) ≝
λle,env,es,f,Env.
  foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs es))
    (λe,p,tl,acc.
      match acc return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒
        match e return λe.exprtyp_present env e → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp.
          match choose_reg le env t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env 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 : ∀le,env,es,f,p,f',rs.
  choose_regs le env es f p = ❬f',rs❭ → |es| = length … rs.
#le #env #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
qed.

lemma present_included : ∀le,env,f,f',l.
  fn_contains le env f f' →
  present ?? (pf_graph … f) l →
  present ?? (pf_graph … f') l.
#le #env #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 ≝ λle,env,s,f'.
∀l. Exists ? (λl'.l=l') (labels_of s) →
∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le env f') l'.

record add_stmt_inv (le:label_env) (env:env) (s:stmt) (f:partial_fn le env) (f':partial_fn le env) : 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 (le:label_env) (env:env) : partial_fn le env → Type[0] ≝
| fn_con_eq : ∀f. fn_con_because le env f
| fn_con_sig : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
    ∀f3:(Σf3:partial_fn le env.fn_contains … f2 f3). fn_con_because le env f3
| fn_con_addinv : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
    ∀s.∀f3:(Σf3:partial_fn le env.add_stmt_inv … s f2 f3). fn_con_because le env f3
.

(* Extract the starting function for a step. *)
let rec fn_con_because_left le env f0  (b:fn_con_because ?? f0) on b : partial_fn le env ≝
  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 ≔ le:label_env, env:env, f:partial_fn le env, dummy:True;
  f' ≟ f,
  b  ≟ fn_con_eq le env f
⊢
  fn_contains le env f f' ≡ fn_contains le env (fn_con_because_left le env f' b) f'
.

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

unification hint 1 ≔ le:label_env, env:env, f1:partial_fn le env, f2:partial_fn le env, H12 : fn_contains le env f1 f2, s:stmt, f3:(Σf3:partial_fn le env. add_stmt_inv le env s f2 f3);
  b ≟ fn_con_addinv le env f1 f2 H12 s f3
⊢
  fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env 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 : ∀le,env,f. ∀b:fn_con_because le env f. fn_contains … (fn_con_because_left … f b) f.
#le #env #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.

axiom BadCminorProgram : String.

let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty)
  (Env:expr_vars ty e (Env_has env)) (f:partial_fn le env)
  (dst:Σdst. fn_env_has … f dst ty)
  on e: Σf':partial_fn le env. fn_contains … f f' ≝
match e return λty,e.expr_vars ty e (Env_has env) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn le env. fn_contains … f f' with
[ Id t i ⇒ λEnv,dst.
    let r ≝ lookup_reg env 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 … env ? 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 … env ? e2 (proj2 … Env) f «r2, ?» in
    let f ≝ add_expr … env ? 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 … env ? e' Env f «r,?» in
      «pi1 … f, ?»
| Cond _ _ _ e' e1 e2 ⇒ λEnv,dst.
    let resume_at ≝ pf_entry … f in
    let f ≝ add_expr … env ? 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 … env ? 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 … env ? e' (proj1 … (proj1 … Env)) f «r, ?» in
      «pi1 … f, ?»
| Ecost _ l e' ⇒ λEnv,dst.
    let f ≝ add_expr … env ? 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 (le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es)
                  (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn le env)
                  (Hdsts:All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn le env. fn_contains le env f f' ≝
match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn le env. fn_contains le env f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
| cons e et ⇒ λEnv.
    match dsts return λx. All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
    [ nil ⇒ λ_.λpf.⊥
    | cons r rt ⇒ λHdsts,pf.
        let f' ≝ add_exprs ? env et ? rt ? f ? in
        match e return λe.exprtyp_present ? e → fn_env_has le env f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr.
          let f'' ≝ add_expr ? env 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.

axiom UnknownLabel : String.
axiom ReturnMismatch : String.

definition stmt_inv : env → label_env → stmt → Prop ≝
λenv,lenv. stmt_P (λs. stmt_vars (Env_has env) s ∧ stmt_labels (present ?? lenv) s).

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

definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝
λA,P,m,l,n.
  match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with
  [ None ⇒ λ_. Error ? m
  | Some a ⇒ λH'. OK ? «a, ?»
  ] (All_nth A P n l (pi2 … l)).
@H' @refl qed.

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 : ∀le,env,s,f'.
  labels_of s = [ ] → Cminor_labels_added le env s f'.
#le #env #s #f' #E whd >E #l *;
qed.

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

lemma Cminor_labels_con : ∀le,env,s,f,f'.
  fn_contains le env f f' →
  Cminor_labels_added … s f →
  Cminor_labels_added … s f'.
#le #env #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 : ∀le,env,s,s',f.
  ∀f':Σf':partial_fn le env. add_stmt_inv le env s' f f'.
  Cminor_labels_added le env s f →
  Cminor_labels_added le env s f'.
#le #env #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 : ∀le,env,s,f.
  ∀f':Σf':partial_fn le env. fn_contains … f f'.
  Cminor_labels_added … s f →
  Cminor_labels_added … s f'.
#le #env #s #f * #f' #H1 #H2
#l #E cases (H2 l E) #l' * #L #P
%{l'} % [ @L | @(present_included … P) @H1 ]
qed.

let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) (exits:Σls:list label. All ? (present ?? (pf_graph … f)) ls) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝
match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with
[ St_skip ⇒ λ_. OK ? «f, ?»
| St_assign t x e ⇒ λEnv.
    let dst ≝ lookup_reg env x t (π1 (π1 Env)) in
    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
| St_store t e1 e2 ⇒ λEnv.
    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in
    OK ? «pi1 … (add_expr ? env ? e2 (π2 (π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 env (\fst idty) (\snd idty) ?)
      ] Env in
    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π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 (π1 Env))) in
        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
        «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) f «fnr, ?»), ?»
      ] in
    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
(*
| St_tailcall e args ⇒ λEnv.
    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
    let f ≝
      match expr_is_Id ? e with
      [ Some id ⇒ add_fresh_to_graph … (λ_. St_tailcall_id id args_regs) f ??
      | None ⇒ 
        let ❬f,fnr❭ ≝ choose_reg … e f (π1 (π1 Env)) in
        let f ≝ add_fresh_to_graph … (λ_. St_tailcall_ptr fnr args_regs) f ?? in
        «pi1 … (add_expr ? env ? e (π1 (π1 Env)) f «fnr, ?»), ?»
      ] in
    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
*)
| St_seq s1 s2 ⇒ λEnv.
    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
    do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»;
      OK ? «pi1 … f1, ?»
| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
    let l_next ≝ pf_entry … f in
    do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;
    let l2 ≝ pf_entry … f2 in
    let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;
    let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in
    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
    OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?»
| St_loop s ⇒ λEnv.
    let f ≝ add_fresh_to_graph … R_skip f ?? in (* dummy statement, fill in afterwards *)
    let l_loop ≝ pf_entry … f in
    do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
    OK ? «pi1 … (fill_in_statement … l_loop (R_skip (pf_entry … f)) f ??), ?»
| St_block s ⇒ λEnv.
    do f ← add_stmt env label_env s (π2 Env) f («pf_entry … f::exits, ?»);
    OK ? «pi1 … f, ?»
| St_exit n ⇒ λEnv.
    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
    OK ? «pi1 … (add_fresh_to_graph … (λ_. R_skip l) f ??), ?»
| St_switch sz sg e tab n ⇒ λEnv.
    let ❬f,r❭ ≝ choose_reg … e f ? in
    do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;
    let f ≝ add_fresh_to_graph … (λ_. R_skip l_default) f ?? in
    do f ← foldr ? (res (Σf':partial_fn ??. ?)) (λcs,f.
      do f ← f;
      let 〈i,n〉 ≝ cs in
      let ❬f,cr❭ ≝ fresh_reg … f (ASTint sz sg) in
      let ❬f,br❭ ≝ fresh_reg … f (ASTint I8 Unsigned) in
      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
      let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in
      let f ≝ add_fresh_to_graph … (St_op2 … (Ocmp sz sg Unsigned Ceq) br r cr) f ?? in
      let f ≝ add_fresh_to_graph … (St_const ? cr (Ointconst sz sg i)) f ?? in
        OK ? «pi1 … f, ?») (OK ? f) tab;
    OK ? «pi1 … (add_expr ? env ? e (π1 Env) f «r, ?»), ?»
| St_return opt_e ⇒ let f0 ≝ f in
    let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
    match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return o) f0 f') with
    [ None ⇒ λEnv. OK ? «pi1 … f, ?»
    | Some e ⇒ 
        match pf_result … f with
        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
        | Some r ⇒ 
            match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return (Some ? e)) f0 f') with
            [ mk_DPair ty e ⇒ λEnv.
                match typ_eq (\snd r) ty with
                [ inl E ⇒ let f ≝ add_expr label_env env ty e ? f «\fst r, ? E (* XXX E goes missing if I don't use it! *)» in
                          OK ? «pi1 … f, ?»
                | inr _ ⇒ Error ? (msg ReturnMismatch)
                ]
            ]
        ]
    ]
| St_label l s' ⇒ λEnv.
    do f ← add_stmt env label_env s' (π2 Env) f exits;
    let l' ≝ lookup_label label_env l ? in
    OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
| St_goto l ⇒ λEnv.
    let l' ≝ lookup_label label_env l ? in
    OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
| St_cost l s' ⇒ λEnv.
    do f ← add_stmt env label_env s' (π2 Env) f exits;
    OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
] Env.
try @(π1 Env)
try @(π2 Env)
try @(π1 (π1 Env))
try @(π2 (π1 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 (π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
| (*4,8:*) @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
| (*5,9:*) @sym_eq @(All2_length … (pi2 ?? args_regs))
| (*6,10:*) @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
| @(π1 (π1 (π1 Env)))
| 8,10,11,16,17: (*11,13,14,19,20:*) (@(All_mp … (pi2 ?? exits))) #i #H @(fn_con_graph … H) repeat @fn_contains_step @I
| #l #H cases (Exists_append … H)
  [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1)
  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ????? (pi2 ?? f2))
  ]
| #l #H @(fn_con_graph … (pi2 ?? l_next)) 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)) 
  ]
| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
| @(pi2 … (pf_entry …))
| @Cminor_labels_sig @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
| % [ @pi2 | @(pi2 ?? exits) ]
| @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
| #l' #H @(pi2 … l)
| #l #H @(fn_con_graph … (pi2 ?? l_default)) repeat @fn_contains_step @I
| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
| #l #H % [ @(fn_con_graph … (pi2 ?? l_case)) repeat @fn_contains_step @I | @H ]
| #l % [ % [ @(fn_con_env … (pi2 ?? r)) | @(fn_con_env … (pi2 ?? cr)) ] | @(fn_con_env … (pi2 ?? br)) ] repeat @fn_contains_step @I
| #l @(fn_con_env … (pi2 ?? cr)) repeat @fn_contains_step @I
| #_ (* see above *) <E @(pi2 ?? r)
| @(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))
        ]
| #l1 #H whd %2 @lookup_label_lpresent
| @(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 λ_.𝚺lr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt)) with
  [ None ⇒ ❬〈locals0, reggen2〉, None ?❭
  | Some ty ⇒
      let 〈r,gen〉 ≝ fresh … reggen2 in
        mk_DPair ? (λlr.option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt))) 〈〈r,ty〉::locals0, gen〉 (Some ? «〈r,ty〉, ?») ] 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 emptyfn ≝
  mk_partial_fn
    label_env
    env
    labgen
    reggen
    params
    locals
    result
    ?
    (f_stacksize f)
    (add ?? (empty_map …) l St_return)
    ?
    ?
    l
    l in
do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
OK ? (mk_internal_function
    (pf_labgen … f)
    (pf_reggen … f)
    (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? (pi1 … rt) ])
    (pf_params … f)
    (pf_locals … f)
    (pf_stacksize … f)
    (pf_graph … f)
    ?
    (pf_typed … f)
    (pf_entry … f)
    (pf_exit … f)
  ).
[ @I
| -emptyfn @(stmt_P_mp … (f_inv f))
  #s * #V #L %
  [ @(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
  ]
| #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')
    ]
  ]
  ]
| #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 ]
  | cases (f_return f) in E3;
    [ whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct
      @Exists_append_l
    | #rt 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')
  ]
| 7,8: whd >lookup_add_hit % #E destruct
| % @refl
]
qed.

definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
λp.transform_partial_program … p (λ_. transf_partial_fundef … c2ra_function).

include "Cminor/initialisation.ma".

definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.