(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "Simulation.ma".
include "common_variable_stack.ma".

definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝ 
λA,B,f,a,b,x.if x == a then b else f x.



let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝ 
match e with
[ Var v ⇒ Var (map v)
| Const n ⇒ Const n
| Plus e1 e2 ⇒ Plus (map_exp e1 map) (map_exp e2 map) 
| Minus e1 e2 ⇒ Minus (map_exp e1 map) (map_exp e2 map)
].

let rec map_cond (c : condition) (map : variable → variable) on c : condition ≝ 
match c with
[Eq e1 e2 ⇒ Eq (map_exp e1 map) (map_exp e2 map)
| Not c1 ⇒ Not (map_cond c1 map)
].

definition map_seq ≝
 λi,map.
  match i with
  [ sAss v e ⇒ Seq_i (sAss (map v) (map_exp e map))
  ].

let rec trans_imp_instr (i : imp_Instructions) (map : variable → variable) on i : frame_Instructions  ≝ 
match i with
[ EMPTY ⇒ EMPTY …
| RETURN rt ⇒ RETURN … rt
| SEQ seq opt_l i ⇒ SEQ … (map_seq seq map) opt_l (trans_imp_instr i map)
| COND cond ltrue i_true lfalse i_false instr ⇒ 
    COND frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse (trans_imp_instr i_false map) 
           (trans_imp_instr instr map)
| LOOP cond ltrue i_true lfalse instr ⇒ 
    LOOP frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse  
           (trans_imp_instr instr map)
| CALL f act_p opt_l instr ⇒
    (CALL frame_state_params flat_labels f (map_exp (\snd act_p) map) opt_l
      (SEQ … (PopReg (\fst act_p)) (None …) (trans_imp_instr instr map)))
| IO lin io lout instr ⇒ ?
].
cases io qed.


definition environment_rel : (variable → variable) → environment → activation_frame → Prop ≝ 
λmap,st1,st2.
 All … (λx.let 〈v,val〉 ≝ x in read_frame … st2 (to_shift + (map v)) O = return val)
  st1.

definition store_rel : (variable → variable) → store_t → frame_store_t → Prop ≝ 
λmap,st1,st2.
All2 ?? (λel1,el2.environment_rel map (\fst el1) el2)
 st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.

lemma store_rel_inv:
 ∀m,env,var,l,st.
  store_rel m (〈env,var〉::l) st →
   ∃hd,tl,fpsp.
    st = 〈hd::tl,fpsp〉 ∧
     store_rel m l 〈tl,fpsp〉 ∧
      environment_rel m env hd.
 #m #env #var #l * #xx #fpsp * whd in ⊢ (% → ?); cases xx [*] normalize nodelta
 #frame #frames * #Rel1 #ALL #EQ destruct (skip fpsp)
 %{frame} %{frames} %{fpsp} % // % // % //
qed.

definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels → 
Program frame_env_params frame_instr_params flat_labels ≝ λmap,prog.
mk_Program ??? 
(foldr … 
   (λx,tail.(mk_env_item …
               (mk_signature frame_env_params … (f_name … (f_sig … x)) 14 ?(*(f_ret …(f_sig … x))*))
               (f_lab … x) (trans_imp_instr (f_body ? imp_instr_params ? x) map)) :: tail) (nil ?) (env … prog))
(trans_imp_instr (main … prog) map).
@(f_ret … (f_sig … x))
qed.

definition trans_imp_cont ≝
 λmap,cont.
  foldr … (λx:(ActionLabel flat_labels)×?.λrem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) cont.

definition imp_variable_pass_rel ≝  
λmap : variable → variable.
λprog : Program imp_state_params imp_state_params imp_state_params.
let t_prog ≝ trans_imp_prog map prog in
mk_relations flat_labels (operational_semantics imp_state_params imp_sem_state_params prog)
 (operational_semantics frame_state_params frame_sem_state_params t_prog) 
(λs1,s2.store_rel map (store … s1) (store … s2) ∧ code … s2 = trans_imp_instr (code … s1) map ∧  
cont … s2 = trans_imp_cont map (cont … s1))
(λ_.λ_.True).

lemma map_exp_ok:
 ∀m: variable → variable.
  ∀e: expr.
  let e' ≝ map_exp e m in
   ∀env: environment.
    ∀env': activation_frame.
     environment_rel m env env' →
      ∀val.
       sem_expr env e = Some … val →
        frame_sem_expr env' e' = Some … val.
 #m #e elim e
 [ #v #env elim env
   [ #env' #_ #val #abs normalize in abs; destruct
   | * #var #val #tl #IH #env' * #RF #Htl #val'
     whd in ⊢ (??%? → ?); inversion (?==?) #Hv_var normalize nodelta
     [ #Hval_val' destruct >(\P Hv_var) assumption
     | #Hread_tl @IH // assumption ]]
 | normalize //
 |*: #e1 #e2 #IH1 #IH2 #env #env' #Rel #v
   change with (m_bind ?????) in match (sem_expr ??);
   #H cases (bind_inversion ????? H) -H #v1 * #He1
   #H cases (bind_inversion ????? H) -H #v2 * #He2
   #H normalize in H; destruct
   change with (m_bind ?????) in ⊢ (??%?);
   >(IH1 … He1) // >(IH2 … He2) // ]
qed.

lemma map_cond_ok:
 ∀m: variable → variable.
  ∀e: condition.
  let e' ≝ map_cond e m in
   ∀env: environment.
    ∀env': activation_frame.
     environment_rel m env env' →
      ∀val.
       sem_condition env e = Some … val →
        frame_sem_condition env' e' = Some … val.
 #m #e elim e
 [ #e1 #e2 #env #env' #Rel #v
   change with (m_bind ?????) in ⊢ (??%? → ?);
   #H cases (bind_inversion ????? H) -H #v1 * #He1
   #H cases (bind_inversion ????? H) -H #v2 * #He2
   #H normalize in H; destruct
   change with (m_bind ?????) in ⊢ (??%?);
   >(map_exp_ok … He1) // >(map_exp_ok … He2) //
 | #c #IH #env #env' #Rel #v
   change with (m_bind ?????) in ⊢ (??%? → ?);
   #H cases (bind_inversion ????? H) -H #v' * #Hv'
   #H normalize in H; destruct
   change with (m_bind ?????) in ⊢ (??%?);
   >(IH … Hv') // ]
qed.

lemma map_assign_ok:
 ∀m,env,frame,v,val,env'.
  environment_rel m env frame →
   assign_frame frame (to_shift + m v) 0 val = return env' →
   environment_rel m (assign env v val) env'.
 #m #env #frame #v #val
 elim env
 [ #env' #_ #H % // @(read_frame_assign_frame_hit … H)
 | * #v' #val' #frames #IH #env' * #Hread #Hall
   change with (environment_rel ???) in Hall;
   whd in match (assign ???);
   inversion (v==v') normalize nodelta
   [2: #Ineq #H %
      [ <Hread @(read_frame_assign_frame_miss … H)
        [ cases daemon
        | cases daemon
        | @(not_to_not ??? (\Pf Ineq)) -Ineq #H
          cases daemon (* MANCA INIETTIVITA' DELLA M *)
        ]
      | @IH // ]
   | #EQ #H %
     [ @(read_frame_assign_frame_hit … H) 
     |change with (environment_rel ???)
      cases daemon (* NOT IMPLIED BY Hall BECAUSE OF DUPLICATES :-( *)]]]
qed.

lemma map_assign_var_ok:
 ∀m,env,var,tl,v,val,frame,frames,st2,fpsp.
 store_rel m tl 〈frames,fpsp〉 →
 environment_rel m env frame →
  assign_var (〈env,var〉::tl) v val = Some … st2 →
   ∃st2'.
    frame_assign_var 〈frame::frames,fpsp〉 (m v) val = Some … st2' ∧
     store_rel m st2 st2'.
     cases daemon (* si è rotto!!!
 #m #env #var #tl #v #val #frame #frames #st2 #fpsp #Rel1 #Rel2
 whd in ⊢ (??%? → ?); #EQ destruct
 whd in match frame_assign_var; normalize nodelta % [2: % [%] | skip]
 cases Rel1 -Rel1 #Rel3 #Rel4 destruct % // whd /6/ *)
qed.

lemma map_seq_ok:
 ∀m: variable → variable.
  ∀e:seq_i.
  let e' ≝ map_seq e m in
   ∀st1.
    ∀st1'.
     store_rel m st1 st1' →
      ∀st2.
       imp_eval_seq e st1 = Some … st2 →
        ∃st2'.
         frame_eval_seq e' st1' = Some … st2' ∧
          store_rel m st2 st2'.
 #m * [2: #v #expr] #st1 * #st1' * #fp #sp #Rel #st2
 whd in match imp_eval_seq; normalize nodelta
 [2: #EQ destruct /3/
 | cases st1 in Rel; normalize nodelta [ #_ #abs destruct ]
   * #env #var #tl #Rel
   cases (store_rel_inv … Rel) -Rel #frame * #frames * #fpsp ** #EQ destruct
   #Rel1 #Rel2 normalize nodelta #H cases (bind_inversion ????? H) -H #val *
   #Hval #H whd in match (frame_eval_seq ??); >(map_exp_ok … Rel2 … Hval)
   normalize nodelta cases (map_assign_var_ok … Rel1 Rel2 … H) #st2' *
   #H1 #H2 %{st2'} % // assumption ]
qed.

definition simulation_imp_frame ≝ 
λprog : Program imp_state_params imp_state_params imp_state_params.
λmap : variable → variable.
λprf : All … (λx.map (f_pars imp_state_params imp_state_params (f_sig … x)) = O) (env … prog).
mk_simulation_conditions … (imp_variable_pass_rel map prog) ???????????.
[ #s1 #s2 ** #H1 #H2 #H3 whd in match (as_initial ???); (*store iniziali in relazione*) cases daemon
| cases daemon
| cases daemon
| #s1 #s2 #s1' #H inversion H
  [ #s11 #s22 * #act #instr #cont #EQcode_s11 #EQcont_s11 #EQ #EQ1 destruct #EQstore #Hio1 #Hio2
    #act_no_ret #EQ1 #EQ2 #EQ3 destruct #_ ** #Hstore #EQcode #EQcont #_ #_
    %{(mk_state … (trans_imp_instr (code … s22) map)
      (trans_imp_cont map (cont … s22)) (store … s2) (io_info … s22))}
    %{(t_ind … (t_base …))} 
    [2: @(cost_act … (None ?)) 
    | @hide_prf whd applyS(empty)
      [9: >EQcode >EQcode_s11 %
      |2: normalize % *
      |3: %
      |4: cases daemon (*da mettere a posto io *)
    |5: % |6: % |7: % |8: >EQcont >EQcont_s11 % |*:]
    | % [ % // % // ] %1 %2 [cases daemon] %1 cases daemon
    ]
  |*: cases daemon  
  ]
|*: cases daemon
]
qed.