summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-04-18 20:06:15 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-04-18 20:06:15 -0400
commita4b12519973682177c23c387b663d55a51dacab0 (patch)
tree348dd7b2ae7aa945f31445b229a9a6c84dc3b7c7
parentb791d89df86efa83df863a9a5ac4e4e7dab0efc8 (diff)
Avoid state space explosion with ECase that just writes a constant in each case
-rw-r--r--src/iflow.sml34
1 files changed, 18 insertions, 16 deletions
diff --git a/src/iflow.sml b/src/iflow.sml
index 1b20f0d1..87103aeb 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -1878,22 +1878,24 @@ fun evalExp env (e as (_, loc)) k =
| EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
| ECase (e, pes, {result = res, ...}) =>
evalExp env e (fn e =>
- let
- val () = St.addPath (e, loc)
- in
- app (fn (p, pe) =>
- let
- val saved = St.stash ()
- in
- let
- val env = evalPat env e p
- in
- evalExp env pe k;
- St.reinstate saved
- end
- handle Cc.Contradiction => St.reinstate saved
- end) pes
- end)
+ if List.all (fn (_, (EWrite (EPrim _, _), _)) => true
+ | _ => false) pes then
+ (St.send true (e, loc);
+ k (Recd []))
+ else
+ (St.addPath (e, loc);
+ app (fn (p, pe) =>
+ let
+ val saved = St.stash ()
+ in
+ let
+ val env = evalPat env e p
+ in
+ evalExp env pe k;
+ St.reinstate saved
+ end
+ handle Cc.Contradiction => St.reinstate saved
+ end) pes))
| EStrcat (e1, e2) =>
evalExp env e1 (fn e1 =>
evalExp env e2 (fn e2 =>