[commit: ghc] type-nats: Tweak the rules, so that they work for the common case. (6ab9460)

[Iavor Diatchki]

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

On branch  : type-nats

http://hackage.haskell.org/trac/ghc/changeset/6ab946000fdb483d1921a1c7f6f068a900bec790

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

commit 6ab946000fdb483d1921a1c7f6f068a900bec790
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Mon Jul 30 20:15:26 2012 -0700

    Tweak the rules, so that they work for the common case.

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

 compiler/typecheck/TcTypeNats.hs      |    9 ++++++---
 compiler/typecheck/TcTypeNatsRules.hs |   24 ++++++++++++++++++------
 2 files changed, 24 insertions(+), 9 deletions(-)

diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index ee8a515..4b58a74 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -29,7 +29,7 @@ import Bag      ( bagToList )
 import Panic    ( panic )
 
 -- From type checker
-import TcTypeNatsRules( bRules, theRules, widenRules
+import TcTypeNatsRules( bRules, impRules, widenRules
                       , axAddDef, axMulDef, axExpDef, axLeqDef
                       , natVars)
 import TcTypeNatsEval ( minus, divide, logExact, rootExact )
@@ -129,7 +129,8 @@ reExamineWanteds asmps0 newWanted = loop [] (newWanted : given) wanted
 
   loop solved asmps (w : ws) =
     case deepSolve (ws ++ asmps) w of
-      Just ev -> do let x = getId w
+      Just ev -> do natTrace "Solved wanted:" (ppr w)
+                    let x = getId w
                     setEvBind x ev
                     loop (x : solved) asmps ws
       Nothing -> loop solved (w : asmps) ws
@@ -730,13 +731,15 @@ interactCt withEv ct asmps =
               $ funRule typeNatAddTyCon
               : funRule typeNatMulTyCon
               : funRule typeNatExpTyCon
-              : map activate theRules
+              : map activate (widen ++ impRules)
 
       newWork = interactActiveRules active asmps
   in partition isBad $ if withEv then map ruleResultToGiven newWork
                                  else map ruleResultToDerived newWork
 
  where
+  widen = if withEv then widenRules else []
+
   -- cf. `fireRule`: the only way to get a non-canonical constraint
   -- is if it impossible to solve.
   isBad (CNonCanonical {})  = True
diff --git a/compiler/typecheck/TcTypeNatsRules.hs b/compiler/typecheck/TcTypeNatsRules.hs
index 388d94b..f00657a 100644
--- a/compiler/typecheck/TcTypeNatsRules.hs
+++ b/compiler/typecheck/TcTypeNatsRules.hs
@@ -27,7 +27,7 @@ typeNatRuleThings :: [TyThing]
 typeNatRuleThings = map ACoAxiomRule $
   [ axAddDef, axMulDef, axExpDef, axLeqDef ]
     ++ bRules
-    ++ map snd theRules
+    ++ map snd impRules
     ++ map snd widenRules
 
 
@@ -121,8 +121,8 @@ bRules =
 
 
 
-theRules :: [(Bool,CoAxiomRule)]
-theRules =
+impRules :: [(Bool,CoAxiomRule)]
+impRules =
   [ (True, mkAx 30 "AddCancelL" (take 4 natVars)
             [ mkAdd a b === d, mkAdd a c === d ] (b === c))
 
@@ -144,7 +144,7 @@ theRules =
   , (True, mkAx 36 "LeqASym" (take 2 natVars)
             [ a <== b, b <== a ] (a === b))
 
-  ] ++ widenRules
+  ]
 
   where
   a : b : c : d : _ = map mkTyVarTy natVars
@@ -162,10 +162,22 @@ widenRules =
 
   , (False, mkAx 42 "LeqTrans" (take 3 natVars)
             [ a <== b, b <== c ] (a <== c))
+
+  , (False, mkAx 43 "AddAssoc1" (take 6 natVars)
+      [ mkAdd a b === x, mkAdd b c === y, mkAdd a y === z ] (mkAdd x c === z))
+
+  , (False, mkAx 44 "AddAssoc2" (take 6 natVars)
+      [ mkAdd a b === x, mkAdd b c === y, mkAdd x c === z ] (mkAdd a y === z))
+
+  , (False, mkAx 45 "MulAssoc1" (take 6 natVars)
+      [ mkMul a b === x, mkMul b c === y, mkMul a y === z ] (mkMul x c === z))
+
+  , (False, mkAx 46 "MulAssoc2" (take 6 natVars)
+      [ mkMul a b === x, mkMul b c === y, mkMul x c === z ] (mkMul a y === z))
+
   ]
   where
-  a : b : c : _ = map mkTyVarTy natVars
-
+  a : b : c : x : y : z : _ = map mkTyVarTy natVars