#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
#endif
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 Unbound.LocallyNameless as Unbound hiding (Arrow,rnf)
import Unbound.LocallyNameless.Alpha (aeqR1,fvR1)
import Unbound.LocallyNameless.Name (Name(Nm,Bn))
import Unbound.LocallyNameless.Ops (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
data TypeView
= FunTy Type Type
| TyConApp TyConName [Type]
| OtherType Type
deriving Show
data ConstTy
= TyCon TyConName
| Arrow
deriving Show
data LitTy
= NumTy Int
| SymTy String
deriving Show
type Kind = Type
type KindOrType = Type
type TyName = Name Type
type KiName = Name Kind
Unbound.derive [''Type,''LitTy,''ConstTy]
instance Alpha Type where
fv' c (VarTy _ n) = fv' c n
fv' c t = fvR1 rep1 c t
aeq' c (VarTy _ n) (VarTy _ m) = aeq' c n m
aeq' c t1 t2 = aeqR1 rep1 c t1 t2
instance Alpha ConstTy
instance Alpha LitTy
instance Subst Type LitTy
instance Subst Term LitTy
instance Subst Type ConstTy
instance Subst Term ConstTy
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
instance NFData Type where
rnf ty = case ty of
VarTy ki nm -> rnf ki `seq` rnf nm
ConstTy c -> rnf c
ForAllTy b -> case unsafeUnbind b of
(tv,ty') -> rnf tv `seq` rnf ty'
AppTy tyL tyR -> rnf tyL `seq` rnf tyR
LitTy l -> rnf l
instance NFData (Name Type) where
rnf nm = case nm of
(Nm _ s) -> rnf s
(Bn _ l r) -> rnf l `seq` rnf r
instance NFData ConstTy where
rnf cty = case cty of
TyCon nm -> rnf nm
Arrow -> ()
instance NFData LitTy where
rnf lty = case lty of
NumTy i -> rnf i
SymTy s -> rnf s
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.CSignal" -> 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.CSignal" -> coreView tcMap (args !! 1)
_ -> case (tcMap HashMap.! tc) of
(AlgTyCon {algTcRhs = (NewTyCon _ nt)})
| length (fst nt) == length args -> coreView tcMap (newTyConInstRhs nt args)
| otherwise -> tView
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