7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./HasCASL/TypeAna.hs
81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : infer the kinds of types
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederStability : experimental
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederPortability : portable
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederanalyse types
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-}
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule HasCASL.TypeAna where
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.As
950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maederimport HasCASL.FoldType
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport HasCASL.AsUtils
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.Le
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport HasCASL.ClassAna
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederimport HasCASL.TypeMixAna
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maederimport Common.DocUtils
8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian Maederimport Common.Id
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Result
a6f84880cea4485fba85b521d122eba73b0df70bChristian Maederimport Common.Utils
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maederimport Common.Lib.State
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maederimport Data.Maybe
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maederimport Data.List as List
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maederimport Control.Monad
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder
878ac75d7acbbb06412e82a4c95356ce60f942deChristian Maeder-- * infer kind
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- | extract kinds of type identifier
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedergetIdKind :: Env -> Id -> Result ((Variance, RawKind, Set.Set Kind), Type)
2ac1742771a267119f1d839054b5e45d0a468085Christian MaedergetIdKind te i =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder case Map.lookup i $ localTypeVars te of
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Nothing -> case Map.lookup i $ typeMap te of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Nothing -> mkError "unknown type" i
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Just (TypeInfo rk l _ _) ->
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian Maeder return ((NonVar, rk, l), TypeName i rk 0)
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder Just (TypeVarDefn v vk rk c) ->
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder return ((v, rk, Set.singleton $ toKind vk), TypeName i rk c)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- | extract kinds of co- or invariant type identifiers
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedergetCoVarKind :: Maybe Bool -> Env -> Id
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -> Result ((RawKind, Set.Set Kind), Type)
2ac1742771a267119f1d839054b5e45d0a468085Christian MaedergetCoVarKind b te i = do
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ((v, rk, l), ty) <- getIdKind te i
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder case (v, b) of
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (ContraVar, Just True) -> Result
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder [mkDiag Hint "wrong contravariance of" i]
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder $ Just ((rk, Set.empty), ty)
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (CoVar, Just False) -> Result
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder [mkDiag Hint "wrong covariance of" i]
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder $ Just ((rk, Set.empty), ty)
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder _ -> return ((rk, l), ty)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | check if there is at least one solution
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedersubKinds :: DiagKind -> ClassMap -> Type -> Set.Set Kind -> Set.Set Kind
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -> Set.Set Kind -> Result (Set.Set Kind)
2ac1742771a267119f1d839054b5e45d0a468085Christian MaedersubKinds dk cm ty sk ks res =
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder if Set.null $ Set.filter (flip (newKind cm) ks) sk then return res
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder else Result [Diag dk
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder ("no kind found for '" ++ showDoc ty "'" ++
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder if Set.null ks then "" else expected sk ks)
522913d1d69be804c9579bbc77868ec6b501b608Christian Maeder $ getRange ty] $ if dk == Error then Nothing else Just Set.empty
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder-- | add an analysed type argument (warn on redeclared types)
b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederaddTypeVarDecl :: Bool -> TypeArg -> State Env ()
b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederaddTypeVarDecl warn (TypeArg i v vk rk c _ _) =
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder addLocalTypeVar warn (TypeVarDefn v vk rk c) i
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder
b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederaddLocalTypeVar :: Bool -> TypeVarDefn -> Id -> State Env ()
b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederaddLocalTypeVar warn tvd i = do
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder e <- get
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder let tvs = localTypeVars e
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder when warn $ do
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder when (Map.member i $ typeMap e)
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder $ addDiags [mkDiag Warning
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder "type variable shadows type constructor" i]
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder when (Map.member i tvs)
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder $ addDiags [mkDiag Hint "rebound type variable" i]
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder when (Map.member i $ localVars e)
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder $ addDiags [mkDiag Warning
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder "type variable does not shadow normal variable" i]
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder putLocalTypeVars $ Map.insert i tvd tvs
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | infer all minimal kinds
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederinferKinds :: Maybe Bool -> Type -> Env
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -> Result ((RawKind, Set.Set Kind), Type)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinferKinds b ty te@Env {classMap = cm} = case ty of
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder TypeName i _ _ -> getCoVarKind b te i
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder TypeAppl t1 t2 -> do
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder ((rk, ks), t3) <- inferKinds b t1 te
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder case rk of
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder FunKind v _ rr _ -> do
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder ((_, l), t4) <- inferKinds (case v of
7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder ContraVar -> Just $ maybe False not b
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder CoVar -> Just $ fromMaybe True b
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder _ -> Nothing) t2 te
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder kks <- mapM (getFunKinds cm) $ Set.toList ks
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder rs <- mapM ( \ fk -> case fk of
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder FunKind _ arg res _ -> subKinds Hint cm t2
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder (Set.singleton arg) l $ Set.singleton res
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder _ -> error "inferKinds: no function kind"
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder ) $ Set.toList $ keepMinKinds cm kks
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder return ((rr, keepMinKinds cm rs), TypeAppl t3 t4)
840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder _ -> mkError "unexpected type argument" t2
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder TypeAbs ta@(TypeArg _ v k r _ _ q) t ps -> do
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder let newEnv = execState (addTypeVarDecl False ta) te
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder ((rk, ks), nt) <- inferKinds Nothing t newEnv
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder return (( FunKind v r rk q
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder , keepMinKinds cm
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder [Set.map (\ j -> FunKind v (toKind k) j q) ks])
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder , TypeAbs ta nt ps)
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder KindedType kt kind ps -> do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let Result ds _ = mapM (`anaKindM` cm) $ Set.toList kind
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder sk <- if null ds then return kind else Result ds Nothing
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder ((rk, ks), t) <- inferKinds b kt te
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder l <- subKinds Hint cm kt sk ks sk
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder return ((rk, l), KindedType t sk ps)
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder ExpandedType t1 t2 -> do
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder ((rk1, ks), t4) <- inferKinds b t2 te
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder ((rk2, aks), t3) <- inferKinds b t1 te
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder rk <- maybe (Result (diffKindDiag ty rk1 rk2) Nothing) return
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder $ minRawKind "" rk1 rk2
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder return ((rk, keepMinKinds cm [aks, ks]), ExpandedType t3 t4)
2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian Maeder _ -> error "inferKinds"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- | extract the raw kind from a type term
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederrawKindOfType :: Type -> RawKind
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaederrawKindOfType = foldType FoldTypeRec
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder { foldTypeName = \ _ _ k _ -> k
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder , foldTypeAppl = \ _ ka _ -> case ka of
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder FunKind _ _ k _ -> k
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder _ -> error "rawKindOfType"
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder , foldExpandedType = \ _ k1 ->
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder fromMaybe (error "rawKindOfType.foldExpandedType") . minRawKind "" k1
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder , foldTypeAbs = \ _ (TypeArg _ v _ r _ _ _) -> FunKind v r
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder , foldKindedType = \ _ k _ _ -> k
4805aaef9706fd26f102ffd712b99cb8778ba3c1Christian Maeder , foldTypeToken = \ _ _ -> rStar
4805aaef9706fd26f102ffd712b99cb8778ba3c1Christian Maeder , foldBracketType = \ _ _ _ _ -> rStar
4805aaef9706fd26f102ffd712b99cb8778ba3c1Christian Maeder , foldMixfixType = \ _ _ -> rStar }
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- | subtyping relation
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaederlesserType :: Env -> Type -> Type -> Bool
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederlesserType te t1 t2 = case (t1, t2) of
cc584a730c98e711c2a244e51b102ba1821e531dChristian Maeder (KindedType t _ _, _) -> lesserType te t t2
cc584a730c98e711c2a244e51b102ba1821e531dChristian Maeder (ExpandedType _ t, _) -> lesserType te t t2
cc584a730c98e711c2a244e51b102ba1821e531dChristian Maeder (_, KindedType t _ _) -> lesserType te t1 t
cc584a730c98e711c2a244e51b102ba1821e531dChristian Maeder (_, ExpandedType _ t) -> lesserType te t1 t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (TypeName {}, TypeAppl (TypeName l _ _) t) | l == lazyTypeId ->
66f4f32855e7e2f0cf79b50ce6bd426598d9b166Christian Maeder lesserType te t1 t
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (TypeAppl c1 a1, TypeAppl c2 a2) ->
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder let b1 = lesserType te a1 a2
d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder b2 = lesserType te a2 a1
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder b = b1 && b2
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder in (case (rawKindOfType c1, rawKindOfType c2) of
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (FunKind v1 _ _ _, FunKind v2 _ _ _) ->
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder if v1 == v2 then case v1 of
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder CoVar -> b1
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ContraVar -> b2
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder _ -> b
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder else b
d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder _ -> error "lesserType: no FunKind") && lesserType te c1 c2
66f4f32855e7e2f0cf79b50ce6bd426598d9b166Christian Maeder || case c2 of
66f4f32855e7e2f0cf79b50ce6bd426598d9b166Christian Maeder (TypeName l _ _) | l == lazyTypeId -> lesserType te t1 a2
66f4f32855e7e2f0cf79b50ce6bd426598d9b166Christian Maeder _ -> False
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (TypeName i1 _ _, TypeName i2 _ _) | i1 == i2 -> True
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (TypeName i k _, _) -> case Map.lookup i $ localTypeVars te of
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Nothing -> case Map.lookup i $ typeMap te of
8dcc70ff9afdfe4aff258676718677a4d7076fd0Christian Maeder Nothing -> False
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Just ti -> any ( \ j -> lesserType te (TypeName j k 0) t2) $
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder Set.toList $ superTypes ti
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Just (TypeVarDefn _ vk _ _) -> case vk of
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Downset t -> lesserType te t t2
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder _ -> False
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (TypeAppl _ _, TypeName {}) -> False
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (TypeAppl _ _, TypeAbs {}) -> False
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (TypeAbs {}, TypeName {}) -> False
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder (t3, t4) -> t3 == t4
d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder
a6f84880cea4485fba85b521d122eba73b0df70bChristian MaederlesserTypeScheme :: Env -> TypeScheme -> TypeScheme -> Bool
a6f84880cea4485fba85b521d122eba73b0df70bChristian MaederlesserTypeScheme e (TypeScheme args1 t1 _) (TypeScheme args2 t2 _) =
a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder null args1 && null args2 && lesserType e t1 t2
a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder
a6f84880cea4485fba85b521d122eba73b0df70bChristian MaederlesserOpInfo :: Env -> OpInfo -> OpInfo -> Bool
a6f84880cea4485fba85b521d122eba73b0df70bChristian MaederlesserOpInfo e o1 = lesserTypeScheme e (opType o1) . opType
a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder
a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder-- | get operations by name removing super profiles
a6f84880cea4485fba85b521d122eba73b0df70bChristian MaedergetMinAssumps :: Env -> Id -> [OpInfo]
a6f84880cea4485fba85b521d122eba73b0df70bChristian MaedergetMinAssumps e i = keepMins (lesserOpInfo e) $ Set.toList
a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder $ Map.findWithDefault Set.empty i $ assumps e
a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder-- | type identifiers of a type
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederidsOf :: (Int -> Bool) -> Type -> Set.Set Id
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaederidsOf b = Set.fromList . map (fst . snd) . leaves b
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder-- * super type ids
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder-- | compute super type ids of one type id
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedersuperIds :: TypeMap -> Id -> Set.Set Id
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedersuperIds tm = supIds tm Set.empty . Set.singleton
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- | compute all super type ids for several type ids given as second argument
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedersupIds :: TypeMap -> Set.Set Id -> Set.Set Id -> Set.Set Id
2ac1742771a267119f1d839054b5e45d0a468085Christian MaedersupIds tm known new =
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder if Set.null new then known else
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder let more = Set.unions $ map ( \ i -> superTypes
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder $ Map.findWithDefault starTypeInfo i tm)
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder $ Set.toList new
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder newKnown = Set.union known new
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder in supIds tm newKnown (more Set.\\ newKnown)
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder-- * expand alias types
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder
d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder-- | expand aliases in a type scheme
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maederexpand :: TypeMap -> TypeScheme -> TypeScheme
2ac1742771a267119f1d839054b5e45d0a468085Christian Maederexpand = mapTypeOfScheme . expandAliases
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederfilterAliases :: TypeMap -> TypeMap
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederfilterAliases = Map.filter ( \ ti -> case typeDefn ti of
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder AliasTypeDefn _ -> True
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder _ -> False)
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- | expand aliases in a type and reduce type map first
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederexpandAlias :: TypeMap -> Type -> Type
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederexpandAlias = expandAliases . filterAliases
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- | expand aliases in a type if type map non-null
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederexpandAliases :: TypeMap -> Type -> Type
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederexpandAliases tm = if Map.null tm then id else expandAux tm
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- | expand aliases in a type
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederexpandAux :: TypeMap -> Type -> Type
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederexpandAux tm = replAlias $ \ i k n -> case Map.lookup i tm of
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder Just TypeInfo {typeDefn = AliasTypeDefn s} ->
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder ExpandedType (TypeName i k n) s
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder _ -> TypeName i k n
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder
d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder-- | find unexpanded alias identifier
d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian MaederhasAlias :: TypeMap -> Type -> [Diagnosis]
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederhasAlias tm t =
d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder map ( \ i -> mkDiag Error ("unexpanded alias '" ++ showId i "' in") t)
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder $ Set.toList $ Set.intersection (idsOf (const True) t) $
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder Map.keysSet $ filterAliases tm
d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- * resolve and analyse types
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | resolve type and infer minimal kinds
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederanaTypeM :: (Maybe Kind, Type) -> Env -> Result ((RawKind, Set.Set Kind), Type)
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederanaTypeM (mk, parsedType) te =
0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder do resolvedType <- mkTypeConstrAppl te parsedType
d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder let tm = typeMap te
d48085f765fca838c1d972d2123601997174583dChristian Maeder adj = adjustPos $ getRange parsedType
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder cm = classMap te
bd6b297dcf467926715d0a6bd36e8d4071b6728eChristian Maeder ((rk, ks), checkedType) <- adj $ inferKinds Nothing resolvedType te
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder l <- adj $ case mk of
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Nothing -> subKinds Error cm parsedType
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder (if Set.null ks then Set.singleton universe else ks) ks ks
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Just k -> subKinds Error cm parsedType (Set.singleton k) ks $
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Set.filter (flip (lesserKind cm) k) ks
bd6b297dcf467926715d0a6bd36e8d4071b6728eChristian Maeder let expandedType = expandAlias tm checkedType
bd6b297dcf467926715d0a6bd36e8d4071b6728eChristian Maeder Result (hasAlias tm expandedType) $ Just ()
bd6b297dcf467926715d0a6bd36e8d4071b6728eChristian Maeder return ((rk, l), expandedType)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- | resolve the type and check if it is of the universe class
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederanaStarTypeM :: Type -> Env -> Result ((RawKind, Set.Set Kind), Type)
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederanaStarTypeM t = anaTypeM (Just universe, t)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- * misc functions on types
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | check if an id occurs in a type
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercyclicType :: Id -> Type -> Bool
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedercyclicType i = Set.member i . idsOf (== 0)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder-- | check for unbound (or if False for too many) type variables
840b2a6f37ec58f3281da16fafbc4121462c856aChristian MaederunboundTypevars :: Bool -> [TypeArg] -> Type -> [Diagnosis]
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederunboundTypevars b args ty =
3bffe0f10ad93403e36288a1a4a92d50356956b5Christian Maeder let fvs = freeTVarIds ty
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder argIds = map getTypeVar args
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder restVars1 = fvs List.\\ argIds
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder restVars2 = argIds List.\\ fvs
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder in (if null restVars1 then []
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder else [mkDiag Error ("unbound type variable(s)\n "
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder ++ showSepList ("," ++) showId
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder restVars1 " in") ty])
840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder ++ if b || null restVars2 then [] else
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder [mkDiag Warning ("ignoring unused variable(s)\n "
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder ++ showSepList ("," ++) showId
bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder restVars2 " in") ty]
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder
9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder-- | check for proper generalizability (False: warn also for unused types)
9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maedergeneralizable :: Bool -> TypeScheme -> [Diagnosis]
9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maedergeneralizable b (TypeScheme args ty _) =
9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder unboundTypevars b args ty ++ checkUniqueTypevars args
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- | check uniqueness of type variables
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaedercheckUniqueTypevars :: [TypeArg] -> [Diagnosis]
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaedercheckUniqueTypevars = checkUniqueness . map getTypeVar