726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiDescription : analyse kinds using a class map

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiMaintainer : Christian.Maeder@dfki.de

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiStability : experimental

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiPortability : portable

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskianalyse kinds using a class map

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski-}

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskimodule HasCASL.ClassAna where

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport HasCASL.As

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowskiimport HasCASL.AsUtils

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport HasCASL.PrintAs ()

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport Common.Id

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport HasCASL.Le

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport qualified Data.Map as Map

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowskiimport qualified Data.Set as Set

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiimport Common.Lib.State

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport Common.Result

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport Common.DocUtils

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport Common.Utils

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski-- * analyse kinds

b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski-- | check the kind and compute the raw kind

80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskianaKindM :: Kind -> ClassMap -> Result RawKind

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskianaKindM k cm = case k of

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski ClassKind ci -> if k == universe then return rStar

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski else case Map.lookup ci cm of

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski Just (ClassInfo rk _) -> return rk

04f798a5a79477754ad20e255444d99757911be0mcodescu Nothing -> Result [mkDiag Error "not a class" ci] $ Just rStar

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski FunKind v k1 k2 ps -> do

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski rk1 <- anaKindM k1 cm

27ae03fc2f67c39292e72f0a69837f34b2521c29mcodescu rk2 <- anaKindM k2 cm

27ae03fc2f67c39292e72f0a69837f34b2521c29mcodescu return $ FunKind v rk1 rk2 ps

09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescu

09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescu-- | get minimal function kinds of (class) kind

09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescugetFunKinds :: Monad m => ClassMap -> Kind -> m (Set.Set Kind)

09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescugetFunKinds cm k = case k of

b0dc688d623e51d3848b4b56d090669f18fc8f17mcodescu FunKind _ _ _ _ -> return $ Set.singleton k

b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu ClassKind c -> case Map.lookup c cm of

27ae03fc2f67c39292e72f0a69837f34b2521c29mcodescu Just info -> do

04f798a5a79477754ad20e255444d99757911be0mcodescu ks <- mapM (getFunKinds cm) $ Set.toList $ classKinds info

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski return $ keepMinKinds cm ks

c0ca1d8524a3ca7f687adf192468541ae68802c9mcodescu _ -> fail $ "not a function kind '" ++ showId c "'"

82a602f211abdebc623f4823b913c8ffea10af06mcodescu

82a602f211abdebc623f4823b913c8ffea10af06mcodescu-- | compute arity from a raw kind

82a602f211abdebc623f4823b913c8ffea10af06mcodescukindArity :: RawKind -> Int

82a602f211abdebc623f4823b913c8ffea10af06mcodescukindArity k =

82a602f211abdebc623f4823b913c8ffea10af06mcodescu case k of

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski ClassKind _ -> 0

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski FunKind _ _ rk _ -> 1 + kindArity rk

156ff56fb6d907911e63df36d12df9220877981amcodescu

156ff56fb6d907911e63df36d12df9220877981amcodescu-- | check if a class occurs in one of its super kinds

80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskicyclicClassId :: ClassMap -> Id -> Kind -> Bool

27de5bf664bde811f402d8e43db0721d3c58362cTill MossakowskicyclicClassId cm ci k =

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski case k of

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski FunKind _ k1 k2 _ ->

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski cyclicClassId cm ci k1 || cyclicClassId cm ci k2

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski ClassKind cj -> if k == universe then False else

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski cj == ci || case Map.lookup cj cm of

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski Nothing -> error "cyclicClassId"

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

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski $ classKinds info

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski

04f798a5a79477754ad20e255444d99757911be0mcodescu-- * subkinding

04f798a5a79477754ad20e255444d99757911be0mcodescu

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

27ae03fc2f67c39292e72f0a69837f34b2521c29mcodescukeepMinKinds :: ClassMap -> [Set.Set Kind] -> Set.Set Kind

80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskikeepMinKinds cm =

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski Set.fromList . keepMins (lesserKind cm) . Set.toList . Set.unions

c0ca1d8524a3ca7f687adf192468541ae68802c9mcodescu

76212ada4c518a69f3125b3531b716c7f5151177mcodescu-- | no kind of the set is lesser than the new kind

04f798a5a79477754ad20e255444d99757911be0mcodescunewKind :: ClassMap -> Kind -> Set.Set Kind -> Bool

80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskinewKind cm k = Set.null . Set.filter (flip (lesserKind cm) k)

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski

b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu-- | add a new kind to a set

04f798a5a79477754ad20e255444d99757911be0mcodescuaddNewKind :: ClassMap -> Kind -> Set.Set Kind -> Set.Set Kind

04f798a5a79477754ad20e255444d99757911be0mcodescuaddNewKind cm k = Set.insert k . Set.filter (not . lesserKind cm k)

04f798a5a79477754ad20e255444d99757911be0mcodescu

09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescu-- | check subkinding (kinds with variances are greater)

09e732ce6115cf6aaedc2622e8e78696bb875b60mcodesculesserKind :: ClassMap -> Kind -> Kind -> Bool

09e732ce6115cf6aaedc2622e8e78696bb875b60mcodesculesserKind cm k1 k2 = case k1 of

09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescu ClassKind c1 -> (case k2 of

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski ClassKind c2 -> c1 == c2 || if k1 == universe then

09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescu False else k2 == universe

04f798a5a79477754ad20e255444d99757911be0mcodescu _ -> False) ||

04f798a5a79477754ad20e255444d99757911be0mcodescu case Map.lookup c1 cm of

04f798a5a79477754ad20e255444d99757911be0mcodescu Just info -> not $ newKind cm k2 $ classKinds info

04f798a5a79477754ad20e255444d99757911be0mcodescu _ -> False

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski FunKind v1 a1 r1 _ -> case k2 of

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski FunKind v2 a2 r2 _ -> (case v2 of

b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu InVar -> True

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

82a602f211abdebc623f4823b913c8ffea10af06mcodescu _ -> False

b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu

27ae03fc2f67c39292e72f0a69837f34b2521c29mcodescurawToKind :: RawKind -> Kind

27ae03fc2f67c39292e72f0a69837f34b2521c29mcodescurawToKind = mapKind (const universeId)

b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu

04f798a5a79477754ad20e255444d99757911be0mcodescu-- * diagnostic messages

09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescu

09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescu-- | create message for different kinds

04f798a5a79477754ad20e255444d99757911be0mcodescudiffKindDiag :: (PosItem a, Pretty a) =>

04f798a5a79477754ad20e255444d99757911be0mcodescu a -> RawKind -> RawKind -> [Diagnosis]

80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskidiffKindDiag a k1 k2 =

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

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

b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu

04f798a5a79477754ad20e255444d99757911be0mcodescu-- | check if raw kinds are equal

35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescucheckKinds :: (PosItem a, Pretty a) =>

35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescu a -> RawKind -> RawKind -> [Diagnosis]

04f798a5a79477754ad20e255444d99757911be0mcodescucheckKinds p k1 k2 =

04f798a5a79477754ad20e255444d99757911be0mcodescu if k1 == k2 then []

35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescu else diffKindDiag p k1 k2

35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescu

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski-- | analyse class decls

35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescuanaClassDecls :: ClassDecl -> State Env ClassDecl

b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescuanaClassDecls (ClassDecl cls k ps) =

35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescu do cm <- gets classMap

b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu let Result ds (Just rk) = anaKindM k cm

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski addDiags ds

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski let ak = if null ds then k else universe

35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescu mapM_ (addClassDecl rk ak) cls

35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescu return $ ClassDecl cls ak ps

04f798a5a79477754ad20e255444d99757911be0mcodescu

b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu-- | store a class

b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescuaddClassDecl :: RawKind -> Kind -> Id -> State Env ()

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski-- check with merge

27de5bf664bde811f402d8e43db0721d3c58362cTill MossakowskiaddClassDecl rk kind ci =

27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski 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