[commit: ghc] type-nats: Use WiredIn names for the axiome rules. (3f2fe73)

[Iavor Diatchki]

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

On branch  : type-nats

http://hackage.haskell.org/trac/ghc/changeset/3f2fe73dd103cba840648d5e3d90c9c6f554e73c

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

commit 3f2fe73dd103cba840648d5e3d90c9c6f554e73c
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sat Jul 21 13:42:19 2012 -0700

    Use WiredIn names for the axiome rules.

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

 compiler/iface/TcIface.lhs            |    7 ++--
 compiler/prelude/PrelInfo.lhs         |    3 ++
 compiler/typecheck/TcTypeNatsRules.hs |   59 +++++++++++++--------------------
 3 files changed, 29 insertions(+), 40 deletions(-)

diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index 5fdad18..7559e71 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -20,7 +20,6 @@ import IfaceEnv
 import BuildTyCl
 import TcRnMonad
 import TcType
-import TcTypeNatsRules (allRules)
 import Type
 import Coercion
 import TypeRep
@@ -1392,9 +1391,9 @@ tcIfaceCoAxiom name = do { thing <- tcIfaceGlobal name
 
 tcIfaceCoAxiomRule :: Name -> IfL CoAxiomRule
 tcIfaceCoAxiomRule n =
-  case lookupUFM allRules n of
-    Just r  -> return r
-    Nothing -> pprPanic "tcIfaceCoAxiomRule" (ppr n)
+  case wiredInNameTyThing_maybe n of
+    Just (ACoAxiomRule ax) -> return ax
+    _  -> pprPanic "tcIfaceCoAxiomRule" (ppr n)
 
 
 
diff --git a/compiler/prelude/PrelInfo.lhs b/compiler/prelude/PrelInfo.lhs
index bb3e54a..d443e27 100644
--- a/compiler/prelude/PrelInfo.lhs
+++ b/compiler/prelude/PrelInfo.lhs
@@ -43,6 +43,8 @@ import Class
 import TyCon
 import Util
 
+import TcTypeNatsRules(typeNatRuleThings)
+
 import Data.Array
 \end{code}
 
@@ -87,6 +89,7 @@ wiredInThings
 
 		-- PrimOps
 	, map (AnId . primOpId) allThePrimOps
+        , typeNatRuleThings
     ]
   where
     tycon_things = map ATyCon ([funTyCon] ++ primTyCons ++ wiredInTyCons)
diff --git a/compiler/typecheck/TcTypeNatsRules.hs b/compiler/typecheck/TcTypeNatsRules.hs
index dbad5f4..388d94b 100644
--- a/compiler/typecheck/TcTypeNatsRules.hs
+++ b/compiler/typecheck/TcTypeNatsRules.hs
@@ -4,7 +4,9 @@ module TcTypeNatsRules where
 import Var      ( TyVar )
 import Type     ( Type,  mkTyVarTy, mkNumLitTy, mkTyConApp
                 , CoAxiomRule, Eqn, co_axr_rule, co_axr_tynum2_rule
+                , TyThing(ACoAxiomRule)
                 )
+import PrelNames ( gHC_PRIM )
 import TysPrim  ( tyVarList
                 , typeNatKind
                 )
@@ -15,20 +17,35 @@ import TysWiredIn ( typeNatAddTyCon
                   , trueTy, falseTy
                   )
 
-import Name     ( Name, mkSystemName )
+import Name     ( Name, mkWiredInName, BuiltInSyntax(..) )
 import OccName  ( mkOccName, tcName )
 import Unique   ( mkAxiomRuleUnique )
-import UniqFM   ( UniqFM, listToUFM )
 
 
-mkAxName :: Int -> String -> Name
-mkAxName n s = mkSystemName (mkAxiomRuleUnique n) (mkOccName tcName s)
+
+typeNatRuleThings :: [TyThing]
+typeNatRuleThings = map ACoAxiomRule $
+  [ axAddDef, axMulDef, axExpDef, axLeqDef ]
+    ++ bRules
+    ++ map snd theRules
+    ++ map snd widenRules
+
+
+--------------------------------------------------------------------------------
+mkAxName :: Int -> String -> (Name -> CoAxiomRule) -> CoAxiomRule
+mkAxName n s r = thing
+  where
+  thing = r name
+
+  -- XXX: I'm not sure that we should be using the type name space here
+  name  = mkWiredInName gHC_PRIM (mkOccName tcName s) (mkAxiomRuleUnique n)
+                          (ACoAxiomRule thing) BuiltInSyntax
 
 mkAx :: Int -> String -> [TyVar] -> [Eqn] -> Eqn -> CoAxiomRule
-mkAx n s = co_axr_rule (mkAxName n s)
+mkAx u s as es e = mkAxName u s $ \n -> co_axr_rule n as es e
 
 mkDef :: Int -> String -> (Integer -> Integer -> Eqn) -> CoAxiomRule
-mkDef n s = co_axr_tynum2_rule (mkAxName n s)
+mkDef u s f = mkAxName u s $ \n -> co_axr_tynum2_rule n f
 
 
 mkAdd :: Type -> Type -> Type
@@ -58,18 +75,6 @@ x <== y = (mkLeq x y, trueTy)
 
 
 --------------------------------------------------------------------------------
-
-allRules :: UniqFM CoAxiomRule
-allRules =
-  let expand x = (x,x)
-  in listToUFM $ map expand $
-      [ axAddDef, axMulDef, axExpDef, axLeqDef ] ++
-      bRules ++
-      map snd theRules
-
-
-
---------------------------------------------------------------------------------
 axAddDef :: CoAxiomRule
 axAddDef = mkDef 0 "AddDef" $ \a b ->
              mkAdd (mkNumLitTy a) (mkNumLitTy b) === mkNumLitTy (a + b)
@@ -163,24 +168,6 @@ widenRules =
 
 
 
---------------------------------------------------------------------------------
-
-
-{-
-
-Consider a problem like this:
-
-  [W] a + b ~ b + a
-
-GHC de-sugars this into:
-
-  [W] p: a + b ~ c
-  [W] q: b + a ~ c
-
-When we add the 2nd one, we should notice that it can be solved in terms
-of the first one...
--}
-