changeset 1248:cf9a636f9b15

Avoid state space explosion with ECase that just writes a constant in each case
author Adam Chlipala <adamc@hcoop.net>
date Sun, 18 Apr 2010 20:06:15 -0400 (2010-04-19)
parents 0c643f51fbc0
children 7c6fc92f6c31
files src/iflow.sml
diffstat 1 files changed, 18 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/iflow.sml	Sun Apr 18 15:54:37 2010 -0400
+++ b/src/iflow.sml	Sun Apr 18 20:06:15 2010 -0400
@@ -1878,22 +1878,24 @@
           | 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 =>