TypeDecl.hs revision 4c4a6faea90bdb95062434ca9b9e85f5c3b2d012
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder Authors: Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder analyse type decls
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maederimport qualified Common.Lib.Map as Map
722e8a91f69209ba0e99bf799c4989801d78cf16Christian Maederimport CASL.MixfixParser(getTokenList, expandPos)
33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian MaedercompatibleTypeDefn :: TypeDefn -> TypeDefn -> Id -> [Diagnosis]
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercompatibleTypeDefn d1 d2 i =
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder if case (d1, d2) of
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder (TypeVarDefn, TypeVarDefn) -> True
e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder (TypeVarDefn, _) -> False
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder (_, TypeVarDefn) -> False
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder then [] else [mkDiag Error "incompatible redeclaration of type" i]
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederaddTypeKind :: TypeDefn -> Id -> Kind -> State Env ()
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederaddTypeKind d i k =
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder do tk <- getTypeMap
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder Nothing -> putTypeMap $ Map.insert i
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder (TypeInfo k [] [] d) tk
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder Just (TypeInfo ok ks sups defn) ->
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder do checkKinds (posOfId i) k ok
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder if any (==k) (ok:ks)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski then addDiag $ mkDiag Warning
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder "redeclared type" i
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder else putTypeMap $ Map.insert i
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder (k:ks) sups defn) tk
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederaddSuperType :: Type -> Id -> State Env ()
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaederaddSuperType t i =
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder do tk <- getTypeMap
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder Nothing -> return () -- previous error
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Just (TypeInfo ok ks sups defn) ->
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder (TypeInfo ok ks (t:sups) defn)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederanaTypeItem :: GenKind -> Instance -> TypeItem -> State Env ()
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederanaTypeItem _ inst (TypeDecl pats kind _) =
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder do k <- anaKind kind
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder let Result ds (Just is) = convertTypePatterns pats
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder appendDiags ds
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder mapM_ (anaTypeId NoTypeDefn inst kind) is
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederanaTypeItem _ inst (SubtypeDecl pats t _) =
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder do sup <- anaType t
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder let Result ds (Just is) = convertTypePatterns pats
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder appendDiags ds
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder mapM_ (anaTypeId NoTypeDefn inst star) is
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder mapM_ (addSuperType t) is
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaederanaTypeItem _ inst (IsoDecl pats _) =
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder do let Result ds (Just is) = convertTypePatterns pats
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder appendDiags ds
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder mapM_ (anaTypeId NoTypeDefn inst star) is
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder mapM_ ( \ i -> mapM_ (addSuperType (TypeName i star 0)) is) is
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederanaTypeItem _ inst (SubtypeDefn pat v t f ps) =
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder do (mk, newT) <- anaType t
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder k <- case mk of
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Nothing -> return star
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Just k -> do checkKinds (posOfType t) k star
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder addDiag $ Diag Warning ("unchecked formula '" ++ showPretty f "'")
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder $ firstPos [v] ps
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder let Result ds m = convertTypePattern pat
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder appendDiags ds
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder Nothing -> return ()
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Just i -> do anaTypeId (Supertype v newT $ item f)
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder addSuperType newT i
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaederanaTypeItem _ inst (AliasType pat mk sc _) =
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder do (ik, newPty) <- anaPseudoType mk sc
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder let Result ds m = convertTypePattern pat
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder appendDiags ds
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder case (m, ik) of
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder (Just i, Just ki) -> anaTypeId (AliasTypeDefn newPty) inst ki i
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder _ -> return ()
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaederanaTypeItem gk inst (Datatype d) = anaDatatype gk inst d
df2a122c5ecd7d995323c3f0754e1a2a4e3dc0a8Christian MaederanaDatatype :: GenKind -> Instance -> DatatypeDecl -> State Env ()
df2a122c5ecd7d995323c3f0754e1a2a4e3dc0a8Christian MaederanaDatatype genKind inst (DatatypeDecl pat kind _alts derivs ps) =
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder do k <- anaKind kind
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder checkKinds (firstPos [pat] ps) k star
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder case derivs of
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder Just c -> do (dk, _) <- anaClass c
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder checkKinds (posOfClass c) dk star
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder Nothing -> return ()
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder let Result ds m = convertTypePattern pat
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder appendDiags ds
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Nothing -> return ()
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder do -- newAlts <- anaAlts i alts
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder anaTypeId (DatatypeDefn genKind) inst k i
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder-- TO DO analyse alternatives and add them to Datatype Defn
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder-- anaAlts :: Id ->
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederanaPseudoType :: Maybe Kind -> TypeScheme -> State Env (Maybe Kind, TypeScheme)
5964438458028e61fdabfa74ca3b4210206cdba6Christian MaederanaPseudoType mk (TypeScheme tArgs (q :=> ty) p) =
5964438458028e61fdabfa74ca3b4210206cdba6Christian Maeder do k <- case mk of
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Nothing -> return Nothing
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Just j -> fmap Just $ anaKind j
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder tm <- getTypeMap -- save global variables
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder mapM_ anaTypeVarDecl tArgs
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder (ik, newTy) <- anaType ty
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder let newPty = TypeScheme tArgs (q :=> newTy) p
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder sik <- case ik of
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Nothing -> return k
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder Just sk -> do let newK = typeArgsListToKind tArgs sk
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Nothing -> return ()
d48085f765fca838c1d972d2123601997174583dChristian Maeder Just ki -> checkKinds (posOfType ty) ki newK
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder return $ Just newK
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder putTypeMap tm -- forget local variables
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder return (sik, newPty)
f6fc70956d64365527d77a521a96f54a1cc18f91Christian MaedertypeArgsListToKind :: [TypeArg] -> Kind -> Kind
f6fc70956d64365527d77a521a96f54a1cc18f91Christian MaedertypeArgsListToKind tArgs k =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder if null tArgs then k
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder else typeArgsListToKind (init tArgs)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder (KindAppl (typeArgToKind $ last tArgs) k [])
3daa82a175c7cfabf22455aa77c4beda327404e4Christian MaedertypeArgToKind :: TypeArg -> Kind
f6fc70956d64365527d77a521a96f54a1cc18f91Christian MaedertypeArgToKind (TypeArg _ k _ _) = k
3daa82a175c7cfabf22455aa77c4beda327404e4Christian MaederanaTypeVarDecl :: TypeArg -> State Env ()
3daa82a175c7cfabf22455aa77c4beda327404e4Christian MaederanaTypeVarDecl(TypeArg t k _ _) =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder do nk <- anaKind k
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder addTypeKind TypeVarDefn t nk
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederkindArity :: ApplMode -> Kind -> Int
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederkindArity m (KindAppl k1 k2 _) =
149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder TopLevel -> kindArity OnlyArg k1 +
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder kindArity TopLevel k2
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaederkindArity m (ExtClass _ _ _) = case m of
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder TopLevel -> 0
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaederanaTypeId :: TypeDefn -> Instance -> Kind -> Id -> State Env ()
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder-- type args not yet considered for kind construction
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian MaederanaTypeId defn _ kind i@(Id ts _ _) =
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder do cMap <- getClassMap
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder let n = length $ filter isPlace ts
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder nk = expandKind cMap kind
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder if n <= kindArity TopLevel nk then
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder addTypeKind defn i kind
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder else addDiag $ mkDiag Error "wrong arity of" i
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaederconvertTypePatterns :: [TypePattern] -> Result [Id]
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaederconvertTypePatterns [] = Result [] $ Just []
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaederconvertTypePatterns (s:r) =
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder let Result d m = convertTypePattern s
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Result ds (Just l) = convertTypePatterns r
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Nothing -> Result (d++ds) $ Just l
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder Just i -> Result (d++ds) $ Just (i:l)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederconvertTypePattern, makeMixTypeId :: TypePattern -> Result Id
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederconvertTypePattern (TypePattern t _ _) = return t
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederconvertTypePattern(TypePatternToken t) =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder if isPlace t then fatal_error ("illegal type '__'") (tokPos t)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder else return $ (simpleIdToId t)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederconvertTypePattern t =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder if {- hasPlaces t && -} hasTypeArgs t then
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder fatal_error ( "arguments in type patterns not yet supported")
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder -- "illegal mix of '__' and '(...)'"
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder (posOfTypePattern t)
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder else makeMixTypeId t
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder-- TODO trailing places are not necessary for curried kinds
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder-- and should be ignored to avoid different Ids "Pred" and "Pred__"
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedertypePatternToTokens :: TypePattern -> [Token]
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedertypePatternToTokens (TypePattern ti _ _) = getTokenList True ti
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedertypePatternToTokens (TypePatternToken t) = [t]
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedertypePatternToTokens (MixfixTypePattern ts) = concatMap typePatternToTokens ts
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedertypePatternToTokens (BracketTypePattern pk ts ps) =
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let tts = map typePatternToTokens ts
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder expand = expandPos (:[]) in
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder Parens -> if length tts == 1 &&
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder length (head tts) == 1 then head tts
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder else concat $ expand "(" ")" tts ps
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder Squares -> concat $ expand "[" "]" tts ps
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder Braces -> concat $ expand "{" "}" tts ps
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedertypePatternToTokens (TypePatternArg (TypeArg v _ _ _) _) =
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder [Token "__" (posOfId v)]
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder-- compound Ids not supported yet
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedergetToken :: GenParser Token st Token
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedergetToken = token tokStr tokPos Just
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederparseTypePatternId :: GenParser Token st Id
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederparseTypePatternId =
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder do ts <- many1 getToken
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder return $ Id ts [] []
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedermakeMixTypeId t =
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder case parse parseTypePatternId "" (typePatternToTokens t) of
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder Left err -> fatal_error (showErrorMessages "or" "unknown parse error"
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder "expecting" "unexpected" "end of input"
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder (errorMessages err))
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder (errorPos err)
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maeder Right x -> return x
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederhasPlaces, hasTypeArgs :: TypePattern -> Bool
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederhasPlaces (TypePattern _ _ _) = False
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederhasPlaces (TypePatternToken t) = isPlace t
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederhasPlaces (MixfixTypePattern ts) = any hasPlaces ts
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederhasPlaces (BracketTypePattern _ ts _) = any hasPlaces ts
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederhasPlaces (TypePatternArg _ _) = False
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederhasTypeArgs (TypePattern _ _ _) = True
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederhasTypeArgs (TypePatternToken _) = False
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederhasTypeArgs (MixfixTypePattern ts) = any hasTypeArgs ts
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederhasTypeArgs (BracketTypePattern _ ts _) = any hasTypeArgs ts
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederhasTypeArgs (TypePatternArg _ _) = True