Changeset 3562 for LTS/variable.ma


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

Legend:

Unmodified
Added
Removed
  • 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)≝
Note: See TracChangeset for help on using the changeset viewer.