TypeAna.hs revision 8197d0be8b81692f311ad5ca34e125e2cf9eecb8
2b873214c9ab511bbca437c036371ab664aedaceChristian Maeder{- |
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederModule : $Header$
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederLicence : All rights reserved.
54ed6a6b1a6c7d27fadb39ec5b59d0806c81f7c8Christian Maeder
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiMaintainer : hets@tzi.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : experimental
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiPortability : portable
75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder analyse types
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder-}
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maedermodule HasCASL.TypeAna where
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder
da955132262baab309a50fdffe228c9efe68251dCui Jianimport HasCASL.As
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederimport HasCASL.AsUtils
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederimport HasCASL.ClassAna
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport HasCASL.Le
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport HasCASL.Unify
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maederimport Data.List
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maederimport Data.Maybe
52d922076b89f12234f721974e82531bc69a6f69Christian Maederimport qualified Common.Lib.Map as Map
52d922076b89f12234f721974e82531bc69a6f69Christian Maederimport qualified Common.Lib.Set as Set
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maederimport Common.Id
4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maederimport Common.Result
91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maederimport Common.Lib.State
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederdata ApplMode = OnlyArg | TopLevel
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder
31bc219bae758272d0f064281b8ce7740a4553e9Till MossakowskimkTypeConstrAppls :: ApplMode -> Type -> State Env (Maybe Type)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskimkTypeConstrAppls _ t@(TypeName _ _ _) =
f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder return $ Just t
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder
9175e29c044318498a40f323f189f9dfd50378efChristian MaedermkTypeConstrAppls m (TypeAppl t1 t2) =
f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder do mt3 <- mkTypeConstrAppls m t1
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder mt4 <- mkTypeConstrAppls OnlyArg t2
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder case (mt3, mt4) of
da333ffa6336cf59a4071fcddad358c5eafd3e61Sonja Gröning (Just t3, Just t4) -> return $ Just $ TypeAppl t3 t4
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder _ -> return Nothing
6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus GrossmkTypeConstrAppls _ (TypeToken t) =
fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder do let i = simpleIdToId t
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder tk <- gets typeMap
0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von Schroeder let m = getKind tk i
fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder c = if isTypeVar tk i then 1 else 0
66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu case m of
834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross Just k -> return $ Just $ TypeName i k c
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder _ -> do addDiags [mkDiag Error "unknown type" t]
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder return Nothing
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder
6e52f1dfc0da4bc4a7701cf856641c9dce08fc7dChristian MaedermkTypeConstrAppls m t@(BracketType b ts ps) =
923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl do mArgs <- mapM (mkTypeConstrAppls m) ts
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova if all isJust mArgs then
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz do let err = do addDiags [mkDiag Error "illegal type" t]
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder return Nothing
14c89b2d830777bf4db2850f038c9f60acaca486Christian Maeder case catMaybes mArgs of
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder [x] -> case b of
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder Parens -> return $ Just x
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder _ -> do let [o,c] = mkBracketToken b ps
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder i = Id [o, Token place $ posOfType
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder $ head ts, c] [] []
923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl tk <- gets typeMap
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder case getKind tk i of
2b873214c9ab511bbca437c036371ab664aedaceChristian Maeder Nothing -> err
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder Just k -> return $ Just $ TypeAppl
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa (TypeName i k 0) x
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder _ -> err
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder else return Nothing
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder
52d922076b89f12234f721974e82531bc69a6f69Christian MaedermkTypeConstrAppls _ (MixfixType []) = error "mkTypeConstrAppl (MixfixType [])"
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus GrossmkTypeConstrAppls _ (MixfixType (f:a)) =
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross do mF <- mkTypeConstrAppls TopLevel f
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder case mF of
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski Nothing -> return Nothing
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski Just newF ->
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski do mA <- mapM (mkTypeConstrAppls OnlyArg) a
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski if all isJust mA then
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder return $ Just $ foldl1 TypeAppl $ newF : catMaybes mA
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder else return Nothing
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder
a31430de8b0632d29f42634d6395e982bf31b14dChristian MaedermkTypeConstrAppls m (KindedType t k p) =
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder do mT <- mkTypeConstrAppls m t
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder return $ fmap ( \ newT -> KindedType newT k p ) mT
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder
a31430de8b0632d29f42634d6395e982bf31b14dChristian MaedermkTypeConstrAppls _ (LazyType t p) =
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder do mT <- mkTypeConstrAppls TopLevel t
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder return $ fmap ( \ newT -> LazyType newT p ) mT
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder
a31430de8b0632d29f42634d6395e982bf31b14dChristian MaedermkTypeConstrAppls _ (ProductType ts ps) =
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder do mTs <- mapM (mkTypeConstrAppls TopLevel) ts
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder if all isJust mTs then
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder return $ Just $ ProductType (catMaybes mTs) ps
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder else return Nothing
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder
9175e29c044318498a40f323f189f9dfd50378efChristian MaedermkTypeConstrAppls _ (FunType t1 a t2 ps) =
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühl do mT1 <- mkTypeConstrAppls TopLevel t1
f63e7684d8db7503c22e5d8d499c94a9405f8f9eChristian Maeder mT2 <- mkTypeConstrAppls TopLevel t2
91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder case (mT1, mT2) of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (Just newT1, Just newT2) ->
f63e7684d8db7503c22e5d8d499c94a9405f8f9eChristian Maeder return $ Just $ FunType newT1 a newT2 ps
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder _ -> return Nothing
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder
bdc103981a28a51938de98a956d8a3767f6cf43dAivaras JakubauskasexpandApplKind :: Class -> State Env Kind
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederexpandApplKind c =
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder case c of
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder Intersection s _ -> if Set.isEmpty s then return star else
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder do mk <- anaClassId $ Set.findMin s
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder case mk of
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder Just k -> case k of
7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von Schroeder ExtClass c2 _ _ -> expandApplKind c2
fa388aea9cef5f9734fec346159899a74432ce26Christian Maeder _ -> return k
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Nothing -> error "expandApplKind"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder _ -> return star
0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von Schroeder
52d922076b89f12234f721974e82531bc69a6f69Christian MaederinferKind :: Type -> State Env Kind
52d922076b89f12234f721974e82531bc69a6f69Christian MaederinferKind (TypeName i _ _) = do j <- getIdKind i
923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl return j
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina SojakovainferKind (TypeAppl t1 t2) =
72079df98b3cb7cc1fd82a0a24984893dcd05ecaEwaryst Schulz do mk1 <- inferKind t1
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case mk1 of
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder KindAppl k1 k2 _ -> do checkTypeKind t2 k1
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder return k2
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder ExtClass c _ _ ->
1c4dfa148603d4fcf4cdd2ed66c8b6e1de0dd696Till Mossakowski do k <- expandApplKind c
bb63f684c4f5f33ffcd1dcc02c58d6a703900fafJonathan von Schroeder case k of
b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder KindAppl k1 k2 _ -> do checkTypeKind t2 k1
b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder return k2
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross _ -> do addDiags
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross [mkDiag Error
d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer "incompatible kind of type"
d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer t1]
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder return star
9175e29c044318498a40f323f189f9dfd50378efChristian MaederinferKind (FunType t1 _ t2 _) =
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder do checkTypeKind t1 star
f1dec6898638ba1131a9fadbc4d1544c93dfabb0Klaus Luettich checkTypeKind t2 star
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder return star
f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian MaederinferKind (ProductType ts _) =
do mapM_ ( \ t -> checkTypeKind t star) ts
return star
inferKind (LazyType t _) =
do checkTypeKind t star
return star
inferKind (TypeToken t) = getIdKind $ simpleIdToId t
inferKind (KindedType t k _) =
do checkTypeKind t k
return k
inferKind t =
do addDiags [mkDiag Error "unresolved type" t]
return star
checkTypeKind :: Type -> Kind -> State Env ()
checkTypeKind t j = do k <- inferKind t
checkKinds t j k
getIdKind :: Id -> State Env Kind
getIdKind i =
do tk <- gets typeMap
let m = getKind tk i
case m of
Nothing -> do addDiags [mkDiag Error "undeclared type" i]
return star
Just k -> return k
getKind :: TypeMap -> Id -> Maybe Kind
getKind tk i =
case Map.lookup i tk of
Nothing -> Nothing
Just (TypeInfo k _ _ _) -> Just k
isTypeVar :: TypeMap -> Id -> Bool
isTypeVar tk i =
case Map.lookup i tk of
Just (TypeInfo _ _ _ TypeVarDefn) -> True
_ -> False
anaType :: (Kind, Type) -> State Env (Kind, Maybe Type)
anaType (k, t) =
do mT <- mkTypeConstrAppls TopLevel t
tm <- gets typeMap
case mT of
Nothing -> return (star, mT)
Just nt -> do let (newT,_) = expandAlias tm nt
newK <- inferKind newT
checkKinds newT newK k
return (newK, Just newT)
anaStarType :: Type -> State Env (Maybe Type)
anaStarType t = fmap snd $ anaType (star, t)
mkBracketToken :: BracketKind -> [Pos] -> [Token]
mkBracketToken k ps =
if null ps then mkBracketToken k [nullPos]
else zipWith Token ((\ (o,c) -> [o,c]) $ getBrackets k)
[head ps, last ps]