Ignore:
Timestamp:
Jun 16, 2015, 7:12:52 PM (4 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/frame_variable_pass.ma

    r3563 r3564  
    2222let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝
    2323match e with
    24 [  Var v ⇒ Var (map v)
     24[ Var v ⇒ Var (map v)
    2525| Const n ⇒ Const n
    2626| Plus e1 e2 ⇒ Plus (map_exp e1 map) (map_exp e2 map)
     
    3434].
    3535
     36definition map_seq ≝
     37 λi,map.
     38  match i with
     39  [ sNop ⇒ sNop
     40  | sAss v e ⇒ sAss (map v) (map_exp e map)
     41  ].
     42
    3643let rec trans_imp_instr (i : imp_Instructions) (map : variable → variable) on i : frame_Instructions  ≝
    3744match i with
    3845[ EMPTY ⇒ EMPTY …
    3946| RETURN rt ⇒ RETURN … rt
    40 | SEQ seq opt_l i ⇒
    41     match seq with
    42     [ sNop ⇒ SEQ … sNop opt_l (trans_imp_instr i map)
    43     | sAss v e ⇒ SEQ frame_state_params flat_labels (sAss (map v) (map_exp e map)) opt_l (trans_imp_instr i map)
    44     ]
     47| SEQ seq opt_l i ⇒ SEQ … (map_seq seq map) opt_l (trans_imp_instr i map)
    4548| COND cond ltrue i_true lfalse i_false instr ⇒
    4649    COND frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse (trans_imp_instr i_false map)
     
    7275 st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.
    7376
     77lemma store_rel_inv:
     78 ∀m,env,var,l,st.
     79  store_rel m (〈env,var〉::l) st →
     80   ∃hd,tl,fpsp.
     81    st = 〈〈hd,var〉::tl,fpsp〉 ∧
     82     store_rel m l 〈tl,fpsp〉 ∧
     83      environment_rel m env hd.
     84 #m #env #var #l * #env #fpsp * whd in ⊢ (% → ?); cases env [*] normalize nodelta
     85 * #frame #var' #frames ** #EQ destruct #Rel #ALL #FPSP
     86 %{frame} %{frames} %{fpsp} % // % // % //
     87qed.
     88
    7489definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels →
    7590Program frame_env_params imp_instr_params flat_labels ≝ λmap,prog.
     
    8196(trans_imp_instr (main … prog) map).
    8297
     98definition trans_imp_cont ≝
     99 λmap,cont.
     100  foldr … (λx:(ActionLabel flat_labels)×?.λrem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) cont.
     101
    83102definition imp_variable_pass_rel ≝ 
    84103λmap : variable → variable.
     
    88107 (operational_semantics frame_state_params frame_sem_state_params t_prog)
    89108(λs1,s2.store_rel map (store … s1) (store … s2) ∧ code … s2 = trans_imp_instr (code … s1) map ∧ 
    90 cont … s2 = foldr … (λx,rem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) (cont … s1))
     109cont … s2 = trans_imp_cont map (cont … s1))
    91110(λ_.λ_.True).
    92111
    93 lemma eval_cond_ok:
     112lemma map_exp_ok:
    94113 ∀m: variable → variable.
    95114  ∀e: expr.
     
    110129 | normalize //
    111130 |*: #e1 #e2 #IH1 #IH2 #env #env' #Rel #v
    112    change with (!x ← ?; ? = return ?) in match (sem_expr ?? = Some ??);
     131   change with (m_bind ?????) in match (sem_expr ??);
    113132   #H cases (bind_inversion ????? H) -H #v1 * #He1
    114133   #H cases (bind_inversion ????? H) -H #v2 * #He2
     
    118137qed.
    119138
     139lemma map_cond_ok:
     140 ∀m: variable → variable.
     141  ∀e: condition.
     142  let e' ≝ map_cond e m in
     143   ∀env: environment.
     144    ∀env': activation_frame.
     145     environment_rel m env env' →
     146      ∀val.
     147       sem_condition env e = Some … val →
     148        frame_sem_condition env' e' = Some … val.
     149 #m #e elim e
     150 [ #e1 #e2 #env #env' #Rel #v
     151   change with (m_bind ?????) in ⊢ (??%? → ?);
     152   #H cases (bind_inversion ????? H) -H #v1 * #He1
     153   #H cases (bind_inversion ????? H) -H #v2 * #He2
     154   #H normalize in H; destruct
     155   change with (m_bind ?????) in ⊢ (??%?);
     156   >(map_exp_ok … He1) // >(map_exp_ok … He2) //
     157 | #c #IH #env #env' #Rel #v
     158   change with (m_bind ?????) in ⊢ (??%? → ?);
     159   #H cases (bind_inversion ????? H) -H #v' * #Hv'
     160   #H normalize in H; destruct
     161   change with (m_bind ?????) in ⊢ (??%?);
     162   >(IH … Hv') // ]
     163qed.
     164
     165lemma map_assign_ok:
     166 ∀m,env,frame,v,val.
     167  environment_rel m env frame →
     168   environment_rel m (assign env v val) (assign_frame frame (m v) 0 val).
     169 #m #env #frame #v #val #Rel whd in match assign_frame; normalize nodelta
     170 elim env in Rel;
     171 [ * % // whd in ⊢ (??%?); cases daemon (* NTH-UPDATE *)
     172 | * #v' #val' #frames #IH * #Hread #Hall change with (environment_rel ???) in Hall;
     173   whd in match (assign ???);
     174   inversion (v==v') normalize nodelta
     175   [2: #Ineq % [ cases daemon (* NTH-UPDATE *) | @IH // ]
     176   | #EQ % [ cases daemon (* NTH-UPDATE *)
     177   |change with (environment_rel ???) cases daemon (* NOT IMPLIED BY Hall BECAUSE
     178    OF DUPLICATES :-( *)]]]
     179qed.
     180
     181lemma map_assign_var_ok:
     182 ∀m,env,var,tl,v,val,frame,frames,st2,fpsp.
     183 store_rel m tl 〈frames,fpsp〉 →
     184 environment_rel m env frame →
     185  assign_var (〈env,var〉::tl) v val = Some … st2 →
     186   ∃st2'.
     187    frame_assign_var 〈〈frame,var〉::frames,fpsp〉 (m v) val = Some … st2' ∧
     188     store_rel m st2 st2'.
     189 #m #env #var #tl #v #val #frame #frames #st2 #fpsp #Rel1 #Rel2
     190 whd in ⊢ (??%? → ?); #EQ destruct
     191 whd in match frame_assign_var; normalize nodelta % [2: % [%] | skip]
     192 cases Rel1 -Rel1 #Rel3 #Rel4 destruct % // whd /6/
     193qed.
     194
     195lemma map_seq_ok:
     196 ∀m: variable → variable.
     197  ∀e:seq_i.
     198  let e' ≝ map_seq e m in
     199   ∀st1.
     200    ∀st1'.
     201     store_rel m st1 st1' →
     202      ∀st2.
     203       imp_eval_seq e st1 = Some … st2 →
     204        ∃st2'.
     205         frame_eval_seq e' st1' = Some … st2' ∧
     206          store_rel m st2 st2'.
     207 #m * [2: #v #expr] #st1 * #st1' * #fp #sp #Rel #st2
     208 whd in match imp_eval_seq; normalize nodelta
     209 [2: #EQ destruct /3/
     210 | cases st1 in Rel; normalize nodelta [ #_ #abs destruct ]
     211   * #env #var #tl #Rel
     212   cases (store_rel_inv … Rel) -Rel #frame * #frames * #fpsp ** #EQ destruct
     213   #Rel1 #Rel2 normalize nodelta #H cases (bind_inversion ????? H) -H #val *
     214   #Hval #H whd in match (frame_eval_seq ??); >(map_exp_ok … Rel2 … Hval)
     215   normalize nodelta cases (map_assign_var_ok … Rel1 Rel2 … H) #st2' *
     216   #H1 #H2 %{st2'} % // assumption ]
     217qed.
     218
    120219definition simulation_imp_frame ≝
    121220λprog : Program imp_state_params imp_state_params imp_state_params.
     
    123222λprf : All … (λx.map (f_pars imp_state_params imp_state_params (f_sig … x)) = O) (env … prog).
    124223mk_simulation_conditions … (imp_variable_pass_rel map prog) ???????????.
    125 cases daemon (*TODO*)
    126 qed.
    127 
    128 (*
    129224[ #s1 #s2 ** #H1 #H2 #H3 whd in match (as_initial ???); (*store iniziali in relazione*) cases daemon
    130225| cases daemon
     
    133228  [ #s11 #s22 * #act #instr #cont #EQcode_s11 #EQcont_s11 #EQ #EQ1 destruct #EQstore #Hio1 #Hio2
    134229    #act_no_ret #EQ1 #EQ2 #EQ3 destruct #_ ** #Hstore #EQcode #EQcont #_ #_
    135     %{(mk_state … (code … s22) (cont … s22) (store … s2) (io_info … s22))}
     230    %{(mk_state … (trans_imp_instr (code … s22) map)
     231      (trans_imp_cont map (cont … s22)) (store … s2) (io_info … s22))}
    136232    %{(t_ind … (t_base …))}
    137233    [2: @(cost_act … (None ?))
    138     | @hide_prf whd applyS(empty) [9: <EQcode assumption |2: normalize % * |3: % |4: cases daemon (*da mettere a posto io *)
    139     |5: % |6: % |7: % |8: <EQcont assumption |*:]
     234    | @hide_prf whd applyS(empty)
     235      [9: >EQcode >EQcode_s11 %
     236      |2: normalize % *
     237      |3: %
     238      |4: cases daemon (*da mettere a posto io *)
     239    |5: % |6: % |7: % |8: >EQcont >EQcont_s11 % |*:]
    140240    | % [ % // % // ] %1 %2 [cases daemon] %1 cases daemon
    141241    ]
     
    144244|*: cases daemon
    145245]
    146 qed.*)
    147    
    148    
     246qed.
Note: See TracChangeset for help on using the changeset viewer.