4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- HetCATS/HasCASL/TypeDecl.hs

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder $Id$

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder Authors: Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder Year: 2003

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder analyse type decls

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder-}

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maedermodule HasCASL.TypeDecl where

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport HasCASL.As

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport HasCASL.AsUtils

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport Common.AS_Annotation(item)

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport HasCASL.ClassAna

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport HasCASL.ClassDecl

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport qualified Common.Lib.Map as Map

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport Common.Id

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport HasCASL.Le

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport Data.Maybe

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport Common.Lib.State

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport Common.Lib.Parsec

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport Common.Lib.Parsec.Error

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport Common.Result

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport Common.PrettyPrint

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport HasCASL.TypeAna

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport HasCASL.DataAna

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport HasCASL.Reader

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder-- ---------------------------------------------------------------------------

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder-- analyse types as state

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder-- ---------------------------------------------------------------------------

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederputTypeMap :: TypeMap -> State Env ()

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederputTypeMap tk = do { e <- get; put e { typeMap = tk } }

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederfromReadR :: a -> ReadR (ClassMap, TypeMap) a -> State Env a

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederfromReadR a r = toState a ( \ e -> (classMap e, typeMap e)) r

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederanaTypeS :: (Kind, Type) -> State Env (Kind, Type)

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederanaTypeS kt = fromReadR kt $ anaType kt

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaedercompatibleTypeDefn :: TypeDefn -> TypeDefn -> Id -> [Diagnosis]

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaedercompatibleTypeDefn d1 d2 i =

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder if case (d1, d2) of

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder (TypeVarDefn, TypeVarDefn) -> True

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder (TypeVarDefn, _) -> False

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder (_, TypeVarDefn) -> False

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder _ -> True

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

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

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

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederaddTypeKind d i k =

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder if isPrefix i then do addSingleTypeKind d i k

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder addSingleTypeKind d (stripFinalPlaces i) k

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder else addSingleTypeKind d i k

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederaddSingleTypeKind :: TypeDefn -> Id -> Kind -> State Env ()

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederaddSingleTypeKind d i k =

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder do tk <- gets typeMap

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder case Map.lookup i tk of

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder Nothing -> putTypeMap $ Map.insert i

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder (TypeInfo k [] [] d) tk

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder Just (TypeInfo ok ks sups defn) ->

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder do checkKindsS i k ok

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder if any (==k) (ok:ks)

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder then addDiag $ mkDiag Warning

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder "redeclared type" i

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder else putTypeMap $ Map.insert i

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder (TypeInfo ok

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder (k:ks) sups defn) tk

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederaddSuperType :: Type -> Id -> State Env ()

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederaddSuperType t i =

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder do tk <- gets typeMap

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder case Map.lookup i tk of

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder Nothing -> return () -- previous error

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder Just (TypeInfo ok ks sups defn) ->

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder putTypeMap $ Map.insert i

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder (TypeInfo ok ks (t:sups) defn)

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder tk

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederanaTypeItem :: GenKind -> Instance -> TypeItem -> State Env ()

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederanaTypeItem _ inst (TypeDecl pats kind _) =

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder do anaKindS kind

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder let Result ds (Just is) = convertTypePatterns pats

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder appendDiags ds

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder mapM_ (anaTypeId NoTypeDefn inst kind) is

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederanaTypeItem _ inst (SubtypeDecl pats t _) =

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder do anaTypeS (star, t)

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder let Result ds (Just is) = convertTypePatterns pats

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder appendDiags ds

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder mapM_ (anaTypeId NoTypeDefn inst star) is

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder mapM_ (addSuperType t) is

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederanaTypeItem _ inst (IsoDecl pats _) =

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder do let Result ds (Just is) = convertTypePatterns pats

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder appendDiags ds

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder mapM_ (anaTypeId NoTypeDefn inst star) is

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder mapM_ ( \ i -> mapM_ (addSuperType (TypeName i star 0)) is) is

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian MaederanaTypeItem _ inst (SubtypeDefn pat v t f ps) =

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder do (k, newT) <- anaTypeS (star, t)

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder checkKindsS t star k

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder addDiag $ Diag Warning ("unchecked formula '" ++ showPretty f "'")

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder $ firstPos [v] ps

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder let Result ds m = convertTypePattern pat

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder appendDiags ds

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder case m of

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder Nothing -> return ()

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder Just i -> do anaTypeId (Supertype v newT $ item f)

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder inst k i

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder addSuperType newT i

anaTypeItem _ inst (AliasType pat mk sc _) =

do (ik, newPty) <- anaPseudoType mk sc

let Result ds m = convertTypePattern pat

appendDiags ds

case m of

Just i -> anaTypeId (AliasTypeDefn newPty) inst ik i

_ -> return ()

anaTypeItem gk inst (Datatype d) = anaDatatype gk inst d

anaDatatype :: GenKind -> Instance -> DatatypeDecl -> State Env ()

anaDatatype genKind inst (DatatypeDecl pat kind alts derivs _) =

do k <- anaKindS kind

checkKindsS pat star k

case derivs of

Just c -> do (dk, _) <- anaClassS (star, c)

checkKindsS c star dk

Nothing -> return ()

let Result ds m = convertTypePattern pat

appendDiags ds

case m of

Nothing -> return ()

Just i ->

do fromReadR [] $ anaAlts (TypeName i k 0) $ map item alts

-- add cons and sels to assumps

anaTypeId (DatatypeDefn genKind []) inst k i

anaPseudoType :: Maybe Kind -> TypeScheme -> State Env (Kind, TypeScheme)

anaPseudoType mk (TypeScheme tArgs (q :=> ty) p) =

do k <- case mk of

Nothing -> return star

Just j -> anaKindS j

tm <- gets typeMap -- save global variables

mapM_ anaTypeVarDecl tArgs

(sk, newTy) <- anaTypeS (k, ty)

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

newK = typeArgsListToKind tArgs sk

case mk of

Nothing -> return ()

Just j -> checkKindsS ty j newK

putTypeMap tm -- forget local variables

return (newK, newPty)

typeArgsListToKind :: [TypeArg] -> Kind -> Kind

typeArgsListToKind tArgs k =

if null tArgs then k

else typeArgsListToKind (init tArgs)

(KindAppl (typeArgToKind $ last tArgs) k [])

typeArgToKind :: TypeArg -> Kind

typeArgToKind (TypeArg _ k _ _) = k

anaTypeVarDecl :: TypeArg -> State Env ()

anaTypeVarDecl(TypeArg t k _ _) =

do nk <- anaKindS k

addTypeKind TypeVarDefn t nk

kindArity :: ApplMode -> Kind -> Int

kindArity m (KindAppl k1 k2 _) =

case m of

TopLevel -> kindArity OnlyArg k1 +

kindArity TopLevel k2

OnlyArg -> 1

kindArity m (ExtClass _ _ _) = 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 _ _) =

do nk <- toState kind classMap $ expandKind kind

let n = length $ filter isPlace ts

if n <= kindArity TopLevel nk 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 place ti

typePatternToTokens (TypePatternToken t) = [t]

typePatternToTokens (MixfixTypePattern ts) = concatMap typePatternToTokens ts

typePatternToTokens (BracketTypePattern pk ts ps) =

let tts = map typePatternToTokens ts

expanded = concat $ expandPos (:[]) (getBrackets pk) tts ps in

case pk of

Parens -> if length tts == 1 &&

length (head tts) == 1 then head tts

else expanded

_ -> expanded

typePatternToTokens (TypePatternArg (TypeArg v _ _ _) _) =

[Token "__" (posOfId v)]

-- 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 _ ts _) = any hasPlaces ts

hasPlaces (TypePatternArg _ _) = False

hasTypeArgs (TypePattern _ _ _) = True

hasTypeArgs (TypePatternToken _) = False

hasTypeArgs (MixfixTypePattern ts) = any hasTypeArgs ts

hasTypeArgs (BracketTypePattern _ ts _) = any hasTypeArgs ts

hasTypeArgs (TypePatternArg _ _) = True