[commit: ghc] wip/gadtpm: literals: more expressive laziness oracle (0370621)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/gadtpm
Link       : http://ghc.haskell.org/trac/ghc/changeset/0370621c94692fcc881c6b44941e1bb9be312b55/ghc

>---------------------------------------------------------------

commit 0370621c94692fcc881c6b44941e1bb9be312b55
Author: George Karachalias <george.karachalias at gmail.com>
Date:   Sun Nov 29 12:57:08 2015 +0100

    literals: more expressive laziness oracle


>---------------------------------------------------------------

0370621c94692fcc881c6b44941e1bb9be312b55
 compiler/deSugar/Check.hs    |  6 ++++--
 compiler/deSugar/TmOracle.hs | 37 +++++++++++++++++++++++++++++--------
 2 files changed, 33 insertions(+), 10 deletions(-)

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index ecbaed5..188a11c 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -763,9 +763,11 @@ pruneVSABound n v = pruneVSABound' n init_cs emptylist v
               False -> []
           Constraint cs vsa -> case splitConstraints cs of
             (new_ty_cs, new_tm_cs, new_bot_ct) -> case tmOracle tm_env new_tm_cs of
-                Just (new_tm_env@(residual, (expr_eqs, subst))) ->
+                Just new_tm_env ->
                   let bot = mergeBotCs new_bot_ct bot_ct
-                      ans = isNothing bot || notNull residual || expr_eqs || notForced (fromJust bot) subst
+                      ans = case bot of
+                              Nothing -> True                    -- covered
+                              Just b  -> canDiverge b new_tm_env -- divergent
                   in  case ans of
                         True  -> pruneVSABound' n (new_ty_cs++ty_cs, new_tm_env, bot) vec vsa
                         False -> return []
diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs
index 75aa649..781e4a2 100644
--- a/compiler/deSugar/TmOracle.hs
+++ b/compiler/deSugar/TmOracle.hs
@@ -10,7 +10,7 @@ module TmOracle (
 
         -- re-exported from PmExpr
         PmExpr(..), PmLit(..), SimpleEq, ComplexEq, PmVarEnv, falsePmExpr,
-        notForced, eqPmLit, filterComplex, isNotPmExprOther, runPmPprM,
+        canDiverge, eqPmLit, filterComplex, isNotPmExprOther, runPmPprM,
         pprPmExprWithParens, lhsExprToPmExpr, hsExprToPmExpr,
 
         -- the term oracle
@@ -50,12 +50,33 @@ type PmVarEnv = Map.Map Id PmExpr
 --     2. A substitution we extend with every step and return as a result.
 type TmOracleEnv = (Bool, PmVarEnv)
 
--- | Check whether a variable has been refined to (at least) a WHNF (Could be
--- improved in terms of expressivity. Too conservative at the moment.).
-notForced :: Id -> PmVarEnv -> Bool
-notForced x env = case varDeepLookup env x of
-  PmExprVar _ -> True
-  _other_expr -> False
+-- | Check whether a constraint (x ~ BOT) can succeed,
+-- given the resulting state of the term oracle.
+canDiverge :: Id -> TmState -> Bool
+canDiverge x (standby, (_unhandled, env))
+  -- If the variable seems not evaluated, there is a possibility for
+  -- constraint x ~ BOT to be satisfiable.
+  | PmExprVar y <- varDeepLookup env x -- seems not forced
+  -- If it is involved (directly or indirectly) in any equality in the
+  -- worklist, we can assume that it is already indirectly evaluated,
+  -- as a side-effect of equality checking. If not, then we can assume
+  -- that the constraint is satisfiable.
+  = not $ any (isForcedByEq x) standby || any (isForcedByEq y) standby
+  -- Variable x is already in WHNF so the constraint is non-satisfiable
+  | otherwise = False
+
+  where
+    isForcedByEq :: Id -> ComplexEq -> Bool
+    isForcedByEq y (e1, e2) = varIn y e1 || varIn y e2
+
+-- | Check whether a variable is in the free variables of an expression
+varIn :: Id -> PmExpr -> Bool
+varIn x e = case e of
+  PmExprVar y    -> x == y
+  PmExprCon _ es -> any (x `varIn`) es
+  PmExprLit _    -> False
+  PmExprEq e1 e2 -> (x `varIn` e1) || (x `varIn` e2)
+  PmExprOther _  -> False
 
 -- | Flatten the DAG (Could be improved in terms of performance.).
 flattenPmVarEnv :: PmVarEnv -> PmVarEnv
@@ -88,7 +109,7 @@ solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
     Just False -> Nothing                     -- we are sure: not equal
     -- Maybe just drop. We use this boolean to check also whether something is forced and I know
     -- that nothing is if both are literals. Hence, just assume true and give (Just solver_state)?
-    Nothing    -> Just (standby, (True, env)) -- no clue (and won't get one)!
+    Nothing    -> Just (standby, (unhandled, env)) -- no clue (and won't get one)!
 
   (PmExprCon c1 ts1, PmExprCon c2 ts2)
     | c1 == c2  -> foldlM solveComplexEq solver_state (zip ts1 ts2)