2dc26996d32244796c48c71fe44413c8ebf8bbc9Christian MaederDescription : analyse kinds using a class map
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederStability : experimental
a0e24c863b78669b05797ff8ce635995a9bede44Christian MaederPortability : portable
2dc26996d32244796c48c71fe44413c8ebf8bbc9Christian Maederanalyse kinds using a class map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport qualified Data.Set as Set
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- * analyse kinds
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder-- | check the kind and compute the raw kind
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederanaKindM :: Kind -> ClassMap -> Result RawKind
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederanaKindM k cm = case k of
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ClassKind ci -> if k == universe then return rStar
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder else case Map.lookup ci cm of
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder Just (ClassInfo rk _) -> return rk
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Nothing -> Result [mkDiag Error "not a class" ci] $ Just rStar
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder FunKind v k1 k2 ps -> do
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder rk1 <- anaKindM k1 cm
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder rk2 <- anaKindM k2 cm
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder return $ FunKind v rk1 rk2 ps
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- | get minimal function kinds of (class) kind
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedergetFunKinds :: Monad m => ClassMap -> Kind -> m (Set.Set Kind)
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaedergetFunKinds cm k = case k of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder FunKind {} -> return $ Set.singleton k
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder ClassKind c -> case Map.lookup c cm of
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Just info -> do
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder ks <- mapM (getFunKinds cm) $ Set.toList $ classKinds info
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder return $ keepMinKinds cm ks
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder _ -> fail $ "not a function kind '" ++ showId c "'"
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- | compute arity from a raw kind
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederkindArity :: RawKind -> Int
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaederkindArity k = case k of
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ClassKind _ -> 0
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder FunKind _ _ rk _ -> 1 + kindArity rk
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- | check if a class occurs in one of its super kinds
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedercyclicClassId :: ClassMap -> Id -> Kind -> Bool
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaedercyclicClassId cm ci k = case k of
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder FunKind _ k1 k2 _ -> cyclicClassId cm ci k1 || cyclicClassId cm ci k2
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder ClassKind cj -> cj /= universeId &&
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder (cj == ci || not (Set.null $ Set.filter (cyclicClassId cm ci)
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder $ classKinds $ Map.findWithDefault (error "cyclicClassId") cj cm))
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- * subkinding
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- | keep only minimal elements according to 'lesserKind'
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederkeepMinKinds :: ClassMap -> [Set.Set Kind] -> Set.Set Kind
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder . keepMins (lesserKind cm) . Set.toList . Set.unions
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder-- | no kind of the set is lesser than the new kind
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedernewKind :: ClassMap -> Kind -> Set.Set Kind -> Bool
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedernewKind cm k = Set.null . Set.filter (flip (lesserKind cm) k)
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder-- | add a new kind to a set
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederaddNewKind :: ClassMap -> Kind -> Set.Set Kind -> Set.Set Kind
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederaddNewKind cm k = Set.insert k . Set.filter (not . lesserKind cm k)
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian MaederlesserVariance :: Variance -> Variance -> Bool
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian MaederlesserVariance v1 v2 = case v1 of
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder InVar -> True
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder _ -> case v2 of
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder NonVar -> True
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder _ -> v1 == v2
034f5450bcde2bfe9c94fa52f03c9592f872af5aChristian Maeder-- | revert variance
034f5450bcde2bfe9c94fa52f03c9592f872af5aChristian MaederrevVariance :: Variance -> Variance
034f5450bcde2bfe9c94fa52f03c9592f872af5aChristian MaederrevVariance v = case v of
034f5450bcde2bfe9c94fa52f03c9592f872af5aChristian Maeder InVar -> NonVar
034f5450bcde2bfe9c94fa52f03c9592f872af5aChristian Maeder CoVar -> ContraVar
034f5450bcde2bfe9c94fa52f03c9592f872af5aChristian Maeder ContraVar -> CoVar
034f5450bcde2bfe9c94fa52f03c9592f872af5aChristian Maeder NonVar -> InVar
034f5450bcde2bfe9c94fa52f03c9592f872af5aChristian Maeder-- | compute the minimal variance
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian MaederminVariance :: Variance -> Variance -> Variance
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian MaederminVariance v1 v2 = case v1 of
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder _ -> case v2 of
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder _ -> if v1 == v2 then v1 else InVar
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- | check subkinding (kinds with variances are greater)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederlesserKind :: ClassMap -> Kind -> Kind -> Bool
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederlesserKind cm k1 k2 = case k1 of
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder ClassKind c1 -> (case k2 of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ClassKind c2 -> c1 == c2 || (k1 /= universe && k2 == universe)
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder _ -> False) ||
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Just info -> not $ newKind cm k2 $ classKinds info
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder FunKind v1 a1 r1 _ -> case k2 of
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder FunKind v2 a2 r2 _ -> lesserVariance v1 v2
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder && lesserKind cm r1 r2 && lesserKind cm a2 a1
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder-- | compare raw kinds
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaederlesserRawKind :: RawKind -> RawKind -> Bool
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaederlesserRawKind k1 k2 = case k1 of
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder ClassKind _ -> case k2 of
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder ClassKind _ -> True
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder FunKind v1 a1 r1 _ -> case k2 of
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder FunKind v2 a2 r2 _ -> lesserVariance v1 v2
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder && lesserRawKind r1 r2 && lesserRawKind a2 a1
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian MaederminRawKind :: Monad m => String -> RawKind -> RawKind -> m RawKind
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian MaederminRawKind str k1 k2 = let err = fail $ diffKindString str k1 k2 in case k1 of
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder ClassKind _ -> case k2 of
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder ClassKind _ -> return $ ClassKind ()
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder FunKind v1 a1 r1 ps -> case k2 of
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder FunKind v2 a2 r2 qs -> do
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder a3 <- minRawKind str a2 a1
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder r3 <- minRawKind str r1 r2
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder return $ FunKind (minVariance v1 v2) a3 r3 $ appRange ps qs
a0e24c863b78669b05797ff8ce635995a9bede44Christian MaederrawToKind :: RawKind -> Kind
a0e24c863b78669b05797ff8ce635995a9bede44Christian MaederrawToKind = mapKind (const universeId)
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- * diagnostic messages
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder-- | create message for different kinds
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian MaederdiffKindString :: String -> RawKind -> RawKind -> String
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian MaederdiffKindString a k1 k2 = "incompatible kind of: " ++ a ++
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder expected (rawToKind k1) (rawToKind k2)
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder-- | create diagnostic for different kinds
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian MaederdiffKindDiag :: (GetRange a, Pretty a) =>
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder a -> RawKind -> RawKind -> [Diagnosis]
a0e24c863b78669b05797ff8ce635995a9bede44Christian MaederdiffKindDiag a k1 k2 =
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder [Diag Error (diffKindString (showDoc a "") k1 k2) $ getRange a]
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder-- | check if raw kinds are compatible
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian MaedercheckKinds :: (GetRange a, Pretty a) =>
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder a -> RawKind -> RawKind -> [Diagnosis]
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaedercheckKinds p k1 k2 =
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder maybe (diffKindDiag p k1 k2) (const []) $ minRawKind "" k1 k2
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | analyse class decls
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederanaClassDecls :: ClassDecl -> State Env ClassDecl
a0e24c863b78669b05797ff8ce635995a9bede44Christian MaederanaClassDecls (ClassDecl cls k ps) =
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder do cm <- gets classMap
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder let Result ds (Just rk) = anaKindM k cm
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder let ak = if null ds then k else universe
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder mapM_ (addClassDecl rk ak) cls
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder return $ ClassDecl cls ak ps
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder-- | store a class
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederaddClassDecl :: RawKind -> Kind -> Id -> State Env ()
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- check with merge
a0e24c863b78669b05797ff8ce635995a9bede44Christian MaederaddClassDecl rk kind ci =
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder if ci == universeId then
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder addDiags [mkDiag Warning "void universe class declaration" ci]
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder let cm = classMap e
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder tm = typeMap e
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder tvs = localTypeVars e
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Just _ -> addDiags [mkDiag Error "class name already a type" ci]
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Nothing -> case Map.lookup ci tvs of
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Just _ -> addDiags
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder [mkDiag Error "class name already a type variable" ci]
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Nothing -> case Map.lookup ci cm of
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder Nothing -> do
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder addSymbol $ idToClassSymbol ci rk
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder putClassMap $ Map.insert ci
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder (ClassInfo rk $ Set.singleton kind) cm
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Just (ClassInfo ork superClasses) ->
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder let Result ds mk = minRawKind (showDoc ci "") rk ork
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder in case mk of
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder Nothing -> addDiags ds
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder if cyclicClassId cm ci kind then
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder addDiags [mkDiag Error "cyclic class" ci]
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder addSymbol $ idToClassSymbol ci nk
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder if newKind cm kind superClasses then do
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder addDiags [mkDiag Warning "refined class" ci]
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder putClassMap $ Map.insert ci
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder (ClassInfo nk $ addNewKind cm kind superClasses) cm
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder else addDiags [mkDiag Warning "unchanged class" ci]