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

definition env ≝ identifier_map SymbolTag register.
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, gen'〉) 〈[ ], en, gen〉.

lemma populates_env : ∀l,e,u,l',e',u'.
  populate_env e u l = 〈l',e',u'〉 →
  ∀i. Exists ? (λx.\fst x = i) l →
      present ?? e' i.
#l elim l
[ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) *
| * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?);
  * [ whd in ⊢ (??%? → ?) #E1 <E1
      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z
      whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E
      whd in E:(??%?); destruct;
      whd >lookup_add_hit % #A destruct
    | #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl)
      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 ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u''
      whd in ⊢ (??%? → ?) #E destruct
      @lookup_add_oblivious
      @(IH … E1 ? H)
    ]
] qed.

lemma populate_extends : ∀l,e,u,l',e',u'.
  populate_env e u l = 〈l',e',u'〉 →
  ∀i. present ?? e i → present ?? e' i.
#l elim l 
[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct //
| * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?);
  change in E:(??(match % with [ _ ⇒ ?])?) with (populate_env e u tl)
  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 RegisterTag u0) #i1 #u1 #E
  whd in E:(??%?)
  >(?:e' = add ?? e0 id i1) [ 2: destruct (E) @refl ]
  #i #H @lookup_add_oblivious @(IH … E0) @H
] 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 in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)
  lapply (refl ? (populate_label_env lbls u t))
  cases (populate_label_env lbls u t) in ⊢ (???% → %)
  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?)
  #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ]
  #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 in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)
  lapply (refl ? (populate_label_env lbls u t))
  cases (populate_label_env lbls u t) in ⊢ (???% → %)
  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?)
  #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ]
  #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 // @eq_identifier_elim // #E cases NE /2/ ]
  ]
] qed.

definition lookup_reg : ∀e:env. ∀id. present ?? e id → register ≝ lookup_present ??.
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. ∀l,s. lookup ?? g l = Some ? s → labels_P (λl. present ?? g l ∨ lpresent e l) s.

(* 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) : Type[0] ≝
{ pf_labgen    : universe LabelTag
; pf_reggen    : universe RegisterTag
; pf_result    : option (register × typ)
; pf_params    : list (register × typ)
; pf_locals    : list (register × typ)
; pf_stacksize : nat
; pf_graph     : graph statement
; pf_closed    : partially_closed lenv pf_graph
; pf_entry     : Σl:label. present ?? pf_graph l
; pf_exit      : Σl:label. present ?? pf_graph l
}.

inductive fn_graph_included (le:label_env) (f1:partial_fn le) (f2:partial_fn le) : Prop ≝
| fn_graph_inc : graph_included (pf_graph ? f1) (pf_graph ? f2) → fn_graph_included le f1 f2.

lemma fn_graph_inc_trans : ∀le,f1,f2,f3.
  fn_graph_included le f1 f2 → fn_graph_included le f2 f3 → fn_graph_included le f1 f3.
#le #f1 #f2 #f3 * #H1 * #H2 % @(graph_inc_trans … H1 H2) qed.

lemma fn_graph_included_refl : ∀label_env,f.
  fn_graph_included label_env f f.
#le #f % #l #H @H qed.

lemma fn_graph_included_sig : ∀label_env,f,f0.
  ∀f':Σf':partial_fn label_env. fn_graph_included ? f0 f'.
  fn_graph_included label_env f f0 →
  fn_graph_included label_env f f'.
#le #f #f0 * #f' #H1 #H2 @(fn_graph_inc_trans … H2 H1)
qed.

lemma add_statement_inv : ∀le,l,s.∀f.
  labels_present (pf_graph le f) s →
  partially_closed le (add … (pf_graph ? f) l s).
#le #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 // @eq_identifier_elim // #E cases NE /2/
  ]
] qed.

(* Add a statement to the graph, *without* updating the entry label. *)
definition fill_in_statement : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝
λle,l,s,f,p.
  mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
                (pf_result ? f) (pf_params ? f) (pf_locals ? f)
                (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
                «pf_entry ? f, ?» «pf_exit ? f, ?».
[ @add_statement_inv @p
| 2,3: @lookup_add_oblivious @use_sig
| % #l' @lookup_add_oblivious 
] qed.

(* Add a statement to the graph, making it the entry label. *)
definition add_to_graph : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝
λle,l,s,f,p.
  mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
                (pf_result ? f) (pf_params ? f) (pf_locals ? f)
                (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
                «l, ?» «pf_exit ? f, ?».
[ @add_statement_inv @p
| whd >lookup_add_hit % #E destruct
| @lookup_add_oblivious @use_sig
| % #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. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_present (pf_graph ? f) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝
λle,s,f,p.
  let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
  let s' ≝ s (pf_entry ? f) in
    (mk_partial_fn le g (pf_reggen ? f)
                   (pf_result ? f) (pf_params ? f) (pf_locals ? f)
                   (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
                   «l, ?» «pf_exit ? f, ?»).
[ % #l' @lookup_add_oblivious
| @add_statement_inv @p @use_sig
| whd >lookup_add_hit % #E destruct
| @lookup_add_oblivious @use_sig
] qed.

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

lemma add_statement_inv' : ∀le,l,s.∀f.
  labels_P (λl. present ?? (pf_graph le f) l ∨ lpresent le l) s →
  partially_closed le (add … (pf_graph ? f) l s).
#le #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 // @eq_identifier_elim // #E cases NE /2/
  ]
] qed.

definition add_fresh_to_graph' : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_P (λl.present ?? (pf_graph ? f) l ∨ lpresent le l) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝
λle,s,f,p.
  let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
  let s' ≝ s (pf_entry ? f) in
    (mk_partial_fn le g (pf_reggen ? f)
                   (pf_result ? f) (pf_params ? f) (pf_locals ? f)
                   (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
                   «l, ?» «pf_exit ? f, ?»).
[ % #l' @lookup_add_oblivious
| @add_statement_inv' @p @use_sig
| whd >lookup_add_hit % #E destruct
| @lookup_add_oblivious @use_sig
] qed.

definition fresh_reg : ∀le. ∀f:partial_fn le. typ → register × (Σf':partial_fn le. fn_graph_included le f f') ≝
λle,f,ty.
  let 〈r,g〉 ≝ fresh … (pf_reggen ? f) in
    〈r, «mk_partial_fn le (pf_labgen ? f) g
                       (pf_result ? f) (pf_params ? f) (〈r,ty〉::(pf_locals ? f))
                       (pf_stacksize ? f) (pf_graph ? f) (pf_closed ? f) (pf_entry ? f) (pf_exit ? f), ?»〉.
% #l // qed.

axiom UnknownVariable : String.

definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') ≝
λle,env,ty,e,f.
  match e return λty,e. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') with
  [ Id _ i ⇒ λEnv. 〈lookup_reg env i Env, «f, ?»〉
  | _ ⇒ λ_.fresh_reg le f ty
  ].
% // 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.

definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ].

definition choose_regs : ∀le. ∀env:env. ∀es:list (Σt:typ.expr t).
                         ∀f:partial_fn le. All ? (exprtyp_present env) es →
                         list register × (Σf':partial_fn le. fn_graph_included le f f') ≝
λle,env,es,f,Env.
  foldr_all (Σt:typ.expr t) ??
    (λe,p,acc. let 〈rs,f〉 ≝ acc in
             let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg le env t e (eject … f) ? ] p in
             〈r::rs,«eject … f', ?»〉) 〈[ ], «f, ?»〉 es Env.
[ @p
| @fn_graph_inc_trans [ 3: @(use_sig ?? f') | skip | @(use_sig ?? f) ]
| % //
]  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,rs,f'.
  choose_regs le env es f p = 〈rs,f'〉 → |es| = |rs|.
#le #env #es #f elim es
[ #p #rs #f normalize #E destruct @refl
| * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E
  cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 -E;
  cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 -E2;
  destruct (E4) skip (E1 E3) @eq_f @IH
  [ @(proj2 … p)
  | 3: @sym_eq @E1
  | 2: skip
  ]
] qed.

lemma present_included : ∀le,f,f',l.
  fn_graph_included le f f' →
  present ?? (pf_graph le f) l →
  present ?? (pf_graph le f') l.
#le #f #f' #l * #H1 #H2 @H1 @H2 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,s,f'.
∀l. Exists ? (λl'.l=l') (labels_of s) →
∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'.

record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝
{ stmt_graph_inc : fn_graph_included ? f f'
; stmt_labels_added : Cminor_labels_added le s f'
}.

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

(* A datatype saying how we intend to prove a step. *)
inductive fn_inc_because (le:label_env) : partial_fn le → Type[0] ≝
| fn_inc_eq : ∀f. fn_inc_because le f
| fn_inc_sig : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
    ∀f3:(Σf3:partial_fn le.fn_graph_included le f2 f3). fn_inc_because le f3
| fn_inc_addinv : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
    ∀s.∀f3:(Σf3:partial_fn le.add_stmt_inv le s f2 f3). fn_inc_because le f3
.

(* Extract the starting function for a step. *)
let rec fn_inc_because_left le f0  (b:fn_inc_because le f0) on b : partial_fn le ≝
  match b with [ fn_inc_eq f ⇒ f | fn_inc_sig f _ _ _ ⇒ f | fn_inc_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, f:partial_fn le, dummy:True;
  f' ≟ f,
  b  ≟ fn_inc_eq le f
⊢
  fn_graph_included le f f' ≡ fn_graph_included le (fn_inc_because_left le f' b) f'
.

unification hint 1 ≔ le:label_env, f1:partial_fn le, f2:partial_fn le, H12 : fn_graph_included le f1 f2, f3:(Σf3:partial_fn le. fn_graph_included le f2 f3);
  b ≟ fn_inc_sig le f1 f2 H12 f3
⊢
  fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
.

unification hint 1 ≔ le:label_env, f1:partial_fn le, f2:partial_fn le, H12 : fn_graph_included le f1 f2, s:stmt, f3:(Σf3:partial_fn le. add_stmt_inv le s f2 f3);
  b ≟ fn_inc_addinv le f1 f2 H12 s f3
⊢
  fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
.

(* A lemma to perform a step of the proof.  We can repeat this to do the whole
   proof. *)  
lemma fn_includes_step : ∀le,f. ∀b:fn_inc_because le f. fn_graph_included le (fn_inc_because_left le f b) f.
#le #f *
[ #f @fn_graph_included_refl
| #f1 #f2 #H12 * #f2 #H23 @(fn_graph_inc_trans … H12 H23)
| #f1 #f2 #H12 #s * #f2 * #H23 #X @(fn_graph_inc_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 (present ?? env)) (dst:register) (f:partial_fn le) on e: Σf':partial_fn le. fn_graph_included le f f' ≝
match e return λty,e.expr_vars ty e (present ?? env) → Σf':partial_fn le. fn_graph_included le f f' with
[ Id t i ⇒ λEnv.
    let r ≝ lookup_reg env i Env in
    match register_eq r dst with
    [ inl _ ⇒ «f, ?»
    | inr _ ⇒ «eject … (add_fresh_to_graph ? (St_op1 t t (Oid t) dst r) f ?), ?»
    ]
| Cst _ c ⇒ λ_. «add_fresh_to_graph ? (St_const dst c) f ?, ?»
| Op1 t t' op e' ⇒ λEnv.
    let 〈r,f〉 ≝ choose_reg ? env ? 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 r f in
      «eject … f, ?»
| Op2 _ _ _ op e1 e2 ⇒ λEnv.
    let 〈r1,f〉 ≝ choose_reg ? env ? e1 f (proj1 … Env) in
    let 〈r2,f〉 ≝ choose_reg ? env ? 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) r2 f in
    let f ≝ add_expr ? env ? e1 (proj1 … Env) r1 f in
      «eject … f, ?»
| Mem _ _ q e' ⇒ λEnv.
    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
    let f ≝ add_fresh_to_graph ? (St_load q r dst) f ? in
    let f ≝ add_expr ? env ? e' Env r f in
      «eject … f, ?»
| Cond _ _ _ e' e1 e2 ⇒ λEnv.
    let resume_at ≝ pf_entry ? f in
    let f ≝ add_expr ? env ? e2 (proj2 … Env) dst f 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)) dst f in
    let 〈r,f〉 as E ≝ choose_reg ? env ? e' f (proj1 … (proj1 … Env)) in
    let f ≝ add_fresh_to_graph ? (λltrue. St_cond r ltrue lfalse) f ? in
    let f ≝ add_expr ? env ? e' (proj1 … (proj1 … Env)) r f in
      «eject … f, ?»
| Ecost _ l e' ⇒ λEnv.
    let f ≝ add_expr ? env ? e' Env dst f in
    let f ≝ add_fresh_to_graph ? (St_cost l) f ? in
      «f, ?»
] Env. 
(* 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_includes_step @I)
try (#l #H @H)
[ #l #H whd % [ @H | @(present_included … (use_sig … lfalse)) repeat @fn_includes_step @I ]
| #l #H @(present_included … (use_sig ?? resume_at)) repeat @fn_includes_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:|es|=|dsts|) (f:partial_fn le) on es: Σf':partial_fn le. fn_graph_included le f f' ≝
match es return λes.All ?? es → |es|=|dsts| → ? with
[ nil ⇒ λ_. match dsts return λx. ?=|x| → Σf':partial_fn le. fn_graph_included le f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
| cons e et ⇒ λEnv.
    match dsts return λx. ?=|x| → ? with
    [ nil ⇒ λpf.⊥
    | cons r rt ⇒ λpf.
        let f ≝ add_exprs ? env et ? rt ? f in
        match e return λe.exprtyp_present ? e → ? with [ dp ty e ⇒ λEnv.
          let f ≝ add_expr ? env ty e ? r f in
            «eject … f, ?» ] (proj1 ?? Env)
    ]
] Env pf.
try (repeat @fn_includes_step @I)
[ 1,2: normalize in pf; destruct
| @Env
| @(proj2 … Env)
| normalize in pf; destruct @e0
] qed.

axiom UnknownLabel : String.
axiom ReturnMismatch : String.

definition stmt_inv : env → label_env → stmt → Prop ≝
λenv,lenv. stmt_P (λs. stmt_vars (present ?? 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)".
alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,14,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 (use_sig … 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,s,f'.
  labels_of s = [ ] → Cminor_labels_added le s f'.
#le #s #f' #E whd >E #l *;
qed.

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

lemma Cminor_labels_inc : ∀le,s,f,f'.
  fn_graph_included le f f' →
  Cminor_labels_added le s f →
  Cminor_labels_added le s f'.
#le #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,s,s',f.
  ∀f':Σf':partial_fn le. add_stmt_inv le s' f f'.
  Cminor_labels_added le s f →
  Cminor_labels_added le s f'.
#le #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,s,f.
  ∀f':Σf':partial_fn le. fn_graph_included le f f'.
  Cminor_labels_added le s f →
  Cminor_labels_added le s f'.
#le #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) (exits:Σls:list label. All ? (present ?? (pf_graph ? f)) ls) on s : res (Σf':partial_fn label_env. add_stmt_inv label_env s f f') ≝
match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env. add_stmt_inv ? s f f') with
[ St_skip ⇒ λ_. OK ? «f, ?»
| St_assign _ x e ⇒ λEnv.
    let dst ≝ lookup_reg env x (π1 (π1 Env)) in
    OK ? «eject … (add_expr ? env ? e (π2 (π1 Env)) dst f), ?»
| St_store _ _ q e1 e2 ⇒ λEnv.
    let 〈val_reg, f〉 ≝ choose_reg ? env ? e2 f (π2 (π1 Env)) in
    let 〈addr_reg, f〉 ≝ choose_reg ? env ? e1 f (π1 (π1 Env)) in
    let f ≝ add_fresh_to_graph ? (St_store q addr_reg val_reg) f ? in
    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) addr_reg f in
    OK ? «eject … (add_expr ? env ? e2 (π2 (π1 Env)) val_reg f), ?»
| St_call return_opt_id e args ⇒ λEnv.
    let return_opt_reg ≝
      match return_opt_id return λo. ? → ? with
      [ None ⇒ λ_. None ?
      | Some id ⇒ λEnv. Some ? (lookup_reg env id ?)
      ] Env in
    let 〈args_regs, f〉 as Eregs ≝ 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 〈fnr, f〉 ≝ choose_reg ? env ? e f (π2 (π1 (π1 Env))) in
        let f ≝ add_fresh_to_graph ? (St_call_ptr fnr args_regs return_opt_reg) f ? in
        «eject … (add_expr ? env ? e (π2 (π1 (π1 Env))) fnr f), ?»
      ] in
    OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
| St_tailcall e args ⇒ λEnv.
    let 〈args_regs, f〉 as Eregs ≝ 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 〈fnr, f〉 ≝ choose_reg ? env ? e f (π1 (π1 Env)) in
        let f ≝ add_fresh_to_graph ? (λ_. St_tailcall_ptr fnr args_regs) f ? in
        «eject … (add_expr ? env ? e (π1 (π1 Env)) fnr f), ?»
      ] in
    OK ? «eject … (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 ? «eject … 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 〈r,f〉 ≝ choose_reg ? env ? e f1 (π1 (π1 (π1 Env))) in
    let f ≝ add_fresh_to_graph ? (λl1. St_cond r l1 l2) f ? in
    OK ? «eject … (add_expr ? env ? e (π1 (π1 (π1 Env))) r f), ?»
| 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 ? «eject … (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 ? «eject … f, ?»
| St_exit n ⇒ λEnv.
    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
    OK ? «eject … (add_fresh_to_graph ? (λ_. R_skip l) f ?), ?»
| St_switch sz sg e tab n ⇒ λEnv.
    let 〈r,f〉 ≝ choose_reg ? env ? 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 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in
      let 〈br,f〉 ≝ 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 (Ocmpu Ceq) (* signed? *) br r cr) f ? in
      let f ≝ add_fresh_to_graph ? (St_const cr (Ointconst ? i)) f ? in
        OK ? «eject … f, ?») (OK ? f) tab;
    OK ? «eject … (add_expr ? env ? e (π1 Env) r f), ?»
| 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.add_stmt_inv ? (St_return o) f0 f') with
    [ None ⇒ λEnv. OK ? «eject … 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.add_stmt_inv label_env (St_return (Some ? e)) f0 f') with
            [ dp ty e ⇒ λEnv. let f ≝ add_expr label_env env ty e ? (\fst r) f in
                              OK ? «eject … f, ?» ]
        ]
    ]
| 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 ? «eject … (add_to_graph ? l' (R_skip (pf_entry ? f)) f ?), ?»
| St_goto l ⇒ λEnv.
    let l' ≝ lookup_label label_env l ? in
    OK ? «eject … (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 ? «eject … (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_includes_step @I)
try (@empty_Cminor_labels_added @refl)
try (@(All_mp … (use_sig ?? exits)))
try (#l #H @I)
try (#l #H @H)
[ -f @(choose_regs_length … (sym_eq … Eregs))
| whd in Env @(π1 (π1 (π1 Env)))
| -f @(choose_regs_length … (sym_eq … Eregs))
| #l #H cases (Exists_append … H)
  [ #H1 @(stmt_labels_added ???? (use_sig ?? f1) ? H1)
  | @(Cminor_labels_inc ?? f2 f1 ???) [ repeat @fn_includes_step @I | @(stmt_labels_added ???? (use_sig ?? f2)) ]
  ]
| #l #H @(present_included … H) repeat @fn_includes_step @I
| #l #H @(present_included … (use_sig ?? l_next)) repeat @fn_includes_step @I
| #l #H cases (Exists_append … H)
  [ @(Cminor_labels_inc … (stmt_labels_added ???? (use_sig ?? f1))) repeat @fn_includes_step @I
  | @(Cminor_labels_inc … (stmt_labels_added ???? (use_sig ?? f2))) repeat @fn_includes_step @I
  ]
| #l #H % [ @H | @(present_included … (use_sig ?? l2)) repeat @fn_includes_step @I ]
| 9,10: #l #H @(present_included … H) repeat @fn_includes_step @I
| @(use_sig ?? (pf_entry ??))
| @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
| % [ @use_sig | @(use_sig ?? exits) ]
| @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
| #l #H @use_sig
| #l #H @(present_included … (use_sig ?? l_default)) repeat @fn_includes_step @I
| #l #H % [ @(present_included … (use_sig ?? l_case)) repeat @fn_includes_step @I | @H ]
| @use_sig
| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
        |@Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?))
        ]
| #l1 #H whd %2 @lookup_label_lpresent
| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
] 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 〈result, locals, reggen〉 ≝
  match f_return f with
  [ None ⇒ 〈None ?, locals0, reggen2〉
  | Some ty ⇒
      let 〈r,gen〉 ≝ fresh … reggen2 in
        〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] 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
    labgen
    reggen
    result
    params
    locals
    (f_stacksize f)
    (add ?? (empty_map …) l St_return)
    ?
    l
    l in
do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
do u1 ← check_universe_ok ? (pf_labgen ? f);
do u2 ← check_universe_ok ? (pf_reggen ? f);
OK ? (mk_internal_function
    (pf_labgen ? f)
    (pf_reggen ? f)
    (pf_result ? f)
    (pf_params ? f)
    (pf_locals ? f)
    (pf_stacksize ? f)
    (pf_graph ? f)
    ?
    (pf_entry ? f)
    (pf_exit ? f)
  ).
[ @I
| -emptyfn @(stmt_P_mp … (f_inv f))
  #s * #V #L %
  [ @(stmt_vars_mp … V)
    #i #H cases (Exists_append … H)
    [ #H1 @(populate_extends ?????? (sym_eq … E2))
          @(populates_env … (sym_eq … E1)) @H1
    | #H1 @(populates_env … (sym_eq … E2)) @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')
    ]
  ]
  ]
| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
  [ * #E1 #E2 >E2 @I
  | whd in ⊢ (??%? → ?) #E' destruct (E')
  ]
| *: whd >lookup_add_hit % #E destruct
]
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'.