Changeset 3562 for LTS/variable.ma

Timestamp:

Jun 16, 2015, 3:19:27 PM (4 years ago)

Author:

piccolo

Message:

 

File:

• LTS/variable.ma (modified) (2 diffs)

LTS/variable.ma

@@ -70 +70 @@
 λi,s.match i with
 [sNop ⇒ Some ? s
-|sAss v e ⇒ match (\fst s) with
-  [nil⇒ None ?
-  |cons hd tl⇒ let 〈env,var〉 ≝ hd in
-               ! n ← frame_sem_expr env e;
-               frame_assign_var s v n
-  ]
+|sAss v e ⇒ !env ← frame_current_env … s;
+            ! n ← frame_sem_expr env e;
+            frame_assign_var s v n
 ].
 
@@ -94 +91 @@
 λsgn,e,st.
     let 〈var,act_exp〉 ≝ e in
-    match (\fst st) with
-    [nil ⇒ None ?
-    |cons hd tl⇒ let 〈env,v〉≝ hd in
-                 !n ← frame_sem_expr env act_exp;
-                 frame_assign_var 〈(〈(nil ?),var〉::(\fst st)),(\snd st)〉 O n
-  ].
+    !env ← frame_current_env … st;
+    !n ← frame_sem_expr env act_exp;
+    frame_assign_var 〈(〈(nil ?),var〉::(\fst st)),(\snd st)〉 O n.
 
 definition frame_return_call:(return_type frame_state_params)→ frame_store_t→ (option frame_store_t)≝