Change the representation and move TcBuiltInSynFamily.
authorIavor S. Diatchki <diatchki@galois.com>
Thu, 14 Nov 2013 18:50:52 +0000 (10:50 -0800)
committerIavor S. Diatchki <diatchki@galois.com>
Thu, 14 Nov 2013 18:50:52 +0000 (10:50 -0800)
The changes in more detail:

  * `TcBuiltInSynFamily` is now known as `BuiltinSynFamily` and
     lives in `CoAxiom`

  * `sfMatchFam` returns (CoAxiomRule, [Type], Type),
     which is enough to make Coersion or TcCoercion,
     depending on what what we need.

  * The rest of the compiler is updated to reflect these changes,
    most notably we can eliminate the cludge (XXX) in FamInstEnv
    and remove the lhs-boot file.

compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcTypeNats.hs
compiler/types/CoAxiom.lhs
compiler/types/FamInstEnv.lhs
compiler/types/FamInstEnv.lhs-boot [deleted file]
compiler/types/TyCon.lhs

index 2b742b2..2484958 100644 (file)
@@ -11,8 +11,8 @@ import TcCanonical
 import VarSet
 import Type
 import Unify
-import FamInstEnv(TcBuiltInSynFamily(..))
 import InstEnv( lookupInstEnv, instanceDFunId )
+import CoAxiom(sfInteractTop, sfInteractInert)
 
 import Var
 import TcType
index c6e8991..78f1be8 100644 (file)
@@ -108,6 +108,7 @@ import Kind
 import TcType
 import DynFlags
 import Type
+import CoAxiom(sfMatchFam)
 
 import TcEvidence
 import Class
@@ -1715,7 +1716,9 @@ matchFam tycon args
         ty = pSnd (tcCoercionKind co)
     in return $ Just (co, ty)
 
-  | Just ops <- isBuiltInSynFamTyCon_maybe tycon = return (sfMatchFam ops args)
+  | Just ops <- isBuiltInSynFamTyCon_maybe tycon =
+    return $ do (r,ts,ty) <- sfMatchFam ops args
+                return (mkTcAxiomRuleCo r ts [], ty)
 
   | otherwise
   = return Nothing
index fe4a25d..7c47658 100644 (file)
@@ -1,7 +1,7 @@
 module TcTypeNats
   ( typeNatTyCons
   , typeNatCoAxiomRules
-  , TcBuiltInSynFamily(..)
+  , BuiltInSynFamily(..)
   ) where
 
 import Type
@@ -10,8 +10,7 @@ import TcType     ( TcType )
 import TyCon      ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..)  )
 import Coercion   ( Role(..) )
 import TcRnTypes  ( Xi )
-import TcEvidence ( mkTcAxiomRuleCo, TcCoercion )
-import CoAxiom    ( CoAxiomRule(..) )
+import CoAxiom    ( CoAxiomRule(..), BuiltInSynFamily(..) )
 import Name       ( Name, BuiltInSyntax(..) )
 import TysWiredIn ( typeNatKind, mkWiredInTyConName
                   , promotedBoolTyCon
@@ -25,7 +24,6 @@ import PrelNames  ( gHC_TYPELITS
                   , typeNatLeqTyFamNameKey
                   , typeNatSubTyFamNameKey
                   )
-import FamInstEnv ( TcBuiltInSynFamily(..) )
 import FastString ( FastString, fsLit )
 import qualified Data.Map as Map
 import Data.Maybe ( isJust )
@@ -45,7 +43,7 @@ typeNatTyCons =
 
 typeNatAddTyCon :: TyCon
 typeNatAddTyCon = mkTypeNatFunTyCon2 name
-  TcBuiltInSynFamily
+  BuiltInSynFamily
     { sfMatchFam      = matchFamAdd
     , sfInteractTop   = interactTopAdd
     , sfInteractInert = interactInertAdd
@@ -56,7 +54,7 @@ typeNatAddTyCon = mkTypeNatFunTyCon2 name
 
 typeNatSubTyCon :: TyCon
 typeNatSubTyCon = mkTypeNatFunTyCon2 name
-  TcBuiltInSynFamily
+  BuiltInSynFamily
     { sfMatchFam      = matchFamSub
     , sfInteractTop   = interactTopSub
     , sfInteractInert = interactInertSub
@@ -67,7 +65,7 @@ typeNatSubTyCon = mkTypeNatFunTyCon2 name
 
 typeNatMulTyCon :: TyCon
 typeNatMulTyCon = mkTypeNatFunTyCon2 name
-  TcBuiltInSynFamily
+  BuiltInSynFamily
     { sfMatchFam      = matchFamMul
     , sfInteractTop   = interactTopMul
     , sfInteractInert = interactInertMul
@@ -78,7 +76,7 @@ typeNatMulTyCon = mkTypeNatFunTyCon2 name
 
 typeNatExpTyCon :: TyCon
 typeNatExpTyCon = mkTypeNatFunTyCon2 name
-  TcBuiltInSynFamily
+  BuiltInSynFamily
     { sfMatchFam      = matchFamExp
     , sfInteractTop   = interactTopExp
     , sfInteractInert = interactInertExp
@@ -99,7 +97,7 @@ typeNatLeqTyCon =
   where
   name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "<=?")
                 typeNatLeqTyFamNameKey typeNatLeqTyCon
-  ops = TcBuiltInSynFamily
+  ops = BuiltInSynFamily
     { sfMatchFam      = matchFamLeq
     , sfInteractTop   = interactTopLeq
     , sfInteractInert = interactInertLeq
@@ -107,7 +105,7 @@ typeNatLeqTyCon =
 
 
 -- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
-mkTypeNatFunTyCon2 :: Name -> TcBuiltInSynFamily -> TyCon
+mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
 mkTypeNatFunTyCon2 op tcb =
   mkSynTyCon op
     (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind)
@@ -278,54 +276,54 @@ mkAxiom1 str f =
 Evaluation
 -------------------------------------------------------------------------------}
 
-matchFamAdd :: [Type] -> Maybe (TcCoercion, TcType)
+matchFamAdd :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
 matchFamAdd [s,t]
-  | Just 0 <- mbX = Just (mkTcAxiomRuleCo axAdd0L [t] [], t)
-  | Just 0 <- mbY = Just (mkTcAxiomRuleCo axAdd0R [s] [], s)
+  | Just 0 <- mbX = Just (axAdd0L, [t], t)
+  | Just 0 <- mbY = Just (axAdd0R, [s], s)
   | Just x <- mbX, Just y <- mbY =
-    Just (mkTcAxiomRuleCo axAddDef [s,t] [], num (x + y))
+    Just (axAddDef, [s,t], num (x + y))
   where mbX = isNumLitTy s
         mbY = isNumLitTy t
 matchFamAdd _ = Nothing
 
-matchFamSub :: [Type] -> Maybe (TcCoercion, TcType)
+matchFamSub :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
 matchFamSub [s,t]
-  | Just 0 <- mbY = Just (mkTcAxiomRuleCo axSub0R [s] [], s)
+  | Just 0 <- mbY = Just (axSub0R, [s], s)
   | Just x <- mbX, Just y <- mbY, Just z <- minus x y =
-    Just (mkTcAxiomRuleCo axSubDef [s,t] [], num z)
+    Just (axSubDef, [s,t], num z)
   where mbX = isNumLitTy s
         mbY = isNumLitTy t
 matchFamSub _ = Nothing
 
-matchFamMul :: [Xi] -> Maybe (TcCoercion, Xi)
+matchFamMul :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
 matchFamMul [s,t]
-  | Just 0 <- mbX = Just (mkTcAxiomRuleCo axMul0L [t] [], num 0)
-  | Just 0 <- mbY = Just (mkTcAxiomRuleCo axMul0R [s] [], num 0)
-  | Just 1 <- mbX = Just (mkTcAxiomRuleCo axMul1L [t] [], t)
-  | Just 1 <- mbY = Just (mkTcAxiomRuleCo axMul1R [s] [], s)
+  | Just 0 <- mbX = Just (axMul0L, [t], num 0)
+  | Just 0 <- mbY = Just (axMul0R, [s], num 0)
+  | Just 1 <- mbX = Just (axMul1L, [t], t)
+  | Just 1 <- mbY = Just (axMul1R, [s], s)
   | Just x <- mbX, Just y <- mbY =
-    Just (mkTcAxiomRuleCo axMulDef [s,t] [], num (x * y))
+    Just (axMulDef, [s,t], num (x * y))
   where mbX = isNumLitTy s
         mbY = isNumLitTy t
 matchFamMul _ = Nothing
 
-matchFamExp :: [Xi] -> Maybe (TcCoercion, Xi)
+matchFamExp :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
 matchFamExp [s,t]
-  | Just 0 <- mbY = Just (mkTcAxiomRuleCo axExp0R [s] [], num 1)
-  | Just 1 <- mbX = Just (mkTcAxiomRuleCo axExp1L [t] [], num 1)
-  | Just 1 <- mbY = Just (mkTcAxiomRuleCo axExp1R [s] [], s)
+  | Just 0 <- mbY = Just (axExp0R, [s], num 1)
+  | Just 1 <- mbX = Just (axExp1L, [t], num 1)
+  | Just 1 <- mbY = Just (axExp1R, [s], s)
   | Just x <- mbX, Just y <- mbY =
-    Just (mkTcAxiomRuleCo axExpDef [s,t] [], num (x ^ y))
+    Just (axExpDef, [s,t], num (x ^ y))
   where mbX = isNumLitTy s
         mbY = isNumLitTy t
 matchFamExp _ = Nothing
 
-matchFamLeq :: [Xi] -> Maybe (TcCoercion, Xi)
+matchFamLeq :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
 matchFamLeq [s,t]
-  | Just 0 <- mbX = Just (mkTcAxiomRuleCo axLeq0L [t] [], bool True)
+  | Just 0 <- mbX = Just (axLeq0L, [t], bool True)
   | Just x <- mbX, Just y <- mbY =
-    Just (mkTcAxiomRuleCo axLeqDef [s,t] [], bool (x <= y))
-  | eqType s t  = Just (mkTcAxiomRuleCo axLeqRefl [s] [], bool True)
+    Just (axLeqDef, [s,t], bool (x <= y))
+  | eqType s t  = Just (axLeqRefl, [s], bool True)
   where mbX = isNumLitTy s
         mbY = isNumLitTy t
 matchFamLeq _ = Nothing
index dd35dde..a0a4974 100644 (file)
@@ -28,7 +28,8 @@ module CoAxiom (
 
        Role(..), fsFromRole,
 
-       CoAxiomRule(..), Eqn
+       CoAxiomRule(..), Eqn,
+       BuiltInSynFamily(..), trivialBuiltInFamily
        ) where 
 
 import {-# SOURCE #-} TypeRep ( Type )
@@ -520,5 +521,23 @@ instance Ord CoAxiomRule where
 
 instance Outputable CoAxiomRule where
   ppr = ppr . coaxrName
+
+
+-- Type checking of built-in families
+data BuiltInSynFamily = BuiltInSynFamily
+  { sfMatchFam      :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
+  , sfInteractTop   :: [Type] -> Type -> [Eqn]
+  , sfInteractInert :: [Type] -> Type ->
+                       [Type] -> Type -> [Eqn]
+  }
+
+-- Provides default implementations that do nothing.
+trivialBuiltInFamily :: BuiltInSynFamily
+trivialBuiltInFamily = BuiltInSynFamily
+  { sfMatchFam      = \_ -> Nothing
+  , sfInteractTop   = \_ _ -> []
+  , sfInteractInert = \_ _ _ _ -> []
+  }
+
 \end{code}
 
index 89805de..b158da2 100644 (file)
@@ -32,10 +32,7 @@ module FamInstEnv (
         normaliseType, normaliseTcApp,
 
         -- Flattening
-        flattenTys,
-
-        -- Built-in type families
-        TcBuiltInSynFamily(..), trivialBuiltInFamily
+        flattenTys
     ) where
 
 #include "HsVersions.h"
@@ -43,8 +40,7 @@ module FamInstEnv (
 import InstEnv
 import Unify
 import Type
-import TcType ( TcType, orphNamesOfTypes )
-import TcEvidence (TcCoercion(TcAxiomRuleCo))
+import TcType ( orphNamesOfTypes )
 import TypeRep
 import TyCon
 import Coercion
@@ -800,16 +796,11 @@ reduceTyFamApp_maybe envs role tc tys
         ty     = pSnd (coercionKind co)
     in Just (args_co `mkTransCo` co, ty)
 
-  | Just ax        <- isBuiltInSynFamTyCon_maybe tc
-  , Just (tcco,ty) <- sfMatchFam ax ntys
-  -- XXX: we have a TcCoercion, but we need a Coercion.
-  -- For the time being, we convert coercions in just this one special case
-  -- but something more general might be nice.
-  , TcAxiomRuleCo coax ts [] <- tcco
+  | Just ax           <- isBuiltInSynFamTyCon_maybe tc
+  , Just (coax,ts,ty) <- sfMatchFam ax ntys
   = let co = mkAxiomRuleCo coax ts []
     in Just (args_co `mkTransCo` co, ty)
 
-
   | otherwise
   = Nothing
 
@@ -1073,28 +1064,3 @@ allTyVarsInTy = go
     go (LitTy {})        = emptyVarSet
 
 \end{code}
-
-
-
-
-Type checking of built-in families
-==================================
-
-\begin{code}
-data TcBuiltInSynFamily = TcBuiltInSynFamily
-  { sfMatchFam      :: [Type] -> Maybe (TcCoercion, TcType)
-  , sfInteractTop   :: [Type] -> Type -> [Pair TcType]
-  , sfInteractInert :: [Type] -> Type ->
-                       [Type] -> Type -> [Pair TcType]
-  }
-
--- Provides default implementations that do nothing.
-trivialBuiltInFamily :: TcBuiltInSynFamily
-trivialBuiltInFamily = TcBuiltInSynFamily
-  { sfMatchFam      = \_ -> Nothing
-  , sfInteractTop   = \_ _ -> []
-  , sfInteractInert = \_ _ _ _ -> []
-  }
-\end{code}
-
-
diff --git a/compiler/types/FamInstEnv.lhs-boot b/compiler/types/FamInstEnv.lhs-boot
deleted file mode 100644 (file)
index 4540148..0000000
+++ /dev/null
@@ -1,5 +0,0 @@
-\begin{code}
-module FamInstEnv where
-
-data TcBuiltInSynFamily
-\end{code}
index f8667b0..e690329 100644 (file)
@@ -96,7 +96,6 @@ module TyCon(
 
 import {-# SOURCE #-} TypeRep ( Kind, Type, PredType )
 import {-# SOURCE #-} DataCon ( DataCon, isVanillaDataCon )
-import {-# SOURCE #-} FamInstEnv ( TcBuiltInSynFamily )
 
 import Var
 import Class
@@ -633,7 +632,7 @@ data SynTyConRhs
    -- type family F a where ..
    | AbstractClosedSynFamilyTyCon
 
-   | BuiltInSynFamTyCon TcBuiltInSynFamily
+   | BuiltInSynFamTyCon BuiltInSynFamily
 \end{code}
 
 Note [Closed type families]
@@ -1242,7 +1241,7 @@ isClosedSynFamilyTyCon_maybe
   (SynTyCon {synTcRhs = ClosedSynFamilyTyCon ax}) = Just ax
 isClosedSynFamilyTyCon_maybe _ = Nothing
 
-isBuiltInSynFamTyCon_maybe :: TyCon -> Maybe TcBuiltInSynFamily
+isBuiltInSynFamTyCon_maybe :: TyCon -> Maybe BuiltInSynFamily
 isBuiltInSynFamTyCon_maybe
   SynTyCon {synTcRhs = BuiltInSynFamTyCon ops } = Just ops
 isBuiltInSynFamTyCon_maybe _ = Nothing