8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova{- |
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaModule : ./HasCASL/TypeAna.hs
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovaDescription : infer the kinds of types
097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina SojakovaCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaLicense : GPLv2 or higher, see LICENSE.txt
211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova
211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaMaintainer : Christian.Maeder@dfki.de
94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaStability : experimental
211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaPortability : portable
211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaanalyse types
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-}
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovamodule HasCASL.TypeAna where
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport HasCASL.As
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport HasCASL.FoldType
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport HasCASL.AsUtils
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport HasCASL.Le
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport HasCASL.ClassAna
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport HasCASL.TypeMixAna
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport qualified Data.Map as Map
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport qualified Data.Set as Set
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.DocUtils
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakovaimport Common.Id
45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakovaimport Common.Result
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.Utils
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Common.Lib.State
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Data.Maybe
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Data.List as List
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Control.Monad
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- * infer kind
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | extract kinds of type identifier
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovagetIdKind :: Env -> Id -> Result ((Variance, RawKind, Set.Set Kind), Type)
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovagetIdKind te i =
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova case Map.lookup i $ localTypeVars te of
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova Nothing -> case Map.lookup i $ typeMap te of
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova Nothing -> mkError "unknown type" i
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova Just (TypeInfo rk l _ _) ->
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova return ((NonVar, rk, l), TypeName i rk 0)
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova Just (TypeVarDefn v vk rk c) ->
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova return ((v, rk, Set.singleton $ toKind vk), TypeName i rk c)
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- | extract kinds of co- or invariant type identifiers
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovagetCoVarKind :: Maybe Bool -> Env -> Id
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova -> Result ((RawKind, Set.Set Kind), Type)
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovagetCoVarKind b te i = do
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova ((v, rk, l), ty) <- getIdKind te i
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova case (v, b) of
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova (ContraVar, Just True) -> Result
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova [mkDiag Hint "wrong contravariance of" i]
81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova $ Just ((rk, Set.empty), ty)
81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova (CoVar, Just False) -> Result
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova [mkDiag Hint "wrong covariance of" i]
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova $ Just ((rk, Set.empty), ty)
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova _ -> return ((rk, l), ty)
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- | check if there is at least one solution
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovasubKinds :: DiagKind -> ClassMap -> Type -> Set.Set Kind -> Set.Set Kind
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova -> Set.Set Kind -> Result (Set.Set Kind)
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovasubKinds dk cm ty sk ks res =
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova if Set.null $ Set.filter (flip (newKind cm) ks) sk then return res
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova else Result [Diag dk
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova ("no kind found for '" ++ showDoc ty "'" ++
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova if Set.null ks then "" else expected sk ks)
81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova $ getRange ty] $ if dk == Error then Nothing else Just Set.empty
81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova-- | add an analysed type argument (warn on redeclared types)
81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaaddTypeVarDecl :: Bool -> TypeArg -> State Env ()
81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaaddTypeVarDecl warn (TypeArg i v vk rk c _ _) =
81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova addLocalTypeVar warn (TypeVarDefn v vk rk c) i
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova
81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaaddLocalTypeVar :: Bool -> TypeVarDefn -> Id -> State Env ()
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovaaddLocalTypeVar warn tvd i = do
81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova e <- get
81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova let tvs = localTypeVars e
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova when warn $ do
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova when (Map.member i $ typeMap e)
f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova $ addDiags [mkDiag Warning
f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova "type variable shadows type constructor" i]
f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova when (Map.member i tvs)
f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova $ addDiags [mkDiag Hint "rebound type variable" i]
f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova when (Map.member i $ localVars e)
f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova $ addDiags [mkDiag Warning
f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova "type variable does not shadow normal variable" i]
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova putLocalTypeVars $ Map.insert i tvd tvs
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova-- | infer all minimal kinds
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovainferKinds :: Maybe Bool -> Type -> Env
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -> Result ((RawKind, Set.Set Kind), Type)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovainferKinds b ty te@Env {classMap = cm} = case ty of
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova TypeName i _ _ -> getCoVarKind b te i
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova TypeAppl t1 t2 -> do
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova ((rk, ks), t3) <- inferKinds b t1 te
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova case rk of
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova FunKind v _ rr _ -> do
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((_, l), t4) <- inferKinds (case v of
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ContraVar -> Just $ maybe False not b
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova CoVar -> Just $ fromMaybe True b
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova _ -> Nothing) t2 te
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova kks <- mapM (getFunKinds cm) $ Set.toList ks
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova rs <- mapM ( \ fk -> case fk of
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova FunKind _ arg res _ -> subKinds Hint cm t2
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (Set.singleton arg) l $ Set.singleton res
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova _ -> error "inferKinds: no function kind"
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ) $ Set.toList $ keepMinKinds cm kks
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova return ((rr, keepMinKinds cm rs), TypeAppl t3 t4)
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova _ -> mkError "unexpected type argument" t2
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova TypeAbs ta@(TypeArg _ v k r _ _ q) t ps -> do
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova let newEnv = execState (addTypeVarDecl False ta) te
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((rk, ks), nt) <- inferKinds Nothing t newEnv
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova return (( FunKind v r rk q
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova , keepMinKinds cm
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova [Set.map (\ j -> FunKind v (toKind k) j q) ks])
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova , TypeAbs ta nt ps)
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova KindedType kt kind ps -> do
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova let Result ds _ = mapM (`anaKindM` cm) $ Set.toList kind
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova sk <- if null ds then return kind else Result ds Nothing
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((rk, ks), t) <- inferKinds b kt te
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova l <- subKinds Hint cm kt sk ks sk
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova return ((rk, l), KindedType t sk ps)
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ExpandedType t1 t2 -> do
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((rk1, ks), t4) <- inferKinds b t2 te
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((rk2, aks), t3) <- inferKinds b t1 te
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova rk <- maybe (Result (diffKindDiag ty rk1 rk2) Nothing) return
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova $ minRawKind "" rk1 rk2
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova return ((rk, keepMinKinds cm [aks, ks]), ExpandedType t3 t4)
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova _ -> error "inferKinds"
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- | extract the raw kind from a type term
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovarawKindOfType :: Type -> RawKind
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovarawKindOfType = foldType FoldTypeRec
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova { foldTypeName = \ _ _ k _ -> k
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova , foldTypeAppl = \ _ ka _ -> case ka of
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova FunKind _ _ k _ -> k
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova _ -> error "rawKindOfType"
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova , foldExpandedType = \ _ k1 ->
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova fromMaybe (error "rawKindOfType.foldExpandedType") . minRawKind "" k1
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova , foldTypeAbs = \ _ (TypeArg _ v _ r _ _ _) -> FunKind v r
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova , foldKindedType = \ _ k _ _ -> k
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova , foldTypeToken = \ _ _ -> rStar
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova , foldBracketType = \ _ _ _ _ -> rStar
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova , foldMixfixType = \ _ _ -> rStar }
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- | subtyping relation
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovalesserType :: Env -> Type -> Type -> Bool
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovalesserType te t1 t2 = case (t1, t2) of
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (KindedType t _ _, _) -> lesserType te t t2
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (ExpandedType _ t, _) -> lesserType te t t2
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (_, KindedType t _ _) -> lesserType te t1 t
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (_, ExpandedType _ t) -> lesserType te t1 t
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (TypeName {}, TypeAppl (TypeName l _ _) t) | l == lazyTypeId ->
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova lesserType te t1 t
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (TypeAppl c1 a1, TypeAppl c2 a2) ->
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova let b1 = lesserType te a1 a2
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova b2 = lesserType te a2 a1
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova b = b1 && b2
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova in (case (rawKindOfType c1, rawKindOfType c2) of
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (FunKind v1 _ _ _, FunKind v2 _ _ _) ->
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova if v1 == v2 then case v1 of
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova CoVar -> b1
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova ContraVar -> b2
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova _ -> b
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova else b
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova _ -> error "lesserType: no FunKind") && lesserType te c1 c2
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova || case c2 of
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (TypeName l _ _) | l == lazyTypeId -> lesserType te t1 a2
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova _ -> False
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (TypeName i1 _ _, TypeName i2 _ _) | i1 == i2 -> True
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (TypeName i k _, _) -> case Map.lookup i $ localTypeVars te of
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova Nothing -> case Map.lookup i $ typeMap te of
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova Nothing -> False
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova Just ti -> any ( \ j -> lesserType te (TypeName j k 0) t2) $
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova Set.toList $ superTypes ti
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova Just (TypeVarDefn _ vk _ _) -> case vk of
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova Downset t -> lesserType te t t2
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova _ -> False
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (TypeAppl _ _, TypeName {}) -> False
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (TypeAppl _ _, TypeAbs {}) -> False
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (TypeAbs {}, TypeName {}) -> False
5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (t3, t4) -> t3 == t4
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova
df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovalesserTypeScheme :: Env -> TypeScheme -> TypeScheme -> Bool
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovalesserTypeScheme e (TypeScheme args1 t1 _) (TypeScheme args2 t2 _) =
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova null args1 && null args2 && lesserType e t1 t2
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovalesserOpInfo :: Env -> OpInfo -> OpInfo -> Bool
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovalesserOpInfo e o1 = lesserTypeScheme e (opType o1) . opType
887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | get operations by name removing super profiles
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetMinAssumps :: Env -> Id -> [OpInfo]
887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovagetMinAssumps e i = keepMins (lesserOpInfo e) $ Set.toList
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova $ Map.findWithDefault Set.empty i $ assumps e
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova-- | type identifiers of a type
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaidsOf :: (Int -> Bool) -> Type -> Set.Set Id
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaidsOf b = Set.fromList . map (fst . snd) . leaves b
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- * super type ids
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | compute super type ids of one type id
887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovasuperIds :: TypeMap -> Id -> Set.Set Id
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasuperIds tm = supIds tm Set.empty . Set.singleton
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova-- | compute all super type ids for several type ids given as second argument
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasupIds :: TypeMap -> Set.Set Id -> Set.Set Id -> Set.Set Id
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasupIds tm known new =
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova if Set.null new then known else
887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova let more = Set.unions $ map ( \ i -> superTypes
887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova $ Map.findWithDefault starTypeInfo i tm)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova $ Set.toList new
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova newKnown = Set.union known new
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in supIds tm newKnown (more Set.\\ newKnown)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- * expand alias types
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova-- | expand aliases in a type scheme
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaexpand :: TypeMap -> TypeScheme -> TypeScheme
887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakovaexpand = mapTypeOfScheme . expandAliases
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
345d3dcc9f809776009851c446916fc770aa428dKristina SojakovafilterAliases :: TypeMap -> TypeMap
345d3dcc9f809776009851c446916fc770aa428dKristina SojakovafilterAliases = Map.filter ( \ ti -> case typeDefn ti of
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova AliasTypeDefn _ -> True
345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova _ -> False)
345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | expand aliases in a type and reduce type map first
a3a6b6ebe9c2d1dc3554e44779dc7361a90e7617Kristina SojakovaexpandAlias :: TypeMap -> Type -> Type
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovaexpandAlias = expandAliases . filterAliases
45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova-- | expand aliases in a type if type map non-null
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaexpandAliases :: TypeMap -> Type -> Type
45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina SojakovaexpandAliases tm = if Map.null tm then id else expandAux tm
45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova
45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova-- | expand aliases in a type
45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina SojakovaexpandAux :: TypeMap -> Type -> Type
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaexpandAux tm = replAlias $ \ i k n -> case Map.lookup i tm of
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova Just TypeInfo {typeDefn = AliasTypeDefn s} ->
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova ExpandedType (TypeName i k n) s
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova _ -> TypeName i k n
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova
cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova-- | find unexpanded alias identifier
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovahasAlias :: TypeMap -> Type -> [Diagnosis]
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovahasAlias tm t =
f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova map ( \ i -> mkDiag Error ("unexpanded alias '" ++ showId i "' in") t)
f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova $ Set.toList $ Set.intersection (idsOf (const True) t) $
f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova Map.keysSet $ filterAliases tm
8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- * resolve and analyse types
f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova
51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- | resolve type and infer minimal kinds
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaanaTypeM :: (Maybe Kind, Type) -> Env -> Result ((RawKind, Set.Set Kind), Type)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaanaTypeM (mk, parsedType) te =
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova do resolvedType <- mkTypeConstrAppl te parsedType
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let tm = typeMap te
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova adj = adjustPos $ getRange parsedType
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova cm = classMap te
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ((rk, ks), checkedType) <- adj $ inferKinds Nothing resolvedType te
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova l <- adj $ case mk of
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> subKinds Error cm parsedType
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (if Set.null ks then Set.singleton universe else ks) ks ks
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just k -> subKinds Error cm parsedType (Set.singleton k) ks $
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Set.filter (flip (lesserKind cm) k) ks
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let expandedType = expandAlias tm checkedType
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result (hasAlias tm expandedType) $ Just ()
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova return ((rk, l), expandedType)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | resolve the type and check if it is of the universe class
45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina SojakovaanaStarTypeM :: Type -> Env -> Result ((RawKind, Set.Set Kind), Type)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaanaStarTypeM t = anaTypeM (Just universe, t)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- * misc functions on types
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | check if an id occurs in a type
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovacyclicType :: Id -> Type -> Bool
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovacyclicType i = Set.member i . idsOf (== 0)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | check for unbound (or if False for too many) type variables
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaunboundTypevars :: Bool -> [TypeArg] -> Type -> [Diagnosis]
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaunboundTypevars b args ty =
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let fvs = freeTVarIds ty
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova argIds = map getTypeVar args
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova restVars1 = fvs List.\\ argIds
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova restVars2 = argIds List.\\ fvs
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in (if null restVars1 then []
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else [mkDiag Error ("unbound type variable(s)\n "
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ showSepList ("," ++) showId
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova restVars1 " in") ty])
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ if b || null restVars2 then [] else
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova [mkDiag Warning ("ignoring unused variable(s)\n "
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ showSepList ("," ++) showId
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova restVars2 " in") ty]
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | check for proper generalizability (False: warn also for unused types)
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovageneralizable :: Bool -> TypeScheme -> [Diagnosis]
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovageneralizable b (TypeScheme args ty _) =
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova unboundTypevars b args ty ++ checkUniqueTypevars args
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | check uniqueness of type variables
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovacheckUniqueTypevars :: [TypeArg] -> [Diagnosis]
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovacheckUniqueTypevars = checkUniqueness . map getTypeVar
9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova