1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{- HetCATS/HasCASL/TypeDecl.hs

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder $Id$

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Authors: Christian Maeder

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu Year: 2003

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder analyse type decls

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maedermodule HasCASL.TypeDecl where

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport HasCASL.As

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport HasCASL.AsUtils

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.AS_Annotation(item)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport HasCASL.ClassAna

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport FiniteMap

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport Common.Id

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maederimport HasCASL.Le

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Data.Maybe

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport Control.Monad.State

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport CASL.MixfixParser(getTokenList, expandPos)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.Lib.Parsec

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.Lib.Parsec.Error

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport HasCASL.PrintAs(showPretty)

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederimport Common.Result

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulzimport HasCASL.TypeAna

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian MaedercompatibleTypeDefn :: TypeDefn -> TypeDefn -> Id -> [Diagnosis]

64e1905404e5135e98a26d2ab4150b6764956576Christian MaedercompatibleTypeDefn d1 d2 i =

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder if case (d1, d2) of

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder (TypeVarDefn, TypeVarDefn) -> True

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder (TypeVarDefn, _) -> False

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz (_, TypeVarDefn) -> False

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder _ -> True

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder then [] else [mkDiag Error "incompatible redeclaration of type" i]

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaederaddTypeKind :: TypeDefn -> Id -> Kind -> State Env ()

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederaddTypeKind d i k =

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do tk <- getTypeMap

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder case lookupFM tk i of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Nothing -> putTypeMap $ addToFM tk i

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder $ TypeInfo k [] [] d

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder Just (TypeInfo ok ks sups defn) ->

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder let ds = eqKindDiag k ok in

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder if null ds then

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder if any (eqKind SameSyntax k) (ok:ks)

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder then addDiag $ mkDiag Warning

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder "redeclared type" i

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz else putTypeMap $ addToFM tk i

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder $ TypeInfo ok

65dce48b81f69e11a36bf1051314a845299446e1Christian Maeder (k:ks) sups defn

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder else appendDiags ds

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian MaederaddSuperType :: Type -> Id -> State Env ()

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederaddSuperType t i =

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do tk <- getTypeMap

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder case lookupFM tk i of

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder Nothing -> error "addSuperType"

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Just (TypeInfo ok ks sups defn) ->

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder putTypeMap $ addToFM tk i

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder $ TypeInfo ok ks (t:sups) defn

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian MaederanaTypeItem :: GenKind -> Instance -> TypeItem -> State Env ()

64e1905404e5135e98a26d2ab4150b6764956576Christian MaederanaTypeItem _ inst (TypeDecl pats kind _) =

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do k <- anaKind kind

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder let Result ds (Just is) = convertTypePatterns pats

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder appendDiags ds

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder mapM_ (anaTypeId NoTypeDefn inst kind) is

67869d63d1725c79e4c07b51acd466a31932b275Christian MaederanaTypeItem _ inst (SubtypeDecl pats t _) =

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do sup <- anaType t

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder let Result ds (Just is) = convertTypePatterns pats

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder appendDiags ds

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder mapM_ (anaTypeId NoTypeDefn inst star) is

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder mapM_ (addSuperType t) is

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

67869d63d1725c79e4c07b51acd466a31932b275Christian MaederanaTypeItem _ inst (IsoDecl pats _) =

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do let Result ds (Just is) = convertTypePatterns pats

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder appendDiags ds

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder mapM_ (anaTypeId NoTypeDefn inst star) is

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder mapM_ ( \ i -> mapM_ (addSuperType (TypeName i 0)) is) is

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian MaederanaTypeItem _ inst (SubtypeDefn pat v t f ps) =

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do (mk, newT) <- anaType t

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder k <- case mk of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Nothing -> return star

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Just k -> do appendDiags $ eqKindDiag k star

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder return k

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder addDiag $ Diag Warning ("unchecked formula '" ++ showPretty f "'")

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder $ firstPos [v] ps

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder let Result ds m = convertTypePattern pat

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder appendDiags ds

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder case m of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Nothing -> return ()

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder Just i -> do anaTypeId (Supertype v newT $ item f)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder inst k i

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder addSuperType newT i

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederanaTypeItem _ inst (AliasType pat mk sc _) =

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do (ik, newPty) <- anaTypeScheme mk sc

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder let Result ds m = convertTypePattern pat

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder appendDiags ds

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder case (m, ik) of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder (Just i, Just ki) -> anaTypeId (AliasTypeDefn newPty) inst ki i

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder _ -> return ()

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederanaTypeItem gk inst (Datatype d) = anaDatatype gk inst d

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

67869d63d1725c79e4c07b51acd466a31932b275Christian MaederanaDatatype :: GenKind -> Instance -> DatatypeDecl -> State Env ()

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederanaDatatype genKind inst (DatatypeDecl pat kind _alts derivs _) =

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder do k <- anaKind kind

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder case derivs of

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder Just c -> anaClass c

935613eb8e67d724f1c4a4d4a37be3324ef6708dChristian Maeder Nothing -> return $ Intersection [] [] -- ignore

935613eb8e67d724f1c4a4d4a37be3324ef6708dChristian Maeder let Result ds m = convertTypePattern pat

935613eb8e67d724f1c4a4d4a37be3324ef6708dChristian Maeder appendDiags ds

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder case m of

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder Nothing -> return ()

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder Just i ->

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder do -- newAlts <- anaAlts i alts

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder anaTypeId (DatatypeDefn genKind) inst k i

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder-- TO DO analyse alternatives and add them to Datatype Defn

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder-- anaAlts :: Id ->

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder

083a5256468076d5a9bfeb22a6e97076c224252eChristian MaederanaTypeScheme :: Maybe Kind -> TypeScheme -> State Env (Maybe Kind, TypeScheme)

083a5256468076d5a9bfeb22a6e97076c224252eChristian MaederanaTypeScheme mk (TypeScheme tArgs (q :=> ty) p) =

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder do k <- case mk of

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder Nothing -> return Nothing

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder Just j -> fmap Just $ anaKind j

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder tm <- getTypeMap -- save global variables

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder mapM_ anaTypeArgs tArgs

65dce48b81f69e11a36bf1051314a845299446e1Christian Maeder (ik, newTy) <- anaType ty

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder let newPty = TypeScheme tArgs (q :=> newTy) p

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder sik <- case ik of

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder Nothing -> return k

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder Just sk -> do let newK = typeArgsListToKind tArgs sk

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder case k of

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder Nothing -> return ()

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder Just ki -> appendDiags $ eqKindDiag ki newK

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder return $ Just newK

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder putTypeMap tm -- forget local variables

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder return (sik, newPty)

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian MaedertypeArgsListToKind :: [TypeArgs] -> Kind -> Kind

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulztypeArgsListToKind tArgs k =

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder if null tArgs then k

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder else typeArgsListToKind (init tArgs)

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder (KindAppl (typeArgsToKind $ last tArgs) k [])

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian MaedertypeArgsToKind :: TypeArgs -> Kind

typeArgsToKind (TypeArgs l ps) = if length l == 1 then typeArgToKind $ head l

else ProdClass (map typeArgToKind l) ps

typeArgToKind :: TypeArg -> Kind

typeArgToKind (TypeArg _ k _ _) = k

anaTypeVarDecl :: TypeArg -> State Env ()

anaTypeVarDecl(TypeArg t k _ _) =

do nk <- anaKind k

addTypeKind TypeVarDefn t k

anaTypeArgs :: TypeArgs -> State Env ()

anaTypeArgs(TypeArgs l _) = mapM_ anaTypeVarDecl l

kindArity :: ApplMode -> Kind -> Int

kindArity m (KindAppl k1 k2 _) =

case m of

TopLevel -> kindArity OnlyArg k1 +

kindArity TopLevel k2

OnlyArg -> 1

kindArity m (ProdClass ks _) =

case m of TopLevel -> 0

OnlyArg -> sum $ map (kindArity m) ks

kindArity m (ExtClass k _ _) = kindArity m k

kindArity m (PlainClass _) = case m of

TopLevel -> 0

OnlyArg -> 1

anaTypeId :: TypeDefn -> Instance -> Kind -> Id -> State Env ()

-- type args not yet considered for kind construction

anaTypeId defn _ kind i@(Id ts _ _) =

let n = length $ filter isPlace ts

in if n == 0 || n == kindArity TopLevel kind then

addTypeKind defn i kind

else addDiag $ mkDiag Error "wrong arity of" i

convertTypePatterns :: [TypePattern] -> Result [Id]

convertTypePatterns [] = Result [] $ Just []

convertTypePatterns (s:r) =

let Result d m = convertTypePattern s

Result ds (Just l) = convertTypePatterns r

in case m of

Nothing -> Result (d++ds) $ Just l

Just i -> Result (d++ds) $ Just (i:l)

convertTypePattern, makeMixTypeId :: TypePattern -> Result Id

convertTypePattern (TypePattern t _ _) = return t

convertTypePattern(TypePatternToken t) =

if isPlace t then fatal_error ("illegal type '__'") (tokPos t)

else return $ (simpleIdToId t)

convertTypePattern t =

if {- hasPlaces t && -} hasTypeArgs t then

fatal_error ( "arguments in type patterns not yet supported")

-- "illegal mix of '__' and '(...)'"

(posOfTypePattern t)

else makeMixTypeId t

-- TODO trailing places are not necessary for curried kinds

-- and should be ignored to avoid different Ids "Pred" and "Pred__"

typePatternToTokens :: TypePattern -> [Token]

typePatternToTokens (TypePattern ti _ _) = getTokenList True ti

typePatternToTokens (TypePatternToken t) = [t]

typePatternToTokens (MixfixTypePattern ts) = concatMap typePatternToTokens ts

typePatternToTokens (BracketTypePattern pk ts ps) =

let tts = map typePatternToTokens ts

expand = expandPos (:[]) in

case pk of

Parens -> if length tts == 1 &&

length (head tts) == 1 then head tts

else concat $ expand "(" ")" tts ps

Squares -> concat $ expand "[" "]" tts ps

Braces -> concat $ expand "{" "}" tts ps

typePatternToTokens (TypePatternArgs as) =

map ( \ (TypeArg v _ _ _) -> Token "__" (posOfId v)) as

-- compound Ids not supported yet

getToken :: GenParser Token st Token

getToken = token tokStr tokPos Just

parseTypePatternId :: GenParser Token st Id

parseTypePatternId =

do ts <- many1 getToken

return $ Id ts [] []

makeMixTypeId t =

case parse parseTypePatternId "" (typePatternToTokens t) of

Left err -> fatal_error (showErrorMessages "or" "unknown parse error"

"expecting" "unexpected" "end of input"

(errorMessages err))

(errorPos err)

Right x -> return x

hasPlaces, hasTypeArgs :: TypePattern -> Bool

hasPlaces (TypePattern _ _ _) = False

hasPlaces (TypePatternToken t) = isPlace t

hasPlaces (MixfixTypePattern ts) = any hasPlaces ts

hasPlaces (BracketTypePattern Parens _ _) = False

hasPlaces (BracketTypePattern _ ts _) = any hasPlaces ts

hasPlaces (TypePatternArgs _) = False

hasTypeArgs (TypePattern _ _ _) = True

hasTypeArgs (TypePatternToken _) = False

hasTypeArgs (MixfixTypePattern ts) = any hasTypeArgs ts

hasTypeArgs (BracketTypePattern Parens _ _) = True

hasTypeArgs (BracketTypePattern _ ts _) = any hasTypeArgs ts

hasTypeArgs (TypePatternArgs _) = True