TypeDecl.hs revision 5d2f1a7947dde4ff340f8d4908ae0f22c74fdeda
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder Authors: Christian Maeder
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder analyse type decls
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maederimport qualified Common.Lib.Map as Map
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maederimport CASL.MixfixParser(getTokenList, expandPos)
32562a567baac248a00782d2727716c13117dc4aChristian Maederimport HasCASL.PrintAs(showPretty)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaedercompatibleTypeDefn :: TypeDefn -> TypeDefn -> Id -> [Diagnosis]
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaedercompatibleTypeDefn d1 d2 i =
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder if case (d1, d2) of
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder (TypeVarDefn, TypeVarDefn) -> True
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder (TypeVarDefn, _) -> False
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder (_, TypeVarDefn) -> False
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder then [] else [mkDiag Error "incompatible redeclaration of type" i]
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederaddTypeKind :: TypeDefn -> Id -> Kind -> State Env ()
16e124196c6b204769042028c74f533509c9b5d3Christian MaederaddTypeKind d i k =
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder do tk <- getTypeMap
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Nothing -> putTypeMap $ Map.insert i
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder (TypeInfo k [] [] d) tk
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Just (TypeInfo ok ks sups defn) ->
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder let ds = eqKindDiag k ok in
d2e1ea7e00412ba6a7c29b491e6fca6ca4d6fb18Christian Maeder if null ds then
d2e1ea7e00412ba6a7c29b491e6fca6ca4d6fb18Christian Maeder if any (eqKind SameSyntax k) (ok:ks)
d2e1ea7e00412ba6a7c29b491e6fca6ca4d6fb18Christian Maeder then addDiag $ mkDiag Warning
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder "redeclared type" i
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder else putTypeMap $ Map.insert i
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (k:ks) sups defn) tk
7bcc3181abc49d4327cfdd4f3d98ee9522f4243eChristian Maeder else appendDiags ds
7bcc3181abc49d4327cfdd4f3d98ee9522f4243eChristian MaederaddSuperType :: Type -> Id -> State Env ()
7bcc3181abc49d4327cfdd4f3d98ee9522f4243eChristian MaederaddSuperType t i =
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder do tk <- getTypeMap
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder Nothing -> error "addSuperType"
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder Just (TypeInfo ok ks sups defn) ->
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (TypeInfo ok ks (t:sups) defn)
dcf7a9c571e15547fd5302de8064663a486c26faChristian MaederanaTypeItem :: GenKind -> Instance -> TypeItem -> State Env ()
918c36f05614a959f186fe02bd4f943e0a1d91e3Christian MaederanaTypeItem _ inst (TypeDecl pats kind _) =
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder do k <- anaKind kind
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder let Result ds (Just is) = convertTypePatterns pats
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder appendDiags ds
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder mapM_ (anaTypeId NoTypeDefn inst kind) is
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederanaTypeItem _ inst (SubtypeDecl pats t _) =
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder do sup <- anaType t
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder let Result ds (Just is) = convertTypePatterns pats
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder appendDiags ds
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder mapM_ (anaTypeId NoTypeDefn inst star) is
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder mapM_ (addSuperType t) is
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederanaTypeItem _ inst (IsoDecl pats _) =
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder do let Result ds (Just is) = convertTypePatterns pats
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder appendDiags ds
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder mapM_ (anaTypeId NoTypeDefn inst star) is
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder mapM_ ( \ i -> mapM_ (addSuperType (TypeName i 0)) is) is
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederanaTypeItem _ inst (SubtypeDefn pat v t f ps) =
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder do (mk, newT) <- anaType t
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder k <- case mk of
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Nothing -> return star
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Just k -> do appendDiags $ eqKindDiag k star
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder addDiag $ Diag Warning ("unchecked formula '" ++ showPretty f "'")
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder $ firstPos [v] ps
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder let Result ds m = convertTypePattern pat
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder appendDiags ds
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder Nothing -> return ()
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder Just i -> do anaTypeId (Supertype v newT $ item f)
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder addSuperType newT i
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederanaTypeItem _ inst (AliasType pat mk sc _) =
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder do (ik, newPty) <- anaTypeScheme mk sc
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder let Result ds m = convertTypePattern pat
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder appendDiags ds
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder case (m, ik) of
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (Just i, Just ki) -> anaTypeId (AliasTypeDefn newPty) inst ki i
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian Maeder _ -> return ()
16e124196c6b204769042028c74f533509c9b5d3Christian MaederanaTypeItem gk inst (Datatype d) = anaDatatype gk inst d
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian MaederanaDatatype :: GenKind -> Instance -> DatatypeDecl -> State Env ()
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian MaederanaDatatype genKind inst (DatatypeDecl pat kind _alts derivs _) =
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder do k <- anaKind kind
32562a567baac248a00782d2727716c13117dc4aChristian Maeder case derivs of
32562a567baac248a00782d2727716c13117dc4aChristian Maeder Just c -> anaClass c
32562a567baac248a00782d2727716c13117dc4aChristian Maeder Nothing -> return $ Intersection [] [] -- ignore
32562a567baac248a00782d2727716c13117dc4aChristian Maeder let Result ds m = convertTypePattern pat
32562a567baac248a00782d2727716c13117dc4aChristian Maeder appendDiags ds
32562a567baac248a00782d2727716c13117dc4aChristian Maeder Nothing -> return ()
32562a567baac248a00782d2727716c13117dc4aChristian Maeder do -- newAlts <- anaAlts i alts
32562a567baac248a00782d2727716c13117dc4aChristian Maeder anaTypeId (DatatypeDefn genKind) inst k i
32562a567baac248a00782d2727716c13117dc4aChristian Maeder-- TO DO analyse alternatives and add them to Datatype Defn
32562a567baac248a00782d2727716c13117dc4aChristian Maeder-- anaAlts :: Id ->
32562a567baac248a00782d2727716c13117dc4aChristian MaederanaTypeScheme :: Maybe Kind -> TypeScheme -> State Env (Maybe Kind, TypeScheme)
57a32fb13a6acc1748bb1c68028cb2382d6bdb3fChristian MaederanaTypeScheme mk (TypeScheme tArgs (q :=> ty) p) =
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder do k <- case mk of
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder Nothing -> return Nothing
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder Just j -> fmap Just $ anaKind j
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder tm <- getTypeMap -- save global variables
32562a567baac248a00782d2727716c13117dc4aChristian Maeder mapM_ anaTypeArgs tArgs
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder (ik, newTy) <- anaType ty
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder let newPty = TypeScheme tArgs (q :=> newTy) p
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder sik <- case ik of
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Nothing -> return k
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Just sk -> do let newK = typeArgsListToKind tArgs sk
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Nothing -> return ()
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Just ki -> appendDiags $ eqKindDiag ki newK
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder return $ Just newK
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder putTypeMap tm -- forget local variables
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder return (sik, newPty)
0243238805d31e597195ef974e8e7eccb587a390Christian MaedertypeArgsListToKind :: [TypeArgs] -> Kind -> Kind
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaedertypeArgsListToKind tArgs k =
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder if null tArgs then k
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder else typeArgsListToKind (init tArgs)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder (KindAppl (typeArgsToKind $ last tArgs) k [])
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaedertypeArgsToKind :: TypeArgs -> Kind
e68cfdc781c4fd65d42f99173efc2aef342ce0eeChristian MaedertypeArgsToKind (TypeArgs l ps) =
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder if length l == 1 then typeArgToKind $ head l
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder else error "ProdClass (map typeArgToKind l) ps"
0243238805d31e597195ef974e8e7eccb587a390Christian MaedertypeArgToKind :: TypeArg -> Kind
0243238805d31e597195ef974e8e7eccb587a390Christian MaedertypeArgToKind (TypeArg _ k _ _) = k
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederanaTypeVarDecl :: TypeArg -> State Env ()
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederanaTypeVarDecl(TypeArg t k _ _) =
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder do nk <- anaKind k
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder addTypeKind TypeVarDefn t k
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederanaTypeArgs :: TypeArgs -> State Env ()
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederanaTypeArgs(TypeArgs l _) = mapM_ anaTypeVarDecl l
0243238805d31e597195ef974e8e7eccb587a390Christian MaederkindArity :: ApplMode -> Kind -> Int
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian MaederkindArity m (KindAppl k1 k2 _) =
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian Maeder TopLevel -> kindArity OnlyArg k1 +
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder kindArity TopLevel k2
0243238805d31e597195ef974e8e7eccb587a390Christian MaederkindArity m (ExtClass _ _ _) = case m of
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder TopLevel -> 0
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederanaTypeId :: TypeDefn -> Instance -> Kind -> Id -> State Env ()
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder-- type args not yet considered for kind construction
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederanaTypeId defn _ kind i@(Id ts _ _) =
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder let n = length $ filter isPlace ts
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder in if n == 0 || n == kindArity TopLevel kind then
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder addTypeKind defn i kind
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder else addDiag $ mkDiag Error "wrong arity of" i
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederconvertTypePatterns :: [TypePattern] -> Result [Id]
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederconvertTypePatterns [] = Result [] $ Just []
0243238805d31e597195ef974e8e7eccb587a390Christian MaederconvertTypePatterns (s:r) =
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder let Result d m = convertTypePattern s
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder Result ds (Just l) = convertTypePatterns r
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Nothing -> Result (d++ds) $ Just l
dcf7a9c571e15547fd5302de8064663a486c26faChristian Maeder Just i -> Result (d++ds) $ Just (i:l)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederconvertTypePattern, makeMixTypeId :: TypePattern -> Result Id
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederconvertTypePattern (TypePattern t _ _) = return t
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian MaederconvertTypePattern(TypePatternToken t) =
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder if isPlace t then fatal_error ("illegal type '__'") (tokPos t)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder else return $ (simpleIdToId t)
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian MaederconvertTypePattern t =
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder if {- hasPlaces t && -} hasTypeArgs t then
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder fatal_error ( "arguments in type patterns not yet supported")
0a757184b9336a91b2ba735dd58c5ed4e4378e51Christian Maeder -- "illegal mix of '__' and '(...)'"
0a757184b9336a91b2ba735dd58c5ed4e4378e51Christian Maeder (posOfTypePattern t)
0a757184b9336a91b2ba735dd58c5ed4e4378e51Christian Maeder else makeMixTypeId t
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian Maeder-- TODO trailing places are not necessary for curried kinds
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder-- and should be ignored to avoid different Ids "Pred" and "Pred__"
0243238805d31e597195ef974e8e7eccb587a390Christian MaedertypePatternToTokens :: TypePattern -> [Token]
0243238805d31e597195ef974e8e7eccb587a390Christian MaedertypePatternToTokens (TypePattern ti _ _) = getTokenList True ti
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaedertypePatternToTokens (TypePatternToken t) = [t]
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaedertypePatternToTokens (MixfixTypePattern ts) = concatMap typePatternToTokens ts
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaedertypePatternToTokens (BracketTypePattern pk ts ps) =
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder let tts = map typePatternToTokens ts
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder expand = expandPos (:[]) in
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder Parens -> if length tts == 1 &&
ac3ee7f6fc2e0b684e8a05485c9309b8eefb665dChristian Maeder length (head tts) == 1 then head tts
ac3ee7f6fc2e0b684e8a05485c9309b8eefb665dChristian Maeder else concat $ expand "(" ")" tts ps
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder Squares -> concat $ expand "[" "]" tts ps
ac3ee7f6fc2e0b684e8a05485c9309b8eefb665dChristian Maeder Braces -> concat $ expand "{" "}" tts ps
ac3ee7f6fc2e0b684e8a05485c9309b8eefb665dChristian MaedertypePatternToTokens (TypePatternArgs as) =
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder map ( \ (TypeArg v _ _ _) -> Token "__" (posOfId v)) as
2dbb344c4f3fe8f3b9c49db7f95f851d0472c2b2Christian Maeder-- compound Ids not supported yet
2dbb344c4f3fe8f3b9c49db7f95f851d0472c2b2Christian MaedergetToken :: GenParser Token st Token
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian MaedergetToken = token tokStr tokPos Just
62d5dbbceb675837039e6bad0971c324cce96a21Mihai CodescuparseTypePatternId :: GenParser Token st Id
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaederparseTypePatternId =
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder do ts <- many1 getToken
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder return $ Id ts [] []
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaedermakeMixTypeId t =
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder case parse parseTypePatternId "" (typePatternToTokens t) of
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder Left err -> fatal_error (showErrorMessages "or" "unknown parse error"
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder "expecting" "unexpected" "end of input"
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian Maeder (errorMessages err))
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder (errorPos err)
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian Maeder Right x -> return x
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaederhasPlaces, hasTypeArgs :: TypePattern -> Bool
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian MaederhasPlaces (TypePattern _ _ _) = False
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian MaederhasPlaces (TypePatternToken t) = isPlace t
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaederhasPlaces (MixfixTypePattern ts) = any hasPlaces ts
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian MaederhasPlaces (BracketTypePattern Parens _ _) = False
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaederhasPlaces (BracketTypePattern _ ts _) = any hasPlaces ts
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian MaederhasPlaces (TypePatternArgs _) = False
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaederhasTypeArgs (TypePattern _ _ _) = True
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaederhasTypeArgs (TypePatternToken _) = False
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaederhasTypeArgs (MixfixTypePattern ts) = any hasTypeArgs ts
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaederhasTypeArgs (BracketTypePattern Parens _ _) = True
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaederhasTypeArgs (BracketTypePattern _ ts _) = any hasTypeArgs ts
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaederhasTypeArgs (TypePatternArgs _) = True