21155e63bac193abc764d791360132392eb79c4dcmaeder{- |

21155e63bac193abc764d791360132392eb79c4dcmaederModule : ./HasCASL/ClassAna.hs

21155e63bac193abc764d791360132392eb79c4dcmaederDescription : analyse kinds using a class map

21155e63bac193abc764d791360132392eb79c4dcmaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

21155e63bac193abc764d791360132392eb79c4dcmaederLicense : GPLv2 or higher, see LICENSE.txt

21155e63bac193abc764d791360132392eb79c4dcmaeder

21155e63bac193abc764d791360132392eb79c4dcmaederMaintainer : Christian.Maeder@dfki.de

21155e63bac193abc764d791360132392eb79c4dcmaederStability : experimental

21155e63bac193abc764d791360132392eb79c4dcmaederPortability : portable

21155e63bac193abc764d791360132392eb79c4dcmaeder

21155e63bac193abc764d791360132392eb79c4dcmaederanalyse kinds using a class map

21155e63bac193abc764d791360132392eb79c4dcmaeder-}

21155e63bac193abc764d791360132392eb79c4dcmaeder

21155e63bac193abc764d791360132392eb79c4dcmaedermodule HasCASL.ClassAna where

21155e63bac193abc764d791360132392eb79c4dcmaeder

21155e63bac193abc764d791360132392eb79c4dcmaederimport HasCASL.As

21155e63bac193abc764d791360132392eb79c4dcmaederimport HasCASL.AsUtils

21155e63bac193abc764d791360132392eb79c4dcmaederimport HasCASL.PrintAs ()

21155e63bac193abc764d791360132392eb79c4dcmaederimport Common.Id

21155e63bac193abc764d791360132392eb79c4dcmaederimport HasCASL.Le

21155e63bac193abc764d791360132392eb79c4dcmaederimport qualified Data.Map as Map

21155e63bac193abc764d791360132392eb79c4dcmaederimport qualified Data.Set as Set

21155e63bac193abc764d791360132392eb79c4dcmaederimport Common.Lib.State

21155e63bac193abc764d791360132392eb79c4dcmaederimport Common.Result

55282ad62e8b6758abec43734ebde0015ac14b89Eugen Kuksaimport Common.DocUtils

21155e63bac193abc764d791360132392eb79c4dcmaederimport Common.Utils

21155e63bac193abc764d791360132392eb79c4dcmaeder

21155e63bac193abc764d791360132392eb79c4dcmaeder-- * analyse kinds

21155e63bac193abc764d791360132392eb79c4dcmaeder

21155e63bac193abc764d791360132392eb79c4dcmaeder-- | check the kind and compute the raw kind

21155e63bac193abc764d791360132392eb79c4dcmaederanaKindM :: Kind -> ClassMap -> Result RawKind

21155e63bac193abc764d791360132392eb79c4dcmaederanaKindM k cm = case k of

21155e63bac193abc764d791360132392eb79c4dcmaeder 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]