(**************************************************************************) (* ___ *) (* ||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 % [ (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.