Commit 19b8809c authored by Iavor S. Diatchki's avatar Iavor S. Diatchki
Browse files

Change the representation and move TcBuiltInSynFamily.

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.
parent 12cdd6da
......@@ -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
......
......@@ -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
......
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
......
......@@ -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}
......@@ -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}
\begin{code}
module FamInstEnv where
data TcBuiltInSynFamily
\end{code}
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment