comparison src/iflow.sml @ 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
parents 0c643f51fbc0
children 7c6fc92f6c31
comparison
equal deleted inserted replaced
1247:0c643f51fbc0 1248:cf9a636f9b15
1876 doFields (xets, []) 1876 doFields (xets, [])
1877 end 1877 end
1878 | EField (e, s) => evalExp env e (fn e => k (Proj (e, s))) 1878 | EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
1879 | ECase (e, pes, {result = res, ...}) => 1879 | ECase (e, pes, {result = res, ...}) =>
1880 evalExp env e (fn e => 1880 evalExp env e (fn e =>
1881 let 1881 if List.all (fn (_, (EWrite (EPrim _, _), _)) => true
1882 val () = St.addPath (e, loc) 1882 | _ => false) pes then
1883 in 1883 (St.send true (e, loc);
1884 app (fn (p, pe) => 1884 k (Recd []))
1885 let 1885 else
1886 val saved = St.stash () 1886 (St.addPath (e, loc);
1887 in 1887 app (fn (p, pe) =>
1888 let 1888 let
1889 val env = evalPat env e p 1889 val saved = St.stash ()
1890 in 1890 in
1891 evalExp env pe k; 1891 let
1892 St.reinstate saved 1892 val env = evalPat env e p
1893 end 1893 in
1894 handle Cc.Contradiction => St.reinstate saved 1894 evalExp env pe k;
1895 end) pes 1895 St.reinstate saved
1896 end) 1896 end
1897 handle Cc.Contradiction => St.reinstate saved
1898 end) pes))
1897 | EStrcat (e1, e2) => 1899 | EStrcat (e1, e2) =>
1898 evalExp env e1 (fn e1 => 1900 evalExp env e1 (fn e1 =>
1899 evalExp env e2 (fn e2 => 1901 evalExp env e2 (fn e2 =>
1900 k (Func (Other "cat", [e1, e2])))) 1902 k (Func (Other "cat", [e1, e2]))))
1901 | EError (e, _) => evalExp env e (fn e => St.send true (e, loc)) 1903 | EError (e, _) => evalExp env e (fn e => St.send true (e, loc))