{- |
Module : ./HasCASL/ClassAna.hs
Description : analyse kinds using a class map
Copyright : (c) Christian Maeder and Uni Bremen 2003-2005
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : experimental
Portability : portable
analyse kinds using a class map
-}
module HasCASL.ClassAna where
import HasCASL.As
import HasCASL.AsUtils
import HasCASL.PrintAs ()
import Common.Id
import HasCASL.Le
import qualified Data.Map as Map
import qualified Data.Set as Set
import Common.Lib.State
import Common.Result
import Common.DocUtils
import Common.Utils
-- * analyse kinds
-- | check the kind and compute the raw kind
anaKindM :: Kind -> ClassMap -> Result RawKind
anaKindM k cm = case k of
ClassKind ci -> if k == universe then return rStar
else case Map.lookup ci cm of
Just (ClassInfo rk _) -> return rk
Nothing -> Result [mkDiag Error "not a class" ci] $ Just rStar
FunKind v k1 k2 ps -> do
rk1 <- anaKindM k1 cm
rk2 <- anaKindM k2 cm
return $ FunKind v rk1 rk2 ps
-- | get minimal function kinds of (class) kind
getFunKinds :: Monad m => ClassMap -> Kind -> m (Set.Set Kind)
getFunKinds cm k = case k of
FunKind {} -> return $ Set.singleton k
ClassKind c -> case Map.lookup c cm of
Just info -> do
ks <- mapM (getFunKinds cm) $ Set.toList $ classKinds info
return $ keepMinKinds cm ks
_ -> fail $ "not a function kind '" ++ showId c "'"
-- | compute arity from a raw kind
kindArity :: RawKind -> Int
kindArity k = case k of
ClassKind _ -> 0
FunKind _ _ rk _ -> 1 + kindArity rk
-- | check if a class occurs in one of its super kinds
cyclicClassId :: ClassMap -> Id -> Kind -> Bool
cyclicClassId cm ci k = case k of
FunKind _ k1 k2 _ -> cyclicClassId cm ci k1 || cyclicClassId cm ci k2
ClassKind cj -> cj /= universeId &&
(cj == ci || not (Set.null $ Set.filter (cyclicClassId cm ci)
$ classKinds $ Map.findWithDefault (error "cyclicClassId") cj cm))
-- * subkinding
-- | keep only minimal elements according to 'lesserKind'
keepMinKinds :: ClassMap -> [Set.Set Kind] -> Set.Set Kind
keepMinKinds cm = Set.fromDistinctAscList
. keepMins (lesserKind cm) . Set.toList . Set.unions
-- | no kind of the set is lesser than the new kind
newKind :: ClassMap -> Kind -> Set.Set Kind -> Bool
newKind cm k = Set.null . Set.filter (flip (lesserKind cm) k)
-- | add a new kind to a set
addNewKind :: ClassMap -> Kind -> Set.Set Kind -> Set.Set Kind
addNewKind cm k = Set.insert k . Set.filter (not . lesserKind cm k)
lesserVariance :: Variance -> Variance -> Bool
lesserVariance v1 v2 = case v1 of
InVar -> True
_ -> case v2 of
NonVar -> True
_ -> v1 == v2
-- | revert variance
revVariance :: Variance -> Variance
revVariance v = case v of
InVar -> NonVar
CoVar -> ContraVar
ContraVar -> CoVar
NonVar -> InVar
-- | compute the minimal variance
minVariance :: Variance -> Variance -> Variance
minVariance v1 v2 = case v1 of
NonVar -> v2
_ -> case v2 of
NonVar -> v1
_ -> if v1 == v2 then v1 else InVar
-- | check subkinding (kinds with variances are greater)
lesserKind :: ClassMap -> Kind -> Kind -> Bool
lesserKind cm k1 k2 = case k1 of
ClassKind c1 -> (case k2 of
ClassKind c2 -> c1 == c2 || (k1 /= universe && k2 == universe)
_ -> False) ||
case Map.lookup c1 cm of
Just info -> not $ newKind cm k2 $ classKinds info
_ -> False
FunKind v1 a1 r1 _ -> case k2 of
FunKind v2 a2 r2 _ -> lesserVariance v1 v2
&& lesserKind cm r1 r2 && lesserKind cm a2 a1
_ -> False
-- | compare raw kinds
lesserRawKind :: RawKind -> RawKind -> Bool
lesserRawKind k1 k2 = case k1 of
ClassKind _ -> case k2 of
ClassKind _ -> True
_ -> False
FunKind v1 a1 r1 _ -> case k2 of
FunKind v2 a2 r2 _ -> lesserVariance v1 v2
&& lesserRawKind r1 r2 && lesserRawKind a2 a1
_ -> False
minRawKind :: Monad m => String -> RawKind -> RawKind -> m RawKind
minRawKind str k1 k2 = let err = fail $ diffKindString str k1 k2 in case k1 of
ClassKind _ -> case k2 of
ClassKind _ -> return $ ClassKind ()
_ -> err
FunKind v1 a1 r1 ps -> case k2 of
FunKind v2 a2 r2 qs -> do
a3 <- minRawKind str a2 a1
r3 <- minRawKind str r1 r2
return $ FunKind (minVariance v1 v2) a3 r3 $ appRange ps qs
_ -> err
rawToKind :: RawKind -> Kind
rawToKind = mapKind (const universeId)
-- * diagnostic messages
-- | create message for different kinds
diffKindString :: String -> RawKind -> RawKind -> String
diffKindString a k1 k2 = "incompatible kind of: " ++ a ++
expected (rawToKind k1) (rawToKind k2)
-- | create diagnostic for different kinds
diffKindDiag :: (GetRange a, Pretty a) =>
a -> RawKind -> RawKind -> [Diagnosis]
diffKindDiag a k1 k2 =
[Diag Error (diffKindString (showDoc a "") k1 k2) $ getRange a]
-- | check if raw kinds are compatible
checkKinds :: (GetRange a, Pretty a) =>
a -> RawKind -> RawKind -> [Diagnosis]
checkKinds p k1 k2 =
maybe (diffKindDiag p k1 k2) (const []) $ minRawKind "" k1 k2
-- | analyse class decls
anaClassDecls :: ClassDecl -> State Env ClassDecl
anaClassDecls (ClassDecl cls k ps) =
do cm <- gets classMap
let Result ds (Just rk) = anaKindM k cm
addDiags ds
let ak = if null ds then k else universe
mapM_ (addClassDecl rk ak) cls
return $ ClassDecl cls ak ps
-- | store a class
addClassDecl :: RawKind -> Kind -> Id -> State Env ()
-- check with merge
addClassDecl rk kind ci =
if ci == universeId then
addDiags [mkDiag Warning "void universe class declaration" ci]
else do
e <- get
let cm = classMap e
tm = typeMap e
tvs = localTypeVars e
case Map.lookup ci tm of
Just _ -> addDiags [mkDiag Error "class name already a type" ci]
Nothing -> case Map.lookup ci tvs of
Just _ -> addDiags
[mkDiag Error "class name already a type variable" ci]
Nothing -> case Map.lookup ci cm of
Nothing -> do
addSymbol $ idToClassSymbol ci rk
putClassMap $ Map.insert ci
(ClassInfo rk $ Set.singleton kind) cm
Just (ClassInfo ork superClasses) ->
let Result ds mk = minRawKind (showDoc ci "") rk ork
in case mk of
Nothing -> addDiags ds
Just nk ->
if cyclicClassId cm ci kind then
addDiags [mkDiag Error "cyclic class" ci]
else do
addSymbol $ idToClassSymbol ci nk
if newKind cm kind superClasses then do
addDiags [mkDiag Warning "refined class" ci]
putClassMap $ Map.insert ci
(ClassInfo nk $ addNewKind cm kind superClasses) cm
else addDiags [mkDiag Warning "unchanged class" ci]