TypeDecl.hs revision 0d88ef164d1e0423b485aa4fabaead397047e59d
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{- HetCATS/HasCASL/TypeDecl.hs
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $Id$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Authors: Christian Maeder
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski Year: 2003
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu analyse type decls
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-}
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedermodule TypeDecl where
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederimport As
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskiimport AsUtils
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskiimport ClassAna
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport FiniteMap
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Id
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Le
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Maybe
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport MonadState
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport MixfixParser(getTokenList, expandPos)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Parsec
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport ParsecPos
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport ParsecError
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport PrettyPrint
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport PrintAs(showPretty)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Result
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport TypeAna
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedermissingAna :: PrettyPrint a => a -> [Pos] -> State Env ()
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedermissingAna t ps = appendDiags [Diag FatalError
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder ("no analysis yet for: " ++ showPretty t "")
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder $ if null ps then nullPos else head ps]
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederaddTypeKind :: Id -> Kind -> State Env ()
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederaddTypeKind t k =
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder do tk <- getTypeKinds
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder case lookupFM tk t of
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder Just ks -> let ds = eqKindDiag k $ head ks in
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder if null ds then
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder putTypeKinds $ addToFM tk t (k:ks)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder else appendDiags ds
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder _ -> putTypeKinds $ addToFM tk t [k]
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederanaTypeItem :: Instance -> TypeItem -> State Env ()
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederanaTypeItem inst (TypeDecl pats kind _) =
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder do k <- anaKind kind
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder mapM_ (anaTypePattern inst k) pats
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederanaTypeItem inst (SubtypeDecl pats t _) =
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder do sup <- anaType t
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder mapM_ (anaTypePattern inst nullKind) pats
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder let rs = map (fromJust . maybeResult) $
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder filter (isJust . maybeResult) $
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder map convertTypePattern pats
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder return ()
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederanaTypeItem _ t@(IsoDecl _ p) = missingAna t p
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederanaTypeItem _ (SubtypeDefn t _ _ _ p) = missingAna t p
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederanaTypeItem _ (Datatype (DatatypeDecl t _ _ _ p)) = missingAna t p
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederanaTypeItem _ (AliasType t _ _ p) = missingAna t p
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederkindArity :: ApplMode -> Kind -> Int
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederkindArity m (KindAppl k1 k2 _) =
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder case m of
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder TopLevel -> kindArity OnlyArg k1 +
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder kindArity TopLevel k2
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder OnlyArg -> 1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederkindArity m (ProdClass ks _) =
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder case m of TopLevel -> 0
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder OnlyArg -> sum $ map (kindArity m) ks
ad270004874ce1d0697fb30d7309f180553bb315Christian MaederkindArity m (ExtClass k _ _) = kindArity m k
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederkindArity m (PlainClass _) = case m of
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski TopLevel -> 0
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang OnlyArg -> 1
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederanaTypePattern :: Instance -> Kind -> TypePattern -> State Env ()
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder-- type args not yet considered for kind construction
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WanganaTypePattern _ kind t =
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder let Result ds mi = convertTypePattern t
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder in if typePatternArgs t == 0 ||
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder typePatternArgs t == kindArity TopLevel kind then
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder case mi of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just ti -> addTypeKind ti kind
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder Nothing -> appendDiags ds
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder else appendDiags [Diag Error "non-matching kind arity"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $ posOfTypePattern t]
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian MaederconvertTypePattern, makeMixTypeId :: TypePattern -> Result Id
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus LuettichconvertTypePattern (TypePattern t _ _) = return t
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaederconvertTypePattern(TypePatternToken t) =
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich if isPlace t then fatal_error ("illegal type '__'") (tokPos t)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder else return $ (simpleIdToId t)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederconvertTypePattern t =
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu if hasPlaces t && hasTypeArgs t then
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder fatal_error ( "illegal mix of '__' and '(...)'" )
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder (posOfTypePattern t)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder else makeMixTypeId t
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertypePatternToTokens :: TypePattern -> [Token]
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertypePatternToTokens (TypePattern ti _ _) = getTokenList True ti
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertypePatternToTokens (TypePatternToken t) = [t]
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedertypePatternToTokens (MixfixTypePattern ts) = concatMap typePatternToTokens ts
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertypePatternToTokens (BracketTypePattern pk ts ps) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let tts = map typePatternToTokens ts
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder expand = expandPos (:[]) in
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder case pk of
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Parens -> if length tts == 1 &&
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder length (head tts) == 1 then head tts
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder else concat $ expand "(" ")" tts ps
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Squares -> concat $ expand "[" "]" tts ps
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Braces -> concat $ expand "{" "}" tts ps
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaedertypePatternToTokens (TypePatternArgs as) =
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder map ( \ (TypeArg v _ _ _) -> Token "__" (tokPos v)) as
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder-- compound Ids not supported yet
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaedergetToken :: GenParser Token st Token
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaedergetToken = token tokStr (( \ (l, c) -> newPos "" l c) . tokPos) Just
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederparseTypePatternId :: GenParser Token st Id
e6dccba746efe07338d3107fed512e713fd50b28Christian MaederparseTypePatternId =
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder do ts <- many1 getToken
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder return $ Id ts [] []
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaedermakeMixTypeId t =
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder case parse parseTypePatternId "" (typePatternToTokens t) of
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder Left err -> fatal_error (showErrorMessages "or" "unknown parse error"
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder "expecting" "unexpected" "end of input"
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder (errorMessages err))
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maeder (let p = errorPos err in (sourceLine p, sourceColumn p))
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder Right x -> return x
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedertypePatternArgs :: TypePattern -> Int
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaedertypePatternArgs (TypePattern _ as _) = length as
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaedertypePatternArgs (TypePatternToken t) = if isPlace t then 1 else 0
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaedertypePatternArgs (MixfixTypePattern ts) = sum (map typePatternArgs ts)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaedertypePatternArgs (BracketTypePattern _ ts _) = sum (map typePatternArgs ts)
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaedertypePatternArgs (TypePatternArgs as) = length as
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederhasPlaces, hasTypeArgs :: TypePattern -> Bool
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederhasPlaces (TypePattern _ _ _) = False
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaederhasPlaces (TypePatternToken t) = isPlace t
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaederhasPlaces (MixfixTypePattern ts) = any hasPlaces ts
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaederhasPlaces (BracketTypePattern Parens _ _) = False
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederhasPlaces (BracketTypePattern _ ts _) = any hasPlaces ts
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederhasPlaces (TypePatternArgs _) = False
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaederhasTypeArgs (TypePattern _ _ _) = True
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederhasTypeArgs (TypePatternToken _) = False
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederhasTypeArgs (MixfixTypePattern ts) = any hasTypeArgs ts
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederhasTypeArgs (BracketTypePattern Parens _ _) = True
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederhasTypeArgs (BracketTypePattern _ ts _) = any hasTypeArgs ts
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederhasTypeArgs (TypePatternArgs _) = True
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder