{- |
Module      :  ./HasCASL/TypeDecl.hs
Description :  analyse type declarations
Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

analyse type declarations
-}

module HasCASL.TypeDecl
    ( anaFormula
    , mapAnMaybe
    , anaTypeItems
    , dataPatToType
    , ana1Datatype
    , anaDatatype
    , addDataSen
    ) where

import Common.Id
import Common.AS_Annotation
import Common.Lib.State
import qualified Data.Map as Map
import qualified Data.Set as Set
import Common.Result

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.Builtin
import HasCASL.Le
import HasCASL.ClassAna
import HasCASL.TypeAna
import HasCASL.ConvertTypePattern
import HasCASL.DataAna
import HasCASL.Unify
import HasCASL.VarDecl
import HasCASL.SubtypeDecl
import HasCASL.MixAna
import HasCASL.TypeCheck

import Control.Monad

import Data.Maybe
import Data.List (group)

-- | resolve and type check a formula
anaFormula :: Annoted Term -> State Env (Maybe (Annoted Term, Annoted Term))
anaFormula :: Annoted Term -> State Env (Maybe (Annoted Term, Annoted Term))
anaFormula at :: Annoted Term
at = do
    Maybe Term
rt <- Term -> State Env (Maybe Term)
resolve (Term -> State Env (Maybe Term)) -> Term -> State Env (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Annoted Term -> Term
forall a. Annoted a -> a
item Annoted Term
at
    case Maybe Term
rt of
      Nothing -> Maybe (Annoted Term, Annoted Term)
-> State Env (Maybe (Annoted Term, Annoted Term))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Annoted Term, Annoted Term)
forall a. Maybe a
Nothing
      Just t :: Term
t -> do
          Maybe Term
mt <- Type -> Term -> State Env (Maybe Term)
typeCheck (Type -> Type
mkLazyType Type
unitType) Term
t
          Maybe (Annoted Term, Annoted Term)
-> State Env (Maybe (Annoted Term, Annoted Term))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Annoted Term, Annoted Term)
 -> State Env (Maybe (Annoted Term, Annoted Term)))
-> Maybe (Annoted Term, Annoted Term)
-> State Env (Maybe (Annoted Term, Annoted Term))
forall a b. (a -> b) -> a -> b
$ case Maybe Term
mt of
              Nothing -> Maybe (Annoted Term, Annoted Term)
forall a. Maybe a
Nothing
              Just e :: Term
e -> (Annoted Term, Annoted Term) -> Maybe (Annoted Term, Annoted Term)
forall a. a -> Maybe a
Just (Annoted Term
at { item :: Term
item = Term
t }, Annoted Term
at { item :: Term
item = Term
e })

anaVars :: Env -> Vars -> Type -> Result Term
anaVars :: Env -> Vars -> Type -> Result Term
anaVars te :: Env
te vv :: Vars
vv t :: Type
t = case Vars
vv of
    Var v :: Id
v -> Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ VarDecl -> Term
QualVar (VarDecl -> Term) -> VarDecl -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
v Type
t SeparatorKind
Other (Range -> VarDecl) -> Range -> VarDecl
forall a b. (a -> b) -> a -> b
$ Id -> Range
posOfId Id
v
    VarTuple vs :: [Vars]
vs ps :: Range
ps -> let
        (topTy :: Type
topTy, ts :: [Type]
ts) = Type -> (Type, [Type])
getTypeAppl Type
t
        n :: Int
n = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts in
        if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 Bool -> Bool -> Bool
&& Env -> Type -> Type -> Bool
lesserType Env
te Type
topTy (Int -> Range -> Type
toProdType Int
n Range
nullRange) then
               if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Vars] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Vars]
vs then
                  let lrs :: [Result Term]
lrs = (Vars -> Type -> Result Term) -> [Vars] -> [Type] -> [Result Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Env -> Vars -> Type -> Result Term
anaVars Env
te) [Vars]
vs [Type]
ts
                      lms :: [Maybe Term]
lms = (Result Term -> Maybe Term) -> [Result Term] -> [Maybe Term]
forall a b. (a -> b) -> [a] -> [b]
map Result Term -> Maybe Term
forall a. Result a -> Maybe a
maybeResult [Result Term]
lrs in
                      if (Maybe Term -> Bool) -> [Maybe Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust [Maybe Term]
lms then
                         Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Range -> Term
TupleTerm ((Maybe Term -> Term) -> [Maybe Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Maybe Term -> Term
forall a. HasCallStack => Maybe a -> a
fromJust [Maybe Term]
lms) Range
ps
                         else [Diagnosis] -> Maybe Term -> Result Term
forall a. [Diagnosis] -> Maybe a -> Result a
Result ((Result Term -> [Diagnosis]) -> [Result Term] -> [Diagnosis]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Result Term -> [Diagnosis]
forall a. Result a -> [Diagnosis]
diags [Result Term]
lrs) Maybe Term
forall a. Maybe a
Nothing
               else String -> Type -> Result Term
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "wrong arity" Type
topTy
        else String -> Type -> Result Term
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "product type expected" Type
topTy

-- | lift a analysis function to annotated items
mapAnMaybe :: (Monad m) => (Annoted a -> m (Maybe b)) -> [Annoted a]
           -> m [Annoted b]
mapAnMaybe :: (Annoted a -> m (Maybe b)) -> [Annoted a] -> m [Annoted b]
mapAnMaybe f :: Annoted a -> m (Maybe b)
f al :: [Annoted a]
al = do
    [Maybe b]
il <- (Annoted a -> m (Maybe b)) -> [Annoted a] -> m [Maybe b]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Annoted a -> m (Maybe b)
f [Annoted a]
al
    [Annoted b] -> m [Annoted b]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted b] -> m [Annoted b]) -> [Annoted b] -> m [Annoted b]
forall a b. (a -> b) -> a -> b
$ ((Maybe b, Annoted a) -> Annoted b)
-> [(Maybe b, Annoted a)] -> [Annoted b]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: Maybe b
i, a :: Annoted a
a) -> b -> Annoted a -> Annoted b
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted (Maybe b -> b
forall a. HasCallStack => Maybe a -> a
fromJust Maybe b
i) Annoted a
a) ([(Maybe b, Annoted a)] -> [Annoted b])
-> [(Maybe b, Annoted a)] -> [Annoted b]
forall a b. (a -> b) -> a -> b
$
           ((Maybe b, Annoted a) -> Bool)
-> [(Maybe b, Annoted a)] -> [(Maybe b, Annoted a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe b -> Bool
forall a. Maybe a -> Bool
isJust (Maybe b -> Bool)
-> ((Maybe b, Annoted a) -> Maybe b)
-> (Maybe b, Annoted a)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe b, Annoted a) -> Maybe b
forall a b. (a, b) -> a
fst) ([(Maybe b, Annoted a)] -> [(Maybe b, Annoted a)])
-> [(Maybe b, Annoted a)] -> [(Maybe b, Annoted a)]
forall a b. (a -> b) -> a -> b
$ [Maybe b] -> [Annoted a] -> [(Maybe b, Annoted a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe b]
il [Annoted a]
al

-- | analyse annotated type items
anaTypeItems :: GenKind -> [Annoted TypeItem] -> State Env [Annoted TypeItem]
anaTypeItems :: GenKind -> [Annoted TypeItem] -> State Env [Annoted TypeItem]
anaTypeItems gk :: GenKind
gk l :: [Annoted TypeItem]
l = do
    [Annoted TypeItem]
ul <- (Annoted TypeItem -> State Env (Maybe TypeItem))
-> [Annoted TypeItem] -> State Env [Annoted TypeItem]
forall (m :: * -> *) a b.
Monad m =>
(Annoted a -> m (Maybe b)) -> [Annoted a] -> m [Annoted b]
mapAnMaybe Annoted TypeItem -> State Env (Maybe TypeItem)
ana1TypeItem [Annoted TypeItem]
l
    [DataPat]
tys <- ([DataPat] -> [DataPat])
-> State Env [DataPat] -> State Env [DataPat]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [DataPat] -> [DataPat]
forall a. [a] -> [a]
reverse (State Env [DataPat] -> State Env [DataPat])
-> State Env [DataPat] -> State Env [DataPat]
forall a b. (a -> b) -> a -> b
$ ([DataPat] -> Annoted TypeItem -> State Env [DataPat])
-> [DataPat] -> [Annoted TypeItem] -> State Env [DataPat]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ( \ r :: [DataPat]
r i :: Annoted TypeItem
i -> case Annoted TypeItem -> TypeItem
forall a. Annoted a -> a
item Annoted TypeItem
i of
      Datatype d :: DatatypeDecl
d -> (DataPat -> [DataPat]) -> State Env DataPat -> State Env [DataPat]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DataPat -> [DataPat] -> [DataPat]
forall a. a -> [a] -> [a]
: [DataPat]
r) (State Env DataPat -> State Env [DataPat])
-> State Env DataPat -> State Env [DataPat]
forall a b. (a -> b) -> a -> b
$ DatatypeDecl -> State Env DataPat
dataPatToType DatatypeDecl
d
      _ -> [DataPat] -> State Env [DataPat]
forall (m :: * -> *) a. Monad m => a -> m a
return [DataPat]
r) [] [Annoted TypeItem]
ul
    [Annoted TypeItem]
rl <- (Annoted TypeItem -> State Env (Maybe TypeItem))
-> [Annoted TypeItem] -> State Env [Annoted TypeItem]
forall (m :: * -> *) a b.
Monad m =>
(Annoted a -> m (Maybe b)) -> [Annoted a] -> m [Annoted b]
mapAnMaybe (GenKind
-> [DataPat] -> Annoted TypeItem -> State Env (Maybe TypeItem)
anaTypeItem GenKind
gk [DataPat]
tys) [Annoted TypeItem]
ul
    [DataPat] -> State Env ()
addDataSen [DataPat]
tys
    [Annoted TypeItem] -> State Env [Annoted TypeItem]
forall (m :: * -> *) a. Monad m => a -> m a
return [Annoted TypeItem]
rl

-- | add sentences for data type definitions
addDataSen :: [DataPat] -> State Env ()
addDataSen :: [DataPat] -> State Env ()
addDataSen tys :: [DataPat]
tys = do
    TypeMap
tm <- (Env -> TypeMap) -> State Env TypeMap
forall s a. (s -> a) -> State s a
gets Env -> TypeMap
typeMap
    let tis :: [Id]
tis = (DataPat -> Id) -> [DataPat] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (DataPat _ i :: Id
i _ _ _) -> Id
i) [DataPat]
tys
        ds :: [DataEntry]
ds = (Id -> [DataEntry] -> [DataEntry])
-> [DataEntry] -> [Id] -> [DataEntry]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ i :: Id
i dl :: [DataEntry]
dl -> case Id -> TypeMap -> Maybe TypeInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i TypeMap
tm of
                     Nothing -> [DataEntry]
dl
                     Just ti :: TypeInfo
ti -> case TypeInfo -> TypeDefn
typeDefn TypeInfo
ti of
                                DatatypeDefn dd :: DataEntry
dd -> DataEntry
dd DataEntry -> [DataEntry] -> [DataEntry]
forall a. a -> [a] -> [a]
: [DataEntry]
dl
                                _ -> [DataEntry]
dl) [] [Id]
tis
        sen :: SenAttr Sentence String
sen = (String -> Sentence -> SenAttr Sentence String
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> String)
-> (Id -> String -> String) -> [Id] -> String -> String
forall a.
(String -> String)
-> (a -> String -> String) -> [a] -> String -> String
showSepList (String -> String -> String
showString "_") Id -> String -> String
showId [Id]
tis "")
              (Sentence -> SenAttr Sentence String)
-> Sentence -> SenAttr Sentence String
forall a b. (a -> b) -> a -> b
$ [DataEntry] -> Sentence
DatatypeSen [DataEntry]
ds) { isDef :: Bool
isDef = Bool
True }
    Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([DataPat] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DataPat]
tys) (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [SenAttr Sentence String] -> State Env ()
appendSentences [SenAttr Sentence String
sen]

ana1TypeItem :: Annoted TypeItem -> State Env (Maybe TypeItem)
ana1TypeItem :: Annoted TypeItem -> State Env (Maybe TypeItem)
ana1TypeItem t :: Annoted TypeItem
t = case Annoted TypeItem -> TypeItem
forall a. Annoted a -> a
item Annoted TypeItem
t of
    Datatype d :: DatatypeDecl
d -> do
        Maybe DatatypeDecl
md <- Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl)
ana1Datatype (Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl))
-> Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl)
forall a b. (a -> b) -> a -> b
$ DatatypeDecl -> Annoted TypeItem -> Annoted DatatypeDecl
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted DatatypeDecl
d Annoted TypeItem
t
        Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeItem -> State Env (Maybe TypeItem))
-> Maybe TypeItem -> State Env (Maybe TypeItem)
forall a b. (a -> b) -> a -> b
$ (DatatypeDecl -> TypeItem) -> Maybe DatatypeDecl -> Maybe TypeItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DatatypeDecl -> TypeItem
Datatype Maybe DatatypeDecl
md
    i :: TypeItem
i -> Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeItem -> State Env (Maybe TypeItem))
-> Maybe TypeItem -> State Env (Maybe TypeItem)
forall a b. (a -> b) -> a -> b
$ TypeItem -> Maybe TypeItem
forall a. a -> Maybe a
Just TypeItem
i

anaTypeDecl :: [TypePattern] -> Kind -> Range -> State Env (Maybe TypeItem)
anaTypeDecl :: [TypePattern] -> Kind -> Range -> State Env (Maybe TypeItem)
anaTypeDecl pats :: [TypePattern]
pats kind :: Kind
kind ps :: Range
ps = do
    ClassMap
cm <- (Env -> ClassMap) -> State Env ClassMap
forall s a. (s -> a) -> State s a
gets Env -> ClassMap
classMap
    let Result cs :: [Diagnosis]
cs _ = Kind -> ClassMap -> Result RawKind
anaKindM Kind
kind ClassMap
cm
        Result ds :: [Diagnosis]
ds (Just is :: [(Id, [TypeArg])]
is) = [TypePattern] -> Result [(Id, [TypeArg])]
convertTypePatterns [TypePattern]
pats
    [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
cs [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
ds
    let ak :: Kind
ak = if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
cs then Kind
kind else Kind
universe
    [Maybe (Id, [TypeArg])]
mis <- ((Id, [TypeArg]) -> State Env (Maybe (Id, [TypeArg])))
-> [(Id, [TypeArg])] -> State Env [Maybe (Id, [TypeArg])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TypeDefn
-> Kind -> (Id, [TypeArg]) -> State Env (Maybe (Id, [TypeArg]))
addTypePattern TypeDefn
NoTypeDefn Kind
ak) [(Id, [TypeArg])]
is
    let newPats :: [TypePattern]
newPats = ((Id, [TypeArg]) -> TypePattern)
-> [(Id, [TypeArg])] -> [TypePattern]
forall a b. (a -> b) -> [a] -> [b]
map (Id, [TypeArg]) -> TypePattern
toTypePattern ([(Id, [TypeArg])] -> [TypePattern])
-> [(Id, [TypeArg])] -> [TypePattern]
forall a b. (a -> b) -> a -> b
$ [Maybe (Id, [TypeArg])] -> [(Id, [TypeArg])]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Id, [TypeArg])]
mis
    Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeItem -> State Env (Maybe TypeItem))
-> Maybe TypeItem -> State Env (Maybe TypeItem)
forall a b. (a -> b) -> a -> b
$ if [TypePattern] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypePattern]
newPats then Maybe TypeItem
forall a. Maybe a
Nothing else TypeItem -> Maybe TypeItem
forall a. a -> Maybe a
Just (TypeItem -> Maybe TypeItem) -> TypeItem -> Maybe TypeItem
forall a b. (a -> b) -> a -> b
$ [TypePattern] -> Kind -> Range -> TypeItem
TypeDecl [TypePattern]
newPats Kind
ak Range
ps

anaIsoDecl :: [TypePattern] -> Range -> State Env (Maybe TypeItem)
anaIsoDecl :: [TypePattern] -> Range -> State Env (Maybe TypeItem)
anaIsoDecl pats :: [TypePattern]
pats ps :: Range
ps = do
    let Result ds :: [Diagnosis]
ds (Just is :: [(Id, [TypeArg])]
is) = [TypePattern] -> Result [(Id, [TypeArg])]
convertTypePatterns [TypePattern]
pats
    [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds
    [Maybe (Id, [TypeArg])]
mis <- ((Id, [TypeArg]) -> State Env (Maybe (Id, [TypeArg])))
-> [(Id, [TypeArg])] -> State Env [Maybe (Id, [TypeArg])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TypeDefn
-> Kind -> (Id, [TypeArg]) -> State Env (Maybe (Id, [TypeArg]))
addTypePattern TypeDefn
NoTypeDefn Kind
universe) [(Id, [TypeArg])]
is
    case [Maybe (Id, [TypeArg])] -> [(Id, [TypeArg])]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Id, [TypeArg])]
mis of
      [] -> Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeItem
forall a. Maybe a
Nothing
      nis :: [(Id, [TypeArg])]
nis -> do
        let (i :: Id
i, _) : ris :: [(Id, [TypeArg])]
ris = [(Id, [TypeArg])] -> [(Id, [TypeArg])]
forall a. [a] -> [a]
reverse [(Id, [TypeArg])]
nis
        ((Id, [TypeArg]) -> State Env Bool)
-> [(Id, [TypeArg])] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (j :: Id
j, _) -> Bool -> Id -> TypeScheme -> Kind -> State Env Bool
addAliasType Bool
False Id
j
              ([TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [] (Id -> RawKind -> Int -> Type
TypeName Id
i RawKind
rStar 0) (Range -> TypeScheme) -> Range -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Id -> Range
posOfId Id
j) Kind
universe) [(Id, [TypeArg])]
ris
        Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeItem -> State Env (Maybe TypeItem))
-> Maybe TypeItem -> State Env (Maybe TypeItem)
forall a b. (a -> b) -> a -> b
$ TypeItem -> Maybe TypeItem
forall a. a -> Maybe a
Just (TypeItem -> Maybe TypeItem) -> TypeItem -> Maybe TypeItem
forall a b. (a -> b) -> a -> b
$ [TypePattern] -> Range -> TypeItem
IsoDecl (((Id, [TypeArg]) -> TypePattern)
-> [(Id, [TypeArg])] -> [TypePattern]
forall a b. (a -> b) -> [a] -> [b]
map (Id, [TypeArg]) -> TypePattern
toTypePattern [(Id, [TypeArg])]
nis) Range
ps

setTypePatternVars :: [(Id, [TypeArg])] -> State Env [(Id, [TypeArg])]
setTypePatternVars :: [(Id, [TypeArg])] -> State Env [(Id, [TypeArg])]
setTypePatternVars ol :: [(Id, [TypeArg])]
ol = do
    [(Id, [TypeArg])]
l <- ((Id, [TypeArg]) -> State Env (Id, [TypeArg]))
-> [(Id, [TypeArg])] -> State Env [(Id, [TypeArg])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ( \ (i :: Id
i, tArgs :: [TypeArg]
tArgs) -> do
            Env
e <- State Env Env
forall s. State s s
get
            [Maybe TypeArg]
newAs <- (TypeArg -> State Env (Maybe TypeArg))
-> [TypeArg] -> State Env [Maybe TypeArg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TypeArg -> State Env (Maybe TypeArg)
anaddTypeVarDecl [TypeArg]
tArgs
            Env -> State Env ()
forall s. s -> State s ()
put Env
e
            (Id, [TypeArg]) -> State Env (Id, [TypeArg])
forall (m :: * -> *) a. Monad m => a -> m a
return (Id
i, [Maybe TypeArg] -> [TypeArg]
forall a. [Maybe a] -> [a]
catMaybes [Maybe TypeArg]
newAs)) [(Id, [TypeArg])]
ol
    let g :: [[[TypeArg]]]
g = [[TypeArg]] -> [[[TypeArg]]]
forall a. Eq a => [a] -> [[a]]
group ([[TypeArg]] -> [[[TypeArg]]]) -> [[TypeArg]] -> [[[TypeArg]]]
forall a b. (a -> b) -> a -> b
$ ((Id, [TypeArg]) -> [TypeArg]) -> [(Id, [TypeArg])] -> [[TypeArg]]
forall a b. (a -> b) -> [a] -> [b]
map (Id, [TypeArg]) -> [TypeArg]
forall a b. (a, b) -> b
snd [(Id, [TypeArg])]
l
    case [[[TypeArg]]]
g of
      [_ : _] -> do
         [Maybe TypeArg]
newAs <- (TypeArg -> State Env (Maybe TypeArg))
-> [TypeArg] -> State Env [Maybe TypeArg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TypeArg -> State Env (Maybe TypeArg)
anaddTypeVarDecl ([TypeArg] -> State Env [Maybe TypeArg])
-> [TypeArg] -> State Env [Maybe TypeArg]
forall a b. (a -> b) -> a -> b
$ (Id, [TypeArg]) -> [TypeArg]
forall a b. (a, b) -> b
snd ((Id, [TypeArg]) -> [TypeArg]) -> (Id, [TypeArg]) -> [TypeArg]
forall a b. (a -> b) -> a -> b
$ [(Id, [TypeArg])] -> (Id, [TypeArg])
forall a. [a] -> a
head [(Id, [TypeArg])]
l
         [(Id, [TypeArg])] -> State Env [(Id, [TypeArg])]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Id, [TypeArg])] -> State Env [(Id, [TypeArg])])
-> [(Id, [TypeArg])] -> State Env [(Id, [TypeArg])]
forall a b. (a -> b) -> a -> b
$ ((Id, [TypeArg]) -> (Id, [TypeArg]))
-> [(Id, [TypeArg])] -> [(Id, [TypeArg])]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: Id
i, _) -> (Id
i, [Maybe TypeArg] -> [TypeArg]
forall a. [Maybe a] -> [a]
catMaybes [Maybe TypeArg]
newAs)) [(Id, [TypeArg])]
l
      _ -> do
        [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> [(Id, [TypeArg])] -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
            "variables must be identical for all types within one item" [(Id, [TypeArg])]
l]
        [(Id, [TypeArg])] -> State Env [(Id, [TypeArg])]
forall (m :: * -> *) a. Monad m => a -> m a
return []

anaSubtypeDecl :: [TypePattern] -> Type -> Range -> State Env (Maybe TypeItem)
anaSubtypeDecl :: [TypePattern] -> Type -> Range -> State Env (Maybe TypeItem)
anaSubtypeDecl pats :: [TypePattern]
pats t :: Type
t ps :: Range
ps = do
    let Result ds :: [Diagnosis]
ds (Just is :: [(Id, [TypeArg])]
is) = [TypePattern] -> Result [(Id, [TypeArg])]
convertTypePatterns [TypePattern]
pats
    [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds
    LocalTypeVars
tvs <- (Env -> LocalTypeVars) -> State Env LocalTypeVars
forall s a. (s -> a) -> State s a
gets Env -> LocalTypeVars
localTypeVars
    [(Id, [TypeArg])]
nis <- [(Id, [TypeArg])] -> State Env [(Id, [TypeArg])]
setTypePatternVars [(Id, [TypeArg])]
is
    let newPats :: [TypePattern]
newPats = ((Id, [TypeArg]) -> TypePattern)
-> [(Id, [TypeArg])] -> [TypePattern]
forall a b. (a -> b) -> [a] -> [b]
map (Id, [TypeArg]) -> TypePattern
toTypePattern [(Id, [TypeArg])]
nis
    Env
te <- State Env Env
forall s. State s s
get
    LocalTypeVars -> State Env ()
putLocalTypeVars LocalTypeVars
tvs
    let Result es :: [Diagnosis]
es mp :: Maybe ((RawKind, Set Kind), Type)
mp = (Maybe Kind, Type) -> Env -> Result ((RawKind, Set Kind), Type)
anaTypeM (Maybe Kind
forall a. Maybe a
Nothing, Type
t) Env
te
    case Maybe ((RawKind, Set Kind), Type)
mp of
      Nothing -> do
        ((Id, [TypeArg]) -> State Env (Maybe (Id, [TypeArg])))
-> [(Id, [TypeArg])] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TypeDefn
-> Kind -> (Id, [TypeArg]) -> State Env (Maybe (Id, [TypeArg]))
addTypePattern TypeDefn
NoTypeDefn Kind
universe) [(Id, [TypeArg])]
is
        if [TypePattern] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypePattern]
newPats then Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeItem
forall a. Maybe a
Nothing else case Type
t of
            TypeToken tt :: Token
tt -> do
                let tid :: Id
tid = Token -> Id
simpleIdToId Token
tt
                    newT :: Type
newT = Id -> RawKind -> Int -> Type
TypeName Id
tid RawKind
rStar 0
                Bool -> TypeDefn -> Kind -> Id -> State Env Bool
addTypeId Bool
False TypeDefn
NoTypeDefn Kind
universe Id
tid
                ((Id, [TypeArg]) -> State Env ())
-> [(Id, [TypeArg])] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Type -> Kind -> (Id, [TypeArg]) -> State Env ()
addSuperType Type
newT Kind
universe) [(Id, [TypeArg])]
nis
                Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeItem -> State Env (Maybe TypeItem))
-> Maybe TypeItem -> State Env (Maybe TypeItem)
forall a b. (a -> b) -> a -> b
$ TypeItem -> Maybe TypeItem
forall a. a -> Maybe a
Just (TypeItem -> Maybe TypeItem) -> TypeItem -> Maybe TypeItem
forall a b. (a -> b) -> a -> b
$ [TypePattern] -> Type -> Range -> TypeItem
SubtypeDecl [TypePattern]
newPats Type
newT Range
ps
            _ -> do
                [Diagnosis] -> State Env ()
addDiags [Diagnosis]
es
                Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeItem -> State Env (Maybe TypeItem))
-> Maybe TypeItem -> State Env (Maybe TypeItem)
forall a b. (a -> b) -> a -> b
$ TypeItem -> Maybe TypeItem
forall a. a -> Maybe a
Just (TypeItem -> Maybe TypeItem) -> TypeItem -> Maybe TypeItem
forall a b. (a -> b) -> a -> b
$ [TypePattern] -> Kind -> Range -> TypeItem
TypeDecl [TypePattern]
newPats Kind
universe Range
ps
      Just ((rk :: RawKind
rk, ks :: Set Kind
ks), newT :: Type
newT) -> Set Kind
-> RawKind
-> Type
-> (Kind -> State Env (Maybe TypeItem))
-> State Env (Maybe TypeItem)
forall a b.
(GetRange a, Pretty a) =>
Set Kind
-> RawKind
-> a
-> (Kind -> State Env (Maybe b))
-> State Env (Maybe b)
nonUniqueKind Set Kind
ks RawKind
rk Type
t ((Kind -> State Env (Maybe TypeItem))
 -> State Env (Maybe TypeItem))
-> (Kind -> State Env (Maybe TypeItem))
-> State Env (Maybe TypeItem)
forall a b. (a -> b) -> a -> b
$ \ kind :: Kind
kind -> do
          ((Id, [TypeArg]) -> State Env (Maybe (Id, [TypeArg])))
-> [(Id, [TypeArg])] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TypeDefn
-> Kind -> (Id, [TypeArg]) -> State Env (Maybe (Id, [TypeArg]))
addTypePattern TypeDefn
NoTypeDefn Kind
kind) [(Id, [TypeArg])]
is
          ((Id, [TypeArg]) -> State Env ())
-> [(Id, [TypeArg])] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Type -> Kind -> (Id, [TypeArg]) -> State Env ()
addSuperType Type
newT (Kind -> (Id, [TypeArg]) -> State Env ())
-> Kind -> (Id, [TypeArg]) -> State Env ()
forall a b. (a -> b) -> a -> b
$ RawKind -> Kind
rawToKind RawKind
rk) [(Id, [TypeArg])]
nis
          Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeItem -> State Env (Maybe TypeItem))
-> Maybe TypeItem -> State Env (Maybe TypeItem)
forall a b. (a -> b) -> a -> b
$ if [(Id, [TypeArg])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Id, [TypeArg])]
nis then Maybe TypeItem
forall a. Maybe a
Nothing else
                       TypeItem -> Maybe TypeItem
forall a. a -> Maybe a
Just (TypeItem -> Maybe TypeItem) -> TypeItem -> Maybe TypeItem
forall a b. (a -> b) -> a -> b
$ [TypePattern] -> Type -> Range -> TypeItem
SubtypeDecl [TypePattern]
newPats Type
newT Range
ps

anaSubtypeDefn :: Annoted TypeItem -> TypePattern -> Vars -> Type
               -> Annoted Term -> Range -> State Env (Maybe TypeItem)
anaSubtypeDefn :: Annoted TypeItem
-> TypePattern
-> Vars
-> Type
-> Annoted Term
-> Range
-> State Env (Maybe TypeItem)
anaSubtypeDefn aitm :: Annoted TypeItem
aitm pat :: TypePattern
pat v :: Vars
v t :: Type
t f :: Annoted Term
f ps :: Range
ps = do
    let Result ds :: [Diagnosis]
ds m :: Maybe (Id, [TypeArg])
m = TypePattern -> Result (Id, [TypeArg])
convertTypePattern TypePattern
pat
    [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds
    case Maybe (Id, [TypeArg])
m of
      Nothing -> Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeItem
forall a. Maybe a
Nothing
      Just (i :: Id
i, tArgs :: [TypeArg]
tArgs) -> do
        LocalTypeVars
tvs <- (Env -> LocalTypeVars) -> State Env LocalTypeVars
forall s a. (s -> a) -> State s a
gets Env -> LocalTypeVars
localTypeVars
        [Maybe TypeArg]
newAs <- (TypeArg -> State Env (Maybe TypeArg))
-> [TypeArg] -> State Env [Maybe TypeArg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TypeArg -> State Env (Maybe TypeArg)
anaddTypeVarDecl [TypeArg]
tArgs
        Maybe Type
mt <- Type -> State Env (Maybe Type)
anaStarType Type
t
        LocalTypeVars -> State Env ()
putLocalTypeVars LocalTypeVars
tvs
        case Maybe Type
mt of
          Nothing -> Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeItem
forall a. Maybe a
Nothing
          Just ty :: Type
ty -> do
            let nAs :: [TypeArg]
nAs = [Maybe TypeArg] -> [TypeArg]
forall a. [Maybe a] -> [a]
catMaybes [Maybe TypeArg]
newAs
                fullKind :: Kind
fullKind = [TypeArg] -> Kind -> Kind
typeArgsListToKind [TypeArg]
nAs Kind
universe
                jTy :: Type
jTy = Id -> RawKind -> Int -> Type
TypeName Id
i ([TypeArg] -> RawKind -> RawKind
typeArgsListToRawKind [TypeArg]
nAs RawKind
rStar) 0
                aTy :: Type
aTy = Type -> [Type] -> Type
mkTypeAppl Type
jTy ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (TypeArg -> Type) -> [TypeArg] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> Type
typeArgToType [TypeArg]
nAs
            Env
e <- State Env Env
forall s. State s s
get
            let Result es :: [Diagnosis]
es mvds :: Maybe Term
mvds = Env -> Vars -> Type -> Result Term
anaVars Env
e Vars
v (Type -> Result Term) -> Type -> Result Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
monoType Type
ty
            [Diagnosis] -> State Env ()
addDiags [Diagnosis]
es
            if Id -> Type -> Bool
cyclicType Id
i Type
ty then do
                [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Type -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                          "illegal recursive subtype definition" Type
ty]
                Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeItem
forall a. Maybe a
Nothing
              else case Maybe Term
mvds of
                Nothing -> Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeItem
forall a. Maybe a
Nothing
                Just vtt :: Term
vtt -> do
                  let vds :: [VarDecl]
vds = Term -> [VarDecl]
extractVars Term
vtt
                  [VarDecl] -> State Env ()
checkUniqueVars [VarDecl]
vds
                  Map Id VarDefn
vs <- (Env -> Map Id VarDefn) -> State Env (Map Id VarDefn)
forall s a. (s -> a) -> State s a
gets Env -> Map Id VarDefn
localVars
                  (VarDecl -> State Env ()) -> [VarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> VarDecl -> State Env ()
addLocalVar Bool
True) [VarDecl]
vds
                  Maybe (Annoted Term, Annoted Term)
mf <- Annoted Term -> State Env (Maybe (Annoted Term, Annoted Term))
anaFormula Annoted Term
f
                  Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
                  case Maybe (Annoted Term, Annoted Term)
mf of
                    Nothing -> Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeItem
forall a. Maybe a
Nothing
                    Just (newF :: Annoted Term
newF, resF :: Annoted Term
resF) -> do
                      Bool -> TypeDefn -> Kind -> Id -> State Env Bool
addTypeId Bool
True TypeDefn
NoTypeDefn Kind
fullKind Id
i
                      Type -> Kind -> (Id, [TypeArg]) -> State Env ()
addSuperType Type
ty Kind
universe (Id
i, [TypeArg]
nAs)
                      let lab1 :: String
lab1 = Annoted Term -> String
forall a. Annoted a -> String
getRLabel Annoted Term
resF
                          lab :: String
lab = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
lab1 then Annoted TypeItem -> String
forall a. Annoted a -> String
getRLabel Annoted TypeItem
aitm else String
lab1
                      [SenAttr Sentence String] -> State Env ()
appendSentences [String -> Sentence -> SenAttr Sentence String
forall a s. a -> s -> SenAttr s a
makeNamed String
lab
                        (Sentence -> SenAttr Sentence String)
-> Sentence -> SenAttr Sentence String
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
Formula (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ Env -> Term -> Range -> Term
mkEnvForall Env
e (
                              [GenVarDecl] -> Term -> Term
mkForall ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl]
vds)
                              (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
ps
                              (Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
vtt TypeQual
InType Type
aTy Range
ps) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Annoted Term -> Term
forall a. Annoted a -> a
item Annoted Term
resF) Range
ps]
                      Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeItem -> State Env (Maybe TypeItem))
-> Maybe TypeItem -> State Env (Maybe TypeItem)
forall a b. (a -> b) -> a -> b
$ TypeItem -> Maybe TypeItem
forall a. a -> Maybe a
Just (TypeItem -> Maybe TypeItem) -> TypeItem -> Maybe TypeItem
forall a b. (a -> b) -> a -> b
$ TypePattern -> Vars -> Type -> Annoted Term -> Range -> TypeItem
SubtypeDefn (Id -> [TypeArg] -> Range -> TypePattern
TypePattern Id
i [TypeArg]
nAs Range
nullRange)
                                    Vars
v Type
ty Annoted Term
newF Range
ps

anaAliasType :: TypePattern -> Maybe Kind -> TypeScheme
             -> Range -> State Env (Maybe TypeItem)
anaAliasType :: TypePattern
-> Maybe Kind -> TypeScheme -> Range -> State Env (Maybe TypeItem)
anaAliasType pat :: TypePattern
pat mk :: Maybe Kind
mk sc :: TypeScheme
sc ps :: Range
ps = do
    let Result ds :: [Diagnosis]
ds m :: Maybe (Id, [TypeArg])
m = TypePattern -> Result (Id, [TypeArg])
convertTypePattern TypePattern
pat
    [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds
    case Maybe (Id, [TypeArg])
m of
      Nothing -> Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeItem
forall a. Maybe a
Nothing
      Just (i :: Id
i, tArgs :: [TypeArg]
tArgs) -> do
        LocalTypeVars
tvs <- (Env -> LocalTypeVars) -> State Env LocalTypeVars
forall s a. (s -> a) -> State s a
gets Env -> LocalTypeVars
localTypeVars -- save variables
        [Maybe TypeArg]
newAs <- (TypeArg -> State Env (Maybe TypeArg))
-> [TypeArg] -> State Env [Maybe TypeArg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TypeArg -> State Env (Maybe TypeArg)
anaddTypeVarDecl [TypeArg]
tArgs
        (ik :: Kind
ik, mt :: Maybe TypeScheme
mt) <- Maybe Kind -> TypeScheme -> State Env (Kind, Maybe TypeScheme)
anaPseudoType Maybe Kind
mk TypeScheme
sc
        LocalTypeVars -> State Env ()
putLocalTypeVars LocalTypeVars
tvs
        case Maybe TypeScheme
mt of
          Nothing -> Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeItem
forall a. Maybe a
Nothing
          Just (TypeScheme args :: [TypeArg]
args ty :: Type
ty qs :: Range
qs) ->
            if Id -> Type -> Bool
cyclicType Id
i Type
ty then do
                [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Type -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "illegal recursive type synonym" Type
ty]
                Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeItem
forall a. Maybe a
Nothing
              else do
                let nAs :: [TypeArg]
nAs = [Maybe TypeArg] -> [TypeArg]
forall a. [Maybe a] -> [a]
catMaybes [Maybe TypeArg]
newAs
                    allArgs :: [TypeArg]
allArgs = [TypeArg]
nAs [TypeArg] -> [TypeArg] -> [TypeArg]
forall a. [a] -> [a] -> [a]
++ [TypeArg]
args
                    fullKind :: Kind
fullKind = [TypeArg] -> Kind -> Kind
typeArgsListToKind [TypeArg]
nAs Kind
ik
                    allSc :: TypeScheme
allSc = [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg]
allArgs Type
ty Range
qs
                Bool
b <- Bool -> Id -> TypeScheme -> Kind -> State Env Bool
addAliasType Bool
True Id
i TypeScheme
allSc Kind
fullKind
                TypeMap
tm <- (Env -> TypeMap) -> State Env TypeMap
forall s a. (s -> a) -> State s a
gets Env -> TypeMap
typeMap
                TypeMap -> State Env ()
putTypeMap (TypeMap -> State Env ()) -> TypeMap -> State Env ()
forall a b. (a -> b) -> a -> b
$ (TypeInfo -> TypeInfo) -> TypeMap -> TypeMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ( \ ti :: TypeInfo
ti -> case TypeInfo -> TypeDefn
typeDefn TypeInfo
ti of
                    AliasTypeDefn y :: Type
y -> TypeInfo
ti
                      { typeDefn :: TypeDefn
typeDefn = Type -> TypeDefn
AliasTypeDefn (Type -> TypeDefn) -> Type -> TypeDefn
forall a b. (a -> b) -> a -> b
$ TypeMap -> Type -> Type
expandAux TypeMap
tm Type
y }
                    _ -> TypeInfo
ti) TypeMap
tm
                Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeItem -> State Env (Maybe TypeItem))
-> Maybe TypeItem -> State Env (Maybe TypeItem)
forall a b. (a -> b) -> a -> b
$ if Bool
b then TypeItem -> Maybe TypeItem
forall a. a -> Maybe a
Just (TypeItem -> Maybe TypeItem) -> TypeItem -> Maybe TypeItem
forall a b. (a -> b) -> a -> b
$ TypePattern -> Maybe Kind -> TypeScheme -> Range -> TypeItem
AliasType
                    (Id -> [TypeArg] -> Range -> TypePattern
TypePattern Id
i [] Range
nullRange) (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
fullKind) TypeScheme
allSc Range
ps
                         else Maybe TypeItem
forall a. Maybe a
Nothing

-- | analyse a 'TypeItem'
anaTypeItem :: GenKind -> [DataPat] -> Annoted TypeItem
            -> State Env (Maybe TypeItem)
anaTypeItem :: GenKind
-> [DataPat] -> Annoted TypeItem -> State Env (Maybe TypeItem)
anaTypeItem gk :: GenKind
gk tys :: [DataPat]
tys aitm :: Annoted TypeItem
aitm = case Annoted TypeItem -> TypeItem
forall a. Annoted a -> a
item Annoted TypeItem
aitm of
    TypeDecl pats :: [TypePattern]
pats kind :: Kind
kind ps :: Range
ps -> [TypePattern] -> Kind -> Range -> State Env (Maybe TypeItem)
anaTypeDecl [TypePattern]
pats Kind
kind Range
ps
    SubtypeDecl pats :: [TypePattern]
pats t :: Type
t ps :: Range
ps -> [TypePattern] -> Type -> Range -> State Env (Maybe TypeItem)
anaSubtypeDecl [TypePattern]
pats Type
t Range
ps
    IsoDecl pats :: [TypePattern]
pats ps :: Range
ps -> [TypePattern] -> Range -> State Env (Maybe TypeItem)
anaIsoDecl [TypePattern]
pats Range
ps
    SubtypeDefn pat :: TypePattern
pat v :: Vars
v t :: Type
t f :: Annoted Term
f ps :: Range
ps -> Annoted TypeItem
-> TypePattern
-> Vars
-> Type
-> Annoted Term
-> Range
-> State Env (Maybe TypeItem)
anaSubtypeDefn Annoted TypeItem
aitm TypePattern
pat Vars
v Type
t Annoted Term
f Range
ps
    AliasType pat :: TypePattern
pat mk :: Maybe Kind
mk sc :: TypeScheme
sc ps :: Range
ps -> TypePattern
-> Maybe Kind -> TypeScheme -> Range -> State Env (Maybe TypeItem)
anaAliasType TypePattern
pat Maybe Kind
mk TypeScheme
sc Range
ps
    Datatype d :: DatatypeDecl
d -> do
        Maybe DatatypeDecl
mD <- GenKind
-> [DataPat]
-> Annoted DatatypeDecl
-> State Env (Maybe DatatypeDecl)
anaDatatype GenKind
gk [DataPat]
tys (Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl))
-> Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl)
forall a b. (a -> b) -> a -> b
$ DatatypeDecl -> Annoted TypeItem -> Annoted DatatypeDecl
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted DatatypeDecl
d Annoted TypeItem
aitm
        case Maybe DatatypeDecl
mD of
          Nothing -> Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeItem
forall a. Maybe a
Nothing
          Just newD :: DatatypeDecl
newD -> Maybe TypeItem -> State Env (Maybe TypeItem)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeItem -> State Env (Maybe TypeItem))
-> Maybe TypeItem -> State Env (Maybe TypeItem)
forall a b. (a -> b) -> a -> b
$ TypeItem -> Maybe TypeItem
forall a. a -> Maybe a
Just (TypeItem -> Maybe TypeItem) -> TypeItem -> Maybe TypeItem
forall a b. (a -> b) -> a -> b
$ DatatypeDecl -> TypeItem
Datatype DatatypeDecl
newD

-- | pre-analyse a data type for 'anaDatatype'
ana1Datatype :: Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl)
ana1Datatype :: Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl)
ana1Datatype aitm :: Annoted DatatypeDecl
aitm = do
    let DatatypeDecl pat :: TypePattern
pat kind :: Kind
kind alts :: [Annoted Alternative]
alts derivs :: [Id]
derivs ps :: Range
ps = Annoted DatatypeDecl -> DatatypeDecl
forall a. Annoted a -> a
item Annoted DatatypeDecl
aitm
    ClassMap
cm <- (Env -> ClassMap) -> State Env ClassMap
forall s a. (s -> a) -> State s a
gets Env -> ClassMap
classMap
    let Result cs :: [Diagnosis]
cs (Just rk :: RawKind
rk) = Kind -> ClassMap -> Result RawKind
anaKindM Kind
kind ClassMap
cm
        k :: Kind
k = if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
cs then Kind
kind else Kind
universe
    [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ TypePattern -> RawKind -> RawKind -> [Diagnosis]
forall a.
(GetRange a, Pretty a) =>
a -> RawKind -> RawKind -> [Diagnosis]
checkKinds TypePattern
pat RawKind
rStar RawKind
rk [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
cs
    let rms :: [Result RawKind]
rms = (Id -> Result RawKind) -> [Id] -> [Result RawKind]
forall a b. (a -> b) -> [a] -> [b]
map ( \ c :: Id
c -> Kind -> ClassMap -> Result RawKind
anaKindM (Id -> Kind
forall a. a -> AnyKind a
ClassKind Id
c) ClassMap
cm) [Id]
derivs
        mcs :: [Maybe RawKind]
mcs = (Result RawKind -> Maybe RawKind)
-> [Result RawKind] -> [Maybe RawKind]
forall a b. (a -> b) -> [a] -> [b]
map Result RawKind -> Maybe RawKind
forall a. Result a -> Maybe a
maybeResult [Result RawKind]
rms
        jcs :: [RawKind]
jcs = [Maybe RawKind] -> [RawKind]
forall a. [Maybe a] -> [a]
catMaybes [Maybe RawKind]
mcs
        newDerivs :: [Id]
newDerivs = ((Id, Maybe RawKind) -> Id) -> [(Id, Maybe RawKind)] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (Id, Maybe RawKind) -> Id
forall a b. (a, b) -> a
fst ([(Id, Maybe RawKind)] -> [Id]) -> [(Id, Maybe RawKind)] -> [Id]
forall a b. (a -> b) -> a -> b
$ ((Id, Maybe RawKind) -> Bool)
-> [(Id, Maybe RawKind)] -> [(Id, Maybe RawKind)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe RawKind -> Bool
forall a. Maybe a -> Bool
isJust (Maybe RawKind -> Bool)
-> ((Id, Maybe RawKind) -> Maybe RawKind)
-> (Id, Maybe RawKind)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, Maybe RawKind) -> Maybe RawKind
forall a b. (a, b) -> b
snd) ([(Id, Maybe RawKind)] -> [(Id, Maybe RawKind)])
-> [(Id, Maybe RawKind)] -> [(Id, Maybe RawKind)]
forall a b. (a -> b) -> a -> b
$ [Id] -> [Maybe RawKind] -> [(Id, Maybe RawKind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
derivs [Maybe RawKind]
mcs
        Result ds :: [Diagnosis]
ds m :: Maybe (Id, [TypeArg])
m = TypePattern -> Result (Id, [TypeArg])
convertTypePattern TypePattern
pat
    [Diagnosis] -> State Env ()
addDiags ([Diagnosis]
ds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ (Result RawKind -> [Diagnosis]) -> [Result RawKind] -> [Diagnosis]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Result RawKind -> [Diagnosis]
forall a. Result a -> [Diagnosis]
diags [Result RawKind]
rms)
    [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ (RawKind -> [Diagnosis]) -> [RawKind] -> [Diagnosis]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (TypePattern -> RawKind -> RawKind -> [Diagnosis]
forall a.
(GetRange a, Pretty a) =>
a -> RawKind -> RawKind -> [Diagnosis]
checkKinds TypePattern
pat RawKind
rStar) [RawKind]
jcs
    case Maybe (Id, [TypeArg])
m of
      Nothing -> Maybe DatatypeDecl -> State Env (Maybe DatatypeDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe DatatypeDecl
forall a. Maybe a
Nothing
      Just (i :: Id
i, tArgs :: [TypeArg]
tArgs) -> do
          LocalTypeVars
tvs <- (Env -> LocalTypeVars) -> State Env LocalTypeVars
forall s a. (s -> a) -> State s a
gets Env -> LocalTypeVars
localTypeVars
          [Maybe TypeArg]
newAs <- (TypeArg -> State Env (Maybe TypeArg))
-> [TypeArg] -> State Env [Maybe TypeArg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TypeArg -> State Env (Maybe TypeArg)
anaddTypeVarDecl [TypeArg]
tArgs
          LocalTypeVars -> State Env ()
putLocalTypeVars LocalTypeVars
tvs
          let nAs :: [TypeArg]
nAs = [Maybe TypeArg] -> [TypeArg]
forall a. [Maybe a] -> [a]
catMaybes [Maybe TypeArg]
newAs
              fullKind :: Kind
fullKind = [TypeArg] -> Kind -> Kind
typeArgsListToKind [TypeArg]
nAs Kind
k
          [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> [Diagnosis]
checkUniqueTypevars [TypeArg]
nAs
          Bool
b <- Bool -> TypeDefn -> Kind -> Id -> State Env Bool
addTypeId Bool
False TypeDefn
PreDatatype Kind
fullKind Id
i
          Maybe DatatypeDecl -> State Env (Maybe DatatypeDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DatatypeDecl -> State Env (Maybe DatatypeDecl))
-> Maybe DatatypeDecl -> State Env (Maybe DatatypeDecl)
forall a b. (a -> b) -> a -> b
$ if Bool
b then DatatypeDecl -> Maybe DatatypeDecl
forall a. a -> Maybe a
Just (DatatypeDecl -> Maybe DatatypeDecl)
-> DatatypeDecl -> Maybe DatatypeDecl
forall a b. (a -> b) -> a -> b
$ TypePattern
-> Kind -> [Annoted Alternative] -> [Id] -> Range -> DatatypeDecl
DatatypeDecl
                     (Id -> [TypeArg] -> Range -> TypePattern
TypePattern Id
i [TypeArg]
nAs Range
nullRange) Kind
k [Annoted Alternative]
alts [Id]
newDerivs Range
ps
                   else Maybe DatatypeDecl
forall a. Maybe a
Nothing

-- | convert a data type with an analysed type pattern to a data pattern
dataPatToType :: DatatypeDecl -> State Env DataPat
dataPatToType :: DatatypeDecl -> State Env DataPat
dataPatToType d :: DatatypeDecl
d = case DatatypeDecl
d of
    DatatypeDecl (TypePattern i :: Id
i nAs :: [TypeArg]
nAs _) k :: Kind
k _ _ _ -> do
      RawKind
rk <- Kind -> State Env RawKind
anaKind Kind
k
      DataPat -> State Env DataPat
forall (m :: * -> *) a. Monad m => a -> m a
return (DataPat -> State Env DataPat) -> DataPat -> State Env DataPat
forall a b. (a -> b) -> a -> b
$ IdMap -> Id -> [TypeArg] -> RawKind -> Type -> DataPat
DataPat IdMap
forall k a. Map k a
Map.empty Id
i [TypeArg]
nAs RawKind
rk (Type -> DataPat) -> Type -> DataPat
forall a b. (a -> b) -> a -> b
$ Id -> [TypeArg] -> RawKind -> Type
patToType Id
i [TypeArg]
nAs RawKind
rk
    _ -> String -> State Env DataPat
forall a. HasCallStack => String -> a
error "dataPatToType"

addDataSubtype :: DataPat -> Kind -> Type -> State Env ()
addDataSubtype :: DataPat -> Kind -> Type -> State Env ()
addDataSubtype (DataPat _ _ nAs :: [TypeArg]
nAs _ rt :: Type
rt) k :: Kind
k st :: Type
st = case Type
st of
    TypeName i :: Id
i _ _ -> Type -> Kind -> (Id, [TypeArg]) -> State Env ()
addSuperType Type
rt Kind
k (Id
i, [TypeArg]
nAs)
    _ -> [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Type -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "data subtype ignored" Type
st]

-- | analyse a pre-analysed data type given all data patterns of the type item
anaDatatype :: GenKind -> [DataPat]
            -> Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl)
anaDatatype :: GenKind
-> [DataPat]
-> Annoted DatatypeDecl
-> State Env (Maybe DatatypeDecl)
anaDatatype genKind :: GenKind
genKind tys :: [DataPat]
tys d :: Annoted DatatypeDecl
d = case Annoted DatatypeDecl -> DatatypeDecl
forall a. Annoted a -> a
item Annoted DatatypeDecl
d of
    itd :: DatatypeDecl
itd@(DatatypeDecl (TypePattern i :: Id
i nAs :: [TypeArg]
nAs _) k :: Kind
k alts :: [Annoted Alternative]
alts _ _) -> do
       -- recompute data pattern rather than looking it up in tys
       dt :: DataPat
dt@(DataPat _ _ _ rk :: RawKind
rk _) <- DatatypeDecl -> State Env DataPat
dataPatToType DatatypeDecl
itd
       let fullKind :: Kind
fullKind = [TypeArg] -> Kind -> Kind
typeArgsListToKind [TypeArg]
nAs Kind
k
       LocalTypeVars
tvs <- (Env -> LocalTypeVars) -> State Env LocalTypeVars
forall s a. (s -> a) -> State s a
gets Env -> LocalTypeVars
localTypeVars
       (TypeArg -> State Env ()) -> [TypeArg] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> TypeArg -> State Env ()
addTypeVarDecl Bool
False (TypeArg -> State Env ())
-> (TypeArg -> TypeArg) -> TypeArg -> State Env ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeArg -> TypeArg
nonVarTypeArg) [TypeArg]
nAs
       Maybe [AltDefn]
mNewAlts <- (Env -> Result [AltDefn]) -> State Env (Maybe [AltDefn])
forall a. (Env -> Result a) -> State Env (Maybe a)
fromResult ((Env -> Result [AltDefn]) -> State Env (Maybe [AltDefn]))
-> (Env -> Result [AltDefn]) -> State Env (Maybe [AltDefn])
forall a b. (a -> b) -> a -> b
$ GenKind
-> [DataPat] -> DataPat -> [Alternative] -> Env -> Result [AltDefn]
anaAlts GenKind
genKind [DataPat]
tys DataPat
dt ((Annoted Alternative -> Alternative)
-> [Annoted Alternative] -> [Alternative]
forall a b. (a -> b) -> [a] -> [b]
map Annoted Alternative -> Alternative
forall a. Annoted a -> a
item [Annoted Alternative]
alts)
       LocalTypeVars -> State Env ()
putLocalTypeVars LocalTypeVars
tvs
       case Maybe [AltDefn]
mNewAlts of
         Nothing -> Maybe DatatypeDecl -> State Env (Maybe DatatypeDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe DatatypeDecl
forall a. Maybe a
Nothing
         Just newAlts :: [AltDefn]
newAlts -> do
           (Type -> State Env ()) -> [Type] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (DataPat -> Kind -> Type -> State Env ()
addDataSubtype DataPat
dt Kind
fullKind) ([Type] -> State Env ()) -> [Type] -> State Env ()
forall a b. (a -> b) -> a -> b
$ (AltDefn -> [Type] -> [Type]) -> [Type] -> [AltDefn] -> [Type]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
             ( \ (Construct mc :: Maybe Id
mc ts :: [Type]
ts _ _) l :: [Type]
l -> case Maybe Id
mc of
               Nothing -> [Type]
ts [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
l
               Just _ -> [Type]
l) [] [AltDefn]
newAlts
           let gArgs :: [TypeArg]
gArgs = [TypeArg] -> [TypeArg]
genTypeArgs [TypeArg]
nAs
               iMap :: IdMap
iMap = [(Id, Id)] -> IdMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Id, Id)] -> IdMap) -> [(Id, Id)] -> IdMap
forall a b. (a -> b) -> a -> b
$ (DataPat -> (Id, Id)) -> [DataPat] -> [(Id, Id)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (DataPat _ j :: Id
j _ _ _) -> (Id
j, Id
j)) [DataPat]
tys
               de :: DataEntry
de = IdMap
-> Id
-> GenKind
-> [TypeArg]
-> RawKind
-> Set AltDefn
-> DataEntry
DataEntry IdMap
iMap Id
i GenKind
genKind [TypeArg]
gArgs RawKind
rk
                    (Set AltDefn -> DataEntry) -> Set AltDefn -> DataEntry
forall a b. (a -> b) -> a -> b
$ [AltDefn] -> Set AltDefn
forall a. Ord a => [a] -> Set a
Set.fromList [AltDefn]
newAlts
               dp :: DataPat
dp = DataEntry -> DataPat
toDataPat DataEntry
de
           (AltDefn -> State Env ()) -> [AltDefn] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( \ (Construct mc :: Maybe Id
mc tc :: [Type]
tc p :: Partiality
p sels :: [[Selector]]
sels) -> case Maybe Id
mc of
               Nothing -> () -> State Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
               Just c :: Id
c -> do
                 let sc :: TypeScheme
sc = DataPat -> Partiality -> [Type] -> TypeScheme
getConstrScheme DataPat
dp Partiality
p [Type]
tc
                 Id -> TypeScheme -> Set OpAttr -> OpDefn -> State Env Bool
addOpId Id
c TypeScheme
sc Set OpAttr
forall a. Set a
Set.empty (Id -> OpDefn
ConstructData Id
i)
                 (Selector -> State Env Bool) -> [Selector] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( \ (Select ms :: Maybe Id
ms ts :: Type
ts pa :: Partiality
pa) -> case Maybe Id
ms of
                   Just s :: Id
s ->
                     Id -> TypeScheme -> Set OpAttr -> OpDefn -> State Env Bool
addOpId Id
s (DataPat -> Partiality -> Type -> TypeScheme
getSelScheme DataPat
dp Partiality
pa Type
ts) Set OpAttr
forall a. Set a
Set.empty (OpDefn -> State Env Bool) -> OpDefn -> State Env Bool
forall a b. (a -> b) -> a -> b
$ Set ConstrInfo -> Id -> OpDefn
SelectData
                         (ConstrInfo -> Set ConstrInfo
forall a. a -> Set a
Set.singleton (ConstrInfo -> Set ConstrInfo) -> ConstrInfo -> Set ConstrInfo
forall a b. (a -> b) -> a -> b
$ Id -> TypeScheme -> ConstrInfo
ConstrInfo Id
c TypeScheme
sc) Id
i
                   Nothing -> Bool -> State Env Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) ([Selector] -> State Env ()) -> [Selector] -> State Env ()
forall a b. (a -> b) -> a -> b
$ [[Selector]] -> [Selector]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Selector]]
sels) [AltDefn]
newAlts
           Bool -> TypeDefn -> Kind -> Id -> State Env Bool
addTypeId Bool
True (DataEntry -> TypeDefn
DatatypeDefn DataEntry
de) Kind
fullKind Id
i
           [SenAttr Sentence String] -> State Env ()
appendSentences ([SenAttr Sentence String] -> State Env ())
-> [SenAttr Sentence String] -> State Env ()
forall a b. (a -> b) -> a -> b
$ DataPat -> [AltDefn] -> [SenAttr Sentence String]
makeDataSelEqs DataPat
dp [AltDefn]
newAlts
           Maybe DatatypeDecl -> State Env (Maybe DatatypeDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DatatypeDecl -> State Env (Maybe DatatypeDecl))
-> Maybe DatatypeDecl -> State Env (Maybe DatatypeDecl)
forall a b. (a -> b) -> a -> b
$ DatatypeDecl -> Maybe DatatypeDecl
forall a. a -> Maybe a
Just DatatypeDecl
itd
    _ -> String -> State Env (Maybe DatatypeDecl)
forall a. HasCallStack => String -> a
error "anaDatatype (not preprocessed)"

-- | analyse a pseudo type (represented as a 'TypeScheme')
anaPseudoType :: Maybe Kind -> TypeScheme -> State Env (Kind, Maybe TypeScheme)
anaPseudoType :: Maybe Kind -> TypeScheme -> State Env (Kind, Maybe TypeScheme)
anaPseudoType mk :: Maybe Kind
mk (TypeScheme tArgs :: [TypeArg]
tArgs ty :: Type
ty p :: Range
p) = do
    ClassMap
cm <- (Env -> ClassMap) -> State Env ClassMap
forall s a. (s -> a) -> State s a
gets Env -> ClassMap
classMap
    let k :: Maybe Kind
k = case Maybe Kind
mk of
              Nothing -> Maybe Kind
forall a. Maybe a
Nothing
              Just j :: Kind
j -> let Result cs :: [Diagnosis]
cs _ = Kind -> ClassMap -> Result RawKind
anaKindM Kind
j ClassMap
cm
                        in Kind -> Maybe Kind
forall a. a -> Maybe a
Just (Kind -> Maybe Kind) -> Kind -> Maybe Kind
forall a b. (a -> b) -> a -> b
$ if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
cs then Kind
j else Kind
universe
    [Maybe TypeArg]
nAs <- (TypeArg -> State Env (Maybe TypeArg))
-> [TypeArg] -> State Env [Maybe TypeArg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TypeArg -> State Env (Maybe TypeArg)
anaddTypeVarDecl [TypeArg]
tArgs
    let ntArgs :: [TypeArg]
ntArgs = [Maybe TypeArg] -> [TypeArg]
forall a. [Maybe a] -> [a]
catMaybes [Maybe TypeArg]
nAs
    Maybe ((RawKind, Set Kind), Type)
mp <- (Maybe Kind, Type) -> State Env (Maybe ((RawKind, Set Kind), Type))
anaType (Maybe Kind
forall a. Maybe a
Nothing, Type
ty)
    case Maybe ((RawKind, Set Kind), Type)
mp of
      Nothing -> (Kind, Maybe TypeScheme) -> State Env (Kind, Maybe TypeScheme)
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind
universe, Maybe TypeScheme
forall a. Maybe a
Nothing)
      Just ((_, sks :: Set Kind
sks), newTy :: Type
newTy) -> case Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
sks of
        [sk :: Kind
sk] -> do
          let newK :: Kind
newK = [TypeArg] -> Kind -> Kind
typeArgsListToKind [TypeArg]
ntArgs Kind
sk
          RawKind
irk <- Kind -> State Env RawKind
anaKind Kind
newK
          case Maybe Kind
k of
            Nothing -> () -> State Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just j :: Kind
j -> do
              RawKind
grk <- Kind -> State Env RawKind
anaKind Kind
j
              [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ Type -> RawKind -> RawKind -> [Diagnosis]
forall a.
(GetRange a, Pretty a) =>
a -> RawKind -> RawKind -> [Diagnosis]
checkKinds Type
ty RawKind
grk RawKind
irk
          (Kind, Maybe TypeScheme) -> State Env (Kind, Maybe TypeScheme)
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind
newK, TypeScheme -> Maybe TypeScheme
forall a. a -> Maybe a
Just (TypeScheme -> Maybe TypeScheme) -> TypeScheme -> Maybe TypeScheme
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg]
ntArgs Type
newTy Range
p)
        _ -> (Kind, Maybe TypeScheme) -> State Env (Kind, Maybe TypeScheme)
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind
universe, Maybe TypeScheme
forall a. Maybe a
Nothing)

-- | add a type pattern
addTypePattern :: TypeDefn -> Kind -> (Id, [TypeArg])
               -> State Env (Maybe (Id, [TypeArg]))
addTypePattern :: TypeDefn
-> Kind -> (Id, [TypeArg]) -> State Env (Maybe (Id, [TypeArg]))
addTypePattern defn :: TypeDefn
defn kind :: Kind
kind (i :: Id
i, tArgs :: [TypeArg]
tArgs) = do
        LocalTypeVars
tvs <- (Env -> LocalTypeVars) -> State Env LocalTypeVars
forall s a. (s -> a) -> State s a
gets Env -> LocalTypeVars
localTypeVars
        [Maybe TypeArg]
newAs <- (TypeArg -> State Env (Maybe TypeArg))
-> [TypeArg] -> State Env [Maybe TypeArg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TypeArg -> State Env (Maybe TypeArg)
anaddTypeVarDecl [TypeArg]
tArgs
        LocalTypeVars -> State Env ()
putLocalTypeVars LocalTypeVars
tvs
        let nAs :: [TypeArg]
nAs = [Maybe TypeArg] -> [TypeArg]
forall a. [Maybe a] -> [a]
catMaybes [Maybe TypeArg]
newAs
            fullKind :: Kind
fullKind = [TypeArg] -> Kind -> Kind
typeArgsListToKind [TypeArg]
nAs Kind
kind
        [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> [Diagnosis]
checkUniqueTypevars [TypeArg]
nAs
        Bool
b <- Bool -> TypeDefn -> Kind -> Id -> State Env Bool
addTypeId Bool
True TypeDefn
defn Kind
fullKind Id
i
        Maybe (Id, [TypeArg]) -> State Env (Maybe (Id, [TypeArg]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Id, [TypeArg]) -> State Env (Maybe (Id, [TypeArg])))
-> Maybe (Id, [TypeArg]) -> State Env (Maybe (Id, [TypeArg]))
forall a b. (a -> b) -> a -> b
$ if Bool
b then (Id, [TypeArg]) -> Maybe (Id, [TypeArg])
forall a. a -> Maybe a
Just (Id
i, [TypeArg]
nAs) else Maybe (Id, [TypeArg])
forall a. Maybe a
Nothing