ClassAna.hs revision 32a7cc7177ecf70e35ec831ff86887b9acc40dca
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettDescription : analyse kinds using a class map
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : Christian.Maeder@dfki.de
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederStability : experimental
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachanalyse kinds using a class map
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport qualified Data.Map as Map
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport qualified Data.Set as Set
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett-- * analyse kinds
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-- | check the kind and compute the raw kind
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederanaKindM :: Kind -> ClassMap -> Result RawKind
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachanaKindM k cm = case k of
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder ClassKind ci -> if k == universe then return rStar
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder else case Map.lookup ci cm of
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblett Just (ClassInfo rk _) -> return rk
04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett Nothing -> Result [mkDiag Error "not a class" ci] $ Just rStar
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett FunKind v k1 k2 ps -> do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly rk1 <- anaKindM k1 cm
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder rk2 <- anaKindM k2 cm
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett return $ FunKind v rk1 rk2 ps
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | get minimal function kinds of (class) kind
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygetFunKinds :: Monad m => ClassMap -> Kind -> m (Set.Set Kind)
842ae753ab848a8508c4832ab64296b929167a97Christian MaedergetFunKinds cm k = case k of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder FunKind _ _ _ _ -> return $ Set.singleton k
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ClassKind c -> case Map.lookup c cm of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just info -> do
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett ks <- mapM (getFunKinds cm) $ Set.toList $ classKinds info
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder return $ keepMinKinds cm ks
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder _ -> fail $ "not a function kind '" ++ showId c "'"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | compute arity from a raw kind
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederkindArity :: RawKind -> Int
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederkindArity k = case k of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder ClassKind _ -> 0
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett FunKind _ _ rk _ -> 1 + kindArity rk
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder-- | check if a class occurs in one of its super kinds
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaedercyclicClassId :: ClassMap -> Id -> Kind -> Bool
a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian MaedercyclicClassId cm ci k = case k of
a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian Maeder FunKind _ k1 k2 _ -> cyclicClassId cm ci k1 || cyclicClassId cm ci k2
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder ClassKind cj -> cj /= universeId &&
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder (cj == ci || not (Set.null $ Set.filter (cyclicClassId cm ci)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder $ classKinds $ Map.findWithDefault (error "cyclicClassId") cj cm))
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder-- * subkinding
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder-- | keep only minimal elements according to 'lesserKind'
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaederkeepMinKinds :: ClassMap -> [Set.Set Kind] -> Set.Set Kind
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder . keepMins (lesserKind cm) . Set.toList . Set.unions
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder-- | no kind of the set is lesser than the new kind
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedernewKind :: ClassMap -> Kind -> Set.Set Kind -> Bool
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedernewKind cm k = Set.null . Set.filter (flip (lesserKind cm) k)
8db2221917c1bc569614f3481bcdb3b988facaedChristian Maeder-- | add a new kind to a set
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederaddNewKind :: ClassMap -> Kind -> Set.Set Kind -> Set.Set Kind
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaederaddNewKind cm k = Set.insert k . Set.filter (not . lesserKind cm k)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | check subkinding (kinds with variances are greater)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettlesserKind :: ClassMap -> Kind -> Kind -> Bool
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettlesserKind cm k1 k2 = case k1 of
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly ClassKind c1 -> (case k2 of
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett ClassKind c2 -> c1 == c2 || if k1 == universe then
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett False else k2 == universe
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett _ -> False) ||
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Just info -> not $ newKind cm k2 $ classKinds info
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder FunKind v1 a1 r1 _ -> case k2 of
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder FunKind v2 a2 r2 _ -> (case v2 of
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett InVar -> True
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett _ -> v1 == v2) && lesserKind cm r1 r2 && lesserKind cm a2 a1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- | compare raw kinds
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettlesserRawKind :: RawKind -> RawKind -> Bool
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaederlesserRawKind k1 k2 = case k1 of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ClassKind _ -> case k2 of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ClassKind _ -> True
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder FunKind v1 a1 r1 _ -> case k2 of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder FunKind v2 a2 r2 _ -> (case v2 of
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder InVar -> True
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder _ -> v1 == v2) && lesserRawKind r1 r2 && lesserRawKind a2 a1
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettminRawKind :: Monad m => String -> RawKind -> RawKind -> m RawKind
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachminRawKind str r1 r2 = if lesserRawKind r1 r2 then return r1 else
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett if lesserRawKind r2 r1 then return r2 else
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder fail $ diffKindString str r1 r2
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederrawToKind :: RawKind -> Kind
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian MaederrawToKind = mapKind (const universeId)
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly-- * diagnostic messages
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly-- | create message for different kinds
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillydiffKindString :: String -> RawKind -> RawKind -> String
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillydiffKindString a k1 k2 = "incompatible kind of: " ++ a ++
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly expected (rawToKind k1) (rawToKind k2)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | create diagnostic for different kinds
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederdiffKindDiag :: (PosItem a, Pretty a) =>
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett a -> RawKind -> RawKind -> [Diagnosis]
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettdiffKindDiag a k1 k2 =
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett [Diag Error (diffKindString (showDoc a "") k1 k2) $ getRange a]
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder-- | check if raw kinds are equal
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettcheckKinds :: (PosItem a, Pretty a) =>
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly a -> RawKind -> RawKind -> [Diagnosis]
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettcheckKinds p k1 k2 =
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett maybe (diffKindDiag p k1 k2) (const []) $ minRawKind "" k1 k2
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | analyse class decls
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyanaClassDecls :: ClassDecl -> State Env ClassDecl
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyanaClassDecls (ClassDecl cls k ps) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder do cm <- gets classMap
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let Result ds (Just rk) = anaKindM k cm
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let ak = if null ds then k else universe
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly mapM_ (addClassDecl rk ak) cls
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ ClassDecl cls ak ps
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | store a class
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederaddClassDecl :: RawKind -> Kind -> Id -> State Env ()
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- check with merge
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyaddClassDecl rk kind ci =
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder if ci == universeId then
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder addDiags [mkDiag Warning "void universe class declaration" ci]
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett cm <- gets classMap
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett tm <- gets typeMap
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder tvs <- gets localTypeVars
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just _ -> addDiags [mkDiag Error "class name already a type" ci]
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder Nothing -> case Map.lookup ci tvs of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just _ -> addDiags
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly [mkDiag Error "class name already a type variable" ci]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Nothing -> case Map.lookup ci cm of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Nothing -> putClassMap $ Map.insert ci
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (ClassInfo rk $ Set.singleton kind) cm
4620f04678d4221ed3547f5bcab117d41ffd86f4Christian Maeder Just (ClassInfo ork superClasses) ->
4620f04678d4221ed3547f5bcab117d41ffd86f4Christian Maeder let ds = checkKinds ci rk ork in
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder if null ds then
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly if cyclicClassId cm ci kind then
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly addDiags [mkDiag Error "cyclic class" ci]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else if newKind cm kind superClasses then do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly addDiags [mkDiag Hint "refined class" ci]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly putClassMap $ Map.insert ci
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (ClassInfo ork $ addNewKind cm kind superClasses) cm
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else addDiags [mkDiag Warning "unchanged class" ci]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly else addDiags ds