TypeAna.hs revision 7c57322afb6342e5cc8b1fdc96050b707407fc61
{- HetCATS/HasCASL/TypeAna.hs
$Id$
Authors: Christian Maeder
Year: 2003
analyse given classes and types
-}
module TypeAna where
import As
import AsUtils
import GlobalAnnotationsFunctions(emptyGlobalAnnos)
import Id
import Le
import List(nub, sort)
import Maybe
import MonadState
import Pretty
import PrettyPrint
import PrintAs()
import FiniteMap
import Result
-- ---------------------------------------------------------------------------
-- analyse class
-- ---------------------------------------------------------------------------
resolveClassSyns :: ClassSyns -> ClassId -> [ClassId]
resolveClassSyns cSyns ci =
case lookupFM cSyns ci of
Nothing -> [ci]
Just cs -> sort $ nub $ concatMap (resolveClassSyns cSyns) cs
anaClassId :: ClassMap -> ClassId -> [Diagnosis]
-- True: declare the class
anaClassId cMap ci =
if isJust $ lookupFM cMap ci then []
else [Diag Error
("undeclared class '" ++ showId ci "'")
$ posOfId ci]
anaClass :: Class -> State Env Class
anaClass (Intersection cs ps) =
do cMap <- getClassMap
let l = zip (map (anaClassId cMap) cs) cs
restCs = map snd $ filter (\ (x, _) -> null x) l
ds = concatMap fst l
in do appendDiags ds
return $ Intersection restCs ps
anaClass (Downset t) =
do newT <- anaType t
return $ Downset newT
-- ----------------------------------------------------------------------------
-- analyse kind
-- ----------------------------------------------------------------------------
anaKind :: Kind -> State Env Kind
anaKind (Kind args c p) =
do ca <- anaClass c
newArgs <- mapM anaProdClass args
return $ Kind newArgs ca p
anaExtClass :: ExtClass -> State Env ExtClass
anaExtClass (ExtClass c v p) =
do ca <- anaClass c
return $ ExtClass ca v p
anaExtClass (KindArg k) =
do n <- anaKind k
return $ KindArg n
anaProdClass :: ProdClass -> State Env ProdClass
anaProdClass (ProdClass l p) =
do cs <- mapM anaExtClass l
return $ ProdClass cs p
-- ---------------------------------------------------------------------------
-- analyse type
-- ---------------------------------------------------------------------------
checkTypeKind :: Id -> Kind -> State Env [Diagnosis]
checkTypeKind i k =
do tk <- getTypeKinds
case lookupFM tk i of
Nothing -> return [Diag Error
("unknown type '" ++ showId i "'")
(posOfId i)]
Just ks -> if eqKind k $ head ks
then return []
else return [Diag Error
("incompatible type kinds\n" ++
indent 2 (showPretty k .
showChar '\n' .
showPretty (head ks)) "")
$ posOfKind k ]
anaTypeId :: Id -> State Env Type
anaTypeId i =
do tk <- getTypeKinds
case lookupFM tk i of
Nothing -> do
appendDiags [Diag Error
("unidentified type '" ++ showId i "'")
(posOfId i)]
return (TypeConstrAppl i 0 nullKind [] [])
Just ks -> return $ TypeConstrAppl i 0 (head ks) [] []
anaType :: Type -> State Env Type
anaType (t@(TypeConstrAppl i v k ts _)) =
let e1 = if length ts > kindArity k then
[Diag Error ("too many type arguments:\n" ++
indent 2 (showPretty t) "")
(posOfType t)] else []
e2 = if v > 0 then
[Diag Error
("too many type arguments:\n" ++
indent 2 (showPretty t) "")
(posOfType t)] else []
in do ds <- checkTypeKind i k
appendDiags $ e1 ++ e2 ++ ds
return t
anaType (TypeToken t) =
anaTypeId $ simpleIdToId t
anaType (BracketType Parens ts ps) =
do newTs <- mapM anaType ts
return $ ProductType newTs ps
anaType (BracketType b ts ps) =
let toks@[o,c] = mkBracketToken b ps
i = if null ts then Id toks [] []
else Id [o, Token place $ posOfType $ head ts, c] [] []
in
do newT <- anaTypeId i
if null ts then return newT
else do args <- mapM anaType ts
case newT of
TypeConstrAppl _ _ k _ _ ->
do if kindArity k < length args then
appendDiags [Diag Error
("too many arguments for '"
++ showId i "'")
$ posOfId i]
else return ()
return $ TypeConstrAppl i 0 k args []
_ -> return $ TypeConstrAppl i 0
(Kind
[ProdClass
(replicate (length args) extUniverse)
[] ] universe []) args []
anaType(KindedType t k ps) =
do newK <- anaKind k
newT <- anaType t
-- getKind of t and compare it with k
return $ KindedType newT newK ps
anaType (MixfixType ts) =
do (f:as) <- mapM anaType ts
return $ case f of
TypeConstrAppl i g k bs _ ->
TypeConstrAppl i g k (bs ++ as) []
_ -> MixfixType (f:as)
anaType (LazyType t p) =
do newT <- anaType t
return $ LazyType newT p
anaType (ProductType ts ps) =
do newTs <- mapM anaType ts
return $ ProductType newTs ps
anaType (FunType t1 a t2 ps) =
do newT1 <- anaType t1
newT2 <- anaType t2
return $ FunType newT1 a newT2 ps
mkBracketToken :: BracketKind -> [Pos] -> [Token]
mkBracketToken k ps =
if null ps then error "mkBracketToken"
else zipWith Token (getBrackets k) [head ps, last ps]
getBrackets :: BracketKind -> [String]
getBrackets k =
case k of Parens -> ["(", ")"]
Squares -> ["[", "]"]
Braces -> ["{", "}"]
-- --------------------------------------------------------------------------
showPretty :: PrettyPrint a => a -> ShowS
showPretty = showString . render . printText0 emptyGlobalAnnos
posOfKind :: Kind -> Pos
posOfKind (Kind l c ps) =
if null l then posOfClass c
else if null ps then posOfProdClass $ head l
else head ps
posOfProdClass :: ProdClass -> Pos
posOfProdClass (ProdClass s ps) =
if null s then if null ps then nullPos else head ps
else posOfExtClass $ head s
posOfExtClass :: ExtClass -> Pos
posOfExtClass (ExtClass c _ _) = posOfClass c
posOfExtClass (KindArg k) = posOfKind k
posOfClass :: Class -> Pos
posOfClass (Downset t) = posOfType t
posOfClass (Intersection is ps) =
if null ps then if null is then nullPos else posOfId $ head is
else head ps
eqKind :: Kind -> Kind -> Bool
eqKind (Kind p1 c1 _) (Kind p2 c2 _) =
eqListBy eqProdClass p1 p2 && eqClass c1 c2
eqListBy :: (a -> a -> Bool) -> [a] -> [a] -> Bool
eqListBy _ [] [] = True
eqListBy f (h1:t1) (h2:t2) = f h1 h2 && eqListBy f t1 t2
eqListBy _ _ _ = False
eqProdClass :: ProdClass -> ProdClass -> Bool
eqProdClass (ProdClass s1 _) (ProdClass s2 _) =
eqListBy eqExtClass s1 s2
eqExtClass :: ExtClass -> ExtClass -> Bool
eqExtClass (ExtClass c1 v1 _) (ExtClass c2 v2 _) =
eqClass c1 c2 && v1 == v2
eqExtClass (KindArg k1) (KindArg k2) = eqKind k1 k2
eqExtClass _ _ = False
eqClass :: Class -> Class -> Bool
eqClass(Intersection i1 _) (Intersection i2 _) = i1 == i2
eqClass (Downset t1) (Downset t2) = eqType t1 t2
eqClass _ _ = False
eqType :: Type -> Type -> Bool
eqType = error "eqType nyi"