Changeset 3376


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Imp.ma

    r3375 r3376  
    6666
    6767definition state: storeT → Type[0] ≝ λS.
    68  cmd × continuation × ((list (ident × (option label) × continuation)) × S).
     68 cmd × continuation × ((list (nat × ident × ((option label) × continuation))) × S).
    6969
    7070definition fetchT ≝ fname → cmd.
     
    116116   step …
    117117    〈Ccall x f e l, k, K, s〉
    118     〈c, [], 〈x,l,k〉::K, set ? s (None …) (eval_expr ? s e)〉
     118    〈c, [], 〈get ? s (None …),x,l,k〉::K, set ? s (None …) (eval_expr ? s e)〉
    119119    (Some … f)
    120 | step_return: ∀e,k1,x,l,k2,K,s.
     120| step_return: ∀e,k1,v,x,l,k2,K,s.
    121121   step …
    122     〈Cret e, k1, 〈x,l,k2〉::K, s〉
    123     〈Cskip, k2, K, set ? s (Some … x) (eval_expr ? s e)
     122    〈Cret e, k1, 〈v,x,l,k2〉::K, s〉
     123    〈Cskip, k2, K, set ? (set ? s (Some … x) (eval_expr ? s e)) (None …) v
    124124    l.
    125125
Note: See TracChangeset for help on using the changeset viewer.