[commit: ghc] type-nats-simple: Move declarations for type-nat TyCons to TcTypeNat (e742f24)

[git at git.haskell.org]

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

On branch  : type-nats-simple
Link       : http://ghc.haskell.org/trac/ghc/changeset/e742f24c5c0ec19639a7dde10fad3e1cd25535b8/ghc

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

commit e742f24c5c0ec19639a7dde10fad3e1cd25535b8
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Wed Sep 4 07:41:17 2013 -0700

    Move declarations for type-nat TyCons to TcTypeNat


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

e742f24c5c0ec19639a7dde10fad3e1cd25535b8
 compiler/prelude/PrelInfo.lhs         |    4 ++
 compiler/prelude/TysWiredIn.lhs       |   36 ------------------
 compiler/typecheck/TcTypeNats.hs      |   67 +++++++++++++++++++++++++++++++--
 compiler/typecheck/TcTypeNats.hs-boot |    5 +++
 4 files changed, 72 insertions(+), 40 deletions(-)

diff --git a/compiler/prelude/PrelInfo.lhs b/compiler/prelude/PrelInfo.lhs
index bb3e54a..542525c 100644
--- a/compiler/prelude/PrelInfo.lhs
+++ b/compiler/prelude/PrelInfo.lhs
@@ -42,6 +42,7 @@ import HscTypes
 import Class
 import TyCon
 import Util
+import {-# SOURCE #-} TcTypeNats ( typeNatTyThings )
 
 import Data.Array
 \end{code}
@@ -87,6 +88,9 @@ wiredInThings
 
 		-- PrimOps
 	, map (AnId . primOpId) allThePrimOps
+
+            -- TyCons and axioms for type-nats
+        , typeNatTyThings
     ]
   where
     tycon_things = map ATyCon ([funTyCon] ++ primTyCons ++ wiredInTyCons)
diff --git a/compiler/prelude/TysWiredIn.lhs b/compiler/prelude/TysWiredIn.lhs
index e996617..5ec290a 100644
--- a/compiler/prelude/TysWiredIn.lhs
+++ b/compiler/prelude/TysWiredIn.lhs
@@ -68,9 +68,6 @@ module TysWiredIn (
         -- * Equality predicates
         eqTyCon_RDR, eqTyCon, eqTyConName, eqBoxDataCon,
 
-        -- * Type-level naturals
-        typeNatAddTyCon, typeNatMulTyCon, typeNatExpTyCon
-
     ) where
 
 #include "HsVersions.h"
@@ -788,36 +785,3 @@ isPArrFakeCon dcon  = dcon == parrFakeCon (dataConSourceArity dcon)
 
 
 
-
-%*******************************************************************
-%*
-\subsection[TysWiredIn-TypeNat]{Type-level Numbers}
-%*
-%*******************************************************************
-
-
-Type functions related to type-nats.
-
-\begin{code}
-
--- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
-mkTypeNatFunTyCon2 :: Name -> TyCon
-mkTypeNatFunTyCon2 op =
-  mkSynTyCon op
-    (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind)
-    (take 2 $ tyVarList typeNatKind)
-    [Nominal,Nominal]
-    OpenSynFamilyTyCon  -- XXX: BuiltIn
-    NoParentTyCon
-
-typeNatAddTyCon :: TyCon
-typeNatAddTyCon = mkTypeNatFunTyCon2 typeNatAddTyFamName
-
-typeNatMulTyCon :: TyCon
-typeNatMulTyCon = mkTypeNatFunTyCon2 typeNatMulTyFamName
-
-typeNatExpTyCon :: TyCon
-typeNatExpTyCon = mkTypeNatFunTyCon2 typeNatExpTyFamName
-
-\end{code}
-
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index e5880b4..a8138f5 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -1,16 +1,57 @@
-module TcTypeNats (tnMatchFam, tnInteractTop) where
+module TcTypeNats (tnMatchFam, tnInteractTop, typeNatTyThings) where
 
 import Type
 import Pair
-import TyCon      ( TyCon )
+import TyCon      ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..)  )
+import Coercion   ( Role(..) )
 import TcRnTypes  ( Xi )
 import TcEvidence ( mkTcAxiomRuleCo, TcCoercion )
 import CoAxiom    ( CoAxiomRule(..) )
 import Name       ( Name, mkWiredInName, BuiltInSyntax(..) )
 import OccName    ( mkOccName, tcName )
 import Unique     ( mkAxiomRuleUnique )
-import PrelNames  ( gHC_PRIM )
-import TysWiredIn ( typeNatAddTyCon, typeNatMulTyCon, typeNatExpTyCon )
+import TysWiredIn ( typeNatKind )
+import TysPrim    ( tyVarList, mkArrowKinds )
+import PrelNames  ( gHC_PRIM
+                  , typeNatAddTyFamName
+                  , typeNatMulTyFamName
+                  , typeNatExpTyFamName
+                  )
+
+typeNatTyThings :: [TyThing]
+typeNatTyThings = typeNatTyCons ++ typeNatAxioms
+
+
+{-------------------------------------------------------------------------------
+Built-in type constructors for functions on type-lelve nats
+-}
+
+typeNatTyCons :: [TyThing]
+typeNatTyCons = map ATyCon
+  [ typeNatAddTyCon
+  , typeNatMulTyCon
+  , typeNatExpTyCon
+  ]
+
+typeNatAddTyCon :: TyCon
+typeNatAddTyCon = mkTypeNatFunTyCon2 typeNatAddTyFamName
+
+typeNatMulTyCon :: TyCon
+typeNatMulTyCon = mkTypeNatFunTyCon2 typeNatMulTyFamName
+
+typeNatExpTyCon :: TyCon
+typeNatExpTyCon = mkTypeNatFunTyCon2 typeNatExpTyFamName
+
+-- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
+mkTypeNatFunTyCon2 :: Name -> TyCon
+mkTypeNatFunTyCon2 op =
+  mkSynTyCon op
+    (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind)
+    (take 2 $ tyVarList typeNatKind)
+    [Nominal,Nominal]
+    OpenSynFamilyTyCon  -- XXX: BuiltIn
+    NoParentTyCon
+
 
 
 
@@ -73,6 +114,24 @@ axExp1L  = mkAxiom1   axExp1LKey  "Exp1L" $ \t -> (num 1 .^. t) === num 1
 axExp0R  = mkAxiom1   axExp0RKey  "Exp0R" $ \t -> (t .^. num 0) === num 1
 axExp1R  = mkAxiom1   axExp1RKey  "Exp1R" $ \t -> (t .^. num 1) === t
 
+typeNatAxioms :: [TyThing]
+typeNatAxioms = map ACoAxiomRule
+  [ axAddDef
+  , axMulDef
+  , axExpDef
+  , axAdd0L
+  , axAdd0R
+  , axMul0L
+  , axMul0R
+  , axMul1L
+  , axMul1R
+  , axExp1L
+  , axExp0R
+  , axExp1R
+  ]
+
+
+
 
 {-------------------------------------------------------------------------------
 Various utilities for making axioms and types
diff --git a/compiler/typecheck/TcTypeNats.hs-boot b/compiler/typecheck/TcTypeNats.hs-boot
new file mode 100644
index 0000000..7bb324b
--- /dev/null
+++ b/compiler/typecheck/TcTypeNats.hs-boot
@@ -0,0 +1,5 @@
+module TcTypeNats where
+
+import TypeRep(TyThing)
+
+typeNatTyThings :: [TyThing]