module CLaSH.Core.Type
( Type (..)
, TypeView (..)
, ConstTy (..)
, LitTy (..)
, Kind
, KindOrType
, KiName
, TyName
, TyVar
, tyView
, coreView
, transparentTy
, typeKind
, mkTyConTy
, mkFunTy
, mkTyConApp
, splitFunTy
, splitFunTys
, splitFunForallTy
, splitTyConAppM
, isPolyFunTy
, isPolyFunCoreTy
, isPolyTy
, isFunTy
, applyFunTy
, applyTy
, findFunSubst
)
where
import Control.DeepSeq as DS
import Control.Monad (zipWithM)
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HashMap
import Data.Maybe (isJust)
import GHC.Generics (Generic(..))
import Unbound.Generics.LocallyNameless (Alpha(..),Bind,Fresh,
Subst(..),SubstName(..),
acompare,aeq,bind,
gacompare,gaeq,gfvAny,
runFreshM,unbind)
import Unbound.Generics.LocallyNameless.Name (Name,name2String)
import Unbound.Generics.LocallyNameless.Extra ()
import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)
import CLaSH.Core.Subst
import CLaSH.Core.Term
import CLaSH.Core.TyCon
import CLaSH.Core.TysPrim
import CLaSH.Core.Var
import CLaSH.Util
data Type
= VarTy !Kind !TyName
| ConstTy !ConstTy
| ForAllTy !(Bind TyVar Type)
| AppTy !Type !Type
| LitTy !LitTy
deriving (Show,Generic,NFData)
data TypeView
= FunTy !Type !Type
| TyConApp !TyConName [Type]
| OtherType !Type
deriving Show
data ConstTy
= TyCon !TyConName
| Arrow
deriving (Show,Generic,NFData,Alpha)
data LitTy
= NumTy !Int
| SymTy !String
deriving (Show,Generic,NFData,Alpha)
type Kind = Type
type KindOrType = Type
type TyName = Name Type
type KiName = Name Kind
instance Alpha Type where
fvAny' c nfn (VarTy t n) = fmap (VarTy t) $ fvAny' c nfn n
fvAny' c nfn t = fmap to . gfvAny c nfn $ from t
aeq' c (VarTy _ n) (VarTy _ m) = aeq' c n m
aeq' c t1 t2 = gaeq c (from t1) (from t2)
acompare' c (VarTy _ n) (VarTy _ m) = acompare' c n m
acompare' c t1 t2 = gacompare c (from t1) (from t2)
instance Subst a LitTy where
subst _ _ lt = lt
substs _ lt = lt
instance Subst a ConstTy where
subst _ _ ct = ct
substs _ ct = ct
instance Subst Term Type
instance Subst Type Type where
isvar (VarTy _ v) = Just (SubstName v)
isvar _ = Nothing
instance Eq Type where
(==) = aeq
instance Ord Type where
compare = acompare
tyView :: Type -> TypeView
tyView ty@(AppTy _ _) = case splitTyAppM ty of
Just (ConstTy Arrow, [ty1,ty2]) -> FunTy ty1 ty2
Just (ConstTy (TyCon tc), args) -> TyConApp tc args
_ -> OtherType ty
tyView (ConstTy (TyCon tc)) = TyConApp tc []
tyView t = OtherType t
transparentTy :: Type -> Type
transparentTy ty@(AppTy (AppTy (ConstTy (TyCon tc)) _) elTy)
= case name2String tc of
"CLaSH.Signal.Internal.Signal'" -> transparentTy elTy
_ -> ty
transparentTy (AppTy ty1 ty2) = AppTy (transparentTy ty1) (transparentTy ty2)
transparentTy (ForAllTy b) = ForAllTy (uncurry bind $ second transparentTy $ unsafeUnbind b)
transparentTy ty = ty
coreView :: HashMap TyConName TyCon -> Type -> TypeView
coreView tcMap ty =
let tView = tyView ty
in case tView of
TyConApp tc args -> case name2String tc of
"CLaSH.Signal.Internal.Signal'" -> coreView tcMap (args !! 1)
_ -> case (tcMap HashMap.! tc) of
AlgTyCon {algTcRhs = (NewTyCon _ nt)}
-> coreView tcMap (newTyConInstRhs nt args)
FunTyCon {tyConSubst = tcSubst} -> case findFunSubst tcSubst args of
Just ty' -> coreView tcMap ty'
_ -> tView
_ -> tView
_ -> tView
newTyConInstRhs :: ([TyName],Type) -> [Type] -> Type
newTyConInstRhs (tvs,ty) tys = foldl AppTy (substTys (zip tvs tys1) ty) tys2
where
(tys1, tys2) = splitAtList tvs tys
mkFunTy :: Type -> Type -> Type
mkFunTy t1 = AppTy (AppTy (ConstTy Arrow) t1)
mkTyConApp :: TyConName -> [Type] -> Type
mkTyConApp tc = foldl AppTy (ConstTy $ TyCon tc)
mkTyConTy :: TyConName -> Type
mkTyConTy ty = ConstTy $ TyCon ty
splitTyConAppM :: Type
-> Maybe (TyConName,[Type])
splitTyConAppM (tyView -> TyConApp tc args) = Just (tc,args)
splitTyConAppM _ = Nothing
isSuperKind :: HashMap TyConName TyCon -> Type -> Bool
isSuperKind tcMap (ConstTy (TyCon ((tcMap HashMap.!) -> SuperKindTyCon {}))) = True
isSuperKind _ _ = False
typeKind :: HashMap TyConName TyCon -> Type -> Kind
typeKind _ (VarTy k _) = k
typeKind m (ForAllTy b) = let (_,ty) = runFreshM $ unbind b
in typeKind m ty
typeKind _ (LitTy (NumTy _)) = typeNatKind
typeKind _ (LitTy (SymTy _)) = typeSymbolKind
typeKind m (tyView -> FunTy _arg res)
| isSuperKind m k = k
| otherwise = liftedTypeKind
where k = typeKind m res
typeKind m (tyView -> TyConApp tc args) = foldl kindFunResult (tyConKind (m HashMap.! tc)) args
typeKind m (AppTy fun arg) = kindFunResult (typeKind m fun) arg
typeKind _ (ConstTy ct) = error $ $(curLoc) ++ "typeKind: naked ConstTy: " ++ show ct
kindFunResult :: Kind -> KindOrType -> Kind
kindFunResult (tyView -> FunTy _ res) _ = res
kindFunResult (ForAllTy b) arg =
let (kv,ki) = runFreshM . unbind $ b
in substKindWith (zip [varName kv] [arg]) ki
kindFunResult k tys =
error $ $(curLoc) ++ "kindFunResult: " ++ show (k,tys)
isPolyTy :: Type -> Bool
isPolyTy (ForAllTy _) = True
isPolyTy (tyView -> FunTy _ res) = isPolyTy res
isPolyTy _ = False
splitFunTy :: HashMap TyConName TyCon
-> Type
-> Maybe (Type, Type)
splitFunTy m (coreView m -> FunTy arg res) = Just (arg,res)
splitFunTy _ _ = Nothing
splitFunTys :: HashMap TyConName TyCon
-> Type
-> ([Type],Type)
splitFunTys m (coreView m -> FunTy arg res) = (arg:args,res')
where
(args,res') = splitFunTys m res
splitFunTys _ ty = ([],ty)
splitFunForallTy :: Type
-> ([Either TyVar Type],Type)
splitFunForallTy = go []
where
go args (ForAllTy b) = let (tv,ty) = runFreshM $ unbind b
in go (Left tv:args) ty
go args (tyView -> FunTy arg res) = go (Right arg:args) res
go args ty = (reverse args,ty)
isPolyFunTy :: Type
-> Bool
isPolyFunTy = not . null . fst . splitFunForallTy
isPolyFunCoreTy :: HashMap TyConName TyCon
-> Type
-> Bool
isPolyFunCoreTy m ty = case coreView m ty of
(FunTy _ _) -> True
(OtherType (ForAllTy _)) -> True
_ -> False
isFunTy :: HashMap TyConName TyCon
-> Type
-> Bool
isFunTy m = isJust . splitFunTy m
applyFunTy :: HashMap TyConName TyCon
-> Type
-> Type
-> Type
applyFunTy m (coreView m -> FunTy _ resTy) _ = resTy
applyFunTy _ _ _ = error $ $(curLoc) ++ "Report as bug: not a FunTy"
applyTy :: Fresh m
=> HashMap TyConName TyCon
-> Type
-> KindOrType
-> m Type
applyTy tcm (coreView tcm -> OtherType (ForAllTy b)) arg = do
(tv,ty) <- unbind b
return (substTy (varName tv) arg ty)
applyTy _ ty arg = error ($(curLoc) ++ "applyTy: not a forall type:\n" ++ show ty ++ "\nArg:\n" ++ show arg)
splitTyAppM :: Type
-> Maybe (Type, [Type])
splitTyAppM = fmap (second reverse) . go []
where
go args (AppTy ty1 ty2) =
case go args ty1 of
Nothing -> Just (ty1,ty2:args)
Just (ty1',ty1args) -> Just (ty1',ty2:ty1args )
go _ _ = Nothing
findFunSubst :: [([Type],Type)] -> [Type] -> Maybe Type
findFunSubst [] _ = Nothing
findFunSubst (tcSubst:rest) args = case funSubsts tcSubst args of
Just ty -> Just ty
Nothing -> findFunSubst rest args
funSubsts :: ([Type],Type) -> [Type] -> Maybe Type
funSubsts (tcSubstLhs,tcSubstRhs) args = do
tySubts <- concat <$> zipWithM funSubst tcSubstLhs args
let tyRhs = substTys tySubts tcSubstRhs
return tyRhs
funSubst :: Type -> Type -> Maybe [(TyName,Type)]
funSubst (VarTy _ nmF) ty = Just [(nmF,ty)]
funSubst tyL@(LitTy _) tyR = if tyL == tyR then Just [] else Nothing
funSubst (tyView -> TyConApp tc argTys) (tyView -> TyConApp tc' argTys')
| tc == tc'
= do
tySubts <- zipWithM funSubst argTys argTys'
return (concat tySubts)
funSubst _ _ = Nothing