source: src/Clight/switchRemoval.ma @ 2160

include "Clight/Csyntax.ma".
include "Clight/fresh.ma".
include "basics/lists/list.ma".
include "common/Identifiers.ma".
include "Clight/Cexec.ma".
include "Clight/CexecInd.ma".

(* -----------------------------------------------------------------------------
   ----------------------------------------------------------------------------*)

(* -----------------------------------------------------------------------------
   Documentation
   ----------------------------------------------------------------------------*)

(* This file implements transformation of switches to linear sequences of
 * if/then/else. The implementation roughly follows the lines of the prototype.
 * /!\ We assume that the program is well-typed (the type of the evaluated 
 * expression must match the constants on each branch of the switch). /!\ *)

(* Documentation. Let the follwing be our input switch construct:
   // ---------------------------------  
   switch(e) {
   case v1:
     stmt1
   case v2:
     stmt2
   .
   .
   .
   default:
     stmt_default
   }
   // ---------------------------------  
  
   Note that stmt1,stmt2, ... stmt_default may contain "break" statements, wich have the effect of exiting 
   the switch statement. In the absence of break, the execution falls through each case sequentially.
 
   Given such a statement, we produce an equivalent sequence of if-then-elses chained by gotos:

   // ---------------------------------  
   fresh = e;
   if(fresh == v1) {
     stmt1';
     goto lbl_case2;
   }
   if(fresh == v2) {
     lbl_case2:
     stmt2';
     goto lbl_case2;
   }   
   ...
   stmt_default';
   exit_label:
   // ---------------------------------    

   where stmt1', stmt2', ... stmt_default' are the statements where all top-level [break] statements
   were replaced by [goto exit_label]. Note that fresh, lbl_casei are fresh identifiers and labels.
*)


(* -----------------------------------------------------------------------------
   Definitions allowing to state that the program resulting of the transformation
   is switch-free. The actual proof is done using Russell.
   ----------------------------------------------------------------------------*)

(* Property of a Clight statement of containing no switch. Could be generalized into a kind of
 * statement_P, if useful elsewhere. *)
let rec switch_free (st : statement) : Prop ≝
match st with
[ Sskip ⇒ True
| Sassign _ _ ⇒ True
| Scall _ _ _ ⇒ True
| Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2
| Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2
| Swhile e body ⇒ switch_free body
| Sdowhile e body ⇒ switch_free body
| Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
| Sbreak ⇒ True
| Scontinue ⇒ True
| Sreturn _ ⇒ True
| Sswitch _ _ ⇒ False
| Slabel _ body ⇒ switch_free body
| Sgoto _ ⇒ True
| Scost _ body ⇒ switch_free body
].

definition sf_statement ≝ Σs:statement. switch_free s.

definition stlist ≝ list (label × (𝚺sz.bvint sz) × sf_statement).

(* Property of a list of labeled statements of being switch-free *)
let rec branches_switch_free (sts : labeled_statements) : Prop ≝ 
match sts with
[ LSdefault st => 
  switch_free st
| LScase _ _ st tl => 
  switch_free st ∧ branches_switch_free tl
].

let rec branch_switch_free_ind
  (sts : labeled_statements)
  (H   : labeled_statements → Prop)  
  (defcase : ∀st. H (LSdefault st))
  (indcase : ∀sz.∀int.∀st.∀sub_cases. H sub_cases → H (LScase sz int st sub_cases)) ≝
match sts with
[ LSdefault st ⇒ 
  defcase st
| LScase sz int st tl ⇒
  indcase sz int st tl (branch_switch_free_ind tl H defcase indcase)
].


(* -----------------------------------------------------------------------------
   Switch-removal code for statements, functions and fundefs.
   ----------------------------------------------------------------------------*)

(* Given a list of switch cases, prefixes each case by a fresh goto label. It is
   assumed as an hypothesis that each sub-statement is already switch-free
   (argument [H]). The whole function returns a list of labelled switch-free switch
   cases, along the particular label of the default statement and its associated
   statement. A fresh label generator [uv] is threaded through the function.  *)
let rec add_starting_lbl_list
  (l : labeled_statements)  
  (H : branches_switch_free l)
  (uv : universe SymbolTag)
  (acc : stlist) : stlist × (label × sf_statement) × (universe SymbolTag) ≝
match l return λl'. l = l' → stlist × (label × sf_statement) × (universe SymbolTag) with
[ LSdefault st ⇒ λEq.
  let 〈default_lab, uv'〉 ≝ fresh ? uv in
  〈rev ? acc, 〈default_lab, «st, ?»〉, uv'〉
| LScase sz tag st other_cases ⇒ λEq.
  let 〈lab, uv'〉 ≝ fresh ? uv in
  let acc' ≝ 〈lab, (mk_DPair ?? sz tag), «st, ?»〉 :: acc in
  add_starting_lbl_list other_cases ? uv' acc'
] (refl ? l).
[ 1: destruct whd in H; //
| 2: letin H1 ≝ H >Eq in H1; 
  #H' normalize in H'; elim H' //
| 3: >Eq in H; normalize * //
] qed.

(* Converts the directly accessible ("free") breaks to gotos toward the [lab] label.  *)
let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝
match st with
[ Sbreak ⇒
  Sgoto lab
| Ssequence s1 s2 ⇒
  Ssequence (convert_break_to_goto s1 lab) (convert_break_to_goto s2 lab)
| Sifthenelse e iftrue iffalse ⇒
  Sifthenelse e (convert_break_to_goto iftrue lab) (convert_break_to_goto iffalse lab)
| Sfor init e update body ⇒
  Sfor (convert_break_to_goto init lab) e update body
| Slabel l body ⇒
  Slabel l (convert_break_to_goto body lab)
| Scost cost body ⇒
  Scost cost (convert_break_to_goto body lab)
| _ ⇒ st
].

(* Converting breaks preserves switch-freeness. *)
lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_break_to_goto s label).
#s elim s //
[ 1: #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
| 2: #e #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
| 3: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize
     try @conj try @conj /3/
| 4: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /2/
| 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/
] qed.

(* Obsolete. This version generates a nested pseudo-sequence of if-then-elses. *)
let rec produce_cond 
  (e : expr) 
  (switch_cases : stlist) 
  (def_case : ident × sf_statement) 
  (exit : label) on switch_cases : sf_statement × label ≝
match switch_cases with
[ nil ⇒
  match def_case with
  [ mk_Prod default_label default_statement ⇒
    〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉
  ]
| cons switch_case tail ⇒
  let 〈case_label, case_value, case_statement〉 ≝ switch_case in
    match case_value with
    [ mk_DPair sz val ⇒
       let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in
       (* let test ≝ Expr (Ebinop Oeq e e) (Tint I32 Unsigned) in *)
       (* let test ≝ Expr (Econst_int I32 (bvzero 32)) (Tint I32 Signed)  in *)
       let 〈sub_statement, sub_label〉 ≝ produce_cond e tail def_case exit in
       let result ≝
         Sifthenelse test
          (Slabel case_label
            (Ssequence (convert_break_to_goto (pi1 … case_statement) exit)
                       (Sgoto sub_label)))
          (pi1 … sub_statement)
      in
      〈«result, ?», case_label〉
    ]
].
[ 1: normalize @convert_break_lift elim default_statement //
| 2: whd @conj normalize try @conj try //
  [ 1: @convert_break_lift elim case_statement //
  | 2: elim sub_statement // ]
] qed.

(* We assume that the expression e is consistely typed w.r.t. the switch branches *)
let rec produce_cond2
  (e : expr)
  (switch_cases : stlist)
  (def_case : ident × sf_statement)
  (exit : label) on switch_cases : sf_statement × label ≝
match switch_cases with
[ nil ⇒
  let 〈default_label, default_statement〉 ≝ def_case in
  〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉
| cons switch_case tail ⇒
  let 〈case_label, case_value, case_statement〉 ≝ switch_case in
  match case_value with
  [ mk_DPair sz val ⇒
    let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in
    let 〈sub_statement, sub_label〉 ≝ produce_cond2 e tail def_case exit in
    let case_statement_res ≝
       Sifthenelse test
        (Slabel case_label
          (Ssequence (convert_break_to_goto (pi1 … case_statement) exit)
                     (Sgoto sub_label)))
        Sskip
    in
    〈«Ssequence case_statement_res (pi1 … sub_statement), ?», case_label〉
  ]
].
[ 1: normalize @convert_break_lift elim default_statement //
| 2: whd @conj
     [ 1: whd @conj try // whd in match (switch_free ?); @conj
          [ 1: @convert_break_lift elim case_statement //
          | 2: // ]
     | 2: elim sub_statement // ]
] qed.     

(* takes an expression, a list of switch-free cases and a freshgen and returns a 
 * switch-free equivalent, along an updated freshgen and a new local variable
 * (for storing the value of the expr). *)
definition simplify_switch : 
  expr → ∀l:labeled_statements. branches_switch_free l → (universe SymbolTag) → sf_statement × (universe SymbolTag) ≝
λe.λswitch_cases.λH.λuv.
 let 〈exit_label, uv1〉            ≝ fresh ? uv in
 let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list switch_cases ? uv1 [ ] in
 let 〈result, useless_label〉      ≝ produce_cond2 e switch_cases defcase exit_label in
 〈«Ssequence (pi1 … result) (Slabel exit_label Sskip), ?», uv2〉.
[ 1:  normalize try @conj try @conj try // elim result //
| 2: @H ]
qed.

(* recursively convert a statement into a switch-free one. *)
let rec switch_removal 
  (st : statement)
  (uv : universe SymbolTag) : (Σresult.switch_free result) × (list (ident × type)) × (universe SymbolTag) ≝
match st return λs.s = st → ? with
[ Sskip       ⇒ λEq. 〈«st,?», [ ], uv〉
| Sassign _ _ ⇒ λEq. 〈«st,?», [ ], uv〉
| Scall _ _ _ ⇒ λEq. 〈«st,?», [ ], uv〉
| Ssequence s1 s2 ⇒ λEq. 
  let 〈s1', vars1, uv'〉  ≝ switch_removal s1 uv in
  let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in
  〈«Ssequence (pi1 … s1') (pi1 … s2'),?», vars1 @ vars2, uv''〉
| Sifthenelse e s1 s2 ⇒ λEq. 
  let 〈s1', vars1, uv'〉  ≝ switch_removal s1 uv in
  let 〈s2', vars2, uv''〉 ≝ switch_removal s2 uv' in
  〈«Sifthenelse e (pi1 … s1') (pi1 … s2'),?», vars1 @ vars2, uv''〉
| Swhile e body ⇒ λEq.
  let 〈body', vars', uv'〉 ≝ switch_removal body uv in
  〈«Swhile e (pi1 … body'),?», vars', uv'〉 
| Sdowhile e body ⇒ λEq.
  let 〈body', vars', uv'〉 ≝ switch_removal body uv in
  〈«Sdowhile e (pi1 … body'),?», vars', uv'〉 
| Sfor s1 e s2 s3 ⇒ λEq.
  let 〈s1', vars1, uv'〉   ≝ switch_removal s1 uv in
  let 〈s2', vars2, uv''〉  ≝ switch_removal s2 uv' in
  let 〈s3', vars3, uv'''〉 ≝ switch_removal s3 uv'' in
  〈«Sfor (pi1 … s1') e (pi1 … s2') (pi1 … s3'),?», vars1 @ vars2 @ vars3, uv'''〉
| Sbreak ⇒ λEq.
  〈«st,?», [ ], uv〉
| Scontinue ⇒ λEq.
  〈«st,?», [ ], uv〉
| Sreturn _ ⇒ λEq.
  〈«st,?», [ ], uv〉
| Sswitch e branches ⇒ λEq.
   let 〈sf_branches, vars', uv1〉 ≝ switch_removal_branches branches uv in
   match sf_branches with
   [ mk_Sig branches' H ⇒ 
     let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in
     let ident             ≝ Expr (Evar switch_tmp) (typeof e) in
     let assign            ≝ Sassign ident e in     
     let 〈result, uv3〉     ≝ simplify_switch ident branches' H uv2 in
     〈«Ssequence assign (pi1 … result), ?», (〈switch_tmp, typeof e〉 :: vars'), uv3〉
   ]
| Slabel label body ⇒ λEq.
  let 〈body', vars', uv'〉 ≝ switch_removal body uv in
  〈«Slabel label (pi1 … body'), ?», vars', uv'〉
| Sgoto _ ⇒ λEq.
  〈«st, ?», [ ], uv〉
| Scost cost body ⇒ λEq.
  let 〈body', vars', uv'〉 ≝ switch_removal body uv in
  〈«Scost cost (pi1 … body'),?», vars', uv'〉 
] (refl ? st)

and switch_removal_branches 
  (l : labeled_statements) 
  (uv : universe SymbolTag) : (Σl'.branches_switch_free l') × (list (ident × type)) × (universe SymbolTag) ≝
match l with
[ LSdefault st ⇒
  let 〈st, vars',  uv'〉 ≝ switch_removal st uv in
  〈«LSdefault (pi1 … st), ?», vars', uv'〉
| LScase sz int st tl =>
  let 〈tl_result, vars', uv'〉 ≝ switch_removal_branches tl uv in
  let 〈st', vars'', uv''〉     ≝ switch_removal st uv' in 
  〈«LScase sz int st' (pi1 … tl_result), ?», vars' @ vars'', uv''〉
].
try @conj destruct try elim s1' try elim s2' try elim s3' try elim body' whd try //
[ 1: #st1 #H1 #st2 #H2 #st3 #H3 @conj //
| 2: elim result //
| 3: elim st //
| 4: elim st' //
| 5: elim tl_result //
] qed.

definition function_switch_removal : function → universe SymbolTag → function × (universe SymbolTag) ≝ 
λf,u.
  let 〈body, new_vars, u'〉 ≝ switch_removal (fn_body f) u in
  let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (pi1 … body) in
  〈f, u'〉.

let rec fundef_switch_removal (f : clight_fundef) (u : universe SymbolTag) : clight_fundef × (universe SymbolTag) ≝
match f with
[ CL_Internal f ⇒
  let 〈f',u'〉 ≝ function_switch_removal f u in
  〈CL_Internal f', u'〉
| CL_External _ _ _ ⇒
  〈f, u〉
].


(* -----------------------------------------------------------------------------
   Switch-removal code for programs.
   ----------------------------------------------------------------------------*)  

(* The functions in fresh.ma do not consider labels. Using [universe_for_program p] may lead to 
 * name clashes for labels. We have no choice but to actually run through the function and to 
 * compute the maximum of labels+identifiers. This way we can generate both fresh variables and
 * fresh labels using the same univ. While we're at it we also consider record fields. 
 * Cost labels are not considered, though. They already live in a separate universe. 
 *
 * Important note: this is partially redundant with fresh.ma. We take care of avoiding name clashes,
 * but in the end it might be good to move the following functions into fresh.ma.
 *)

(* This is certainly overkill: variables adressed in an expression should be declared in the
 * enclosing function's prototype. *)
let rec max_of_expr (e : expr) (current : ident) : ident ≝
match e with
[ Expr ed _ ⇒
  match ed with
  [ Econst_int _ _ ⇒ current
  | Econst_float _ ⇒ current
  | Evar id ⇒ max_id id current
  | Ederef e1 ⇒ max_of_expr e1 current
  | Eaddrof e1 ⇒ max_of_expr e1 current
  | Eunop _ e1 ⇒ max_of_expr e1 current
  | Ebinop _ e1 e2 ⇒ max_of_expr e1 (max_of_expr e2 current)
  | Ecast _ e1 ⇒ max_of_expr e1 current
  | Econdition e1 e2 e3 ⇒
    max_of_expr e1 (max_of_expr e2 (max_of_expr e3 current))
  | Eandbool e1 e2 ⇒
    max_of_expr e1 (max_of_expr e2 current)
  | Eorbool e1 e2 ⇒
    max_of_expr e1 (max_of_expr e2 current)
  | Esizeof _ ⇒ current
  | Efield r f ⇒ max_id f (max_of_expr r current)
  | Ecost _ e1 ⇒ max_of_expr e1 current
  ]
].

(* Reeasoning about this promises to be a serious pain. Especially the Scall case. *)
let rec max_of_statement (s : statement) (current : ident) : ident ≝
match s with
[ Sskip ⇒ current
| Sassign e1 e2 ⇒ max_of_expr e2 (max_of_expr e1 current)
| Scall ret f args ⇒
  let retmax ≝ 
    match ret with
    [ None ⇒ current
    | Some e ⇒ max_of_expr e current ]
  in
  foldl ?? (λacc,elt. max_of_expr elt acc) (max_of_expr f retmax) args
| Ssequence s1 s2 ⇒ 
  max_of_statement s1 (max_of_statement s2 current)
| Sifthenelse e s1 s2 ⇒
  max_of_expr e (max_of_statement s1 (max_of_statement s2 current))
| Swhile e body ⇒
  max_of_expr e (max_of_statement body current)
| Sdowhile e body ⇒
  max_of_expr e (max_of_statement body current)
| Sfor init test incr body ⇒
  max_of_statement init (max_of_expr test (max_of_statement incr (max_of_statement body current)))
| Sbreak ⇒ current
| Scontinue ⇒ current
| Sreturn opt ⇒
  match opt with
  [ None ⇒ current
  | Some e ⇒ max_of_expr e current
  ]
| Sswitch e ls ⇒
  max_of_expr e (max_of_ls ls current)
| Slabel lab body ⇒
  max_id lab (max_of_statement body current)
| Sgoto lab ⇒
  max_id lab current
| Scost _ body ⇒
  max_of_statement body current  
]
and max_of_ls (ls : labeled_statements) (current : ident) : ident ≝
match ls with
[ LSdefault s ⇒ max_of_statement s current
| LScase _ _ s ls' ⇒ max_of_ls ls' (max_of_statement s current)
].

definition max_id_of_function : function → ident ≝
λf. max_of_statement (fn_body f) (max_id_of_fn f).

definition max_id_of_fundef_deep : clight_fundef → ident ≝
λf. match f with
  [ CL_Internal f ⇒ max_id_of_function f
  | CL_External id _ _ ⇒ id
  ].

let rec max_id_of_functs_deep (funcs : list (ident × clight_fundef)) (current : ident) : ident ≝
let func_max ≝
  foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef_deep (\snd idf))) id) (an_identifier ? one) funcs
in max_id func_max current.

definition max_id_of_program_deep : clight_program → ident ≝
λp.
  max_id
    (max_id_of_functs_deep (prog_funct ?? p) (prog_main ?? p))
    (max_id_of_globvars (prog_vars ?? p)).
        
(* The previous functions compute an (over?)-approximation of the identifiers and labels.
   The following function builds a "good" universe for a complete clight program. *)
definition universe_for_program_deep : clight_program → universe SymbolTag ≝
λp. universe_of_max (max_id_of_program_deep p).


let rec program_switch_removal (p : clight_program) : clight_program ≝
 let uv         ≝ universe_for_program_deep p in
 let prog_funcs ≝ prog_funct ?? p in
 let 〈sf_funcs, final_uv〉 ≝ 
  foldr ?? (λcl_fundef.λacc.
    let 〈fundefs, uv1〉    ≝ acc in    
    let 〈fun_id, fun_def〉 ≝ cl_fundef in
    let 〈new_fun_def,uv2〉 ≝ fundef_switch_removal fun_def uv1 in
    〈〈fun_id, new_fun_def〉 :: fundefs, uv2〉
   ) 〈[ ], uv〉 prog_funcs 
 in 
 mk_program ??
  (prog_vars … p)
  sf_funcs
  (prog_main … p).

(* -----------------------------------------------------------------------------
   Simulation proof and related voodoo.
   ----------------------------------------------------------------------------*)

(* Copied from SimplifyCasts.ma. Might be good to create a new file for shared stuff. *)
inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝
| SimOk   :  (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2
| SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2.

definition expr_lvalue_ind_combined ≝
λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
conj ??
 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
 
let rec expr_ind2 
    (P : expr → Prop) (Q : expr_descr → type → Prop)
    (IE : ∀ed. ∀t. Q ed t → P (Expr ed t))
    (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t)
    (Iconst_float : ∀f, t. Q (Econst_float f) t)
    (Ivar : ∀id, t. Q (Evar id) t)
    (Ideref : ∀e, t. P e → Q (Ederef e) t)
    (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t)
    (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t)
    (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t)
    (Icast : ∀castt, e, t. P e →  Q (Ecast castt e) t)  
    (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t)
    (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t)
    (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t)
    (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t)
    (Ifield : ∀e,f,t. P e → Q (Efield e f) t)
    (Icost : ∀c,e,t. P e → Q (Ecost c e) t) 
    (e : expr) on e : P e ≝
match e with
[ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed t) ]

and expr_desc_ind2
    (P : expr → Prop) (Q : expr_descr → type → Prop)
    (IE : ∀ed. ∀t. Q ed t → P (Expr ed t))
    (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t)
    (Iconst_float : ∀f, t. Q (Econst_float f) t)
    (Ivar : ∀id, t. Q (Evar id) t)
    (Ideref : ∀e, t. P e → Q (Ederef e) t)
    (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t)
    (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t)
    (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t)
    (Icast : ∀castt, e, t. P e →  Q (Ecast castt e) t)  
    (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t)
    (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t)
    (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t)
    (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t)
    (Ifield : ∀e,f,t. P e → Q (Efield e f) t)
    (Icost : ∀c,e,t. P e → Q (Ecost c e) t) 
    (ed : expr_descr) (t : type) on ed : Q ed t ≝
match ed with
[ Econst_int sz i ⇒ Iconst_int sz i t
| Econst_float f ⇒ Iconst_float f t
| Evar id ⇒ Ivar id t
| Ederef e ⇒ Ideref e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
| Eaddrof e ⇒ Iaddrof e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
| Eunop op e ⇒ Iunop op e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
| Ebinop op e1 e2 ⇒ Ibinop op e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
| Ecast castt e ⇒ Icast castt e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
| Econdition e1 e2 e3 ⇒ Icond e1 e2 e3 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e3)
| Eandbool e1 e2 ⇒ Iandbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
| Eorbool e1 e2 ⇒ Iorbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
| Esizeof sizeoft ⇒ Isizeof sizeoft t
| Efield e field ⇒ Ifield e field t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
| Ecost c e ⇒ Icost c e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e)
].

(* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched
   by a non-constant number of evaluations in the converted program. More precisely, 
   [seq_of_labeled_statement (select_switch sz n sl)] will be matched by all the steps
   necessary to execute all the "if-then-elses" corresponding to cases /before/ [n]. *)
   
(* A version of simplify_switch hiding the ugly proj *)
definition sw_rem : statement → (universe SymbolTag) → statement ≝
λs,u.
  \fst (\fst (switch_removal s u)).

definition fresh_for_expression ≝
λe,u. fresh_for_univ SymbolTag (max_of_expr e (an_identifier ? one)) u.  
  
definition fresh_for_statement ≝
λs,u. fresh_for_univ SymbolTag (max_of_statement s (an_identifier ? one)) u.

definition fresh_for_function ≝
λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u.

let rec fresh_for_continuation (k : cont) (u : universe SymbolTag) : Prop ≝
match k with
[ Kstop ⇒ True
| Kseq s k0 ⇒ (fresh_for_statement s u) ∧ (fresh_for_continuation k0 u)
| Kwhile e body k0 ⇒ (fresh_for_expression e u) ∧ (fresh_for_statement body u) ∧ (fresh_for_continuation k0 u)
| Kdowhile e body k0 ⇒ (fresh_for_expression e u) ∧ (fresh_for_statement body u) ∧ (fresh_for_continuation k0 u)
| Kfor2 e s1 s2 k0 ⇒
  (fresh_for_expression e u) ∧ (fresh_for_statement s1 u) ∧
  (fresh_for_statement s2 u) ∧ (fresh_for_continuation k0 u)
| Kfor3 e s1 s2 k0 ⇒
  (fresh_for_expression e u) ∧ (fresh_for_statement s1 u) ∧
  (fresh_for_statement s2 u) ∧ (fresh_for_continuation k0 u)
| Kswitch k0 ⇒ fresh_for_continuation k0 u
| Kcall _ f e k ⇒ (fresh_for_function f u) ∧ (fresh_for_continuation k u)
].

inductive switch_cont_sim : cont → cont → Prop ≝
| swc_stop : 
    switch_cont_sim Kstop Kstop
| swc_seq : ∀s,k,k',u.
    fresh_for_statement s u →
    switch_cont_sim k k' → 
    switch_cont_sim (Kseq s k) (Kseq (sw_rem s u) k')
| swc_while : ∀e,s,k,k',u.
    fresh_for_expression e u →
    fresh_for_statement s u →
    switch_cont_sim k k' →
    switch_cont_sim (Kwhile e s k) (Kwhile e (sw_rem s u) k')
| swc_dowhile : ∀e,s,k,k',u.
    fresh_for_expression e u →
    fresh_for_statement s u →
    switch_cont_sim k k' →
    switch_cont_sim (Kdowhile e s k) (Kdowhile e (sw_rem s u) k')
| swc_for1 : ∀e,s1,s2,k,k',u1,u2.
    fresh_for_statement s1 u1 →
    fresh_for_statement s2 u2 →
    switch_cont_sim k k' →
    switch_cont_sim (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip e (sw_rem s1 u1) (sw_rem s2 u2)) k')
| swc_for2 : ∀e,s1,s2,k,k',u1,u2.
    fresh_for_statement s1 u1 →
    fresh_for_statement s2 u2 →
    switch_cont_sim k k' →
    switch_cont_sim (Kfor2 e s1 s2 k) (Kfor2 e (sw_rem s1 u1) (sw_rem s2 u2) k')
| swc_for3 : ∀e,s1,s2,k,k',u1,u2.
    fresh_for_statement s1 u1 →
    fresh_for_statement s2 u2 →
    switch_cont_sim k k' → 
    switch_cont_sim (Kfor3 e s1 s2 k) (Kfor3 e (sw_rem s1 u1) (sw_rem s2 u2) k')
| swc_switch : ∀k,k'.
    switch_cont_sim k k' → 
    switch_cont_sim (Kswitch k) (Kswitch k')
| swc_call : ∀r,f,en,k,k',u. 
    fresh_for_function f u →
    switch_cont_sim k k' →
    switch_cont_sim (Kcall r f en k) (Kcall r (\fst (function_switch_removal f u)) en k').


inductive switch_state_sim : state → state → Prop ≝
| sws_state : ∀uf,us,uk,f,s,k,k',e,m.
    fresh_for_function f uf →
    fresh_for_statement s us →
    fresh_for_continuation k' uk →
    switch_cont_sim k k' → 
    switch_state_sim (State f s k e m) (State (\fst (function_switch_removal f uf)) (sw_rem s us) k' e m)
(* Extra matching states that we can reach that don't quite correspond to the
   labelling function *)
(*   
| sws_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' →
    switch_state_sim (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
| sws_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' →
    switch_state_sim (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
| sws_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. switch_cont_sim k k' →
    switch_state_sim (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
*)
(* and the rest *)
| sws_callstate : ∀ufd,fd,args,k,k',m. 
    switch_cont_sim k k' → 
    switch_state_sim (Callstate fd args k m) (Callstate (\fst (fundef_switch_removal fd ufd)) args k' m)
| sws_returnstate : ∀res,k,k',m. 
    switch_cont_sim k k' → 
    switch_state_sim (Returnstate res k m) (Returnstate res k' m)
| sws_finalstate : ∀r. 
    switch_state_sim (Finalstate r) (Finalstate r)
.

inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝
| eventually_base : ∀s,t,s'. 
    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
    P s' →
    eventually ge P s t
| eventually_step : ∀s,t,s',t'.
    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
    eventually ge P s' t' →
    eventually ge P s (t ⧺ t').
    
(* [eventually] is not so nice to use directly, we would like to make the mandatory
 * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not
   to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *)     
lemma eventually_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → 
                                      eventually ge P s t.
#ge #P #s #t * #s' * #Hexec #HP %1{? Hexec HP}
qed.

record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
  rg_find_symbol: ∀s.
    find_symbol ? ge s = find_symbol ? ge' s;
  rg_find_funct: ∀v,f.
    find_funct ? ge v = Some ? f →
    find_funct ? ge' v = Some ? (t f);
  rg_find_funct_ptr: ∀b,f.
    find_funct_ptr ? ge b = Some ? f →
    find_funct_ptr ? ge' b = Some ? (t f)
}.

(* TODO ... fundef_switch_removal wants a universe which is fresh-for-its argument. *)
(*
lemma sim_related_globals : ∀ge,ge',en,m,u. related_globals ? fundef_switch_removal ge ge' → 
  (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧
  (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)).
*)  

(* The return type of any function is invariant under switch removal *)
lemma fn_return_simplify : ∀f,u. fn_return (\fst (function_switch_removal f u)) = fn_return f.
#f #u elim f #ret #args #vars #body normalize elim (switch_removal body u)
* * #body' #Hswitch_free #new_vars #u' normalize //
qed.

lemma while_commute : ∀e0, s0, us0. Swhile e0 (sw_rem s0 us0) = (sw_rem (Swhile e0 s0) us0).
#e0 #s0 #us0 normalize 
cases (switch_removal s0 us0) * * #body #Hswfree #newvars #u' normalize //
qed.

lemma max_one_neutral : ∀v. max v one = v.
* // qed.

lemma max_id_one_neutral : ∀v. max_id v (an_identifier ? one) = v.
* #p whd in ⊢ (??%?); >max_one_neutral // qed.

lemma max_id_commutative : ∀v1, v2. max_id v1 v2 = max_id v2 v1.
* #p1 * #p2 whd in match (max_id ??) in ⊢ (??%%);
>commutative_max // qed.

lemma transitive_le : transitive ? le. // qed.

lemma le_S_weaken : ∀a,b. le (succ a) b → le a b.
#a #b /2/ qed.

(* cycle of length 1 *)
lemma le_S_contradiction_1 : ∀a. le (succ a) a → False.
* /2 by absurd/ qed.

(* cycle of length 2 *)
lemma le_S_contradiction_2 : ∀a,b. le (succ a) b → le (succ b) a → False.
#a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2))
#Heq @(le_S_contradiction_1 a) destruct // qed.

(* cycle of length 3 *)
lemma le_S_contradiction_3 : ∀a,b,c. le (succ a) b → le (succ b) c → le (succ c) a → False.
#a #b #c #H1 #H2 #H3 lapply (transitive_le … H1 (le_S_weaken ?? H2)) #H4
@(le_S_contradiction_2 … H3 H4)
qed.

lemma reflexive_leb : ∀a. leb a a = true.
#a @(le_to_leb_true a a) // qed.

(*
lemma le_S_contradiction : ∀a,b. le (succ a) b → le (succ b) a → False.
#a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2)) #Heq
destruct inversion H2 
[ 2: #m #H1 #H2 #H3
elim b; normalize in match (succ ?);
[ 1: #H destruct (H)
| 2: #p #H 
*)
(* This should be somewhere else. *)
lemma associative_max : associative ? max.
#a #b #c
whd in ⊢ (??%%); whd in match (max a b); whd in match (max b c);
lapply (pos_compare_to_Prop a b)
cases (pos_compare a b) whd in ⊢ (% → ?); #Hab
[ 1: >(le_to_leb_true a b) normalize nodelta /2/
     lapply (pos_compare_to_Prop b c)
     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
     [ 1: >(le_to_leb_true b c) normalize nodelta
          lapply (pos_compare_to_Prop a c)
          cases (pos_compare a c) whd in ⊢ (% → ?); #Hac
          [ 1: >(le_to_leb_true a c) /2/
          | 2: destruct cases (leb c c) //
          | 3: (* There is an obvious contradiction in the hypotheses. omega, I miss you *)
               @(False_ind … (le_S_contradiction_3 ??? Hab Hbc Hac))            
          ]
          @le_S_weaken //
     | 2: destruct
          cases (leb c c) normalize nodelta
          >(le_to_leb_true a c) /2/
     | 3: >(not_le_to_leb_false b c) normalize nodelta /2/
          >(le_to_leb_true a b) /2/
     ]
| 2: destruct (Hab) >reflexive_leb normalize nodelta
     lapply (pos_compare_to_Prop b c)
     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
     [ 1: >(le_to_leb_true b c) normalize nodelta
          >(le_to_leb_true b c) normalize nodelta
          /2/
     | 2: destruct >reflexive_leb normalize nodelta
          >reflexive_leb //
     | 3: >(not_le_to_leb_false b c) normalize nodelta
          >reflexive_leb /2/ ]
| 3: >(not_le_to_leb_false a b) normalize nodelta /2/
     lapply (pos_compare_to_Prop b c)
     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
     [ 1: >(le_to_leb_true b c) normalize nodelta /2/
     | 2: destruct >reflexive_leb normalize nodelta @refl
     | 3: >(not_le_to_leb_false b c) normalize nodelta
          >(not_le_to_leb_false a b) normalize nodelta
          >(not_le_to_leb_false a c) normalize nodelta
          lapply (transitive_le … Hbc (le_S_weaken … Hab))
          #Hca /2/
     ]
] qed.       

lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3).
* #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max //
qed.

lemma max_of_expr_rewrite : 
  ∀e,id. max_of_expr e id = max_id (max_of_expr e (an_identifier SymbolTag one)) id.
@(expr_ind2 … (λed,t. ∀id. max_of_expr (Expr ed t) id=max_id (max_of_expr (Expr ed t) (an_identifier SymbolTag one)) id))
[ 1: #ed #t // ]
[ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
| 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
#ty
[ 3: * #id_p whd in match (max_of_expr ??); cases var_id #var_p normalize nodelta
     whd in match (max_id ??) in ⊢ (???%);
     >max_one_neutral // ]
[ 1,2,11: * * //
| 3,4,5,7,13: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); @Hind
| 6,9,10: #Hind1 #Hind2 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%);
     >(Hind1 (max_of_expr e2 (an_identifier SymbolTag one)))
     >max_id_associative
     >Hind1
     cases (max_of_expr e1 ?)
     #v1 <Hind2 @refl
| 8: #Hind1 #Hind2 #Hind3 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%);
     >Hind1 in ⊢ (??%?); >Hind2 in ⊢ (??%?); >Hind3 in ⊢ (??%?);
     >Hind1 in ⊢ (???%); >Hind2 in ⊢ (???%);
     >max_id_associative >max_id_associative @refl
| 12: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%);
      cases field #p normalize nodelta 
      >Hind cases (max_of_expr e1 ?) #e'
      cases id #id'
      whd in match (max_id ??); normalize nodelta
      whd in match (max_id ??); >associative_max @refl
] qed.

lemma expr_fresh_lift : 
  ∀e,u,id. 
      fresh_for_expression e u →
      fresh_for_univ SymbolTag id u →
      fresh_for_univ SymbolTag (max_of_expr e id) u.
#e #u #id
normalize in match (fresh_for_expression e u);
#H1 #H2
>max_of_expr_rewrite
normalize in match (fresh_for_univ ???);
cases (max_of_expr e ?) in H1; #p #H1 
cases id in H2; #p' #H2
normalize nodelta
cases (leb p p') normalize nodelta
[ 1: @H2 | 2: @H1 ]
qed. 


lemma while_fresh_lift : ∀e,s,u.
   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u.
#e #s #u normalize #Hfresh_expr
elim (max_of_statement s (an_identifier SymbolTag one)) #p 
#Hfresh_p
@expr_fresh_lift
[ 2: //
| 1: @Hfresh_expr ]
qed.

(*    
theorem switch_removal_correction : ∀ge, ge', u.
  related_globals ? (λclfd.\fst (fundef_switch_removal clfd u)) ge ge' →
  ∀s1, s1', tr, s2. 
  switch_state_sim s1 s1' →
  exec_step ge s1 = Value … 〈tr,s2〉 →
  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
#ge #ge' #u #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
inversion Hsim_state
[ 1: (* regular state *)
  #uf #us #uk #f #s #k #k' #e #m #Huf_fresh #Hus_fresh #Huk_fresh #Hsim_cont #Hs1_eq #Hs1_eq' #_
  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
  cases s in Hus_fresh;
  (* Perform the intros for the statements*)
  [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
  | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
  | 14: #lab | 15: #cost #body ]
  #Hus_fresh
  [ 1: (* Skip *)
    whd in match (sw_rem ??);
    inversion Hsim_cont normalize nodelta
    [ 1: #Hk #Hk' #_ #Hexec_step
         @(eventually_base … (Returnstate Vundef Kstop (free_list m (blocks_of_env e))))
         [ 1: whd in match (exec_step ??); >fn_return_simplify ]
         cases (fn_return f) in Hexec_step;
         [ 1,10: | 2,11: #sz #sg | 3,12: #fsz | 4,13: #rg #ptr_ty | 5,14: #rg #array_ty #array_sz | 6,15: #domain #codomain
         | 7,16: #structname #fieldspec | 8,17: #unionname #fieldspec | 9,18: #rg #id ]
         normalize nodelta
         [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H) // %3 destruct //
         | *: #H destruct (H) ]
    | 2: #s0 #k0 #k0' #us0 #Hus0_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
         whd in match (ret ??) in Heq; destruct (Heq)
         @(eventually_now ????) whd in match (exec_step ??);
         %{(State (\fst  (function_switch_removal f uf)) (sw_rem s0 us0) k0' e m)} @conj try //
         %1{uf us0 uk} //
         >Hk in Huk_fresh; whd in match (fresh_for_continuation ??); >Hk'
         whd in ⊢ (% → ?); * #_ //
    | 3: #e0 #s0 #k0 #k0' #us0 #Hus0_freshexpr #Hus0_freshstm #Hsim_cont #_ #Hk #Hk' #_ #Heq
         @(eventually_now ????) whd in match (exec_step ??);
         whd in match (ret ??) in Heq; destruct (Heq)
         %{(State (\fst  (function_switch_removal f uf)) (Swhile e0 (sw_rem s0 us0)) k0' e m)} @conj try //
         >while_commute %1{uf us0 uk} //
         [ 1: @while_fresh_lift assumption
         | 2: >Hk' in Huk_fresh; whd in ⊢ (% → ?); * #_ // ]
    | 4: #eO #s0 #k0 #k0' #us0 #Hus0_freshexpr #Hus0_freshstm #Hsim_cont #_ #Hk #Hk' #_ #Heq
         @(eventually_now ????) whd in match (exec_step ??);
 
         
         
         [ 1: @uk
         | 2: >Hk in Huk_fresh; whd in match (fresh_for_continuation ??); * * // ]
                  
         whd
         normalize
         
         cut (Swhile e0 (sw_rem s0 us0) = (sw_rem (Swhile e0 s0) us0))
         [ 1: whd in match (sw_rem (Swhile ??) ?);
              whd in match (switch_removal ??);
         whd in match (exec_step ??);

(* foireux pour le (Expr (Econst_int sz n) ?) *)
lemma convert :
∀uv. 
  ∀sz,n,sl. 
    seq_of_labeled_statements (select_switch sz n sl)
    ~~~u
    let 〈exit_label, uv1〉            ≝ fresh ? uv in    
    let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list sl ? uv1 [ ] in    
    Ssequence (pi1 … (produce_cond2 (Expr (Econst_int sz n)) sl defcase exit_label)) (Slabel exit_label Sskip)
    

lemma convert :
∀f,cond,ls,k,ge,e,m.
  ∀t.
    ∀sz,n. exec_step ge (State f (Sswitch cond ls) k e m) = Value ??? 〈t,State f (seq_of_labeled_statement (select_switch sz n ls)) (Kswitch k) e m〉 →
    ∀uf,us.
     fresh_for_function f uf →
     fresh_for_statement (Sswitch cond ls) us →   
    ∃s',k'.
     (exec_plus ge 
        E0 (State (\fst (function_switch_removal f uf)) (sw_rem (Sswitch cond ls) us) k' e m)
        t s')
     ∧ switch_cont_sim k k'
     ∧ switch_state_sim 
        (State f (seq_of_labeled_statement (select_switch sz n ls)) (Kswitch k) e m)
        s'.
#f #cond #ls #k #ge #e #m #t #sz #n #Hexec #uf #us #Huf #Hus
whd in match (sw_rem ??);
whd in match (switch_removal ??);
check eq_ind



whd in Hexec:(??%?); cases (exec_expr ge e m cond) in Hexec;
[ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd) ]
* #cond_val #cond_trace 
whd in match (bindIO ??????);
cases cond_val
[ 1: | 2: #sz' #n' | 3: #fl | 4: #rg | 5: #ptr ]
[ 1,3,4,5: #Habsurd normalize in Habsurd; destruct (Habsurd) ]
normalize nodelta #Heq whd in match (ret ??) in Heq;


    
    
      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
      match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
                    | _ ⇒ Wrong ??? (msg TypeMismatch) ]    

theorem step_with_labels : ∀ge,ge'.
  related_globals ? label_fundef ge ge' →
  state_with_labels s1 s1' →
  exec_expr ge en m e = OK ? 〈Vint sz v, tr〉 →
  (seq_of_labeled_statement (select_switch sz n sl) ~ simplify_switch 
  (exec_step ge st (Sswitch e ls)
  
  
   ∃tr',s2'. plus ge' s1' tr' s2' ∧
             trace_with_extra_labels tr tr' ∧
             state_with_labels s2 s2').


*)