From a4b12519973682177c23c387b663d55a51dacab0 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 18 Apr 2010 20:06:15 -0400 Subject: Avoid state space explosion with ECase that just writes a constant in each case --- src/iflow.sml | 34 ++++++++++++++++++---------------- 1 file changed, 18 insertions(+), 16 deletions(-) (limited to 'src/iflow.sml') 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 => -- cgit v1.2.3