ClassAna.hs revision 034f5450bcde2bfe9c94fa52f03c9592f872af5a
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceModule : $Header$
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceDescription : analyse kinds using a class map
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceMaintainer : Christian.Maeder@dfki.de
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceStability : experimental
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancePortability : portable
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceanalyse kinds using a class map
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport qualified Data.Map as Map
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport qualified Data.Set as Set
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- * analyse kinds
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- | check the kind and compute the raw kind
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceanaKindM :: Kind -> ClassMap -> Result RawKind
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceanaKindM k cm = case k of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ClassKind ci -> if k == universe then return rStar
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance else case Map.lookup ci cm of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Just (ClassInfo rk _) -> return rk
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Nothing -> Result [mkDiag Error "not a class" ci] $ Just rStar
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance FunKind v k1 k2 ps -> do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance rk1 <- anaKindM k1 cm
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance rk2 <- anaKindM k2 cm
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance return $ FunKind v rk1 rk2 ps
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- | get minimal function kinds of (class) kind
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancegetFunKinds :: Monad m => ClassMap -> Kind -> m (Set.Set Kind)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancegetFunKinds cm k = case k of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance FunKind _ _ _ _ -> return $ Set.singleton k
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ClassKind c -> case Map.lookup c cm of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Just info -> do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ks <- mapM (getFunKinds cm) $ Set.toList $ classKinds info
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance return $ keepMinKinds cm ks
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance _ -> fail $ "not a function kind '" ++ showId c "'"
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- | compute arity from a raw kind
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancekindArity :: RawKind -> Int
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancekindArity k = case k of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ClassKind _ -> 0
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance FunKind _ _ rk _ -> 1 + kindArity rk
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- | check if a class occurs in one of its super kinds
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancecyclicClassId :: ClassMap -> Id -> Kind -> Bool
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancecyclicClassId cm ci k = case k of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance FunKind _ k1 k2 _ -> cyclicClassId cm ci k1 || cyclicClassId cm ci k2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ClassKind cj -> cj /= universeId &&
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (cj == ci || not (Set.null $ Set.filter (cyclicClassId cm ci)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance $ classKinds $ Map.findWithDefault (error "cyclicClassId") cj cm))
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- * subkinding
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- | keep only minimal elements according to 'lesserKind'
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancekeepMinKinds :: ClassMap -> [Set.Set Kind] -> Set.Set Kind
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancekeepMinKinds cm = Set.fromDistinctAscList
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance . keepMins (lesserKind cm) . Set.toList . Set.unions
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance-- | no kind of the set is lesser than the new kind
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancenewKind :: ClassMap -> Kind -> Set.Set Kind -> Bool
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancenewKind cm k = Set.null . Set.filter (flip (lesserKind cm) k)
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance-- | add a new kind to a set
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceaddNewKind :: ClassMap -> Kind -> Set.Set Kind -> Set.Set Kind
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceaddNewKind cm k = Set.insert k . Set.filter (not . lesserKind cm k)
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancelesserVariance :: Variance -> Variance -> Bool
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancelesserVariance v1 v2 = case v1 of
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance _ -> case v2 of
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance NonVar -> True
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance-- | revert variance
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancerevVariance :: Variance -> Variance
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancerevVariance v = case v of
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance InVar -> NonVar
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance CoVar -> ContraVar
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance ContraVar -> CoVar
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance NonVar -> InVar
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance-- | compute the minimal variance
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceminVariance :: Variance -> Variance -> Variance
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceminVariance v1 v2 = case v1 of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance _ -> case v2 of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance _ -> if v1 == v2 then v1 else InVar
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance-- | check subkinding (kinds with variances are greater)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancelesserKind :: ClassMap -> Kind -> Kind -> Bool
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancelesserKind cm k1 k2 = case k1 of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ClassKind c1 -> (case k2 of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ClassKind c2 -> c1 == c2 || if k1 == universe then
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance False else k2 == universe
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance _ -> False) ||
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance Just info -> not $ newKind cm k2 $ classKinds info
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance FunKind v1 a1 r1 _ -> case k2 of
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance FunKind v2 a2 r2 _ -> lesserVariance v1 v2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance && lesserKind cm r1 r2 && lesserKind cm a2 a1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- | compare raw kinds
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancelesserRawKind :: RawKind -> RawKind -> Bool
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancelesserRawKind k1 k2 = case k1 of
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance ClassKind _ -> case k2 of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ClassKind _ -> True
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance FunKind v1 a1 r1 _ -> case k2 of
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance FunKind v2 a2 r2 _ -> lesserVariance v1 v2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance && lesserRawKind r1 r2 && lesserRawKind a2 a1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceminRawKind :: Monad m => String -> RawKind -> RawKind -> m RawKind
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceminRawKind str k1 k2 = let err = fail $ diffKindString str k1 k2 in case k1 of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ClassKind _ -> case k2 of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ClassKind _ -> return $ ClassKind ()
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance FunKind v1 a1 r1 ps -> case k2 of
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance FunKind v2 a2 r2 qs -> do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance a3 <- minRawKind str a2 a1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance r3 <- minRawKind str r1 r2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance return $ FunKind (minVariance v1 v2) a3 r3 $ appRange ps qs
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancerawToKind :: RawKind -> Kind
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancerawToKind = mapKind (const universeId)
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance-- * diagnostic messages
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance-- | create message for different kinds
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancediffKindString :: String -> RawKind -> RawKind -> String
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancediffKindString a k1 k2 = "incompatible kind of: " ++ a ++
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance expected (rawToKind k1) (rawToKind k2)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- | create diagnostic for different kinds
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancediffKindDiag :: (PosItem a, Pretty a) =>
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance a -> RawKind -> RawKind -> [Diagnosis]
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel MancediffKindDiag a k1 k2 =
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance [Diag Error (diffKindString (showDoc a "") k1 k2) $ getRange a]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- | check if raw kinds are compatible
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancecheckKinds :: (PosItem a, Pretty a) =>
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance a -> RawKind -> RawKind -> [Diagnosis]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancecheckKinds p k1 k2 =
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance maybe (diffKindDiag p k1 k2) (const []) $ minRawKind "" k1 k2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- | analyse class decls
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceanaClassDecls :: ClassDecl -> State Env ClassDecl
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceanaClassDecls (ClassDecl cls k ps) =
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance do cm <- gets classMap
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance let Result ds (Just rk) = anaKindM k cm
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance let ak = if null ds then k else universe
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance mapM_ (addClassDecl rk ak) cls
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance return $ ClassDecl cls ak ps
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance-- | store a class
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceaddClassDecl :: RawKind -> Kind -> Id -> State Env ()
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance-- check with merge
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceaddClassDecl rk kind ci =
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance if ci == universeId then
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance addDiags [mkDiag Warning "void universe class declaration" ci]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance let cm = classMap e
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance tm = typeMap e
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance tvs = localTypeVars e
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Just _ -> addDiags [mkDiag Error "class name already a type" ci]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Nothing -> case Map.lookup ci tvs of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Just _ -> addDiags
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance [mkDiag Error "class name already a type variable" ci]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Nothing -> case Map.lookup ci cm of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance addSymbol $ idToClassSymbol e ci rk
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance putClassMap $ Map.insert ci
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (ClassInfo rk $ Set.singleton kind) cm
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Just (ClassInfo ork superClasses) ->
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance let Result ds mk = minRawKind (showDoc ci "") rk ork
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Nothing -> addDiags ds
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance if cyclicClassId cm ci kind then
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance addDiags [mkDiag Error "cyclic class" ci]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance addSymbol $ idToClassSymbol e ci nk
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance if newKind cm kind superClasses then do
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance addDiags [mkDiag Hint "refined class" ci]
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance putClassMap $ Map.insert ci
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance (ClassInfo nk $ addNewKind cm kind superClasses) cm
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance else addDiags [mkDiag Warning "unchanged class" ci]