Changeset 3376

Timestamp:

Jul 1, 2013, 5:55:43 PM (4 years ago)

Author:

sacerdot

Message:

Semantics fixed: the value of the anonymous variable was corrupted by
function calls.

File:

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

LTS/Imp.ma

@@ -66 +66 @@
 
 definition state: storeT → Type[0] ≝ λS.
- cmd × continuation × ((list (ident × (option label) × continuation)) × S).
+ cmd × continuation × ((list (nat × ident × ((option label) × continuation))) × S).
 
 definition fetchT ≝ fname → cmd.
@@ -116 +116 @@
    step …
     〈Ccall x f e l, k, K, s〉
-    〈c, [], 〈x,l,k〉::K, set ? s (None …) (eval_expr ? s e)〉
+    〈c, [], 〈get ? s (None …),x,l,k〉::K, set ? s (None …) (eval_expr ? s e)〉
     (Some … f)
-| step_return: ∀e,k1,x,l,k2,K,s.
+| step_return: ∀e,k1,v,x,l,k2,K,s.
    step …
-    〈Cret e, k1, 〈x,l,k2〉::K, s〉
-    〈Cskip, k2, K, set ? s (Some … x) (eval_expr ? s e)〉
+    〈Cret e, k1, 〈v,x,l,k2〉::K, s〉
+    〈Cskip, k2, K, set ? (set ? s (Some … x) (eval_expr ? s e)) (None …) v〉
     l.