diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2010-04-18 20:06:15 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2010-04-18 20:06:15 -0400 |
| commit | a4b12519973682177c23c387b663d55a51dacab0 (patch) | |
| tree | 348dd7b2ae7aa945f31445b229a9a6c84dc3b7c7 | |
| parent | b791d89df86efa83df863a9a5ac4e4e7dab0efc8 (diff) | |
Avoid state space explosion with ECase that just writes a constant in each case
| -rw-r--r-- | src/iflow.sml | 34 |
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 => |