TypeAna.hs revision f0742398d4587242b1a115de113cd17f63dcb6d0
c58a94c44b76b072ace930f2126c889c0b64cb2aChristian Maeder Authors: Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder analyse given classes and types
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maedermodule TypeAna where
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maederimport AsUtils
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport GlobalAnnotationsFunctions(emptyGlobalAnnos)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport MonadState
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport PrettyPrint
dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian Maederimport PrintAs()
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport FiniteMap
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-- ---------------------------------------------------------------------------
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- analyse class
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder-- ---------------------------------------------------------------------------
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- transitiv super classes
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- PRE: all superclasses and defns must be defined in ClassEnv
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- and there must be no cycle!
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederallSuperClasses :: ClassMap -> ClassId -> [ClassId]
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian MaederallSuperClasses ce ci =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder let recurse = nub . concatMap (allSuperClasses ce) in
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder case lookupFM ce ci of
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder Just info -> nub $ ci:
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder (case classDefn info of
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder Nothing -> []
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Just (Intersection cis _) -> recurse cis
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Just _ -> [])
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder ++ recurse (superClasses info)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Nothing -> error "allSuperClasses"
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederresolveClassSyn :: ClassMap -> ClassId -> [ClassId]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederresolveClassSyn cMap ci =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder case lookupFM cMap ci of
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder Nothing -> error "resolveClassSyn"
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder Just info -> case classDefn info of
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Nothing -> [ci]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Just (Intersection cis _) -> resolveClassSyns cMap cis
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederresolveClassSyns :: ClassMap -> [ClassId] -> [ClassId]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederresolveClassSyns cSyns cis = nub $
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder concatMap (resolveClassSyn cSyns) cis
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederanaClassId :: ClassMap -> ClassId -> [Diagnosis]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- True: declare the class
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederanaClassId cMap ci =
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder if isJust $ lookupFM cMap ci then []
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder else [Diag Error
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ("undeclared class '" ++ showId ci "'")
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder $ posOfId ci]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederanaClass :: Class -> State Env Class
27912d626bf179b82fcb337077e5cd9653bb71cfChristian MaederanaClass (Intersection cs ps) =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder do cMap <- getClassMap
cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder let l = zip (map (anaClassId cMap) cs) cs
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder restCs = map snd $ filter (\ (x, _) -> null x) l
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ds = concatMap fst l
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder appendDiags ds
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder return $ Intersection restCs ps
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederanaClass (Downset t) =
5ba323da9f037264b4a356085e844889aedeac23Christian Maeder do newT <- anaType t
5ba323da9f037264b4a356085e844889aedeac23Christian Maeder return $ Downset newT
5ba323da9f037264b4a356085e844889aedeac23Christian Maeder-- ----------------------------------------------------------------------------
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- analyse kind
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- ----------------------------------------------------------------------------
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederanaKind :: Kind -> State Env Kind
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederanaKind (Kind args c p) =
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder do ca <- anaClass c
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder newArgs <- mapM anaProdClass args
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder return $ Kind newArgs ca p
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederanaExtClass :: ExtClass -> State Env ExtClass
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederanaExtClass (ExtClass c v p) =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder do ca <- anaClass c
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return $ ExtClass ca v p
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederanaExtClass (KindArg k) =
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder do n <- anaKind k
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return $ KindArg n
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederanaProdClass :: ProdClass -> State Env ProdClass
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederanaProdClass (ProdClass l p) =
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder do cs <- mapM anaExtClass l
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return $ ProdClass cs p
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- ---------------------------------------------------------------------------
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- analyse type
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- ---------------------------------------------------------------------------
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedercheckTypeKind :: Id -> Kind -> State Env [Diagnosis]
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedercheckTypeKind i k =
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder do tk <- getTypeKinds
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder case lookupFM tk i of
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder Nothing -> return [Diag Error
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ("unknown type '" ++ showId i "'")
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Just ks -> if eqKind k $ head ks
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder then return []
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder else return [Diag Error
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ("incompatible type kinds\n" ++
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder indent 2 (showPretty k .
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder showChar '\n' .
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder showPretty (head ks)) "")
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder $ posOfKind k ]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederindent :: Int -> ShowS -> ShowS
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maederindent i s = showString $ concat $
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder intersperse ('\n' : replicate i ' ') (lines $ s "")
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian MaederanaTypeId :: Id -> State Env Type
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder do tk <- getTypeKinds
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder case lookupFM tk i of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Nothing -> do
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder appendDiags [Diag Error
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ("unidentified type '" ++ showId i "'")
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder return (TypeConstrAppl i 0 nullKind [] [])
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder Just ks -> return $ TypeConstrAppl i 0 (head ks) [] []
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederanaType :: Type -> State Env Type
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederanaType (t@(TypeConstrAppl i v k ts _)) = do
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder let e1 = if length ts > kindArity k then
5ba323da9f037264b4a356085e844889aedeac23Christian Maeder [Diag Error ("too many type arguments:\n" ++
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder indent 2 (showPretty t) "")
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder (posOfType t)] else []
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder e2 = if v > 0 then
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ("too many type arguments:\n" ++
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder indent 2 (showPretty t) "")
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (posOfType t)] else []
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ds <- checkTypeKind i k
5ba323da9f037264b4a356085e844889aedeac23Christian Maeder appendDiags $ e1 ++ e2 ++ ds
5ba323da9f037264b4a356085e844889aedeac23Christian MaederanaType (TypeToken t) =
5ba323da9f037264b4a356085e844889aedeac23Christian Maeder anaTypeId $ simpleIdToId t
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederanaType (BracketType Parens ts ps) =
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder do newTs <- mapM anaType ts
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder return $ ProductType newTs ps
c9892acbf03a509d874ac6d79b9a2cb09042e0dcChristian MaederanaType (BracketType b ts ps) = do
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder let toks@[o,c] = mkBracketToken b ps
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder i = if null ts then Id toks [] []
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder else Id [o, Token place $ posOfType $ head ts, c] [] []
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder newT <- anaTypeId i
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder if null ts then return newT
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder else do args <- mapM anaType ts
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder TypeConstrAppl _ _ k _ _ ->
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder do if kindArity k < length args then
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder appendDiags [Diag Error
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ("too many arguments for '"
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ++ showId i "'")
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder else return ()
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return $ TypeConstrAppl i 0 k args []
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder _ -> return $ TypeConstrAppl i 0
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder (replicate (length args) extUniverse)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder [] ] universe []) args []
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederanaType(KindedType t k ps) =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder do newK <- anaKind k
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder newT <- anaType t
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder -- getKind of t and compare it with k
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder return $ KindedType newT newK ps
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederanaType (MixfixType ts) =
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder do (f:as) <- mapM anaType ts
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder return $ case f of
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder TypeConstrAppl i g k bs _ ->
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder TypeConstrAppl i g k (bs ++ as) []
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder _ -> MixfixType (f:as)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederanaType (LazyType t p) =
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder do newT <- anaType t
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder return $ LazyType newT p
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederanaType (ProductType ts ps) =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder do newTs <- mapM anaType ts
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder return $ ProductType newTs ps
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederanaType (FunType t1 a t2 ps) =
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder do newT1 <- anaType t1
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder newT2 <- anaType t2
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder return $ FunType newT1 a newT2 ps
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedermkBracketToken :: BracketKind -> [Pos] -> [Token]
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedermkBracketToken k ps =
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder if null ps then error "mkBracketToken"
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder else zipWith Token (getBrackets k) [head ps, last ps]
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaedergetBrackets :: BracketKind -> [String]
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedergetBrackets k =
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder case k of Parens -> ["(", ")"]
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder Squares -> ["[", "]"]
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Braces -> ["{", "}"]
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- --------------------------------------------------------------------------
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedershowPretty :: PrettyPrint a => a -> ShowS
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedershowPretty = showString . render . printText0 emptyGlobalAnnos
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederposOfKind :: Kind -> Pos
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederposOfKind (Kind l c ps) =
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder if null l then posOfClass c
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder else if null ps then posOfProdClass $ head l
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederposOfProdClass :: ProdClass -> Pos
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederposOfProdClass (ProdClass s ps) =
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder if null s then if null ps then nullPos else head ps
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder else posOfExtClass $ head s
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaederposOfExtClass :: ExtClass -> Pos
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederposOfExtClass (ExtClass c _ _) = posOfClass c
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaederposOfExtClass (KindArg k) = posOfKind k
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederposOfClass :: Class -> Pos
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederposOfClass (Downset t) = posOfType t
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederposOfClass (Intersection is ps) =
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder if null ps then if null is then nullPos else posOfId $ head is
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaedereqKind :: Kind -> Kind -> Bool
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedereqKind (Kind p1 c1 _) (Kind p2 c2 _) =
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder eqListBy eqProdClass p1 p2 && eqClass c1 c2
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedereqListBy :: (a -> a -> Bool) -> [a] -> [a] -> Bool
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedereqListBy _ [] [] = True
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedereqListBy f (h1:t1) (h2:t2) = f h1 h2 && eqListBy f t1 t2
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedereqListBy _ _ _ = False
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedereqProdClass :: ProdClass -> ProdClass -> Bool
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedereqProdClass (ProdClass s1 _) (ProdClass s2 _) =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder eqListBy eqExtClass s1 s2
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedereqExtClass :: ExtClass -> ExtClass -> Bool
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedereqExtClass (ExtClass c1 v1 _) (ExtClass c2 v2 _) =
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder eqClass c1 c2 && v1 == v2
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedereqExtClass (KindArg k1) (KindArg k2) = eqKind k1 k2
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedereqExtClass _ _ = False
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedereqClass :: Class -> Class -> Bool
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedereqClass(Intersection i1 _) (Intersection i2 _) = i1 == i2
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedereqClass (Downset t1) (Downset t2) = eqType t1 t2
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedereqClass _ _ = False
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaedereqType :: Type -> Type -> Bool
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedereqType = error "eqType nyi"