Changeset 3562


Ignore:
Timestamp:
Jun 16, 2015, 3:19:27 PM (4 years ago)
Author:
piccolo
Message:
 
Location:
LTS
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • LTS/stack.ma

    r3560 r3562  
    8282
    8383definition stack_state_params:state_params≝
    84 mk_state_params stack_instr_params imp_env_params flat_labels frame_store_t (*DeqEnv*).
     84mk_state_params stack_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
    8585
    8686definition push : (store_type stack_state_params) → DeqNat → option (store_type stack_state_params) ≝
     
    131131  [ mk_signature fun fpt rt ⇒
    132132    !〈n,st1〉 ← pop st;
    133     frame_assign_var 〈(〈(nil ?),var〉::(\fst st1)),(\snd st1)〉 fpt n
     133    frame_assign_var 〈(〈(nil ?),var〉::(\fst st1)),(\snd st1)〉 O n
    134134  ].
    135135
     
    154154
    155155
    156 definition stack_envitem≝ (env_item imp_env_params stack_instr_params flat_labels).
     156definition stack_envitem≝ (env_item frame_env_params stack_instr_params flat_labels).
  • LTS/variable.ma

    r3561 r3562  
    7070λi,s.match i with
    7171[sNop ⇒ Some ? s
    72 |sAss v e ⇒ match (\fst s) with
    73   [nil⇒ None ?
    74   |cons hd tl⇒ let 〈env,var〉 ≝ hd in
    75                ! n ← frame_sem_expr env e;
    76                frame_assign_var s v n
    77   ]
     72|sAss v e ⇒ !env ← frame_current_env … s;
     73            ! n ← frame_sem_expr env e;
     74            frame_assign_var s v n
    7875].
    7976
     
    9491λsgn,e,st.
    9592    let 〈var,act_exp〉 ≝ e in
    96     match (\fst st) with
    97     [nil ⇒ None ?
    98     |cons hd tl⇒ let 〈env,v〉≝ hd in
    99                  !n ← frame_sem_expr env act_exp;
    100                  frame_assign_var 〈(〈(nil ?),var〉::(\fst st)),(\snd st)〉 O n
    101   ].
     93    !env ← frame_current_env … st;
     94    !n ← frame_sem_expr env act_exp;
     95    frame_assign_var 〈(〈(nil ?),var〉::(\fst st)),(\snd st)〉 O n.
    10296
    10397definition frame_return_call:(return_type frame_state_params)→ frame_store_t→ (option frame_store_t)≝
  • LTS/variable_stack_pass.ma

    r3560 r3562  
    5353qed.
    5454
    55 definition trans_var_prog : Program imp_env_params imp_instr_params flat_labels →
    56 Program imp_env_params stack_instr_params flat_labels ≝ λprog.
     55definition trans_var_prog : Program frame_env_params imp_instr_params flat_labels →
     56Program frame_env_params stack_instr_params flat_labels ≝ λprog.
    5757mk_Program …
    5858(foldr … (λx,tail.(mk_env_item …
     
    6161(trans_var_instr … (main … prog)).
    6262
     63include "Simulation.ma".
     64
     65definition frame_variable_pass_rel ≝ 
     66λprog : Program frame_state_params frame_state_params frame_state_params.
     67let t_prog ≝ trans_var_prog prog in
     68mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
     69 (operational_semantics stack_state_params stack_sem_state_params t_prog)
     70 (λs1,s2.store … s1 = store … s2 ∧ code … s2 = trans_var_instr (code … s1) ∧
     71         cont … s2 = foldr … (λx,tail. 〈(\fst x),trans_var_instr (\snd x)〉 :: tail) (nil ?) (cont … s1))
     72 (λ_.λ_.True).
     73
     74
     75lemma eval_exp_ok : ∀env:activation_frame.∀e: expr.∀n.
     76frame_sem_expr env e = return n →
     77∃st'.
     78m_fold Option … eval_combinators (trans_expr e)  = return st' ∧
     79
     80 
     81definition simulation_imp_frame ≝
     82λprog : Program frame_state_params frame_state_params frame_state_params.
     83mk_simulation_conditions … (frame_variable_pass_rel prog) ???????????.
     84cases daemon
     85qed.
     86 
Note: See TracChangeset for help on using the changeset viewer.