# HG changeset patch # User Adam Chlipala # Date 1271635575 14400 # Node ID cf9a636f9b156af475608404d2ff75e473836a0d # Parent 0c643f51fbc01303b2a883eae10394898ad3c3d6 Avoid state space explosion with ECase that just writes a constant in each case diff -r 0c643f51fbc0 -r cf9a636f9b15 src/iflow.sml --- 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 =>