52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder{- |

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederModule : $Header$

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2003

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederLicence : All rights reserved.

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederMaintainer : hets@tzi.de

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederStability : provisional

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederPortability : non-portable (MonadState)

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederanalyse type decls

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder-}

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maedermodule HasCASL.TypeDecl where

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder

8191ab400cc9ebb5a3f6c6f18104a208aae187e8Christian Maederimport HasCASL.As

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport HasCASL.AsUtils

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport Common.AS_Annotation

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport HasCASL.ClassAna

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport qualified Common.Lib.Map as Map

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport Common.Id

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport HasCASL.Le

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport Data.Maybe

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport Data.List

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport Common.Lib.State

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport Common.Lib.Parsec

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport Common.Lib.Parsec.Error

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder

8191ab400cc9ebb5a3f6c6f18104a208aae187e8Christian Maederimport Common.Result

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport Common.GlobalAnnotations

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport HasCASL.ClassAna

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport HasCASL.TypeAna

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport HasCASL.DataAna

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport HasCASL.VarDecl

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport HasCASL.TypeCheck

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder-- | add a supertype to a given type id

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederaddSuperType :: Type -> Id -> State Env ()

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederaddSuperType t i =

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder do tk <- gets typeMap

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder case Map.lookup i tk of

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder Nothing -> return () -- previous error

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder Just (TypeInfo ok ks sups defn) ->

8191ab400cc9ebb5a3f6c6f18104a208aae187e8Christian Maeder putTypeMap $ Map.insert i

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder (TypeInfo ok ks (t:sups) defn)

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder tk

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederidsToTypePatterns :: [Maybe Id] -> [TypePattern]

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederidsToTypePatterns mis = map ( \ i -> TypePattern i [] [] )

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder $ catMaybes mis

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederanaFormula :: GlobalAnnos -> Annoted Term -> State Env (Maybe (Annoted Term))

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederanaFormula ga at =

186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder do mt <- resolveTerm ga (Just logicalType) $ item at

186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder return $ case mt of Nothing -> Nothing

186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder Just e -> Just at { item = e }

186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder

186de7a36bdf5910e0616c3a0447603e98217dc7Christian MaederanaVars :: Vars -> Type -> Result [VarDecl]

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederanaVars (Var v) t = return [VarDecl v t Other []]

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederanaVars (VarTuple vs _) t =

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder case t of

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder ProductType ts _ ->

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder if length ts == length vs then

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder let lrs = zipWith anaVars vs ts

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder lms = map maybeResult lrs in

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder if all isJust lms then

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder return $ concatMap fromJust lms

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder else Result (concatMap diags lrs) Nothing

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder else Result [mkDiag Error "wrong arity" t] Nothing

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder _ -> Result [mkDiag Error "product type expected instead" t] Nothing

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder-- | analyse a 'TypeItem'

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederanaTypeItem :: GlobalAnnos -> GenKind -> Instance -> TypeItem

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder -> State Env TypeItem

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederanaTypeItem _ _ inst (TypeDecl pats kind ps) =

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder do ak <- anaKind kind

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder let Result ds (Just is) = convertTypePatterns pats

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder addDiags ds

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder mis <- mapM (addTypeId NoTypeDefn inst ak) is

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder return $ TypeDecl (idsToTypePatterns mis) ak ps

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederanaTypeItem _ _ inst (SubtypeDecl pats t ps) =

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder do let Result ds (Just is) = convertTypePatterns pats

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder addDiags ds

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder mis <- mapM (addTypeId NoTypeDefn inst star) is

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder let newPats = idsToTypePatterns mis

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder mt <- anaStarType t

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder case mt of

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder Nothing -> return $ TypeDecl newPats star ps

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder Just newT -> do mapM_ (addSuperType newT) is

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder return $ SubtypeDecl newPats newT ps

8191ab400cc9ebb5a3f6c6f18104a208aae187e8Christian Maeder

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederanaTypeItem _ _ inst (IsoDecl pats ps) =

52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder do let Result ds (Just is) = convertTypePatterns pats

addDiags ds

mis <- mapM (addTypeId NoTypeDefn inst star) is

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

return $ IsoDecl (idsToTypePatterns mis) ps

anaTypeItem ga _ inst (SubtypeDefn pat v t f ps) =

do let Result ds m = convertTypePattern pat

addDiags ds

mty <- anaStarType t

let Result es mvds = case mty of

Nothing -> Result [] Nothing

Just ty -> anaVars v ty

addDiags es

as <- gets assumps

mv <- case mvds of

Nothing -> return Nothing

Just vds -> do checkUniqueVars vds

mvs <- mapM addVarDecl vds

if all isJust mvs then

return $ Just v

else return Nothing

mt <- anaFormula ga f

putAssumps as

case m of

Nothing -> return $ TypeDecl [] star ps

Just i -> case (mt, mv) of

(Just newF, Just _) -> do

let newT = fromJust mty

mi <- addTypeId (Supertype v newT $ item newF)

inst star i

addSuperType newT i

case mi of

Nothing -> return $ TypeDecl [] star ps

Just _ -> return $ SubtypeDefn

(TypePattern i [] []) v newT newF ps

_ -> do mi <- addTypeId NoTypeDefn inst star i

return $ TypeDecl (idsToTypePatterns [mi]) star ps

anaTypeItem _ _ inst (AliasType pat mk sc ps) =

do let Result ds m = convertTypePattern pat

addDiags ds

(ik, mt) <- anaPseudoType mk sc

case m of

Just i -> case mt of

Nothing -> return $ TypeDecl [] star ps

Just newPty -> do addTypeId (AliasTypeDefn newPty) inst ik i

return $ AliasType (TypePattern i [] [])

(Just ik) newPty ps

_ -> return $ TypeDecl [] star ps

anaTypeItem _ gk inst (Datatype d) =

do newD <- anaDatatype gk inst d

return $ Datatype newD

-- | analyse a 'DatatypeDecl'

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

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

do k <- anaKind kind

checkKinds pat star k

newDerivs <- case derivs of

Just c -> do (dk, newC) <- anaClass c

checkKinds newC star dk

return $ Just newC

Nothing -> return Nothing

let Result ds m = convertTypePattern pat

addDiags ds

case m of

Nothing -> return $ DatatypeDecl pat k [] newDerivs ps

Just i ->

do let dt = TypeName i k 0

newAlts <- anaAlts dt

$ map item alts

mapM_ ( \ (Construct c tc p sels) -> do

let ty = simpleTypeScheme $ getConstrType dt p tc

addOpId c ty

[] (ConstructData i)

mapM_ ( \ (Select s ts pa) ->

addOpId s (simpleTypeScheme $

getSelType dt pa ts)

[] (SelectData [ConstrInfo c ty] i)

) sels) newAlts

mi <- addTypeId (DatatypeDefn genKind [] newAlts) inst k i

return $ DatatypeDecl (TypePattern i [] []) k

(case mi of Nothing -> []

Just _ -> alts)

newDerivs ps

-- | analyse a pseudo type (represented as a 'TypeScheme')

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

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

do k <- case mk of

Nothing -> return star

Just j -> anaKind j

tm <- gets typeMap -- save global variables

mapM_ anaTypeVarDecl tArgs

(sk, mt) <- anaType (k, ty)

let newK = typeArgsListToKind tArgs sk

case mk of

Nothing -> return ()

Just j -> checkKinds ty j newK

putTypeMap tm -- forget local variables

case mt of

Nothing -> return (newK, Nothing)

Just newTy -> return (newK, Just $ TypeScheme tArgs (q :=> newTy) p)

-- | extent a kind to expect further type arguments

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

typeArgsListToKind tArgs k =

if null tArgs then k

else typeArgsListToKind (init tArgs)

(KindAppl (( \ (TypeArg _ xk _ _) -> xk) $ last tArgs) k [])

-- | convert mixfix type patterns to ids

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)

-- | convert a 'TypePattern' to a type 'Id' via 'makeMixTypeId'

convertTypePattern :: 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 hasTypeArgs t then

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

(posOfTypePattern t)

else makeMixTypeId t

-- trailing places are not necessary for curried kinds

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

-- | decompose a 'TypePattern' into tokens

typePatternToTokens :: TypePattern -> [Token]

typePatternToTokens (TypePattern ti _ _) = getPlainTokenList 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, tts) of

(Parens, [t@[_]]) -> t

_ -> expanded

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

[Token "__" (posOfId v)]

-- compound Ids not supported yet

-- | get the next 'Token' from a token list

getToken :: GenParser Token st Token

getToken = token tokStr tokPos Just

-- | parse a type 'Id' from a token list

parseTypePatternId :: GenParser Token st Id

parseTypePatternId =

do ts <- many1 getToken

return $ Id ts [] []

-- | convert a 'TypePattern' to a type 'Id' via 'typePatternToTokens'

-- and 'parseTypePatternId'

makeMixTypeId :: TypePattern -> Result Id

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

-- | check for type arguments

hasTypeArgs:: TypePattern -> Bool

hasTypeArgs (TypePattern _ _ _) = True

hasTypeArgs (TypePatternToken _) = False

hasTypeArgs (MixfixTypePattern ts) = any hasTypeArgs ts

hasTypeArgs (BracketTypePattern _ ts _) = any hasTypeArgs ts

hasTypeArgs (TypePatternArg _ _) = True