1N/A{- |

1N/AModule : $Header$

1N/ACopyright : (c) Christian Maeder and Uni Bremen 2002-2003

1N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

1N/A

1N/AMaintainer : maeder@tzi.de

1N/AStability : provisional

1N/APortability : portable

1N/A

1N/Aanalyse type decls

1N/A

1N/A-}

1N/A

1N/Amodule HasCASL.TypeDecl where

1N/A

1N/Aimport Data.Maybe

1N/A

1N/Aimport Common.Lexer

1N/Aimport Common.Id

1N/Aimport Common.AS_Annotation

1N/Aimport Common.Lib.State

1N/Aimport qualified Common.Lib.Map as Map

1N/Aimport Common.Result

1N/Aimport Common.GlobalAnnotations

1N/A

1N/Aimport HasCASL.As

1N/Aimport HasCASL.Le

1N/Aimport HasCASL.ClassAna

1N/Aimport HasCASL.AsUtils

1N/Aimport HasCASL.TypeAna

1N/Aimport HasCASL.DataAna

1N/Aimport HasCASL.VarDecl

1N/Aimport HasCASL.TypeCheck

1N/A

1N/AidsToTypePatterns :: [Maybe (Id, [TypeArg])] -> [TypePattern]

1N/AidsToTypePatterns mis = map ( \ (i, tArgs) -> TypePattern i tArgs [] )

1N/A $ catMaybes mis

1N/A

1N/AanaFormula :: GlobalAnnos -> Annoted Term -> State Env (Maybe (Annoted Term))

1N/AanaFormula ga at =

1N/A do mt <- resolveTerm ga (Just unitType) $ item at

1N/A return $ case mt of Nothing -> Nothing

1N/A Just e -> Just at { item = e }

1N/A

1N/AanaVars :: Vars -> Type -> Result [VarDecl]

1N/AanaVars (Var v) t = return [VarDecl v t Other []]

1N/AanaVars (VarTuple vs _) t =

1N/A case unalias t of

1N/A ProductType ts _ ->

1N/A if length ts == length vs then

1N/A let lrs = zipWith anaVars vs ts

1N/A lms = map maybeResult lrs in

1N/A if all isJust lms then

1N/A return $ concatMap fromJust lms

1N/A else Result (concatMap diags lrs) Nothing

1N/A else mkError "wrong arity" t

1N/A _ -> mkError "product type expected" t

1N/A

1N/AmapAnMaybe :: (Monad m) => (a -> m (Maybe b)) -> [Annoted a] -> m [Annoted b]

1N/AmapAnMaybe f al =

1N/A do il <- mapAnM f al

1N/A return $ map ( \ a -> replaceAnnoted (fromJust $ item a) a) $

1N/A filter (isJust . item) il

1N/A

1N/AanaTypeItems :: GlobalAnnos -> GenKind -> Instance -> [Annoted TypeItem]

1N/A -> State Env [Annoted TypeItem]

1N/AanaTypeItems ga gk inst l = do

1N/A ul <- mapAnMaybe ana1TypeItem l

1N/A let tys = map ( \ (Datatype d) -> dataPatToType d) $

1N/A filter ( \ t -> case t of

1N/A Datatype _ -> True

1N/A _ -> False) $ map item ul

1N/A rl <- mapAnMaybe (anaTypeItem ga gk inst tys) ul

1N/A addDataSen tys

1N/A return rl

1N/A

1N/AaddDataSen :: [DataPat] -> State Env ()

1N/AaddDataSen tys = do

1N/A tm <- gets typeMap

1N/A let tis = map ( \ (i, _, _) -> i) tys

1N/A ds = foldr ( \ i dl -> case Map.lookup i tm of

1N/A Nothing -> dl

1N/A Just ti -> case typeDefn ti of

1N/A DatatypeDefn dd -> dd : dl

1N/A _ -> dl) [] tis

1N/A sen = NamedSen ("ga_" ++ showSepList (showString "_") showId tis "")

1N/A True $ DatatypeSen ds

1N/A if null tys then return () else appendSentences [sen]

1N/A

1N/Aana1TypeItem :: TypeItem -> State Env (Maybe TypeItem)

1N/Aana1TypeItem (Datatype d) =

1N/A do md <- ana1Datatype d

1N/A return $ fmap Datatype md

1N/Aana1TypeItem t = return $ Just t

1N/A

1N/A-- | analyse a 'TypeItem'

1N/AanaTypeItem :: GlobalAnnos -> GenKind -> Instance -> [DataPat] -> TypeItem

1N/A -> State Env (Maybe TypeItem)

1N/AanaTypeItem _ _ inst _ (TypeDecl pats kind ps) =

1N/A do cm <- gets classMap

1N/A let Result cs (Just rrk) = anaKindM kind cm

1N/A Result ds (Just is) = convertTypePatterns pats

1N/A addDiags $ cs ++ ds

1N/A let (rk, ak) = if null cs then (rrk, kind) else (star, star)

1N/A mis <- mapM (addTypePattern NoTypeDefn inst (rk, [ak])) is

1N/A let newPats = idsToTypePatterns mis

1N/A return $ if null newPats then Nothing else

1N/A Just $ TypeDecl newPats ak ps

1N/A

1N/AanaTypeItem _ _ inst _ (SubtypeDecl pats t ps) =

1N/A do let Result ds (Just is) = convertTypePatterns pats

1N/A addDiags ds

1N/A te <- get

1N/A let Result es mp = anaTypeM (Nothing, t) te

1N/A case mp of

1N/A Nothing -> do

1N/A mis <- mapM (addTypePattern NoTypeDefn inst (star, [star])) is

1N/A let newPats = idsToTypePatterns mis

1N/A if null newPats then return Nothing else case t of

1N/A TypeToken tt -> do

1N/A let tid = simpleIdToId tt

1N/A newT = TypeName tid star 0

1N/A addTypeId False NoTypeDefn inst star star tid

1N/A mapM_ (addSuperType newT) $ map fst is

1N/A return $ Just $ SubtypeDecl newPats newT ps

1N/A _ -> do

1N/A addDiags es

1N/A return $ Just $ TypeDecl newPats star ps

1N/A Just (ak, newT) -> do

1N/A mis <- mapM (addTypePattern NoTypeDefn inst ak) is

1N/A let newPats = idsToTypePatterns mis

1N/A mapM_ (addSuperType newT) $ map fst is

1N/A return $ if null newPats then Nothing else

1N/A Just $ SubtypeDecl newPats newT ps

1N/A

1N/AanaTypeItem _ _ inst _ (IsoDecl pats ps) =

1N/A do let Result ds (Just is) = convertTypePatterns pats

1N/A js = map fst is

1N/A addDiags ds

1N/A mis <- mapM (addTypePattern NoTypeDefn inst (star, [star])) is

1N/A mapM_ ( \ i -> mapM_ (addSuperType (TypeName i star 0)) js) js

1N/A return $ if null mis then Nothing else

1N/A Just $ IsoDecl (idsToTypePatterns mis) ps

1N/A

1N/AanaTypeItem ga _ inst _ (SubtypeDefn pat v t f ps) =

1N/A do let Result ds m = convertTypePattern pat

1N/A addDiags ds

1N/A case m of

1N/A Nothing -> return Nothing

1N/A Just (i, tArgs) -> do

1N/A tvs <- gets localTypeVars

1N/A newAs <- mapM anaddTypeVarDecl tArgs

1N/A mt <- anaStarType t

1N/A let nAs = catMaybes newAs

1N/A newPat = TypePattern i nAs []

1N/A case mt of

1N/A Nothing -> do

1N/A putLocalTypeVars tvs

1N/A return Nothing

1N/A Just ty -> do

1N/A newPty <- generalizeS $ TypeScheme nAs ty []

1N/A let fullKind = typeArgsListToKind nAs star

1N/A rk <- anaKind fullKind

1N/A let Result es mvds = anaVars v $ monoType ty

1N/A altDecl = Just $ AliasType newPat (Just fullKind)

1N/A newPty ps

1N/A altAct = do

1N/A putLocalTypeVars tvs

1N/A addTypeId True (AliasTypeDefn newPty) inst

1N/A rk fullKind i

1N/A return altDecl

1N/A addDiags es

1N/A if cyclicType i ty then do

1N/A addDiags [mkDiag Error

1N/A "illegal recursive subtype definition" ty]

1N/A putLocalTypeVars tvs

1N/A return Nothing

1N/A else case mvds of

1N/A Nothing -> altAct

1N/A Just vds -> do

1N/A checkUniqueVars vds

1N/A vs <- gets localVars

1N/A mapM_ (addLocalVar True) vds

1N/A mf <- anaFormula ga f

1N/A putLocalVars vs

1N/A case mf of

1N/A Nothing -> altAct

1N/A Just newF -> do

1N/A addTypeId True (Supertype v newPty

1N/A $ item newF)

1N/A inst rk fullKind i

1N/A addSuperType ty i

1N/A putLocalTypeVars tvs

1N/A return $ Just $ SubtypeDefn newPat v ty

1N/A newF ps

1N/A

1N/AanaTypeItem _ _ inst _ (AliasType pat mk sc ps) =

1N/A do let Result ds m = convertTypePattern pat

1N/A addDiags ds

1N/A case m of

1N/A Nothing -> return Nothing

1N/A Just (i, tArgs) -> do

1N/A tvs <- gets localTypeVars -- save variables

1N/A newAs <- mapM anaddTypeVarDecl tArgs

1N/A (ik, mt) <- anaPseudoType mk sc

1N/A let nAs = catMaybes newAs

1N/A case mt of

1N/A Nothing -> do putLocalTypeVars tvs

1N/A return Nothing

1N/A Just (TypeScheme args ty qs) ->

1N/A if cyclicType i ty then

1N/A do addDiags [mkDiag Error

1N/A "illegal recursive type synonym" ty]

1N/A putLocalTypeVars tvs

1N/A return Nothing

1N/A else do

1N/A let allArgs = nAs++args

1N/A fullKind = typeArgsListToKind nAs ik

1N/A allSc = TypeScheme allArgs ty qs

1N/A rk <- anaKind fullKind

1N/A newPty <- generalizeS allSc

1N/A putLocalTypeVars tvs

1N/A b <- addTypeId True (AliasTypeDefn newPty)

1N/A inst rk fullKind i

1N/A return $ if b then Just $ AliasType

1N/A (TypePattern i [] [])

1N/A (Just fullKind) newPty ps

1N/A else Nothing

1N/A

1N/AanaTypeItem _ gk inst tys (Datatype d) =

1N/A do mD <- anaDatatype gk inst tys d

1N/A case mD of

1N/A Nothing -> return Nothing

1N/A Just newD -> return $ Just $ Datatype newD

1N/A

1N/Aana1Datatype :: DatatypeDecl -> State Env (Maybe DatatypeDecl)

1N/Aana1Datatype (DatatypeDecl pat kind alts derivs ps) =

1N/A do cm <- gets classMap

1N/A let Result cs (Just rk) = anaKindM kind cm

1N/A k = if null cs then kind else star

1N/A addDiags $ checkKinds pat star rk ++ cs

1N/A let rms = map ( \ c -> anaKindM (ClassKind c) cm) derivs

1N/A mcs = map maybeResult rms

1N/A jcs = catMaybes mcs

1N/A newDerivs = map fst $ filter (isJust . snd) $ zip derivs mcs

1N/A Result ds m = convertTypePattern pat

1N/A addDiags (ds ++ concatMap diags rms)

1N/A addDiags $ concatMap (checkKinds pat star) jcs

1N/A case m of

1N/A Nothing -> return Nothing

1N/A Just (i, tArgs) -> do

1N/A tvs <- gets localTypeVars

1N/A newAs <- mapM anaddTypeVarDecl tArgs

1N/A putLocalTypeVars tvs

1N/A let nAs = catMaybes newAs

1N/A fullKind = typeArgsListToKind nAs k

1N/A addDiags $ checkUniqueTypevars nAs

1N/A frk <- anaKind fullKind

1N/A b <- addTypeId False PreDatatype Plain frk fullKind i

1N/A return $ if b then Just $ DatatypeDecl

1N/A (TypePattern i nAs []) k alts newDerivs ps else Nothing

1N/A

1N/AdataPatToType :: DatatypeDecl -> DataPat

1N/AdataPatToType (DatatypeDecl (TypePattern i nAs _) k _ _ _) =

1N/A (i, nAs, k)

1N/AdataPatToType _ = error "dataPatToType"

1N/A

1N/A-- | add a supertype to a given type id

1N/AaddSuperType :: Type -> Id -> State Env ()

1N/AaddSuperType t i =

1N/A do tm <- gets typeMap

1N/A case Map.lookup i tm of

1N/A Nothing -> return () -- previous error

1N/A Just (TypeInfo ok ks sups defn) ->

1N/A if any (== t) sups then

1N/A addDiags[mkDiag Hint "repeated supertype" t]

else putTypeMap $ Map.insert i

(TypeInfo ok ks (t:sups) defn) tm

addDataSubtype :: DataPat -> Type -> State Env ()

addDataSubtype dt st =

case st of

TypeName i _ _ -> addSuperType (typeIdToType dt) i

_ -> addDiags [mkDiag Warning "data subtype ignored" st]

-- | analyse a 'DatatypeDecl'

anaDatatype :: GenKind -> Instance -> [DataPat]

-> DatatypeDecl -> State Env (Maybe DatatypeDecl)

anaDatatype genKind inst tys

d@(DatatypeDecl (TypePattern i nAs _) k alts _ _) =

do let dt = dataPatToType d

fullKind = typeArgsListToKind nAs k

tvs <- gets localTypeVars

mapM_ (addTypeVarDecl False) nAs

mNewAlts <- fromResult $ anaAlts tys dt (map item alts)

case mNewAlts of

Nothing -> do

putLocalTypeVars tvs

return Nothing

Just newAlts -> do

mapM_ (addDataSubtype dt) $ foldr

( \ (Construct mc ts _ _) l -> case mc of

Nothing -> ts ++ l

Just _ -> l) [] newAlts

mapM_ ( \ (Construct mc tc p sels) -> case mc of

Nothing -> return ()

Just c -> do

let ty = TypeScheme nAs (getConstrType dt p tc) []

sc <- generalizeS ty

addOpId c sc [] (ConstructData i)

mapM_ ( \ (Select ms ts pa) -> case ms of

Just s -> addOpId s (getSelType dt pa ts) []

$ SelectData [ConstrInfo c sc] i

Nothing -> return False) $ concat sels) newAlts

let de = DataEntry Map.empty i genKind nAs newAlts

rk <- anaKind fullKind

addTypeId True (DatatypeDefn de) inst rk fullKind i

appendSentences $ makeDataSelEqs de k

putLocalTypeVars tvs

return $ Just d

anaDatatype _ _ _ _ = error "anaDatatype (not preprocessed)"

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

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

anaPseudoType mk (TypeScheme tArgs ty p) =

do cm <- gets classMap

let k = case mk of

Nothing -> Nothing

Just j -> let Result cs (Just rk) = anaKindM j cm

in Just $ if null cs then j else rk

nAs <- mapM anaddTypeVarDecl tArgs

let ntArgs = catMaybes nAs

mp <- anaType (Nothing, ty)

case mp of

Nothing -> return (star, Nothing)

Just ((_, sks), newTy) -> case sks of

[sk] -> do

let newK = typeArgsListToKind ntArgs sk

irk <- anaKind newK

case k of

Nothing -> return ()

Just j -> do grk <- anaKind j

addDiags $ checkKinds ty grk irk

return (newK, Just $ TypeScheme ntArgs newTy p)

_ -> return (star, Nothing)

-- | add a type pattern

addTypePattern :: TypeDefn -> Instance -> (RawKind, [Kind])

-> (Id, [TypeArg]) -> State Env (Maybe (Id, [TypeArg]))

addTypePattern defn inst (_, ks) (i, tArgs) =

nonUniqueKind ks i $ \ kind -> do

tvs <- gets localTypeVars

newAs <- mapM anaddTypeVarDecl tArgs

let nAs = catMaybes newAs

fullKind = typeArgsListToKind nAs kind

putLocalTypeVars tvs

addDiags $ checkUniqueTypevars nAs

frk <- anaKind fullKind

b <- addTypeId True defn inst frk fullKind i

return $ if b then Just (i, nAs) else Nothing

-- | convert type patterns

convertTypePatterns :: [TypePattern] -> Result [(Id, [TypeArg])]

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)

illegalTypePattern, illegalTypePatternArg, illegalTypeId

:: TypePattern -> Result a

illegalTypePattern tp = mkError "illegal type pattern" tp

illegalTypePatternArg tp = mkError "illegal type pattern argument" tp

illegalTypeId tp = mkError "illegal type pattern identifier" tp

-- | convert a 'TypePattern'

convertTypePattern :: TypePattern -> Result (Id, [TypeArg])

convertTypePattern (TypePattern t as _) = return (t, as)

convertTypePattern tp@(TypePatternToken t) =

if isPlace t then illegalTypePattern tp

else return (simpleIdToId t, [])

convertTypePattern tp@(MixfixTypePattern

[ra, ri@(TypePatternToken inTok), rb]) =

if head (tokStr inTok) `elem` signChars

then let inId = Id [Token place $ get_pos ra, inTok,

Token place $ get_pos rb] [] [] in

case (ra, rb) of

(TypePatternToken (Token "__" _),

TypePatternToken (Token "__" _)) -> return (inId, [])

_ -> do a <- convertToTypeArg ra

b <- convertToTypeArg rb

return (inId, [a, b])

else case ra of

TypePatternToken t1 -> do

a <- convertToTypeArg ri

b <- convertToTypeArg rb

return (simpleIdToId t1, [a, b])

_ -> illegalTypePattern tp

convertTypePattern tp@(MixfixTypePattern (TypePatternToken t1 : rp)) =

if isPlace t1 then

case rp of

[TypePatternToken inId, TypePatternToken t2] ->

if isPlace t2 && head (tokStr inId) `elem` signChars

then return (Id [t1,inId,t2] [] [], [])

else illegalTypePattern tp

_ -> illegalTypePattern tp

else case rp of

[BracketTypePattern Squares as@(_:_) ps] -> do

is <- mapM convertToId as

return (Id [t1] is ps, [])

_ -> do as <- mapM convertToTypeArg rp

return (simpleIdToId t1, as)

convertTypePattern (BracketTypePattern bk [ap] ps) =

case bk of

Parens -> convertTypePattern ap

_ -> let (o, c) = getBrackets bk

tid = Id [Token o ps, Token place $ get_pos ap,

Token c ps] [] [] in

case ap of

TypePatternToken t -> if isPlace t then

return (tid, [])

else return (tid, [TypeArg (simpleIdToId t) MissingKind Other []])

_ -> do a <- convertToTypeArg ap

return (tid, [a])

convertTypePattern tp = illegalTypePattern tp

convertToTypeArg :: TypePattern -> Result TypeArg

convertToTypeArg tp@(TypePatternToken t) =

if isPlace t then illegalTypePatternArg tp

else return $ TypeArg (simpleIdToId t) MissingKind Other []

convertToTypeArg (TypePatternArg a _) = return a

convertToTypeArg (BracketTypePattern Parens [tp] _) = convertToTypeArg tp

convertToTypeArg tp = illegalTypePatternArg tp

convertToId :: TypePattern -> Result Id

convertToId tp@(TypePatternToken t) =

if isPlace t then illegalTypeId tp

else return $ Id [t] [] []

convertToId (MixfixTypePattern []) = error "convertToId: MixfixTypePattern []"

convertToId (MixfixTypePattern (hd:tps)) =

if null tps then convertToId hd

else do

let (toks, comps) = break ( \ p ->

case p of BracketTypePattern Squares (_:_) _ -> True

_ -> False) tps

ts <- mapM convertToToks (hd:toks)

(is, ps) <- if null comps then return ([], [])

else convertToIds $ head comps

pls <- if null comps then return []

else mapM convertToPlace $ tail comps

return $ Id (concat ts ++ pls) is ps

convertToId tp = do

ts <- convertToToks tp

return $ Id ts [] []

convertToIds :: TypePattern -> Result ([Id], [Pos])

convertToIds (BracketTypePattern Squares tps@(_:_) ps) = do

is <- mapM convertToId tps

return (is, ps)

convertToIds tp = illegalTypeId tp

convertToToks :: TypePattern -> Result [Token]

convertToToks (TypePatternToken t) = return [t]

convertToToks (BracketTypePattern bk [tp] ps) = case bk of

Parens -> illegalTypeId tp

_ -> do let [o,c] = mkBracketToken bk ps

ts <- convertToToks tp

return (o : ts ++ [c])

convertToToks(MixfixTypePattern tps) = do

ts <- mapM convertToToks tps

return $ concat ts

convertToToks tp = illegalTypeId tp

convertToPlace :: TypePattern -> Result Token

convertToPlace tp@(TypePatternToken t) =

if isPlace t then return t

else illegalTypeId tp

convertToPlace tp = illegalTypeId tp