{-# LANGUAGE GADTs #-}
module Language.PureScript.TypeChecker.Synonyms
( SynonymMap
, KindMap
, replaceAllTypeSynonyms
, replaceAllTypeSynonymsM
) where
import Prelude
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State (MonadState)
import Data.Maybe (fromMaybe)
import Data.Map qualified as M
import Data.Text (Text)
import Language.PureScript.Environment (Environment(..), TypeKind)
import Language.PureScript.Errors (MultipleErrors, SimpleErrorMessage(..), SourceSpan, errorMessage')
import Language.PureScript.Names (ProperName, ProperNameType(..), Qualified)
import Language.PureScript.TypeChecker.Monad (CheckState, getEnv)
import Language.PureScript.Types (SourceType, Type(..), completeBinderList, everywhereOnTypesTopDownM, getAnnForType, replaceAllTypeVars)
type SynonymMap = M.Map (Qualified (ProperName 'TypeName)) ([(Text, Maybe SourceType)], SourceType)
type KindMap = M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
replaceAllTypeSynonyms'
:: SynonymMap
-> KindMap
-> SourceType
-> Either MultipleErrors SourceType
replaceAllTypeSynonyms' :: SynonymMap
-> KindMap
-> Type SourceAnn
-> Either MultipleErrors (Type SourceAnn)
replaceAllTypeSynonyms' SynonymMap
syns KindMap
kinds = forall (m :: * -> *) a.
Monad m =>
(Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesTopDownM Type SourceAnn -> Either MultipleErrors (Type SourceAnn)
try
where
try :: SourceType -> Either MultipleErrors SourceType
try :: Type SourceAnn -> Either MultipleErrors (Type SourceAnn)
try Type SourceAnn
t = forall a. a -> Maybe a -> a
fromMaybe Type SourceAnn
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceSpan
-> Int
-> [Type SourceAnn]
-> [Type SourceAnn]
-> Type SourceAnn
-> Either MultipleErrors (Maybe (Type SourceAnn))
go (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. Type a -> a
getAnnForType Type SourceAnn
t) Int
0 [] [] Type SourceAnn
t
go :: SourceSpan -> Int -> [SourceType] -> [SourceType] -> SourceType -> Either MultipleErrors (Maybe SourceType)
go :: SourceSpan
-> Int
-> [Type SourceAnn]
-> [Type SourceAnn]
-> Type SourceAnn
-> Either MultipleErrors (Maybe (Type SourceAnn))
go SourceSpan
ss Int
c [Type SourceAnn]
kargs [Type SourceAnn]
args (TypeConstructor SourceAnn
_ Qualified (ProperName 'TypeName)
ctor)
| Just ([(Text, Maybe (Type SourceAnn))]
synArgs, Type SourceAnn
body) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'TypeName)
ctor SynonymMap
syns
, Int
c forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Text, Maybe (Type SourceAnn))]
synArgs
, [Text]
kindArgs <- Qualified (ProperName 'TypeName) -> [Text]
lookupKindArgs Qualified (ProperName 'TypeName)
ctor
, forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type SourceAnn]
kargs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
kindArgs
= let repl :: Type SourceAnn
repl = forall a. [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Text, Maybe (Type SourceAnn))]
synArgs) [Type SourceAnn]
args forall a. Semigroup a => a -> a -> a
<> forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
kindArgs [Type SourceAnn]
kargs) Type SourceAnn
body
in forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type SourceAnn -> Either MultipleErrors (Type SourceAnn)
try Type SourceAnn
repl
| Just ([(Text, Maybe (Type SourceAnn))]
synArgs, Type SourceAnn
_) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'TypeName)
ctor SynonymMap
syns
, forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Text, Maybe (Type SourceAnn))]
synArgs forall a. Ord a => a -> a -> Bool
> Int
c
= forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' SourceSpan
ss forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'TypeName) -> SimpleErrorMessage
PartiallyAppliedSynonym Qualified (ProperName 'TypeName)
ctor
go SourceSpan
ss Int
c [Type SourceAnn]
kargs [Type SourceAnn]
args (TypeApp SourceAnn
_ Type SourceAnn
f Type SourceAnn
arg) = SourceSpan
-> Int
-> [Type SourceAnn]
-> [Type SourceAnn]
-> Type SourceAnn
-> Either MultipleErrors (Maybe (Type SourceAnn))
go SourceSpan
ss (Int
c forall a. Num a => a -> a -> a
+ Int
1) [Type SourceAnn]
kargs (Type SourceAnn
arg forall a. a -> [a] -> [a]
: [Type SourceAnn]
args) Type SourceAnn
f
go SourceSpan
ss Int
c [Type SourceAnn]
kargs [Type SourceAnn]
args (KindApp SourceAnn
_ Type SourceAnn
f Type SourceAnn
arg) = SourceSpan
-> Int
-> [Type SourceAnn]
-> [Type SourceAnn]
-> Type SourceAnn
-> Either MultipleErrors (Maybe (Type SourceAnn))
go SourceSpan
ss Int
c (Type SourceAnn
arg forall a. a -> [a] -> [a]
: [Type SourceAnn]
kargs) [Type SourceAnn]
args Type SourceAnn
f
go SourceSpan
_ Int
_ [Type SourceAnn]
_ [Type SourceAnn]
_ Type SourceAnn
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
lookupKindArgs :: Qualified (ProperName 'TypeName) -> [Text]
lookupKindArgs :: Qualified (ProperName 'TypeName) -> [Text]
lookupKindArgs Qualified (ProperName 'TypeName)
ctor = forall a. a -> Maybe a -> a
fromMaybe [] forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> Maybe ([(a, (Text, Type a))], Type a)
completeBinderList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'TypeName)
ctor KindMap
kinds
replaceAllTypeSynonyms :: (e ~ MultipleErrors, MonadState CheckState m, MonadError e m) => SourceType -> m SourceType
replaceAllTypeSynonyms :: forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
Type SourceAnn -> m (Type SourceAnn)
replaceAllTypeSynonyms Type SourceAnn
d = do
Environment
env <- forall (m :: * -> *). MonadState CheckState m => m Environment
getEnv
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SynonymMap
-> KindMap
-> Type SourceAnn
-> Either MultipleErrors (Type SourceAnn)
replaceAllTypeSynonyms' (Environment -> SynonymMap
typeSynonyms Environment
env) (Environment -> KindMap
types Environment
env) Type SourceAnn
d
replaceAllTypeSynonymsM
:: MonadError MultipleErrors m
=> SynonymMap
-> KindMap
-> SourceType
-> m SourceType
replaceAllTypeSynonymsM :: forall (m :: * -> *).
MonadError MultipleErrors m =>
SynonymMap -> KindMap -> Type SourceAnn -> m (Type SourceAnn)
replaceAllTypeSynonymsM SynonymMap
syns KindMap
kinds = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynonymMap
-> KindMap
-> Type SourceAnn
-> Either MultipleErrors (Type SourceAnn)
replaceAllTypeSynonyms' SynonymMap
syns KindMap
kinds