module FrontEnd.Tc.Type(
Kind(..),
KBase(..),
MetaVar(..),
MetaVarType(..),
Pred(..),
Preds(),
Qual(..),
Tycon(..),
Type(..),
Tyvar(..),
kindStar,
kindFunRet,
kindUTuple,
unfoldKind,
fn,
fromTAp,
fromTArrow,
module FrontEnd.Tc.Type,
prettyPrintType,
tForAll,
tList,
Constraint(..),
Class(),
Kindvar(..),
tTTuple,
tTTuple',
tAp,
tArrow,
tyvar
) where
import Control.Monad.Identity
import Control.Monad.Writer
import Data.IORef
import Data.List
import qualified Data.Map as Map
import qualified Data.Set as S
import Doc.DocLike
import Doc.PPrint
import FrontEnd.Representation
import FrontEnd.SrcLoc
import FrontEnd.Tc.Kind
import Name.Name
import Name.Names
import Support.FreeVars
import Support.Tickle
type Sigma' = Sigma
type Tau' = Tau
type Rho' = Rho
type Sigma = Type
type Rho = Type
type Tau = Type
type SkolemTV = Tyvar
type BoundTV = Tyvar
type Preds = [Pred]
data Constraint = Equality {
constraintSrcLoc :: SrcLoc,
constraintType1 :: Type,
constraintType2 :: Type
}
instance HasLocation Constraint where
srcLoc Equality { constraintSrcLoc = sl } = sl
applyTyvarMap :: [(Tyvar,Type)] -> Type -> Type
applyTyvarMap ts t = f initMp t where
initMp = Map.fromList [ (tyvarName v,t) | (v,t) <- ts ]
f mp (TForAll as qt) = TForAll as (fq (foldr Map.delete mp (map tyvarName as)) qt)
f mp (TExists as qt) = TExists as (fq (foldr Map.delete mp (map tyvarName as)) qt)
f mp (TVar tv) = case Map.lookup (tyvarName tv) mp of
Just t' -> t'
Nothing -> (TVar tv)
f mp t = tickle (f mp) t
fq mp (ps :=> t) = map (tickle (f mp)) ps :=> f mp t
applyTyvarMapQT :: [(Tyvar,Type)] -> Qual Type -> Qual Type
applyTyvarMapQT ts qt = qt' where
(TForAll [] qt') = applyTyvarMap ts (TForAll [] qt)
typeOfType :: Type -> (MetaVarType,Bool)
typeOfType TForAll { typeArgs = as, typeBody = _ :=> t } = (Sigma,isBoxy t)
typeOfType t | isTau' t = (Tau,isBoxy t)
typeOfType t = (Rho,isBoxy t)
fromType :: Sigma -> ([Tyvar],[Pred],Type)
fromType s = case s of
TForAll as (ps :=> r) -> (as,ps,r)
r -> ([],[],r)
isTau :: Type -> Bool
isTau TForAll {} = False
isTau (TMetaVar MetaVar { metaType = t })
| t == Tau = True
| otherwise = False
isTau t = getAll $ tickleCollect (All . isTau) t
isTau' :: Type -> Bool
isTau' TForAll {} = False
isTau' t = getAll $ tickleCollect (All . isTau') t
isBoxy :: Type -> Bool
isBoxy (TMetaVar MetaVar { metaType = t }) | t > Tau = True
isBoxy t = getAny $ tickleCollect (Any . isBoxy) t
isRho' :: Type -> Bool
isRho' TForAll {} = False
isRho' _ = True
isRho :: Type -> Bool
isRho r = isRho' r && not (isBoxy r)
isBoxyMetaVar :: MetaVar -> Bool
isBoxyMetaVar MetaVar { metaType = t } = t > Tau
extractTyVar :: Monad m => Type -> m Tyvar
extractTyVar (TVar tv) = return tv
extractTyVar t = fail $ "not a Var:" ++ show t
extractMetaVar :: Monad m => Type -> m MetaVar
extractMetaVar (TMetaVar t) = return t
extractMetaVar t = fail $ "not a metaTyVar:" ++ show t
extractBox :: Monad m => Type -> m MetaVar
extractBox (TMetaVar mv) | metaType mv > Tau = return mv
extractBox t = fail $ "not a metaTyVar:" ++ show t
newtype UnVarOpt = UnVarOpt {
failEmptyMetaVar :: Bool
}
flattenType :: (MonadIO m, UnVar t) => t -> m t
flattenType t = liftIO $ unVar' t
class UnVar t where
unVar' :: t -> IO t
instance UnVar t => UnVar [t] where
unVar' xs = mapM unVar' xs
instance UnVar Pred where
unVar' (IsIn c t) = IsIn c `liftM` unVar' t
unVar' (IsEq t1 t2) = liftM2 IsEq (unVar' t1) (unVar' t2)
instance (UnVar a,UnVar b) => UnVar (a,b) where
unVar' (a,b) = do
a <- unVar' a
b <- unVar' b
return (a,b)
instance UnVar t => UnVar (Qual t) where
unVar' (ps :=> t) = liftM2 (:=>) (unVar' ps) (unVar' t)
instance UnVar Type where
unVar' tv = do
let ft (TForAll vs qt) = do
qt' <- unVar' qt
return $ TForAll vs qt'
ft (TExists vs qt) = do
qt' <- unVar' qt
return $ TExists vs qt'
ft (TAp (TAp (TCon arr) a1) a2) | tyconName arr == tc_Arrow = ft (TArrow a1 a2)
ft t@(TMetaVar _) = return t
ft t = tickleM (unVar' . (id :: Type -> Type)) t
tv' <- findType tv
ft tv'
followTaus :: MonadIO m => Type -> m Type
followTaus tv@(TMetaVar mv@MetaVar {metaRef = r }) | not (isBoxyMetaVar mv) = liftIO $ do
rt <- readIORef r
case rt of
Nothing -> return tv
Just t -> do
t' <- followTaus t
writeIORef r (Just t')
return t'
followTaus tv = return tv
findType :: MonadIO m => Type -> m Type
findType tv@(TMetaVar MetaVar {metaRef = r }) = liftIO $ do
rt <- readIORef r
case rt of
Nothing -> return tv
Just t -> do
t' <- findType t
writeIORef r (Just t')
return t'
findType tv = return tv
readMetaVar :: MonadIO m => MetaVar -> m (Maybe Type)
readMetaVar MetaVar { metaRef = r } = liftIO $ do
rt <- readIORef r
case rt of
Nothing -> return Nothing
Just t -> do
t' <- findType t
writeIORef r (Just t')
return (Just t')
freeMetaVars :: Type -> S.Set MetaVar
freeMetaVars t = f t where
f (TMetaVar mv) = S.singleton mv
f (TAp l r) = f l `S.union` f r
f (TArrow l r) = f l `S.union` f r
f (TAssoc c cas eas) = S.unions (map f cas ++ map f eas)
f (TForAll ta (ps :=> t)) = S.unions (f t:map f2 ps)
f (TExists ta (ps :=> t)) = S.unions (f t:map f2 ps)
f _ = S.empty
f2 (IsIn c t) = f t
f2 (IsEq t1 t2) = f t1 `S.union` f t2
instance FreeVars Type [Tyvar] where
freeVars (TVar u) = [u]
freeVars (TForAll vs qt) = freeVars qt Data.List.\\ vs
freeVars (TExists vs qt) = freeVars qt Data.List.\\ vs
freeVars t = foldr union [] $ tickleCollect ((:[]) . (freeVars :: Type -> [Tyvar])) t
instance FreeVars Type [MetaVar] where
freeVars t = S.toList $ freeMetaVars t
instance FreeVars Type (S.Set MetaVar) where
freeVars t = freeMetaVars t
instance (FreeVars t b,FreeVars Pred b) => FreeVars (Qual t) b where
freeVars (ps :=> t) = freeVars t `mappend` freeVars ps
instance FreeVars Type b => FreeVars Pred b where
freeVars (IsIn _c t) = freeVars t
freeVars (IsEq t1 t2) = freeVars (t1,t2)
instance Tickleable Type Pred where
tickleM f (IsIn c t) = liftM (IsIn c) (f t)
tickleM f (IsEq t1 t2) = liftM2 IsEq (f t1) (f t2)
instance Tickleable Type Type where
tickleM f (TAp l r) = liftM2 tAp (f l) (f r)
tickleM f (TArrow l r) = liftM2 TArrow (f l) (f r)
tickleM f (TAssoc c cas eas) = liftM2 (TAssoc c) (mapM f cas) (mapM f eas)
tickleM f (TForAll ta (ps :=> t)) = do
ps <- mapM (tickleM f) ps
liftM (TForAll ta . (ps :=>)) (f t)
tickleM f (TExists ta (ps :=> t)) = do
ps <- mapM (tickleM f) ps
liftM (TExists ta . (ps :=>)) (f t)
tickleM _ t = return t
data Rule = RuleSpec {
ruleUniq :: (Module,Int),
ruleName :: Name,
ruleSuper :: Bool,
ruleType :: Type
} |
RuleUser {
ruleUniq :: (Module,Int),
ruleFreeTVars :: [(Name,Kind)]
}
data CoerceTerm = CTId | CTAp [Type] | CTAbs [Tyvar] | CTFun CoerceTerm | CTCompose CoerceTerm CoerceTerm
instance Show CoerceTerm where
showsPrec _ CTId = showString "id"
showsPrec n (CTAp ts) = ptrans (n > 10) parens $ char '@' <+> hsep (map (parens . prettyPrintType) ts)
showsPrec n (CTAbs ts) = ptrans (n > 10) parens $ char '\\' <+> hsep (map pprint ts)
showsPrec n (CTFun ct) = ptrans (n > 10) parens $ text "->" <+> showsPrec 11 ct
showsPrec n (CTCompose ct1 ct2) = ptrans (n > 10) parens $ (showsPrec 11 ct1) <+> char '.' <+> (showsPrec 11 ct2)
ptrans :: Bool -> (a -> a) -> (a -> a)
ptrans b f = if b then f else id
instance Monoid CoerceTerm where
mempty = CTId
mappend = composeCoerce
ctFun :: CoerceTerm -> CoerceTerm
ctFun CTId = CTId
ctFun x = CTFun x
ctAbs :: [Tyvar] -> CoerceTerm
ctAbs [] = CTId
ctAbs xs = CTAbs xs
ctAp :: [Type] -> CoerceTerm
ctAp [] = CTId
ctAp xs = CTAp xs
ctId :: CoerceTerm
ctId = CTId
composeCoerce :: CoerceTerm -> CoerceTerm -> CoerceTerm
composeCoerce CTId x = x
composeCoerce x CTId = x
composeCoerce x y = CTCompose x y
instance UnVar Type => UnVar CoerceTerm where
unVar' (CTAp ts) = CTAp `liftM` unVar' ts
unVar' (CTFun ct) = CTFun `liftM` unVar' ct
unVar' (CTCompose c1 c2) = liftM2 CTCompose (unVar' c1) (unVar' c2)
unVar' x = return x