{-# LANGUAGE LambdaCase, ViewPatterns #-}
module TypeLevel.Rewrite.Internal.TypeTemplate where
import Type (TyVar, Type, getTyVar_maybe)
import Data.Rewriting.Term (Term(Fun, Var))
import TypeLevel.Rewrite.Internal.TypeNode
type TypeTemplate = Term TypeNode TyVar
toTypeTemplate_maybe
:: Type
-> Maybe TypeTemplate
toTypeTemplate_maybe :: Type -> Maybe TypeTemplate
toTypeTemplate_maybe (Type -> Maybe TyVar
getTyVar_maybe -> Just TyVar
tyVar)
= TypeTemplate -> Maybe TypeTemplate
forall a. a -> Maybe a
Just (TypeTemplate -> Maybe TypeTemplate)
-> (TyVar -> TypeTemplate) -> TyVar -> Maybe TypeTemplate
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> TypeTemplate
forall f v. v -> Term f v
Var (TyVar -> Maybe TypeTemplate) -> TyVar -> Maybe TypeTemplate
forall a b. (a -> b) -> a -> b
$ TyVar
tyVar
toTypeTemplate_maybe (Type -> Maybe (TypeNode, [Type])
toTypeNodeApp_maybe -> Just (TypeNode
tyNode, [Type]
args))
= TypeNode -> [TypeTemplate] -> TypeTemplate
forall f v. f -> [Term f v] -> Term f v
Fun TypeNode
tyNode ([TypeTemplate] -> TypeTemplate)
-> Maybe [TypeTemplate] -> Maybe TypeTemplate
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> Maybe TypeTemplate) -> [Type] -> Maybe [TypeTemplate]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Type -> Maybe TypeTemplate
toTypeTemplate_maybe [Type]
args
toTypeTemplate_maybe Type
_
= Maybe TypeTemplate
forall a. Maybe a
Nothing