(name, rev args)
end
-fun exec evs e =
- let
- fun exec' evs (eAll as (e, _)) =
- case e of
- ESkip => SM.empty
- | ESet (ev, e) => SM.insert (SM.empty, ev, e)
- | EGet (x, ev, e) => exec' evs (Reduce.subst x (lookup (evs, ev)) e)
- | ESeq es =>
- let
- val (new, _) =
- foldl (fn (e, (new, keep)) =>
- let
- val new' = exec' keep e
- in
- (conjoin (new, new'),
- conjoin (keep, new'))
- end) (SM.empty, evs) es
- in
- new
- end
- | ELocal (e1, e2) =>
- let
- val evs' = exec' evs e1
- val evs'' = exec' (conjoin (evs, evs')) e2
- in
- conjoin (evs, evs'')
- end
- | EWith (e1, e2) =>
+fun exec' evs (eAll as (e, _)) =
+ case e of
+ ESkip => SM.empty
+ | ESet (ev, e) => SM.insert (SM.empty, ev, e)
+ | EGet (x, _, ev, e) => exec' evs (Reduce.subst x (lookup (evs, ev)) e)
+ | ESeq es =>
+ let
+ val (new, _) =
+ foldl (fn (e, (new, keep)) =>
+ let
+ val new' = exec' keep e
+ in
+ (conjoin (new, new'),
+ conjoin (keep, new'))
+ end) (SM.empty, evs) es
+ in
+ new
+ end
+ | ELocal (e1, e2) =>
+ let
+ val evs' = exec' evs e1
+ in
+ exec' (conjoin (evs, evs')) e2
+ end
+ | EWith (e1, e2) =>
+ let
+ val (prim, args) = findPrimitive e1
+ in
+ case Env.container prim of
+ NONE => raise Fail "Unbound primitive container"
+ | SOME (action, cleanup) =>
let
- val (prim, args) = findPrimitive e1
+ val evs' = action (evs, args)
+ val evs'' = exec' evs e2
in
- case Env.container prim of
- NONE => raise Fail "Unbound primitive container"
- | SOME (action, cleanup) =>
- let
- val evs' = action (evs, args)
- val evs'' = exec' evs e2
- in
- cleanup ();
- evs'
- end
+ cleanup ();
+ evs'
end
+ end
- | _ =>
- let
- val (prim, args) = findPrimitive eAll
- in
- case Env.action prim of
- NONE => raise Fail "Unbound primitive action"
- | SOME action => action (evs, args)
- end
+ | _ =>
+ let
+ val (prim, args) = findPrimitive eAll
+ in
+ case Env.action prim of
+ NONE => raise Fail "Unbound primitive action"
+ | SOME action => action (evs, args)
+ end
+fun exec evs e =
+ let
val _ = Env.pre ()
val evs' = exec' evs e
in