[commit: ghc] type-nats: Improvements to use of ordering model (and remove traces). (c811cef)

[Iavor Diatchki]

Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : type-nats

http://hackage.haskell.org/trac/ghc/changeset/c811cef219a90b51ebe0d808606d587bd844fbda

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

commit c811cef219a90b51ebe0d808606d587bd844fbda
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Thu Sep 6 19:43:00 2012 -0700

    Improvements to use of ordering model (and remove traces).

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

 compiler/typecheck/TcTypeNats.hs |   64 +++++++++++++++++++++++++++++---------
 1 files changed, 49 insertions(+), 15 deletions(-)

diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index fd253a6..d4531c2 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -10,8 +10,9 @@ import PrelNames( typeNatAddTyFamName
 import Outputable ( ppr, pprWithCommas
                   , Outputable
                   , SDoc
-                  , (<>), (<+>), colon, text, vcat, parens, braces
-                  , showSDoc
+                  , (<>), (<+>), text, vcat, parens
+                  -- , showSDoc
+                  , hsep
                   )
 import SrcLoc   ( noSrcSpan )
 import Var      ( TyVar )
@@ -29,6 +30,7 @@ import TysWiredIn ( typeNatAddTyCon
                   )
 import Bag      ( bagToList )
 import Panic    ( panic )
+import Pair     (Pair(..))
 
 -- From type checker
 import TcTypeNatsRules( bRules, impRules, widenRules
@@ -51,6 +53,7 @@ import TcEvidence ( EvTerm(..)
                   , evTermCoercion
                   , TcCoercion(TcTypeNatCo)
                   , mkTcSymCo, mkTcTransCo
+                  , tcCoercionKind
                   )
 import TcSMonad ( TcS, emitFrozenError, setEvBind
                 , InertSet
@@ -69,12 +72,14 @@ import Control.Monad ( msum, guard, when )
 import qualified Data.Set as S
 import qualified Data.Map as M
 
+{-
 -- Just fore debugging
 import Debug.Trace
 import DynFlags ( tracingDynFlags )
 
 ppsh :: SDoc -> String
 ppsh = showSDoc tracingDynFlags
+-}
 
 --------------------------------------------------------------------------------
 
@@ -423,6 +428,19 @@ data ActiveRule = AR
 
   }
 
+instance Outputable ActiveRule where
+  ppr r = args <+> text "=>" <+> eq (concl r)
+
+    where eq (x,y) = ppr x <+> text "~" <+> ppr y
+          todo (n, e) = (n, text"?:" <+> eq e)
+          done (n, ev) = let Pair x y = tcCoercionKind (evTermCoercion ev)
+                         in (n, text "!:" <+> eq (x,y))
+
+          args = hsep
+               $ map snd
+               $ sortBy (comparing fst)
+               $ map todo (todoArgs r) ++ map done (doneArgs r)
+
 {- Note [Symmetric Rules]
 
 For symmetric rules, we look for at most one argument that can be
@@ -436,6 +454,7 @@ one because we would just end up with another way to prove the same thing.
 
 -}
 
+{-
 instance Outputable ActiveRule where
   ppr r =
     braces (pprWithCommas ppr (doneTys r)) <+>
@@ -444,7 +463,7 @@ instance Outputable ActiveRule where
     where
     ppArg (x,e) = ppr x <> colon <+> ppr e
     ppEq (a,b)  = ppr a <+> text "~" <+> ppr b
-
+-}
 
 
 
@@ -522,15 +541,14 @@ by proofs for them.
 -}
 fireRule :: LeqFacts -> ActiveRule -> Maybe RuleResult
 fireRule leq r =
-  trace "Trying to fire rule -------------------" $
   do doneSides <- mapM solveSide $ todoArgs r
 
-     ts        <- trace "done with sides" $ mapM cvt (doneTys r)
+     ts        <- mapM cvt (doneTys r)
      (lhs,rhs) <- cvt2 (concl r)
      guard $ not $ eqType lhs rhs   -- Not interested in trivial results.
 
 
-     trace ("fired, concluding: " ++ ppsh (ppr lhs) ++ " ~ " ++ ppsh (ppr rhs)) $return RuleResult
+     return RuleResult
        { conclusion = (lhs,rhs)
        , evidence = \_ -> proof r ts $ map snd $ sortBy (comparing fst)
                                      $ doneSides ++ doneArgs r
@@ -545,13 +563,10 @@ fireRule leq r =
   cvt _           = Nothing
 
 
-  solveSide (n, eq@(a,b)) = trace (unwords [ "TRYING SIDE:", ppsh (ppr a), ppsh (ppr b)]) $
-    do (t1,t2) <- cvt2 eq
-       trace "cvt2" $ guard (eqType t2 trueTy)
-       (tc,[x,y]) <- splitTyConApp_maybe t1
-       trace "equals True" $ guard (tyConName tc == typeNatLeqTyFamName)
-       ev <- trace "is leq" $ isLeq leq x y
-       trace "found proof" $ return (n, ev)
+  solveSide (n, eq) =
+    do (x,y) <- isLeqEqn =<< cvt2 eq
+       ev    <- isLeq leq x y
+       return (n, ev)
 
 
 eqnToCt :: Eqn -> Maybe EvTerm -> Ct
@@ -708,14 +723,25 @@ The first set of constraints are ones that indicate a contradiction
 The second set are "good" constraints (not obviously contradicting each other).
 -}
 interactCt :: Bool -> Ct -> [Ct] -> ([Ct],[Ct])
-interactCt withEv ct asmps0 =
+interactCt withEv ct asmps0
+  | Just _ <- isLeqCt ct =
+  let active  = map activate impRules
+      -- XXX: We only really need to consider impRules that have
+      -- a side condition.
+
+      (leq, asmps) = makeLeqModel (ct : asmps0)
+      newWork = interactActiveRules leq active asmps
+  in partition isBad $ if withEv then map ruleResultToGiven newWork
+                                 else map ruleResultToDerived newWork
+
+  | otherwise =
   let active  = concatMap (`applyAsmp` ct)
               $ funRule typeNatAddTyCon
               : funRule typeNatMulTyCon
               : funRule typeNatExpTyCon
               : map activate (widen ++ impRules)
 
-      (leq, asmps) = makeLeqModel (ct : asmps0)
+      (leq, asmps) = makeLeqModel asmps0
       newWork = interactActiveRules leq active asmps
   in partition isBad $ if withEv then map ruleResultToGiven newWork
                                  else map ruleResultToDerived newWork
@@ -1028,6 +1054,14 @@ isLeqCt (CFunEqCan { cc_fun = tc, cc_tyargs = [t1,t2], cc_rhs = t })
   | tyConName tc == typeNatLeqTyFamName && eqType t trueTy = Just (t1,t2)
 isLeqCt _ = Nothing
 
+isLeqEqn :: Eqn -> Maybe (Type,Type)
+isLeqEqn (t1,t2) =
+  do guard (eqType t2 trueTy)
+     (tc,[x,y]) <- splitTyConApp_maybe t1
+     guard (tyConName tc == typeNatLeqTyFamName)
+     return (x,y)
+
+
 -- | Get the evidence associated with a constraint, if any.
 ctEvTermMaybe :: Ct -> Maybe EvTerm
 ctEvTermMaybe ct =