#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
, splitFunForallTy
, splitTyConAppM
, isPolyTy
, isFunTy
, applyFunTy
, applyTy
)
where
import Data.Maybe (isJust)
import Unbound.LocallyNameless as Unbound hiding (Arrow)
import Unbound.LocallyNameless.Alpha (aeqR1,fvR1)
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 TyCon [Type]
| OtherType Type
deriving Show
data ConstTy
= TyCon TyCon
| 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
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 (AppTy (ConstTy (TyCon tc)) ty)
= case name2String (tyConName tc) of
"CLaSH.Signal.Signal" -> transparentTy ty
"CLaSH.Signal.SignalP" -> transparentTy ty
_ -> AppTy (ConstTy (TyCon tc)) (transparentTy ty)
transparentTy (AppTy ty1 ty2) = AppTy (transparentTy ty1) (transparentTy ty2)
transparentTy (ForAllTy b) = ForAllTy (uncurry bind $ second transparentTy $ unsafeUnbind b)
transparentTy ty = ty
coreView :: Type -> TypeView
coreView ty =
let tView = tyView ty
in case tView of
TyConApp (AlgTyCon {algTcRhs = (NewTyCon _ nt)}) args
| length (fst nt) == length args -> coreView (newTyConInstRhs nt args)
| otherwise -> tView
TyConApp tc args -> case name2String (tyConName tc) of
"CLaSH.Signal.Signal" -> coreView (head args)
"CLaSH.Signal.SignalP" -> coreView (head args)
_ -> 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 :: TyCon -> [Type] -> Type
mkTyConApp tc = foldl AppTy (ConstTy $ TyCon tc)
mkTyConTy :: TyCon -> Type
mkTyConTy ty = ConstTy $ TyCon ty
splitTyConAppM :: Type
-> Maybe (TyCon,[Type])
splitTyConAppM (tyView -> TyConApp tc args) = Just (tc,args)
splitTyConAppM _ = Nothing
isSuperKind :: Type -> Bool
isSuperKind (ConstTy (TyCon (SuperKindTyCon {}))) = True
isSuperKind _ = False
typeKind :: Type -> Kind
typeKind (VarTy k _) = k
typeKind (ForAllTy b) = let (_,ty) = runFreshM $ unbind b
in typeKind ty
typeKind (LitTy (NumTy _)) = typeNatKind
typeKind (LitTy (SymTy _)) = typeSymbolKind
typeKind (tyView -> FunTy _arg res)
| isSuperKind k = k
| otherwise = liftedTypeKind
where k = typeKind res
typeKind (tyView -> TyConApp tc args) = foldl kindFunResult (tyConKind tc) args
typeKind (AppTy fun arg) = kindFunResult (typeKind 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 :: Type
-> Maybe (Type, Type)
splitFunTy (coreView -> FunTy arg res) = Just (arg,res)
splitFunTy _ = Nothing
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)
isFunTy :: Type
-> Bool
isFunTy = isJust . splitFunTy
applyFunTy :: Type
-> Type
-> Type
applyFunTy (coreView -> FunTy _ resTy) _ = resTy
applyFunTy _ _ = error $ $(curLoc) ++ "Report as bug: not a FunTy"
applyTy :: Fresh m
=> Type
-> KindOrType
-> m Type
applyTy (ForAllTy b) arg = do
(tv,ty) <- unbind b
return $ substTy (varName tv) arg ty
applyTy _ _ = error $ $(curLoc) ++ "applyTy: not a forall type"
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