include "Clight/Csyntax.ma".
include "Clight/fresh.ma".
include "basics/lists/list.ma".

(* This file implements transformation of switches to linear, nested 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). /!\ *)

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

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.

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

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.

(* We assume that the expression e is consistely typed w.r.t. the switch branches *)

alias id "bvzero" = "cic:/matita/cerco/ASM/BitVector/zero.def(2)".

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.

(* 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_cond 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)
  (vars : list (ident × type)) 
  (uv : universe SymbolTag) : (Σresult.switch_free result) × (list (ident × type)) × (universe SymbolTag) ≝
match st return λs.s = st → ? with
[ Sskip       ⇒ λEq. 〈«st,?», vars, uv〉
| Sassign _ _ ⇒ λEq. 〈«st,?», vars, uv〉
| Scall _ _ _ ⇒ λEq. 〈«st,?», vars, uv〉
| Ssequence s1 s2 ⇒ λEq. 
  let 〈s1', vars1, uv'〉  ≝ switch_removal s1 vars uv in
  let 〈s2', vars2, uv''〉 ≝ switch_removal s2 vars1 uv' in
  〈«Ssequence (pi1 … s1') (pi1 … s2'),?», vars2, uv''〉
| Sifthenelse e s1 s2 ⇒ λEq. 
  let 〈s1', vars1, uv'〉  ≝ switch_removal s1 vars uv in
  let 〈s2', vars2, uv''〉 ≝ switch_removal s2 vars1 uv' in
  〈«Sifthenelse e (pi1 … s1') (pi1 … s2'),?», vars2, uv''〉
| Swhile e body ⇒ λEq.
  let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in
  〈«Swhile e (pi1 … body'),?», vars', uv'〉 
| Sdowhile e body ⇒ λEq.
  let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in
  〈«Sdowhile e (pi1 … body'),?», vars', uv'〉 
| Sfor s1 e s2 s3 ⇒ λEq.
  let 〈s1', vars1, uv'〉   ≝ switch_removal s1 vars uv in
  let 〈s2', vars2, uv''〉  ≝ switch_removal s2 vars1 uv' in
  let 〈s3', vars3, uv'''〉 ≝ switch_removal s3 vars2 uv'' in  
  〈«Sfor (pi1 … s1') e (pi1 … s2') (pi1 … s3'),?», vars3, uv'''〉  
| Sbreak ⇒ λEq.
  〈«st,?», vars, uv〉
| Scontinue ⇒ λEq.
  〈«st,?», vars, uv〉
| Sreturn _ ⇒ λEq.
  〈«st,?», vars, uv〉
| Sswitch e branches ⇒ λEq.
   let 〈sf_branches, vars', uv1〉 ≝ switch_removal_branches branches vars 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 vars uv in
  〈«Slabel label (pi1 … body'), ?», vars', uv'〉
| Sgoto _ ⇒ λEq.
  〈«st, ?», vars, uv〉
| Scost cost body ⇒ λEq.
  let 〈body', vars', uv'〉 ≝ switch_removal body vars uv in
  〈«Scost cost (pi1 … body'),?», vars', uv'〉 
] (refl ? st)

and switch_removal_branches 
  (l : labeled_statements) 
  (vars : list (ident × type)) 
  (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 vars uv in
  〈«LSdefault (pi1 … st), ?», vars', uv'〉
| LScase sz int st tl =>
  let 〈tl_result, vars', uv'〉 ≝ switch_removal_branches tl vars uv in
  let 〈st', vars'', uv''〉     ≝ switch_removal st vars' uv' in 
  〈«LScase sz int st' (pi1 … tl_result), ?», 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.

let rec program_switch_removal (p : clight_program) : clight_program ≝
 let uv         ≝ universe_for_program 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
    match fun_def with
    [ CL_Internal func ⇒
      let 〈body', fun_vars, uv2〉 ≝ switch_removal (fn_body func) (fn_vars func) uv1 in
      let new_func ≝ mk_function (fn_return func) (fn_params func) fun_vars (pi1 … body') in
      〈(〈fun_id, CL_Internal new_func〉 :: fundefs), uv2〉
    | CL_External _ _ _ ⇒ 
      〈cl_fundef :: fundefs, uv1〉
    ]
   ) 〈[ ], uv〉 prog_funcs 
 in 
 mk_program ??
  (prog_vars … p)
  sf_funcs
  (prog_main … p)
.