{- |
Module      :  ./HasCASL/VarDecl.hs
Description :  analyse var decls
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 generic var (or type var) decls

-}

module HasCASL.VarDecl where

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.Builtin
import HasCASL.ClassAna
import HasCASL.FoldTerm
import HasCASL.FoldType
import HasCASL.Le
import HasCASL.MapTerm
import HasCASL.Merge
import HasCASL.ParseTerm
import HasCASL.PrintLe
import HasCASL.TypeAna
import HasCASL.Unify

import Common.AnnoState
import Common.DocUtils
import Common.Id
import Common.Lib.MapSet (setToMap)
import Common.Lib.State
import Common.Parsec
import Common.Result

import Text.ParserCombinators.Parsec (runParser, eof)

import Control.Monad
import qualified Control.Monad.Fail as Fail

import Data.List as List
import Data.Maybe

import qualified Data.Map as Map
import qualified Data.Set as Set

-- | quantify
mkEnvForall :: Env -> Term -> Range -> Term
mkEnvForall :: Env -> Term -> Range -> Term
mkEnvForall e :: Env
e t :: Term
t ps :: Range
ps =
  let tys :: [Type]
tys = Term -> [Type]
getAllTypes Term
t
      tyVs :: [TypeArg]
tyVs = LocalTypeVars -> [Type] -> Range -> [TypeArg]
getTypeVars (Env -> LocalTypeVars
localTypeVars Env
e) [Type]
tys Range
ps
      vs :: [GenVarDecl]
vs = (TypeArg -> GenVarDecl) -> [TypeArg] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> GenVarDecl
GenTypeVarDecl ([TypeArg] -> [TypeArg]
genTypeArgs [TypeArg]
tyVs)
           [GenVarDecl] -> [GenVarDecl] -> [GenVarDecl]
forall a. [a] -> [a] -> [a]
++ (VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl (Set VarDecl -> [VarDecl]
forall a. Set a -> [a]
Set.toList (Set VarDecl -> [VarDecl]) -> Set VarDecl -> [VarDecl]
forall a b. (a -> b) -> a -> b
$ Term -> Set VarDecl
freeVars Term
t)
  in if [GenVarDecl] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GenVarDecl]
vs then Term
t else
         Rename -> Term -> Term
mapTerm ((Id, TypeScheme) -> (Id, TypeScheme)
forall a. a -> a
id, (Id -> RawKind -> Int -> Type) -> Type -> Type
replAlias (\ i :: Id
i rk :: RawKind
rk v :: Int
v ->
               Id -> RawKind -> Int -> Type
TypeName Id
i RawKind
rk (Int -> Type) -> Int -> Type
forall a b. (a -> b) -> a -> b
$
               case Id -> [Id] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex Id
i ([Id] -> Maybe Int) -> [Id] -> Maybe Int
forall a b. (a -> b) -> a -> b
$ (TypeArg -> Id) -> [TypeArg] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> Id
getTypeVar [TypeArg]
tyVs of
                 Just j :: Int
j -> - (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
                 _ -> Int
v))
         (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
Universal [GenVarDecl]
vs Term
t Range
ps

getTypeVars :: LocalTypeVars -> [Type] -> Range -> [TypeArg]
getTypeVars :: LocalTypeVars -> [Type] -> Range -> [TypeArg]
getTypeVars e :: LocalTypeVars
e tys :: [Type]
tys ps :: Range
ps =
  let is :: Set Id
is = [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ (Type -> Set Id) -> [Type] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Bool) -> Type -> Set Id
idsOf (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0)) [Type]
tys
      tyVs :: LocalTypeVars
tyVs = LocalTypeVars -> Map Id Id -> LocalTypeVars
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection LocalTypeVars
e (Map Id Id -> LocalTypeVars) -> Map Id Id -> LocalTypeVars
forall a b. (a -> b) -> a -> b
$ Set Id -> Map Id Id
forall a. Ord a => Set a -> Map a a
setToMap Set Id
is
      dTys :: [Type]
dTys = (TypeVarDefn -> [Type] -> [Type])
-> [Type] -> LocalTypeVars -> [Type]
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (\ (TypeVarDefn _ vk :: VarKind
vk _ _) l :: [Type]
l -> case VarKind
vk of
             Downset ty :: Type
ty -> Type
ty Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
l
             _ -> [Type]
l) [] LocalTypeVars
tyVs
      dis :: Set Id
dis = [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ (Type -> Set Id) -> [Type] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Bool) -> Type -> Set Id
idsOf (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0)) [Type]
dTys
  in if Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set Id
dis Set Id
is then
          ((Id, TypeVarDefn) -> TypeArg) -> [(Id, TypeVarDefn)] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: Id
i, TypeVarDefn v :: Variance
v vk :: VarKind
vk rk :: RawKind
rk c :: Int
c) -> Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
v VarKind
vk RawKind
rk Int
c SeparatorKind
Other Range
ps)
          ([(Id, TypeVarDefn)] -> [TypeArg])
-> [(Id, TypeVarDefn)] -> [TypeArg]
forall a b. (a -> b) -> a -> b
$ LocalTypeVars -> [(Id, TypeVarDefn)]
forall k a. Map k a -> [(k, a)]
Map.toList LocalTypeVars
tyVs
     else LocalTypeVars -> [Type] -> Range -> [TypeArg]
getTypeVars LocalTypeVars
e ([Type]
dTys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
tys) Range
ps

anaStarType :: Type -> State Env (Maybe Type)
anaStarType :: Type -> State Env (Maybe Type)
anaStarType t :: Type
t = (Maybe ((RawKind, Set Kind), Type) -> Maybe Type)
-> State Env (Maybe ((RawKind, Set Kind), Type))
-> State Env (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((((RawKind, Set Kind), Type) -> Type)
-> Maybe ((RawKind, Set Kind), Type) -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((RawKind, Set Kind), Type) -> Type
forall a b. (a, b) -> b
snd) (State Env (Maybe ((RawKind, Set Kind), Type))
 -> State Env (Maybe Type))
-> State Env (Maybe ((RawKind, Set Kind), Type))
-> State Env (Maybe Type)
forall a b. (a -> b) -> a -> b
$ (Maybe Kind, Type) -> State Env (Maybe ((RawKind, Set Kind), Type))
anaType (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
universe, Type
t)

anaType :: (Maybe Kind, Type)
        -> State Env (Maybe ((RawKind, Set.Set Kind), Type))
anaType :: (Maybe Kind, Type) -> State Env (Maybe ((RawKind, Set Kind), Type))
anaType = (Env -> Result ((RawKind, Set Kind), Type))
-> State Env (Maybe ((RawKind, Set Kind), Type))
forall a. (Env -> Result a) -> State Env (Maybe a)
fromResult ((Env -> Result ((RawKind, Set Kind), Type))
 -> State Env (Maybe ((RawKind, Set Kind), Type)))
-> ((Maybe Kind, Type)
    -> Env -> Result ((RawKind, Set Kind), Type))
-> (Maybe Kind, Type)
-> State Env (Maybe ((RawKind, Set Kind), Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Kind, Type) -> Env -> Result ((RawKind, Set Kind), Type)
anaTypeM

anaTypeScheme :: TypeScheme -> State Env (Maybe TypeScheme)
anaTypeScheme :: TypeScheme -> State Env (Maybe TypeScheme)
anaTypeScheme (TypeScheme tArgs :: [TypeArg]
tArgs ty :: Type
ty p :: Range
p) =
    do LocalTypeVars
tvs <- (Env -> LocalTypeVars) -> State Env LocalTypeVars
forall s a. (s -> a) -> State s a
gets Env -> LocalTypeVars
localTypeVars    -- save global variables
       [Maybe TypeArg]
mArgs <- (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 newArgs :: [TypeArg]
newArgs = [Maybe TypeArg] -> [TypeArg]
forall a. [Maybe a] -> [a]
catMaybes [Maybe TypeArg]
mArgs
       Maybe Type
mt <- Type -> State Env (Maybe Type)
anaStarType Type
ty
       case Maybe Type
mt of
           Nothing -> do LocalTypeVars -> State Env ()
putLocalTypeVars LocalTypeVars
tvs       -- forget local variables
                         Maybe TypeScheme -> State Env (Maybe TypeScheme)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeScheme
forall a. Maybe a
Nothing
           Just newTy :: Type
newTy -> do
               let newSc :: TypeScheme
newSc = [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg]
newArgs Type
newTy Range
p
               TypeScheme
gTy <- TypeScheme -> State Env TypeScheme
generalizeS TypeScheme
newSc
               LocalTypeVars -> State Env ()
putLocalTypeVars LocalTypeVars
tvs       -- forget local variables
               Maybe TypeScheme -> State Env (Maybe TypeScheme)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeScheme -> State Env (Maybe TypeScheme))
-> Maybe TypeScheme -> State Env (Maybe TypeScheme)
forall a b. (a -> b) -> a -> b
$ TypeScheme -> Maybe TypeScheme
forall a. a -> Maybe a
Just TypeScheme
gTy

generalizeS :: TypeScheme -> State Env TypeScheme
generalizeS :: TypeScheme -> State Env TypeScheme
generalizeS sc :: TypeScheme
sc@(TypeScheme tArgs :: [TypeArg]
tArgs ty :: Type
ty p :: Range
p) = do
    let fvs :: [(Int, (Id, RawKind))]
fvs = Type -> [(Int, (Id, RawKind))]
freeTVars Type
ty
        svs :: [(Int, (Id, RawKind))]
svs = ((Int, (Id, RawKind)) -> (Int, (Id, RawKind)) -> Ordering)
-> [(Int, (Id, RawKind))] -> [(Int, (Id, RawKind))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Int, (Id, RawKind)) -> (Int, (Id, RawKind)) -> Ordering
forall a b b. Ord a => (a, b) -> (a, b) -> Ordering
comp [(Int, (Id, RawKind))]
fvs
        comp :: (a, b) -> (a, b) -> Ordering
comp a :: (a, b)
a b :: (a, b)
b = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((a, b) -> a
forall a b. (a, b) -> a
fst (a, b)
a) (a -> Ordering) -> a -> Ordering
forall a b. (a -> b) -> a -> b
$ (a, b) -> a
forall a b. (a, b) -> a
fst (a, b)
b
    LocalTypeVars
tvs <- (Env -> LocalTypeVars) -> State Env LocalTypeVars
forall s a. (s -> a) -> State s a
gets Env -> LocalTypeVars
localTypeVars
    let newArgs :: [TypeArg]
newArgs = ((Int, (Id, RawKind)) -> TypeArg)
-> [(Int, (Id, RawKind))] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (_, (i :: Id
i, _)) -> case Id -> LocalTypeVars -> Maybe TypeVarDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i LocalTypeVars
tvs of
                  Nothing -> [Char] -> TypeArg
forall a. HasCallStack => [Char] -> a
error "generalizeS"
                  Just (TypeVarDefn v :: Variance
v vk :: VarKind
vk rk :: RawKind
rk c :: Int
c) ->
                      Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
v VarKind
vk RawKind
rk Int
c SeparatorKind
Other Range
nullRange) [(Int, (Id, RawKind))]
svs
        newSc :: TypeScheme
newSc = [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme ([TypeArg] -> [TypeArg]
genTypeArgs [TypeArg]
newArgs) ([TypeArg] -> Type -> Type
generalize [TypeArg]
newArgs Type
ty) Range
p
    if [TypeArg] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeArg]
tArgs then TypeScheme -> State Env TypeScheme
forall (m :: * -> *) a. Monad m => a -> m a
return TypeScheme
newSc
       else do
         [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ Bool -> TypeScheme -> [Diagnosis]
generalizable Bool
False TypeScheme
sc
         TypeScheme -> State Env TypeScheme
forall (m :: * -> *) a. Monad m => a -> m a
return TypeScheme
newSc

-- | store type id and check kind arity (warn on redeclared types)
addTypeId :: Bool -> TypeDefn -> Kind -> Id -> State Env Bool
addTypeId :: Bool -> TypeDefn -> Kind -> Id -> State Env Bool
addTypeId warn :: Bool
warn dfn :: TypeDefn
dfn k :: Kind
k i :: Id
i = do
    LocalTypeVars
tvs <- (Env -> LocalTypeVars) -> State Env LocalTypeVars
forall s a. (s -> a) -> State s a
gets Env -> LocalTypeVars
localTypeVars
    case Id -> LocalTypeVars -> Maybe TypeVarDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i LocalTypeVars
tvs of
        Just _ -> do
            Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
warn (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning
                                  "new type shadows type variable" Id
i]
            LocalTypeVars -> State Env ()
putLocalTypeVars (LocalTypeVars -> State Env ()) -> LocalTypeVars -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> LocalTypeVars -> LocalTypeVars
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Id
i LocalTypeVars
tvs
        Nothing -> () -> State Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    ClassMap
cm <- (Env -> ClassMap) -> State Env ClassMap
forall s a. (s -> a) -> State s a
gets Env -> ClassMap
classMap
    case Id -> ClassMap -> Maybe ClassInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i ClassMap
cm of
      Just _ -> do
          [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "class name used as type" Id
i]
          Bool -> State Env Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Nothing -> Bool -> TypeDefn -> Id -> Kind -> State Env Bool
addTypeKind Bool
warn TypeDefn
dfn Id
i Kind
k

-- | check if the kind only misses variance indicators of the known raw kind
isLiberalKind :: ClassMap -> Bool -> RawKind -> Kind -> Maybe Kind
isLiberalKind :: ClassMap -> Bool -> RawKind -> Kind -> Maybe Kind
isLiberalKind cm :: ClassMap
cm b :: Bool
b ok :: RawKind
ok k :: Kind
k = case RawKind
ok of
    ClassKind _ -> Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
k
    FunKind ov :: Variance
ov fok :: RawKind
fok aok :: RawKind
aok _ -> case Kind
k of
        FunKind v :: Variance
v fk :: Kind
fk ak :: Kind
ak ps :: Range
ps -> do
            Kind
nfk <- ClassMap -> Bool -> RawKind -> Kind -> Maybe Kind
isLiberalKind ClassMap
cm (Bool -> Bool
not Bool
b) RawKind
fok Kind
fk
            Kind
nak <- ClassMap -> Bool -> RawKind -> Kind -> Maybe Kind
isLiberalKind ClassMap
cm Bool
b RawKind
aok Kind
ak
            Kind -> Maybe Kind
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Maybe Kind) -> Kind -> Maybe Kind
forall a b. (a -> b) -> a -> b
$ Variance -> Kind -> Kind -> Range -> Kind
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind (Bool -> Variance -> Variance -> Variance
liberalVariance Bool
b Variance
ov Variance
v) Kind
nfk Kind
nak Range
ps
        ClassKind i :: Id
i -> case Id -> ClassMap -> Maybe ClassInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i ClassMap
cm of
           Just ci :: ClassInfo
ci -> Maybe Kind
-> (RawKind -> Maybe Kind) -> Maybe RawKind -> Maybe Kind
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe Kind
forall a. Maybe a
Nothing (Maybe Kind -> RawKind -> Maybe Kind
forall a b. a -> b -> a
const (Maybe Kind -> RawKind -> Maybe Kind)
-> Maybe Kind -> RawKind -> Maybe Kind
forall a b. (a -> b) -> a -> b
$ Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
k) (Maybe RawKind -> Maybe Kind) -> Maybe RawKind -> Maybe Kind
forall a b. (a -> b) -> a -> b
$ [Char] -> RawKind -> RawKind -> Maybe RawKind
forall (m :: * -> *).
MonadFail m =>
[Char] -> RawKind -> RawKind -> m RawKind
minRawKind "" RawKind
ok
                      (RawKind -> Maybe RawKind) -> RawKind -> Maybe RawKind
forall a b. (a -> b) -> a -> b
$ ClassInfo -> RawKind
rawKind ClassInfo
ci
           _ -> Maybe Kind
forall a. Maybe a
Nothing

liberalVariance :: Bool -> Variance -> Variance -> Variance
liberalVariance :: Bool -> Variance -> Variance -> Variance
liberalVariance b :: Bool
b v1 :: Variance
v1 v2 :: Variance
v2 = if Bool
b then Variance -> Variance -> Variance
minVariance Variance
v1 Variance
v2 else
       Variance -> Variance
revVariance (Variance -> Variance) -> Variance -> Variance
forall a b. (a -> b) -> a -> b
$ Variance -> Variance -> Variance
minVariance (Variance -> Variance
revVariance Variance
v1) (Variance -> Variance) -> Variance -> Variance
forall a b. (a -> b) -> a -> b
$ Variance -> Variance
revVariance Variance
v2

-- | lifted 'anaKindM'
anaKind :: Kind -> State Env RawKind
anaKind :: Kind -> State Env RawKind
anaKind k :: Kind
k = do
    Maybe RawKind
mrk <- (Env -> Result RawKind) -> State Env (Maybe RawKind)
forall a. (Env -> Result a) -> State Env (Maybe a)
fromResult ((Env -> Result RawKind) -> State Env (Maybe RawKind))
-> (Env -> Result RawKind) -> State Env (Maybe RawKind)
forall a b. (a -> b) -> a -> b
$ Kind -> ClassMap -> Result RawKind
anaKindM Kind
k (ClassMap -> Result RawKind)
-> (Env -> ClassMap) -> Env -> Result RawKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ClassMap
classMap
    case Maybe RawKind
mrk of
      Nothing -> [Char] -> State Env RawKind
forall a. HasCallStack => [Char] -> a
error "anaKind"
      Just rk :: RawKind
rk -> RawKind -> State Env RawKind
forall (m :: * -> *) a. Monad m => a -> m a
return RawKind
rk

-- | store type as is (warn on redeclared types)
addTypeKind :: Bool -> TypeDefn -> Id -> Kind -> State Env Bool
addTypeKind :: Bool -> TypeDefn -> Id -> Kind -> State Env Bool
addTypeKind warn :: Bool
warn d :: TypeDefn
d i :: Id
i k :: Kind
k = do
  Env
e <- State Env Env
forall s. State s s
get
  RawKind
rk <- Kind -> State Env RawKind
anaKind Kind
k
  let tm :: TypeMap
tm = Env -> TypeMap
typeMap Env
e
      cm :: ClassMap
cm = Env -> ClassMap
classMap Env
e
      addTypeSym :: RawKind -> State Env ()
addTypeSym = Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Id -> TypeMap -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
i TypeMap
bTypes)
                        (State Env () -> State Env ())
-> (RawKind -> State Env ()) -> RawKind -> State Env ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> State Env ()
addSymbol (Symbol -> State Env ())
-> (RawKind -> Symbol) -> RawKind -> State Env ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> RawKind -> Symbol
idToTypeSymbol Id
i
  Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Id -> Int
placeCount Id
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= RawKind -> Int
kindArity RawKind
rk)
    (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "wrong arity of" Id
i]
  case Id -> TypeMap -> Maybe TypeInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i TypeMap
tm of
    Nothing -> do
      RawKind -> State Env ()
addTypeSym RawKind
rk
      TypeMap -> State Env ()
putTypeMap (TypeMap -> State Env ()) -> TypeMap -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> TypeInfo -> TypeMap -> TypeMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i (RawKind -> Set Kind -> Set Id -> TypeDefn -> TypeInfo
TypeInfo RawKind
rk (Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
k) Set Id
forall a. Set a
Set.empty TypeDefn
d) TypeMap
tm
      Bool -> State Env Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Just (TypeInfo ok :: RawKind
ok oldks :: Set Kind
oldks sups :: Set Id
sups dfn :: TypeDefn
dfn) ->
      case [Char] -> RawKind -> RawKind -> Maybe RawKind
forall (m :: * -> *).
MonadFail m =>
[Char] -> RawKind -> RawKind -> m RawKind
minRawKind "" RawKind
ok RawKind
rk of
      Nothing -> do
        [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> RawKind -> [Diagnosis]
forall a.
(GetRange a, Pretty a) =>
a -> RawKind -> RawKind -> [Diagnosis]
diffKindDiag Id
i RawKind
ok RawKind
rk
        Bool -> State Env Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Just r :: RawKind
r -> case ClassMap -> Bool -> RawKind -> Kind -> Maybe Kind
isLiberalKind ClassMap
cm Bool
True RawKind
r Kind
k of
       Just nk :: Kind
nk -> do
        let isNewInst :: Bool
isNewInst = ClassMap -> Kind -> Set Kind -> Bool
newKind ClassMap
cm Kind
nk Set Kind
oldks
            insts :: Set Kind
insts = if Bool
isNewInst then ClassMap -> Kind -> Set Kind -> Set Kind
addNewKind ClassMap
cm Kind
nk Set Kind
oldks else Set Kind
oldks
            Result ds :: [Diagnosis]
ds mDef :: Maybe TypeDefn
mDef = TypeDefn -> TypeDefn -> Result TypeDefn
mergeTypeDefn TypeDefn
dfn TypeDefn
d
        Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
warn Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
isNewInst Bool -> Bool -> Bool
&& case (TypeDefn
dfn, TypeDefn
d) of
           (PreDatatype, DatatypeDefn _) -> Bool
False
           _ -> Bool
True)
          (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Hint "redeclared type" Id
i]
        case Maybe TypeDefn
mDef of
          Just newDefn :: TypeDefn
newDefn -> do
            RawKind -> State Env ()
addTypeSym RawKind
r
            TypeMap -> State Env ()
putTypeMap (TypeMap -> State Env ()) -> TypeMap -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> TypeInfo -> TypeMap -> TypeMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i (RawKind -> Set Kind -> Set Id -> TypeDefn -> TypeInfo
TypeInfo RawKind
r Set Kind
insts Set Id
sups TypeDefn
newDefn) TypeMap
tm
            Bool -> State Env Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
          _ -> do
            [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ (Diagnosis -> Diagnosis) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> Diagnosis -> Diagnosis
forall a. (GetRange a, Pretty a) => a -> Diagnosis -> Diagnosis
improveDiag Id
i) [Diagnosis]
ds
            Bool -> State Env Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
       Nothing -> do
         [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "cannot refine kind" Id
i]
         Bool -> State Env Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

nonUniqueKind :: (GetRange a, Pretty a) => Set.Set Kind -> RawKind -> a ->
                 (Kind -> State Env (Maybe b)) -> State Env (Maybe b)
nonUniqueKind :: Set Kind
-> RawKind
-> a
-> (Kind -> State Env (Maybe b))
-> State Env (Maybe b)
nonUniqueKind ks :: Set Kind
ks rk :: RawKind
rk a :: a
a f :: Kind -> State Env (Maybe b)
f = case Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
ks of
    [k :: Kind
k] -> Kind -> State Env (Maybe b)
f Kind
k
    _ -> do
      [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> a -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning "non-unique kind for" a
a]
      Kind -> State Env (Maybe b)
f (RawKind -> Kind
rawToKind RawKind
rk)

-- | analyse a type argument
anaddTypeVarDecl :: TypeArg -> State Env (Maybe TypeArg)
anaddTypeVarDecl :: TypeArg -> State Env (Maybe TypeArg)
anaddTypeVarDecl (TypeArg i :: Id
i v :: Variance
v vk :: VarKind
vk _ _ s :: SeparatorKind
s ps :: Range
ps) = do
  ClassMap
cm <- (Env -> ClassMap) -> State Env ClassMap
forall s a. (s -> a) -> State s a
gets Env -> ClassMap
classMap
  case Id -> ClassMap -> Maybe ClassInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i ClassMap
cm of
    Just _ -> do
        [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "class used as type variable" Id
i]
        Maybe TypeArg -> State Env (Maybe TypeArg)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeArg
forall a. Maybe a
Nothing
    Nothing -> do
     Int
c <- State Int Int -> State Env Int
forall a. State Int a -> State Env a
toEnvState State Int Int
inc
     case VarKind
vk of
      VarKind k :: Kind
k ->
        let Result ds :: [Diagnosis]
ds (Just rk :: RawKind
rk) = Kind -> ClassMap -> Result RawKind
anaKindM Kind
k ClassMap
cm
        in if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds then do
            Bool -> TypeVarDefn -> Id -> State Env ()
addLocalTypeVar Bool
True (Variance -> VarKind -> RawKind -> Int -> TypeVarDefn
TypeVarDefn Variance
v VarKind
vk RawKind
rk Int
c) Id
i
            Maybe TypeArg -> State Env (Maybe TypeArg)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeArg -> State Env (Maybe TypeArg))
-> Maybe TypeArg -> State Env (Maybe TypeArg)
forall a b. (a -> b) -> a -> b
$ TypeArg -> Maybe TypeArg
forall a. a -> Maybe a
Just (TypeArg -> Maybe TypeArg) -> TypeArg -> Maybe TypeArg
forall a b. (a -> b) -> a -> b
$ Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
v VarKind
vk RawKind
rk Int
c SeparatorKind
s Range
ps
        else do [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds
                Maybe TypeArg -> State Env (Maybe TypeArg)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeArg
forall a. Maybe a
Nothing
      Downset t :: Type
t -> do
        Maybe ((RawKind, Set Kind), Type)
mt <- (Maybe Kind, Type) -> State Env (Maybe ((RawKind, Set Kind), Type))
anaType (Maybe Kind
forall a. Maybe a
Nothing, Type
t)
        case Maybe ((RawKind, Set Kind), Type)
mt of
            Nothing -> Maybe TypeArg -> State Env (Maybe TypeArg)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeArg
forall a. Maybe a
Nothing
            Just ((rk :: RawKind
rk, ks :: Set Kind
ks), nt :: Type
nt) ->
                Set Kind
-> RawKind
-> Type
-> (Kind -> State Env (Maybe TypeArg))
-> State Env (Maybe TypeArg)
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 TypeArg)) -> State Env (Maybe TypeArg))
-> (Kind -> State Env (Maybe TypeArg)) -> State Env (Maybe TypeArg)
forall a b. (a -> b) -> a -> b
$ \ k :: Kind
k -> do
                   let nd :: VarKind
nd = Type -> VarKind
Downset (Type -> Set Kind -> Range -> Type
KindedType Type
nt (Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
k) Range
nullRange)
                   Bool -> TypeVarDefn -> Id -> State Env ()
addLocalTypeVar Bool
True (Variance -> VarKind -> RawKind -> Int -> TypeVarDefn
TypeVarDefn Variance
NonVar VarKind
nd RawKind
rk Int
c) Id
i
                   Maybe TypeArg -> State Env (Maybe TypeArg)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeArg -> State Env (Maybe TypeArg))
-> Maybe TypeArg -> State Env (Maybe TypeArg)
forall a b. (a -> b) -> a -> b
$ TypeArg -> Maybe TypeArg
forall a. a -> Maybe a
Just (TypeArg -> Maybe TypeArg) -> TypeArg -> Maybe TypeArg
forall a b. (a -> b) -> a -> b
$ Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
v (Type -> VarKind
Downset Type
nt) RawKind
rk Int
c SeparatorKind
s Range
ps
      MissingKind -> do
        LocalTypeVars
tvs <- (Env -> LocalTypeVars) -> State Env LocalTypeVars
forall s a. (s -> a) -> State s a
gets Env -> LocalTypeVars
localTypeVars
        case Id -> LocalTypeVars -> Maybe TypeVarDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i LocalTypeVars
tvs of
            Nothing -> do
                [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "unknown type variable" Id
i]
                let dvk :: VarKind
dvk = Kind -> VarKind
VarKind Kind
universe
                Bool -> TypeVarDefn -> Id -> State Env ()
addLocalTypeVar Bool
True (Variance -> VarKind -> RawKind -> Int -> TypeVarDefn
TypeVarDefn Variance
v VarKind
dvk RawKind
rStar Int
c) Id
i
                Maybe TypeArg -> State Env (Maybe TypeArg)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeArg -> State Env (Maybe TypeArg))
-> Maybe TypeArg -> State Env (Maybe TypeArg)
forall a b. (a -> b) -> a -> b
$ TypeArg -> Maybe TypeArg
forall a. a -> Maybe a
Just (TypeArg -> Maybe TypeArg) -> TypeArg -> Maybe TypeArg
forall a b. (a -> b) -> a -> b
$ Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
v VarKind
dvk RawKind
rStar Int
c SeparatorKind
s Range
ps
            Just (TypeVarDefn v0 :: Variance
v0 dvk :: VarKind
dvk rk :: RawKind
rk _) -> do
                Bool -> TypeVarDefn -> Id -> State Env ()
addLocalTypeVar Bool
False (Variance -> VarKind -> RawKind -> Int -> TypeVarDefn
TypeVarDefn Variance
v0 VarKind
dvk RawKind
rk Int
c) Id
i
                Maybe TypeArg -> State Env (Maybe TypeArg)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeArg -> State Env (Maybe TypeArg))
-> Maybe TypeArg -> State Env (Maybe TypeArg)
forall a b. (a -> b) -> a -> b
$ TypeArg -> Maybe TypeArg
forall a. a -> Maybe a
Just (TypeArg -> Maybe TypeArg) -> TypeArg -> Maybe TypeArg
forall a b. (a -> b) -> a -> b
$ Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
v0 VarKind
dvk RawKind
rk Int
c SeparatorKind
s Range
ps

-- | partition information of an uninstantiated identifier
partitionOpId :: Env -> Id -> TypeScheme -> (Set.Set OpInfo, Set.Set OpInfo)
partitionOpId :: Env -> Id -> TypeScheme -> (Set OpInfo, Set OpInfo)
partitionOpId e :: Env
e i :: Id
i sc :: TypeScheme
sc =
    (OpInfo -> Bool) -> Set OpInfo -> (Set OpInfo, Set OpInfo)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition ((TypeScheme
sc TypeScheme -> TypeScheme -> Bool
forall a. Eq a => a -> a -> Bool
==) (TypeScheme -> Bool) -> (OpInfo -> TypeScheme) -> OpInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpInfo -> TypeScheme
opType)
           (Set OpInfo -> (Set OpInfo, Set OpInfo))
-> Set OpInfo -> (Set OpInfo, Set OpInfo)
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> Id -> Map Id (Set OpInfo) -> Set OpInfo
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set OpInfo
forall a. Set a
Set.empty Id
i (Map Id (Set OpInfo) -> Set OpInfo)
-> Map Id (Set OpInfo) -> Set OpInfo
forall a b. (a -> b) -> a -> b
$ Env -> Map Id (Set OpInfo)
assumps Env
e

checkUnusedTypevars :: TypeScheme -> State Env TypeScheme
checkUnusedTypevars :: TypeScheme -> State Env TypeScheme
checkUnusedTypevars sc :: TypeScheme
sc@(TypeScheme tArgs :: [TypeArg]
tArgs t :: Type
t ps :: Range
ps) = do
    let ls :: [Id]
ls = ((Int, (Id, RawKind)) -> Id) -> [(Int, (Id, RawKind))] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map ((Id, RawKind) -> Id
forall a b. (a, b) -> a
fst ((Id, RawKind) -> Id)
-> ((Int, (Id, RawKind)) -> (Id, RawKind))
-> (Int, (Id, RawKind))
-> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (Id, RawKind)) -> (Id, RawKind)
forall a b. (a, b) -> b
snd) ([(Int, (Id, RawKind))] -> [Id]) -> [(Int, (Id, RawKind))] -> [Id]
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> Type -> [(Int, (Id, RawKind))]
leaves (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0) Type
t -- generic vars
        rest :: [Id]
rest = (TypeArg -> Id) -> [TypeArg] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> Id
getTypeVar [TypeArg]
tArgs [Id] -> [Id] -> [Id]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [Id]
ls
    Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
rest)
      (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Range -> Diagnosis
Diag DiagKind
Warning ("unused type variables: "
                                [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
forall a. Show a => a -> [Char]
show ([Id] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [Id]
rest)) Range
ps]
    TypeScheme -> State Env TypeScheme
forall (m :: * -> *) a. Monad m => a -> m a
return TypeScheme
sc

checkPlaceCount :: Env -> Id -> TypeScheme -> [Diagnosis]
checkPlaceCount :: Env -> Id -> TypeScheme -> [Diagnosis]
checkPlaceCount e :: Env
e i :: Id
i (TypeScheme _ ty :: Type
ty _) =
    if Id -> Int
placeCount Id
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 then
        let (fty :: Type
fty, fargs :: [Type]
fargs) = Type -> (Type, [Type])
getTypeAppl Type
ty in
        if [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
fargs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 2 Bool -> Bool -> Bool
&& Env -> Type -> Type -> Bool
lesserType Env
e Type
fty (Arrow -> Type
toFunType Arrow
PFunArr) then
            let (pty :: Type
pty, ts :: [Type]
ts) = Type -> (Type, [Type])
getTypeAppl ([Type] -> Type
forall a. [a] -> a
head [Type]
fargs)
                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
e Type
pty (Int -> Range -> Type
toProdType Int
n Range
nullRange) then
                    [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning "wrong number of places in" Id
i
                    | Id -> Int
placeCount Id
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
n ]
            else [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning "expected tuple argument for" Id
i]
        else [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning "expected function type for" Id
i]
    else []

-- | storing an operation
addOpId :: Id -> TypeScheme -> Set.Set OpAttr -> OpDefn -> State Env Bool
addOpId :: Id -> TypeScheme -> Set OpAttr -> OpDefn -> State Env Bool
addOpId i :: Id
i oldSc :: TypeScheme
oldSc attrs :: Set OpAttr
attrs dfn :: OpDefn
dfn = do
    sc :: TypeScheme
sc@(TypeScheme _ ty :: Type
ty _) <- TypeScheme -> State Env TypeScheme
checkUnusedTypevars TypeScheme
oldSc
    Env
e <- State Env Env
forall s. State s s
get
    let as :: Map Id (Set OpInfo)
as = Env -> Map Id (Set OpInfo)
assumps Env
e
        bs :: Map Id Id
bs = Env -> Map Id Id
binders Env
e
        ds :: [Diagnosis]
ds = Env -> Id -> TypeScheme -> [Diagnosis]
checkPlaceCount Env
e Id
i TypeScheme
sc
        (l :: Set OpInfo
l, r :: Set OpInfo
r) = Env -> Id -> TypeScheme -> (Set OpInfo, Set OpInfo)
partitionOpId Env
e Id
i TypeScheme
sc
        oInfo :: OpInfo
oInfo = TypeScheme -> Set OpAttr -> OpDefn -> OpInfo
OpInfo TypeScheme
sc Set OpAttr
attrs OpDefn
dfn
        Result es :: [Diagnosis]
es mo :: Maybe OpInfo
mo = (OpInfo -> OpInfo -> Result OpInfo)
-> OpInfo -> [OpInfo] -> Result OpInfo
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM OpInfo -> OpInfo -> Result OpInfo
mergeOpInfo OpInfo
oInfo ([OpInfo] -> Result OpInfo) -> [OpInfo] -> Result OpInfo
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
l
    [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds
    [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ (Diagnosis -> Diagnosis) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> Diagnosis -> Diagnosis
forall a. (GetRange a, Pretty a) => a -> Diagnosis -> Diagnosis
improveDiag Id
i) [Diagnosis]
es
    if Id
i Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Id, TypeScheme) -> Id) -> [(Id, TypeScheme)] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (Id, TypeScheme) -> Id
forall a b. (a, b) -> a
fst [(Id, TypeScheme)]
bList then
      [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning "ignoring declaration for builtin identifier" Id
i]
      else Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set OpInfo -> Bool
forall a. Set a -> Bool
Set.null Set OpInfo
l) (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags
      [DiagKind -> [Char] -> Type -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Hint ("repeated declaration of '" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Id -> [Char] -> [Char]
showId Id
i "' with type") Type
ty]
    Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id -> Map Id Id -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
i Map Id Id
bs) (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ do
      [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning "identifier shadows binder" Id
i]
      Map Id Id -> State Env ()
putBinders (Map Id Id -> State Env ()) -> Map Id Id -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> Map Id Id -> Map Id Id
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Id
i Map Id Id
bs
    case Maybe OpInfo
mo of
      Nothing -> Bool -> State Env Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Just oi :: OpInfo
oi -> do
        Symbol -> State Env ()
addSymbol (Symbol -> State Env ()) -> Symbol -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> TypeScheme -> Symbol
idToOpSymbol Id
i (TypeScheme -> Symbol) -> TypeScheme -> Symbol
forall a b. (a -> b) -> a -> b
$ OpInfo -> TypeScheme
opType OpInfo
oi
        Map Id (Set OpInfo) -> State Env ()
putAssumps (Map Id (Set OpInfo) -> State Env ())
-> Map Id (Set OpInfo) -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> Set OpInfo -> Map Id (Set OpInfo) -> Map Id (Set OpInfo)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i (OpInfo -> Set OpInfo -> Set OpInfo
forall a. Ord a => a -> Set a -> Set a
Set.insert OpInfo
oi Set OpInfo
r) Map Id (Set OpInfo)
as
        Bool -> State Env Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

-- | add a local variable with an analysed type (if True then warn)
addLocalVar :: Bool -> VarDecl -> State Env ()
addLocalVar :: Bool -> VarDecl -> State Env ()
addLocalVar warn :: Bool
warn (VarDecl v :: Id
v t :: Type
t _ _) =
    do Env
e <- State Env Env
forall s. State s s
get
       let vs :: Map Id VarDefn
vs = Env -> Map Id VarDefn
localVars Env
e
       Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
warn (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ do
         Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id -> Map Id (Set OpInfo) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
v (Map Id (Set OpInfo) -> Bool) -> Map Id (Set OpInfo) -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> Map Id (Set OpInfo)
assumps Env
e)
           (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Hint "variable shadows global name(s)" Id
v]
         Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id -> Map Id VarDefn -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
v Map Id VarDefn
vs)
           (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Hint "rebound variable" Id
v]
         Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id -> LocalTypeVars -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
v (LocalTypeVars -> Bool) -> LocalTypeVars -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> LocalTypeVars
localTypeVars Env
e)
           (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning "variable also known as type variable" Id
v]
       Map Id VarDefn -> State Env ()
putLocalVars (Map Id VarDefn -> State Env ()) -> Map Id VarDefn -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> VarDefn -> Map Id VarDefn -> Map Id VarDefn
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
v (Type -> VarDefn
VarDefn Type
t) Map Id VarDefn
vs

-- | add analysed local variable or type variable declaration
addGenVarDecl :: GenVarDecl -> State Env ()
addGenVarDecl :: GenVarDecl -> State Env ()
addGenVarDecl (GenVarDecl v :: VarDecl
v) = Bool -> VarDecl -> State Env ()
addLocalVar Bool
True VarDecl
v
addGenVarDecl (GenTypeVarDecl t :: TypeArg
t) = Bool -> TypeArg -> State Env ()
addTypeVarDecl Bool
False TypeArg
t

-- | analyse and add local variable or type variable declaration
anaddGenVarDecl :: Bool -> GenVarDecl -> State Env (Maybe GenVarDecl)
anaddGenVarDecl :: Bool -> GenVarDecl -> State Env (Maybe GenVarDecl)
anaddGenVarDecl warn :: Bool
warn gv :: GenVarDecl
gv = case GenVarDecl
gv of
    GenVarDecl v :: VarDecl
v -> Bool -> VarDecl -> State Env (Maybe GenVarDecl)
optAnaddVarDecl Bool
warn VarDecl
v
    GenTypeVarDecl t :: TypeArg
t -> (Maybe TypeArg -> Maybe GenVarDecl)
-> State Env (Maybe TypeArg) -> State Env (Maybe GenVarDecl)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TypeArg -> GenVarDecl) -> Maybe TypeArg -> Maybe GenVarDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeArg -> GenVarDecl
GenTypeVarDecl) (State Env (Maybe TypeArg) -> State Env (Maybe GenVarDecl))
-> State Env (Maybe TypeArg) -> State Env (Maybe GenVarDecl)
forall a b. (a -> b) -> a -> b
$ TypeArg -> State Env (Maybe TypeArg)
anaddTypeVarDecl TypeArg
t

convTypeToKind :: Type -> Maybe (Variance, Kind)
convTypeToKind :: Type -> Maybe (Variance, Kind)
convTypeToKind ty :: Type
ty = let s :: [Char]
s = Type -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc Type
ty "" in
    case GenParser Char (AnnoState ()) (Variance, Kind)
-> AnnoState ()
-> [Char]
-> [Char]
-> Either ParseError (Variance, Kind)
forall tok st a.
GenParser tok st a -> st -> [Char] -> [tok] -> Either ParseError a
runParser (GenParser Char (AnnoState ()) (Variance, Kind)
forall st. AParser st (Variance, Kind)
extKind GenParser Char (AnnoState ()) (Variance, Kind)
-> ParsecT [Char] (AnnoState ()) Identity ()
-> GenParser Char (AnnoState ()) (Variance, Kind)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] (AnnoState ()) Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof) (() -> AnnoState ()
forall st. st -> AnnoState st
emptyAnnos ()) "" [Char]
s of
    Right (v :: Variance
v, k :: Kind
k) -> (Variance, Kind) -> Maybe (Variance, Kind)
forall a. a -> Maybe a
Just (Variance
v, Kind
k)
    _ -> Maybe (Variance, Kind)
forall a. Maybe a
Nothing

convertTypeToKind :: Env -> Type -> Result (Variance, Kind)
convertTypeToKind :: Env -> Type -> Result (Variance, Kind)
convertTypeToKind e :: Env
e ty :: Type
ty = case Type -> Maybe (Variance, Kind)
convTypeToKind Type
ty of
    Just (v :: Variance
v, k :: Kind
k) -> let Result ds :: [Diagnosis]
ds _ = Kind -> ClassMap -> Result RawKind
anaKindM Kind
k (ClassMap -> Result RawKind) -> ClassMap -> Result RawKind
forall a b. (a -> b) -> a -> b
$ Env -> ClassMap
classMap Env
e in
               if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds then (Variance, Kind) -> Result (Variance, Kind)
forall (m :: * -> *) a. Monad m => a -> m a
return (Variance
v, Kind
k) else [Diagnosis] -> Maybe (Variance, Kind) -> Result (Variance, Kind)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (Variance, Kind)
forall a. Maybe a
Nothing
    _ -> [Char] -> Result (Variance, Kind)
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ([Char] -> Result (Variance, Kind))
-> [Char] -> Result (Variance, Kind)
forall a b. (a -> b) -> a -> b
$ "not a kind '" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc Type
ty "'"

-- | local variable or type variable declaration
optAnaddVarDecl :: Bool -> VarDecl -> State Env (Maybe GenVarDecl)
optAnaddVarDecl :: Bool -> VarDecl -> State Env (Maybe GenVarDecl)
optAnaddVarDecl warn :: Bool
warn vd :: VarDecl
vd@(VarDecl v :: Id
v t :: Type
t s :: SeparatorKind
s q :: Range
q) =
    let varDecl :: State Env (Maybe GenVarDecl)
varDecl = do Maybe VarDecl
mvd <- VarDecl -> State Env (Maybe VarDecl)
anaVarDecl VarDecl
vd
                     case Maybe VarDecl
mvd of
                         Nothing -> Maybe GenVarDecl -> State Env (Maybe GenVarDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe GenVarDecl
forall a. Maybe a
Nothing
                         Just nvd :: VarDecl
nvd -> do
                             let movd :: VarDecl
movd = VarDecl -> VarDecl
makeMonomorph VarDecl
nvd
                             Bool -> VarDecl -> State Env ()
addLocalVar Bool
warn VarDecl
movd
                             Maybe GenVarDecl -> State Env (Maybe GenVarDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe GenVarDecl -> State Env (Maybe GenVarDecl))
-> Maybe GenVarDecl -> State Env (Maybe GenVarDecl)
forall a b. (a -> b) -> a -> b
$ GenVarDecl -> Maybe GenVarDecl
forall a. a -> Maybe a
Just (GenVarDecl -> Maybe GenVarDecl) -> GenVarDecl -> Maybe GenVarDecl
forall a b. (a -> b) -> a -> b
$ VarDecl -> GenVarDecl
GenVarDecl VarDecl
movd
    in if Id -> Bool
isSimpleId Id
v then
    do Env
e <- State Env Env
forall s. State s s
get
       let Result ds :: [Diagnosis]
ds mk :: Maybe (Variance, Kind)
mk = Env -> Type -> Result (Variance, Kind)
convertTypeToKind Env
e Type
t
       case Maybe (Variance, Kind)
mk of
           Just (vv :: Variance
vv, k :: Kind
k) -> do
               [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Hint "is type variable" Id
v]
               Maybe TypeArg
tv <- TypeArg -> State Env (Maybe TypeArg)
anaddTypeVarDecl (TypeArg -> State Env (Maybe TypeArg))
-> TypeArg -> State Env (Maybe TypeArg)
forall a b. (a -> b) -> a -> b
$ Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
v Variance
vv (Kind -> VarKind
VarKind Kind
k) RawKind
rStar 0 SeparatorKind
s Range
q
               Maybe GenVarDecl -> State Env (Maybe GenVarDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe GenVarDecl -> State Env (Maybe GenVarDecl))
-> Maybe GenVarDecl -> State Env (Maybe GenVarDecl)
forall a b. (a -> b) -> a -> b
$ (TypeArg -> GenVarDecl) -> Maybe TypeArg -> Maybe GenVarDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeArg -> GenVarDecl
GenTypeVarDecl Maybe TypeArg
tv
           _ -> do [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ (Diagnosis -> Diagnosis) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map ( \ d :: Diagnosis
d -> DiagKind -> [Char] -> Range -> Diagnosis
Diag DiagKind
Hint (Diagnosis -> [Char]
diagString Diagnosis
d) Range
q) [Diagnosis]
ds
                   State Env (Maybe GenVarDecl)
varDecl
    else State Env (Maybe GenVarDecl)
varDecl

makeMonomorph :: VarDecl -> VarDecl
makeMonomorph :: VarDecl -> VarDecl
makeMonomorph (VarDecl v :: Id
v t :: Type
t sk :: SeparatorKind
sk ps :: Range
ps) = Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
v (Type -> Type
monoType Type
t) SeparatorKind
sk Range
ps

monoType :: Type -> Type
monoType :: Type -> Type
monoType = FoldTypeRec Type -> Type -> Type
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec Type
mapTypeRec
  { foldTypeName :: Type -> Id -> RawKind -> Int -> Type
foldTypeName = \ t :: Type
t i :: Id
i k :: RawKind
k n :: Int
n -> if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 then Id -> RawKind -> Int -> Type
TypeName Id
i RawKind
k 0 else Type
t }

-- | analyse variable declaration
anaVarDecl :: VarDecl -> State Env (Maybe VarDecl)
anaVarDecl :: VarDecl -> State Env (Maybe VarDecl)
anaVarDecl (VarDecl v :: Id
v oldT :: Type
oldT sk :: SeparatorKind
sk ps :: Range
ps) =
    do Maybe Type
mt <- Type -> State Env (Maybe Type)
anaStarType Type
oldT
       Maybe VarDecl -> State Env (Maybe VarDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe VarDecl -> State Env (Maybe VarDecl))
-> Maybe VarDecl -> State Env (Maybe VarDecl)
forall a b. (a -> b) -> a -> b
$ case Maybe Type
mt of
               Nothing -> Maybe VarDecl
forall a. Maybe a
Nothing
               Just t :: Type
t -> VarDecl -> Maybe VarDecl
forall a. a -> Maybe a
Just (VarDecl -> Maybe VarDecl) -> VarDecl -> Maybe VarDecl
forall a b. (a -> b) -> a -> b
$ Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
v Type
t SeparatorKind
sk Range
ps