TypeAna.hs revision c00adad2e9459b422dee09e3a2bddba66b433bb7
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync{- HetCATS/HasCASL/TypeAna.hs
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync $Id$
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync Authors: Christian Maeder
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync Year: 2003
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync analyse types
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync-}
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncmodule TypeAna where
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncimport As
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncimport AsUtils
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncimport GlobalAnnotationsFunctions(emptyGlobalAnnos)
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncimport Id
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncimport Le
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncimport MonadState
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncimport Pretty
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncimport PrettyPrint
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncimport PrintAs
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncimport FiniteMap
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncimport Result
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncimport Set
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynccheckTypeKind :: Id -> Kind -> Type -> State Env (Result Type)
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynccheckTypeKind i k t =
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync do tk <- getTypeKinds
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync case lookupFM tk i of
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync Nothing -> return $ plain_error t
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync ("unknown type '" ++ showId i "'")
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync (posOfId i)
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync Just k2 -> if eqKind k2 k
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync then return $ return t
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync else return $ plain_error t
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync ("incompatible type kinds\n" ++
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync indent 2 (showPretty k .
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync showChar '\n' .
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync showPretty k2) "")
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync (posOfKind k)
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncanaType :: Type -> State Env (Result Type)
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncanaType (t@(TypeConstrAppl i k ts _)) =
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync if length ts > kindArity k then
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync return $ plain_error t
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync ("too many type arguments:\n" ++
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync indent 2 (showPretty t) "")
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync (posOfType t)
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync else checkTypeKind i k t
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncanaType (t@(TypeVar i k v _)) =
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync if v > 0 then return $ plain_error t
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync ("unexpected generic variable '" ++ showId i "i")
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync (posOfId i)
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync else checkTypeKind i k t
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncanaType (TypeToken t) =
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync let i = simpleIdToId t in
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync do tk <- getTypeKinds
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync case lookupFM tk i of
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync Nothing -> return $ plain_error (TypeToken t)
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync ("unidentified type token '" ++ tokStr t)
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync (tokPos t)
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync Just k -> do ts <- getTypeVars
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync return $ return $ if i `elementOf` ts
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync then TypeVar i k 0 []
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync else TypeConstrAppl i k [] []
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncanaType (BracketType Parens ts ps) =
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync do Result ds (Just newTs) <- anaList anaType ts
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync return $ Result ds $ Just $ ProductType newTs ps
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync-- --------------------------------------------------------------------------
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncshowPretty :: PrettyPrint a => a -> ShowS
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncshowPretty = showString . render . printText0 emptyGlobalAnnos
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncposOfKind :: Kind -> Pos
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncposOfKind (Kind l c ps) =
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync if null l then posOfClass c
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync else if null ps then posOfProdClass $ head l
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync else head ps
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncposOfProdClass :: ProdClass -> Pos
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncposOfProdClass (ProdClass s ps) =
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync if null s then if null ps then nullPos else head ps
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync else posOfExtClass $ head s
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncposOfExtClass :: ExtClass -> Pos
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncposOfExtClass (ExtClass c _ _) = posOfClass c
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncposOfExtClass (KindAppl k _) = posOfKind k
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncposOfClass :: Class -> Pos
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncposOfClass (Downset t) = posOfType t
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsyncposOfClass (Intersection is ps) =
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync if null ps then if null is then nullPos else tokPos $ head is
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync else head ps
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqKind :: Kind -> Kind -> Bool
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqKind (Kind p1 c1 _) (Kind p2 c2 _) =
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync eqListBy eqProdClass p1 p2 && eqClass c1 c2
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqListBy :: (a -> a -> Bool) -> [a] -> [a] -> Bool
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqListBy _ [] [] = True
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqListBy f (h1:t1) (h2:t2) = f h1 h2 && eqListBy f t1 t2
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqListBy _ _ _ = False
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqProdClass :: ProdClass -> ProdClass -> Bool
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqProdClass (ProdClass s1 _) (ProdClass s2 _) =
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync eqListBy eqExtClass s1 s2
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqExtClass :: ExtClass -> ExtClass -> Bool
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqExtClass (ExtClass c1 v1 _) (ExtClass c2 v2 _) =
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync eqClass c1 c2 && v1 == v2
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqExtClass (KindAppl f1 a1) (KindAppl f2 a2) =
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync eqKind f1 f2 && eqKind a1 a2
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqExtClass _ _ = False
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqClass :: Class -> Class -> Bool
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqClass(Intersection i1 _) (Intersection i2 _) =
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync i1 == i2
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqClass (Downset t1) (Downset t2) = eqType t1 t2
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqClass _ _ = False
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqType :: Type -> Type -> Bool
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsynceqType = error "eqType nyi"
38ae7e4efe803ea78b6499cd05a394db32623e41vboxsync