[commit: ghc] type-nats: A bit more integration for reasoning about order. (81609b6)

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

On branch  : type-nats

http://hackage.haskell.org/trac/ghc/changeset/81609b630c719b85a5b0de127d431ae5a0029174

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

commit 81609b630c719b85a5b0de127d431ae5a0029174
Author: Iavor S. Diatchki <[email protected]>
Date:   Mon Sep 3 22:48:42 2012 -0700

    A bit more integration for reasoning about order.

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

 compiler/typecheck/TcTypeNats.hs      |   62 +++++++++++++++++++++++++--------
 compiler/typecheck/TcTypeNatsRules.hs |    5 ---
 2 files changed, 47 insertions(+), 20 deletions(-)

diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index fc0fc7c..d8bf9e7 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -24,7 +24,6 @@ import Type     ( Type, isNumLitTy, getTyVar_maybe, isTyVarTy, mkNumLitTy
 import TysWiredIn ( typeNatAddTyCon
                   , typeNatMulTyCon
                   , typeNatExpTyCon
-                  -- , typeNatLeqTyCon
                   , trueTy, falseTy
                   )
 import Bag      ( bagToList )
@@ -66,7 +65,7 @@ import TcSMonad ( TcS, emitFrozenError, setEvBind
 import Data.Maybe ( isNothing, mapMaybe )
 import Data.List  ( sortBy, partition, find )
 import Data.Ord   ( comparing )
-import Control.Monad ( msum, guard, when, mplus )
+import Control.Monad ( msum, guard, when )
 import qualified Data.Set as S
 import qualified Data.Map as M
 
@@ -162,10 +161,14 @@ this happened automatically because of the custom system for reasoning
 about <=.
 -}
 deepSolve :: [Ct] -> Ct -> Maybe EvTerm
-deepSolve asmps ct = solve ct `mplus` fmap ev (find this (widenAsmps asmps))
+deepSolve asmps0 ct = msum [ solve ct
+                           , solveLeq leq ct
+                           , fmap ev (find this (widenAsmps asmps))
+                           ]
   where
   ev   = ctEvTerm . ctEvidence
   this = sameCt ct
+  (leq,asmps) = makeLeqModel asmps0
 
 
 impossible :: Ct -> Bool
@@ -410,6 +413,14 @@ solveWithAxiom (CFunEqCan { cc_fun = tc, cc_tyargs = ts, cc_rhs = t }) =
      return ev
 solveWithAxiom _ = Nothing
 
+solveLeq :: LeqFacts -> Ct -> Maybe EvTerm
+solveLeq m ct =
+  do (t1,t2) <- isLeqCt ct
+     let (_,m1) = leqInsNode t1 m
+         (_,m2) = leqInsNode t2 m1
+     leqReachable m2 t1 t2
+
+
 --------------------------------------------------------------------------------
 
 -- An `ActiveRule` is a partially constructed proof for some predicate.
@@ -706,6 +717,7 @@ getFacts =
      return $ bagToList $ fst $ partCtFamHeadMap isGivenCt
                               $ inert_funeqs $ inert_cans is
 
+-- Get constraints with evidence (given or wanted)
 getEvCt:: TcS [Ct]
 getEvCt =
   do is <- getTcSInerts
@@ -713,6 +725,7 @@ getEvCt =
                               $ inert_funeqs $ inert_cans is
   where hasEv c = isGivenCt c || isWantedCt c
 
+-- Get all constraints (given, wanted, derived)
 getAllCts :: TcS [Ct]
 getAllCts =
   do is <- getTcSInerts
@@ -740,6 +753,7 @@ interactCt withEv ct asmps =
               : funRule typeNatExpTyCon
               : map activate (widen ++ impRules)
 
+      -- (leq, asmps) = makeLeqModel asmps0
       newWork = interactActiveRules active asmps
   in partition isBad $ if withEv then map ruleResultToGiven newWork
                                  else map ruleResultToDerived newWork
@@ -869,6 +883,8 @@ leqReachable m smaller larger =
          in search vis (notDone new `S.union` notDone rest)
 
 {-
+The linking function is a bit complex because we keep the ordering database
+minimal.
 
 This diagram illustrates what we do when we link two nodes (leqLink).
 
@@ -898,10 +914,12 @@ leqLink :: EvTerm -> (Type,LeqEdges) -> (Type,LeqEdges) ->
 
 leqLink ev (lower, ledges) (upper, uedges) m0 =
 
-  let uus         = S.mapMonotonic (LeqType . leqTarget) (leqAbove uedges)
-      lls         = S.mapMonotonic (LeqType . leqTarget) (leqBelow ledges)
+  let leqTgt      = LeqType . leqTarget
 
-      rm x        = S.filter (not . (`S.member` x) . LeqType . leqTarget)
+      uus         = S.mapMonotonic leqTgt (leqAbove uedges)
+      lls         = S.mapMonotonic leqTgt (leqBelow ledges)
+
+      rm x        = S.filter (not . (`S.member` x) . leqTgt)
 
       newLedges   = ledges { leqAbove =
                                S.insert (LeqEdge { leqProof  = ev
@@ -989,13 +1007,6 @@ leqInsNode t model@(LeqFacts m0) =
                  _ <- isNumLitTy n
                  return (n,(n,e))
 
--- | Try to find a proof that the first term is smaller then the second.
-leqProve :: LeqFacts -> Type -> Type -> Maybe EvTerm
-leqProve model s t =
-  let (_,m1) = leqInsNode s model
-      (_,m2) = leqInsNode t m1
-  in leqReachable m2 s t
-
 
 -- | The result of trying to extend a collection of facts with a new one.
 data AddLeqFact
@@ -1024,8 +1035,28 @@ addFact ev t1 t2 m0 =
           but propose an equality instead. -}
        Just pOp -> LeqImproved (useAxiom leqAsym [t1,t2] [ev, pOp])
 
-
-
+-- | Construct an ordering model and return the remaining, not-leq constraints.
+makeLeqModel :: [Ct] -> (LeqFacts,[Ct])
+makeLeqModel = foldr add (noLeqFacts,[])
+  where
+  add ct (m,rest)
+    | Just (t1,t2) <- isLeqCt ct
+    , Just ev      <- ctEvTermMaybe ct
+    , LeqAdded m1  <- addFact ev t1 t2 m = (m1, rest)
+  add ct (m,rest)                        = (m, ct : rest)
+
+-- | Is this an `a <= b` constraint?
+isLeqCt :: Ct -> Maybe (Type, Type)
+isLeqCt (CFunEqCan { cc_fun = tc, cc_tyargs = [t1,t2], cc_rhs = t })
+  | tyConName tc == typeNatLeqTyFamName && eqType t trueTy = Just (t1,t2)
+isLeqCt _ = Nothing
+
+-- | Get the evidence associated with a constraint, if any.
+ctEvTermMaybe :: Ct -> Maybe EvTerm
+ctEvTermMaybe ct =
+  do let ev = ctEvidence ct
+     guard $ not $ isDerived ev
+     return (ctEvTerm ev)
 
 
 --------------------------------------------------------------------------------
@@ -1033,3 +1064,4 @@ addFact ev t1 t2 m0 =
 natTrace :: String -> SDoc -> TcS ()
 natTrace x y = traceTcS ("[NATS] " ++ x) y
 
+
diff --git a/compiler/typecheck/TcTypeNatsRules.hs b/compiler/typecheck/TcTypeNatsRules.hs
index 2ad2446..fd50862 100644
--- a/compiler/typecheck/TcTypeNatsRules.hs
+++ b/compiler/typecheck/TcTypeNatsRules.hs
@@ -108,9 +108,6 @@ bRules =
   , bRule 17 "TnExp0R" (mkExp a n0 === n1)
   , bRule 18 "TnExp1L" (mkExp n1 a === n1)
   , bRule 19 "TnExp1R" (mkExp a n1 === a)
-
-  , leq0
-  , leqRefl
   ]
   where
   bRule s n = mkAx s n (take 1 natVars) []
@@ -174,8 +171,6 @@ widenRules =
   , (True, mkAx 41 "MulComm" (take 3 natVars)
             [ mkMul a b === c ] (mkMul b a === c))
 
-  , (False, leqTrans)
-
   , (False, mkAx 43 "AddAssoc1" (take 6 natVars)
       [ mkAdd a b === x, mkAdd b c === y, mkAdd a y === z ] (mkAdd x c === z))