TypeDecl.hs revision e289294500ad68fa0706b09521af340bbb356a69
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder{- HetCATS/HasCASL/TypeDecl.hs
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder $Id$
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder Authors: Christian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder Year: 2003
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder analyse type decls
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder-}
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maedermodule TypeDecl where
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport As
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport AsUtils
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maederimport ClassAna
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport FiniteMap
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport Id
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport Le
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport MonadState
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport MixfixParser(getTokenList, expandPos)
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport Parsec
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport ParsecPos
04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport ParsecError
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport PrettyPrint
04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport PrintAs(showPretty)
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maederimport Result
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian MaedermissingAna :: PrettyPrint a => a -> [Pos] -> State Env ()
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian MaedermissingAna t ps = appendDiags [Diag FatalError
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder ("no analysis yet for: " ++ showPretty t "")
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder $ if null ps then nullPos else head ps]
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian MaederaddTypeKind :: Id -> Kind -> State Env ()
04dada28736b4a237745e92063d8bdd49a362debChristian MaederaddTypeKind t k =
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder do tk <- getTypeKinds
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder case lookupFM tk t of
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder Just ks -> let ds = eqKindDiag k $ head ks in
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder if null ds then
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder putTypeKinds $ addToFM tk t (k:ks)
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder else appendDiags ds
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder _ -> putTypeKinds $ addToFM tk t [k]
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian MaederanaTypeItem :: Instance -> TypeItem -> State Env ()
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian MaederanaTypeItem inst (TypeDecl pats kind _) =
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder do k <- anaKind kind
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder mapM_ (anaTypePattern inst k) pats
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian MaederanaTypeItem _ (SubtypeDecl _ t p) = missingAna t p
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian MaederanaTypeItem _ t@(IsoDecl _ p) = missingAna t p
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian MaederanaTypeItem _ (SubtypeDefn t _ _ _ p) = missingAna t p
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian MaederanaTypeItem _ (Datatype (DatatypeDecl t _ _ _ p)) = missingAna t p
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian MaederanaTypeItem _ (AliasType t _ _ p) = missingAna t p
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederdata ApplMode = OnlyArg | TopLevel
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian MaederkindArity :: ApplMode -> Kind -> Int
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian MaederkindArity m (KindAppl k1 k2 _) =
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder case m of
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder TopLevel -> kindArity OnlyArg k1 +
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder kindArity TopLevel k2
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder OnlyArg -> 1
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian MaederkindArity m (ProdClass ks _) =
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder case m of TopLevel -> 0
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder OnlyArg -> sum $ map (kindArity m) ks
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederkindArity m (ExtClass k _ _) = kindArity m k
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederkindArity m (PlainClass _) = case m of
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder TopLevel -> 0
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder OnlyArg -> 1
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederanaTypePattern :: Instance -> Kind -> TypePattern -> State Env ()
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder-- type args not yet considered for kind construction
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian MaederanaTypePattern _ kind t =
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder let Result ds mi = convertTypePattern t
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder in if typePatternArgs t == 0 ||
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder typePatternArgs t == kindArity TopLevel kind then
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder case mi of
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder Just ti -> addTypeKind ti kind
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder Nothing -> appendDiags ds
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder else appendDiags [Diag Error "non-matching kind arity"
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder $ posOfTypePattern t]
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederconvertTypePattern, makeMixTypeId :: TypePattern -> Result Id
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederconvertTypePattern (TypePattern t _ _) = return t
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederconvertTypePattern(TypePatternToken t) =
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder if isPlace t then fatal_error ("illegal type '__'") (tokPos t)
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder else return $ (simpleIdToId t)
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederconvertTypePattern t =
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder if hasPlaces t && hasTypeArgs t then
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder fatal_error ( "illegal mix of '__' and '(...)'" )
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder (posOfTypePattern t)
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder else makeMixTypeId t
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaedertypePatternToTokens :: TypePattern -> [Token]
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaedertypePatternToTokens (TypePattern ti _ _) = getTokenList True ti
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian MaedertypePatternToTokens (TypePatternToken t) = [t]
04dada28736b4a237745e92063d8bdd49a362debChristian MaedertypePatternToTokens (MixfixTypePattern ts) = concatMap typePatternToTokens ts
04dada28736b4a237745e92063d8bdd49a362debChristian MaedertypePatternToTokens (BracketTypePattern pk ts ps) =
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder let tts = map typePatternToTokens ts
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder expand = expandPos (:[]) in
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder case pk of
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder Parens -> if length tts == 1 &&
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder length (head tts) == 1 then head tts
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder else concat $ expand "(" ")" tts ps
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder Squares -> concat $ expand "[" "]" tts ps
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder Braces -> concat $ expand "{" "}" tts ps
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaedertypePatternToTokens (TypePatternArgs as) =
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder map ( \ (TypeArg v _ _ _) -> Token "__" (tokPos v)) as
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder-- compound Ids not supported yet
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian MaedergetToken :: GenParser Token st Token
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian MaedergetToken = token tokStr (( \ (l, c) -> newPos "" l c) . tokPos) Just
04dada28736b4a237745e92063d8bdd49a362debChristian MaederparseTypePatternId :: GenParser Token st Id
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian MaederparseTypePatternId =
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder do ts <- many1 getToken
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder return $ Id ts [] []
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian MaedermakeMixTypeId t =
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder case parse parseTypePatternId "" (typePatternToTokens t) of
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder Left err -> fatal_error (showErrorMessages "or" "unknown parse error"
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder "expecting" "unexpected" "end of input"
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder (errorMessages err))
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder (let p = errorPos err in (sourceLine p, sourceColumn p))
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder Right x -> return x
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian MaedertypePatternArgs :: TypePattern -> Int
04dada28736b4a237745e92063d8bdd49a362debChristian MaedertypePatternArgs (TypePattern _ as _) = length as
04dada28736b4a237745e92063d8bdd49a362debChristian MaedertypePatternArgs (TypePatternToken t) = if isPlace t then 1 else 0
04dada28736b4a237745e92063d8bdd49a362debChristian MaedertypePatternArgs (MixfixTypePattern ts) = sum (map typePatternArgs ts)
04dada28736b4a237745e92063d8bdd49a362debChristian MaedertypePatternArgs (BracketTypePattern _ ts _) = sum (map typePatternArgs ts)
04dada28736b4a237745e92063d8bdd49a362debChristian MaedertypePatternArgs (TypePatternArgs as) = length as
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian MaederhasPlaces, hasTypeArgs :: TypePattern -> Bool
04dada28736b4a237745e92063d8bdd49a362debChristian MaederhasPlaces (TypePattern _ _ _) = False
04dada28736b4a237745e92063d8bdd49a362debChristian MaederhasPlaces (TypePatternToken t) = isPlace t
04dada28736b4a237745e92063d8bdd49a362debChristian MaederhasPlaces (MixfixTypePattern ts) = any hasPlaces ts
04dada28736b4a237745e92063d8bdd49a362debChristian MaederhasPlaces (BracketTypePattern Parens _ _) = False
04dada28736b4a237745e92063d8bdd49a362debChristian MaederhasPlaces (BracketTypePattern _ ts _) = any hasPlaces ts
04dada28736b4a237745e92063d8bdd49a362debChristian MaederhasPlaces (TypePatternArgs _) = False
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian MaederhasTypeArgs (TypePattern _ _ _) = True
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian MaederhasTypeArgs (TypePatternToken _) = False
04dada28736b4a237745e92063d8bdd49a362debChristian MaederhasTypeArgs (MixfixTypePattern ts) = any hasTypeArgs ts
04dada28736b4a237745e92063d8bdd49a362debChristian MaederhasTypeArgs (BracketTypePattern Parens _ _) = True
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian MaederhasTypeArgs (BracketTypePattern _ ts _) = any hasTypeArgs ts
04dada28736b4a237745e92063d8bdd49a362debChristian MaederhasTypeArgs (TypePatternArgs _) = True
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder