ClassAna.hs revision abae801b829b32e32fff31d106245cf3b8c0a21f
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco{- |
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoModule : $Header$
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoMaintainer : maeder@tzi.de
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoStability : experimental
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoPortability : portable
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoanalysing kinds using a class map
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-}
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescomodule HasCASL.ClassAna where
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoimport HasCASL.As
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoimport HasCASL.AsUtils
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoimport Common.Id
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoimport HasCASL.Le
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoimport Common.PrettyPrint
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoimport qualified Common.Lib.Map as Map
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoimport Common.Lib.State
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoimport Common.Result
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- * analyse kinds
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- | check the kind and compute the raw kind
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoanaKindM :: Kind -> ClassMap -> Result RawKind
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoanaKindM k cm = case k of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ClassKind ci -> if k == star then return star
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco else case Map.lookup ci cm of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco Just (ClassInfo rk _) -> return rk
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco Nothing -> Result [mkDiag Error "not a class" ci] $ Just star
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco FunKind k1 k2 ps -> do rk1 <- anaKindM k1 cm
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco rk2 <- anaKindM k2 cm
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco return $ FunKind rk1 rk2 ps
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ExtKind ek v ps -> do rk <- anaKindM ek cm
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco return $ ExtKind rk v ps
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco-- | get minimal function kinds of (class) kind
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescogetFunKinds :: Monad m => ClassMap -> Kind -> m [Kind]
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescogetFunKinds cm k = case k of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco FunKind _ _ _ -> return [k]
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ClassKind c -> case Map.lookup c cm of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco Just (ClassInfo _ cs) -> do
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ks <- mapM (getFunKinds cm) cs
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco return $ keepMinKinds cm $ concat ks
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco _ -> fail $ "not a function kind '" ++ showId c "'"
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ExtKind ek _ _ -> getFunKinds cm ek
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- | a list of argument kinds with result kind
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescogetKindAppl :: ClassMap -> Kind -> [a] -> [([Kind], Kind)]
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescogetKindAppl cm k args = if null args then [([], k)] else
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco case k of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco FunKind k1 k2 _ -> let ks = getKindAppl cm k2 (tail args)
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco in map ( \ (kargs, rk) -> (k1 : kargs, rk)) ks
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ClassKind ci -> case Map.lookup ci cm of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco Just (ClassInfo _ ks) -> case ks of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco [] -> error $ "getKindAppl1 " ++ show k
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco _ -> concatMap (\ fk -> getKindAppl cm fk args) ks
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco _ -> error $ "getKindAppl2 " ++ show k
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco _ -> error $ "getKindAppl3 " ++ show k
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- | compute arity from a raw kind
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescokindArity :: RawKind -> Int
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescokindArity k =
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco case k of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ClassKind _ -> if k == star then 1 else error "kindArity: not a raw kind"
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco FunKind _ rk _ -> 1 + kindArity rk
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ExtKind ek _ _ -> kindArity ek
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- | check if a class occurs in one of its super kinds
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescocyclicClassId :: ClassMap -> ClassId -> Kind -> Bool
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescocyclicClassId cm ci k =
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco case k of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco FunKind k1 k2 _ -> cyclicClassId cm ci k1 || cyclicClassId cm ci k2
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ExtKind ek _ _ -> cyclicClassId cm ci ek
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ClassKind cj -> if k == star then False else
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco cj == ci || case Map.lookup cj cm of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco Nothing -> error "cyclicClassId"
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco Just info -> any (cyclicClassId cm ci) $ classKinds info
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- * subkinding
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- | keep only minimal elements
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescokeepMins :: (a -> a -> Bool) -> [a] -> [a]
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescokeepMins lt l = case l of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco [] -> []
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco x : r -> let s = filter ( \ y -> not (lt x y)) r
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco m = keepMins lt s
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco in if any ( \ y -> lt y x) s then m
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco else x : m
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- | keep only minimal elements according to 'lesserKind'
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescokeepMinKinds :: ClassMap -> [Kind] -> [Kind]
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescokeepMinKinds cm = keepMins (lesserKind cm)
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- | check subkinding (kinds with variances are greater)
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescolesserKind :: ClassMap -> Kind -> Kind -> Bool
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescolesserKind cm k1 k2 = case (k1, k2) of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco (ClassKind c1, ClassKind c2) -> c1 == c2 || if k1 == star then
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco False else k2 == star ||
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco case Map.lookup c1 cm of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco Just (ClassInfo _ ks) -> any ( \ k -> lesserKind cm k k2) ks
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco _ -> error "lesserKind"
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco (ExtKind e1 v1 _, ExtKind e2 v2 _) -> v1 == v2 && lesserKind cm e1 e2
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco (_, ExtKind e2 _ _) -> lesserKind cm k1 e2
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco (FunKind a1 r1 _, FunKind a2 r2 _) ->
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco lesserKind cm r1 r2 && lesserKind cm a2 a1
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco _ -> False
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- | invert (or delete if false) the variance of an extended kind
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoinvertKindVariance :: Bool -> Kind -> Kind
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoinvertKindVariance b k = case k of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ExtKind ek v ps -> if b then ExtKind ek (invertVariance v) ps else ek
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco _ -> k
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco where
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco invertVariance :: Variance -> Variance
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco invertVariance v = case v of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco CoVar -> ContraVar
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ContraVar -> CoVar
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- * diagnostic messages
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- | create message for different kinds
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescodiffKindDiag :: (PosItem a, PrettyPrint a) =>
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco a -> Kind -> Kind -> [Diagnosis]
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescodiffKindDiag a k1 k2 =
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco [ Diag Error
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ("incompatible kind of: " ++ showPretty a "" ++ expected k1 k2)
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco $ getRange a ]
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- | check if raw kinds are equal
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescocheckKinds :: (PosItem a, PrettyPrint a) =>
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco a -> RawKind -> RawKind -> [Diagnosis]
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescocheckKinds p k1 k2 =
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco if k1 == k2 then []
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco else diffKindDiag p k1 k2
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- | analyse class decls
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoanaClassDecls :: ClassDecl -> State Env ClassDecl
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoanaClassDecls (ClassDecl cls k ps) =
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco do cm <- gets classMap
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco let Result ds (Just rk) = anaKindM k cm
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco addDiags ds
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco let ak = if null ds then k else rk
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco mapM_ (addClassDecl rk ak) cls
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco return $ ClassDecl cls ak ps
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- | store a class
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoaddClassDecl :: RawKind -> Kind -> ClassId -> State Env ()
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco-- check with merge
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoaddClassDecl rk kind ci =
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco if showId ci "" == "Type" then
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco do addDiags [mkDiag Warning
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco "void universe class declaration" ci]
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco else do
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco cm <- gets classMap
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco tm <- gets typeMap
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco tvs <- gets localTypeVars
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco case Map.lookup ci tm of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco Just _ -> addDiags [mkDiag Error "class name already a type" ci]
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco Nothing -> do
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco case Map.lookup ci tvs of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco Just _ ->
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco addDiags [mkDiag Error "class name already a type variable" ci]
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco Nothing -> do
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco case Map.lookup ci cm of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco Nothing ->
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco putClassMap $ Map.insert ci (ClassInfo rk [kind]) cm
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco Just (ClassInfo ork superClasses) -> do
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco let ds = checkKinds ci rk ork
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco addDiags ds
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco if null ds then
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco if cyclicClassId cm ci kind then
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco addDiags [mkDiag Error "cyclic class" ci]
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco else if any (\ k -> lesserKind cm k kind) superClasses
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco then addDiags [mkDiag Warning "unchanged class" ci]
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco else do addDiags [mkDiag Hint
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco "refined class" ci]
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco putClassMap $ Map.insert ci
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco (ClassInfo ork $ keepMinKinds cm $
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco kind : superClasses) cm
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco else return ()
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco