{- |

Module : $Header$

Description : analyse kinds using a class map

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

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.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 -> if k == universe then False else

cj == ci || case Map.lookup cj cm of

Nothing -> error "cyclicClassId"

Just info -> not $ Set.null $ Set.filter (cyclicClassId cm ci)

$ classKinds info

-- * subkinding

-- | keep only minimal elements according to 'lesserKind'

keepMinKinds :: ClassMap -> [Set.Set Kind] -> Set.Set Kind

keepMinKinds cm =

Set.fromList . 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)

-- | 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 || if k1 == universe then

False else 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 _ -> (case v2 of

InVar -> True

_ -> v1 == v2) && lesserKind cm r1 r2 && lesserKind cm a2 a1

_ -> False

rawToKind :: RawKind -> Kind

rawToKind = mapKind (const universeId)

-- * diagnostic messages

-- | create message for different kinds

diffKindDiag :: (PosItem a, Pretty a) =>

a -> RawKind -> RawKind -> [Diagnosis]

diffKindDiag a k1 k2 =

[ Diag Error ("incompatible kind of: " ++ showDoc a "" ++

expected (rawToKind k1) (rawToKind k2)) $ getRange a ]

-- | check if raw kinds are equal

checkKinds :: (PosItem a, Pretty a) =>

a -> RawKind -> RawKind -> [Diagnosis]

checkKinds p k1 k2 =

if k1 == k2 then []

else diffKindDiag p 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

cm <- gets classMap

tm <- gets typeMap

tvs <- gets localTypeVars

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 -> putClassMap $ Map.insert ci

(ClassInfo rk $ Set.singleton kind) cm

Just (ClassInfo ork superClasses) ->

let ds = checkKinds ci rk ork in

if null ds then

if cyclicClassId cm ci kind then

addDiags [mkDiag Error "cyclic class" ci]

else if newKind cm kind superClasses then do

addDiags [mkDiag Hint "refined class" ci]

putClassMap $ Map.insert ci

(ClassInfo ork $ addNewKind cm kind superClasses) cm

else addDiags [mkDiag Warning "unchanged class" ci]

else addDiags ds