e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski

0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowski{- HetCATS/HasCASL/ClassAna.hs

0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowski $Id$

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski Authors: Christian Maeder

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski Year: 2003

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski analyse given classes

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski-}

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskimodule HasCASL.ClassAna where

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport HasCASL.As

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport HasCASL.AsUtils()

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Common.Id

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport HasCASL.Le

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Data.List

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Data.Maybe

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport HasCASL.PrintAs()

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Common.PrettyPrint

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport qualified Common.Lib.Map as Map

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport qualified Common.Lib.Set as Set

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Common.Result

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport HasCASL.Reader

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski-- ---------------------------------------------------------------------------

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski-- analyse class

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski-- ---------------------------------------------------------------------------

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski-- transitiv super classes

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski-- PRE: all superclasses and defns must be defined in ClassEnv

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski-- and there must be no cycle!

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till MossakowskiallSuperClasses :: ClassMap -> ClassId -> Set.Set ClassId

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskiallSuperClasses ce ci =

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski let recurse = Set.unions . map (allSuperClasses ce) in

da955132262baab309a50fdffe228c9efe68251dCui Jian case Map.lookup ci ce of

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski Just info -> (case classDefn info of

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski Just (Intersection cis _) -> recurse $ Set.toList cis

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski _ -> Set.single ci)

7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski `Set.union` recurse (Set.toList $ superClasses info)

7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski Nothing -> error "allSuperClasses"

7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski

7474388b4c2236f8ab2327289555000268c7901aTill MossakowskianaClassId :: ClassMap -> ClassId -> Maybe Kind

7474388b4c2236f8ab2327289555000268c7901aTill MossakowskianaClassId cMap ci =

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski case Map.lookup ci cMap of

da955132262baab309a50fdffe228c9efe68251dCui Jian Nothing -> Nothing

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski Just i -> Just $ classKind i

8d6aa4bda97770cc79cf96de3c0f9dfa4d7d7aafChristian Maeder

99249aeda5fac6f8f0b2316ca357bac898af1928Christian MaederexpandKind :: ClassMap -> Kind -> Kind

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till MossakowskiexpandKind cMap (ExtClass c _ _) =

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski case c of

4918e2f622cfb96f9a57b7617cd18ca7e4f8b5d4Christian Maeder Intersection s _ ->

if Set.isEmpty s then star else

case anaClassId cMap $ Set.findMin s of

Just k -> expandKind cMap k

_ -> error "expandKind"

_ -> star

expandKind cMap (KindAppl k1 k2 ps) =

KindAppl (expandKind cMap k1) (expandKind cMap k2) ps

anaClass :: Class -> ReadR ClassMap (Kind, Class)

anaClass (Intersection s ps) =

do cMap <- ask

let cs = Set.toList s

l = zip (map (anaClassId cMap) cs) cs

(js, ns) = partition (isJust . fst) l

ds = map (mkDiag Error "undeclared class" . snd) ns

restCs = Set.fromList $ map snd js

ks = map (fromJust. fst) js

k = if null ks then star else expandKind cMap $

fromJust $ fst $ head js

es = filter (not . eqKind k . expandKind cMap .

fromJust . fst) js

fs = map (\ (Just wk, i) -> mkDiag Error

("wrong kind '" ++ showPretty wk "' of")

i) es

lift $ Result (ds ++ fs) $ Just (k, Intersection restCs ps)

anaClass (Downset t) =

lift $ Result [downsetWarning t] $ Just (star, Downset t)

downsetWarning :: Type -> Diagnosis

downsetWarning t = mkDiag Warning "unchecked type" t

-- ----------------------------------------------------------------------------

-- analyse kind

-- ----------------------------------------------------------------------------

anaKind :: Kind -> ReadR ClassMap Kind

anaKind (KindAppl k1 k2 p) =

do k1e <- anaKind k1

k2e <- anaKind k2

return $ KindAppl k1e k2e p

anaKind (ExtClass k v p) =

do (_, c) <- anaClass k

return $ ExtClass c v p

-- ---------------------------------------------------------------------

-- comparing kinds

-- ---------------------------------------------------------------------

checkKinds :: ClassMap -> Pos -> Kind -> Kind -> [Diagnosis]

checkKinds cMap p k1 k2 =

eqKindDiag p (expandKind cMap k1)

$ expandKind cMap k2

eqKindDiag :: Pos -> Kind -> Kind -> [Diagnosis]

eqKindDiag p k1 k2 =

if eqKind k1 k2 then []

else [ Diag Error

("incompatible kinds\n" ++

indent 2 (showPretty k1 .

showChar '\n' .

showPretty k2) "")

$ p ]

eqKind :: Kind -> Kind -> Bool

eqKind (KindAppl p1 c1 _) (KindAppl p2 c2 _) =

eqKind p1 p2 && eqKind c1 c2

eqKind (ExtClass _ _ _) (ExtClass _ _ _) = True

eqKind _ _ = False

-- ---------------------------------------------------------------------