{-# LANGUAGE GADTs #-}

-- |
-- Functions for replacing fully applied type synonyms
--
module Language.PureScript.TypeChecker.Synonyms
  ( SynonymMap
  , KindMap
  , replaceAllTypeSynonyms
  , replaceAllTypeSynonymsM
  ) where

import           Prelude

import           Control.Monad.Error.Class (MonadError(..))
import           Control.Monad.State
import           Data.Maybe (fromMaybe)
import qualified Data.Map as M
import           Data.Text (Text)
import           Language.PureScript.Environment
import           Language.PureScript.Errors
import           Language.PureScript.Names
import           Language.PureScript.TypeChecker.Monad
import           Language.PureScript.Types

-- | Type synonym information (arguments with kinds, aliased type), indexed by name
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

-- | Replace fully applied type synonyms
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

-- | Replace fully applied type synonyms by explicitly providing a 'SynonymMap'.
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