{- |

Module : $Header$

Copyright : (c) Christian Maeder and Uni Bremen 2002-2005

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : maeder@tzi.de

Stability : provisional

Portability : portable

analyse type decls

-}

module HasCASL.TypeDecl where

import Data.Maybe

import Common.Lexer

import Common.Id

import Common.AS_Annotation

import Common.Lib.State

import qualified Common.Lib.Map as Map

import Common.Result

import Common.GlobalAnnotations

import HasCASL.As

import HasCASL.AsUtils

import HasCASL.Le

import HasCASL.ClassAna

import HasCASL.TypeAna

import HasCASL.DataAna

import HasCASL.Unify

import HasCASL.VarDecl

import HasCASL.TypeCheck

idsToTypePatterns :: [Maybe (Id, [TypeArg])] -> [TypePattern]

idsToTypePatterns mis = map ( \ (i, tArgs) -> TypePattern i tArgs [] )

$ catMaybes mis

anaFormula :: GlobalAnnos -> Annoted Term -> State Env (Maybe (Annoted Term))

anaFormula ga at =

do mt <- resolveTerm ga (Just unitType) $ item at

return $ case mt of Nothing -> Nothing

Just e -> Just at { item = e }

anaVars :: Vars -> Type -> Result [VarDecl]

anaVars (Var v) t = return [VarDecl v t Other []]

anaVars (VarTuple vs _) t =

case unalias t of

ProductType ts _ ->

if length ts == length vs then

let lrs = zipWith anaVars vs ts

lms = map maybeResult lrs in

if all isJust lms then

return $ concatMap fromJust lms

else Result (concatMap diags lrs) Nothing

else mkError "wrong arity" t

_ -> mkError "product type expected" t

mapAnMaybe :: (Monad m) => (a -> m (Maybe b)) -> [Annoted a] -> m [Annoted b]

mapAnMaybe f al =

do il <- mapAnM f al

return $ map ( \ a -> replaceAnnoted (fromJust $ item a) a) $

filter (isJust . item) il

anaTypeItems :: GlobalAnnos -> GenKind -> Instance -> [Annoted TypeItem]

-> State Env [Annoted TypeItem]

anaTypeItems ga gk inst l = do

ul <- mapAnMaybe ana1TypeItem l

tys <- mapM ( \ (Datatype d) -> dataPatToType d) $

filter ( \ t -> case t of

Datatype _ -> True

_ -> False) $ map item ul

rl <- mapAnMaybe (anaTypeItem ga gk inst tys) ul

addDataSen tys

return rl

addDataSen :: [DataPat] -> State Env ()

addDataSen tys = do

tm <- gets typeMap

let tis = map ( \ (DataPat i _ _ _) -> i) tys

ds = foldr ( \ i dl -> case Map.lookup i tm of

Nothing -> dl

Just ti -> case typeDefn ti of

DatatypeDefn dd -> dd : dl

_ -> dl) [] tis

sen = NamedSen ("ga_" ++ showSepList (showString "_") showId tis "")

True $ DatatypeSen ds

if null tys then return () else appendSentences [sen]

ana1TypeItem :: TypeItem -> State Env (Maybe TypeItem)

ana1TypeItem (Datatype d) =

do md <- ana1Datatype d

return $ fmap Datatype md

ana1TypeItem t = return $ Just t

-- | analyse a 'TypeItem'

anaTypeItem :: GlobalAnnos -> GenKind -> Instance -> [DataPat] -> TypeItem

-> State Env (Maybe TypeItem)

anaTypeItem _ _ inst _ (TypeDecl pats kind ps) =

do cm <- gets classMap

let Result cs (Just rrk) = anaKindM kind cm

Result ds (Just is) = convertTypePatterns pats

addDiags $ cs ++ ds

let (rk, ak) = if null cs then (rrk, kind) else (star, star)

mis <- mapM (addTypePattern NoTypeDefn inst (rk, [ak])) is

let newPats = idsToTypePatterns mis

return $ if null newPats then Nothing else

Just $ TypeDecl newPats ak ps

anaTypeItem _ _ inst _ (SubtypeDecl pats t ps) =

do let Result ds (Just is) = convertTypePatterns pats

addDiags ds

te <- get

let Result es mp = anaTypeM (Nothing, t) te

case mp of

Nothing -> do

mis <- mapM (addTypePattern NoTypeDefn inst (star, [star])) is

let newPats = idsToTypePatterns mis

if null newPats then return Nothing else case t of

TypeToken tt -> do

let tid = simpleIdToId tt

newT = TypeName tid star 0

addTypeId False NoTypeDefn inst star star tid

mapM_ (addSuperType newT) $ map fst is

return $ Just $ SubtypeDecl newPats newT ps

_ -> do

addDiags es

return $ Just $ TypeDecl newPats star ps

Just (ak, newT) -> do

mis <- mapM (addTypePattern NoTypeDefn inst ak) is

let newPats = idsToTypePatterns mis

mapM_ (addSuperType newT) $ map fst is

return $ if null newPats then Nothing else

Just $ SubtypeDecl newPats newT ps

anaTypeItem _ _ inst _ (IsoDecl pats ps) =

do let Result ds (Just is) = convertTypePatterns pats

js = map fst is

addDiags ds

mis <- mapM (addTypePattern NoTypeDefn inst (star, [star])) is

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

return $ if null mis then Nothing else

Just $ IsoDecl (idsToTypePatterns mis) ps

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

do let Result ds m = convertTypePattern pat

addDiags ds

case m of

Nothing -> return Nothing

Just (i, tArgs) -> do

tvs <- gets localTypeVars

newAs <- mapM anaddTypeVarDecl tArgs

mt <- anaStarType t

let nAs = catMaybes newAs

newPat = TypePattern i nAs []

case mt of

Nothing -> do

putLocalTypeVars tvs

return Nothing

Just ty -> do

newPty <- generalizeS $ TypeScheme nAs ty []

let fullKind = typeArgsListToKind nAs star

rk <- anaKind fullKind

let Result es mvds = anaVars v $ monoType ty

altDecl = Just $ AliasType newPat (Just fullKind)

newPty ps

altAct = do

putLocalTypeVars tvs

addTypeId True (AliasTypeDefn newPty) inst

rk fullKind i

return altDecl

addDiags es

if cyclicType i ty then do

addDiags [mkDiag Error

"illegal recursive subtype definition" ty]

putLocalTypeVars tvs

return Nothing

else case mvds of

Nothing -> altAct

Just vds -> do

checkUniqueVars vds

vs <- gets localVars

mapM_ (addLocalVar True) vds

mf <- anaFormula ga f

putLocalVars vs

case mf of

Nothing -> altAct

Just newF -> do

addTypeId True (Supertype v newPty

$ item newF)

inst rk fullKind i

addSuperType ty i

putLocalTypeVars tvs

return $ Just $ SubtypeDefn newPat v ty

newF ps

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

do let Result ds m = convertTypePattern pat

addDiags ds

case m of

Nothing -> return Nothing

Just (i, tArgs) -> do

tvs <- gets localTypeVars -- save variables

newAs <- mapM anaddTypeVarDecl tArgs

(ik, mt) <- anaPseudoType mk sc

let nAs = catMaybes newAs

case mt of

Nothing -> do putLocalTypeVars tvs

return Nothing

Just (TypeScheme args ty qs) ->

if cyclicType i ty then

do addDiags [mkDiag Error

"illegal recursive type synonym" ty]

putLocalTypeVars tvs

return Nothing

else do

let allArgs = nAs++args

fullKind = typeArgsListToKind nAs ik

allSc = TypeScheme allArgs ty qs

rk <- anaKind fullKind

newPty <- generalizeS allSc

putLocalTypeVars tvs

b <- addTypeId True (AliasTypeDefn newPty)

inst rk fullKind i

return $ if b then Just $ AliasType

(TypePattern i [] [])

(Just fullKind) newPty ps

else Nothing

anaTypeItem _ gk inst tys (Datatype d) =

do mD <- anaDatatype gk inst tys d

case mD of

Nothing -> return Nothing

Just newD -> return $ Just $ Datatype newD

ana1Datatype :: DatatypeDecl -> State Env (Maybe DatatypeDecl)

ana1Datatype (DatatypeDecl pat kind alts derivs ps) =

do cm <- gets classMap

let Result cs (Just rk) = anaKindM kind cm

k = if null cs then kind else star

addDiags $ checkKinds pat star rk ++ cs

let rms = map ( \ c -> anaKindM (ClassKind c) cm) derivs

mcs = map maybeResult rms

jcs = catMaybes mcs

newDerivs = map fst $ filter (isJust . snd) $ zip derivs mcs

Result ds m = convertTypePattern pat

addDiags (ds ++ concatMap diags rms)

addDiags $ concatMap (checkKinds pat star) jcs

case m of

Nothing -> return Nothing

Just (i, tArgs) -> do

tvs <- gets localTypeVars

newAs <- mapM anaddTypeVarDecl tArgs

putLocalTypeVars tvs

let nAs = catMaybes newAs

fullKind = typeArgsListToKind nAs k

addDiags $ checkUniqueTypevars nAs

frk <- anaKind fullKind

b <- addTypeId False PreDatatype Plain frk fullKind i

return $ if b then Just $ DatatypeDecl

(TypePattern i nAs []) k alts newDerivs ps else Nothing

dataPatToType :: DatatypeDecl -> State Env DataPat

dataPatToType (DatatypeDecl (TypePattern i nAs _) k _ _ _) = do

rk <- anaKind k

return $ DataPat i nAs rk $ patToType i nAs rk

dataPatToType _ = error "dataPatToType"

-- | add a supertype to a given type id

addSuperType :: Type -> Id -> State Env ()

addSuperType t i =

do tm <- gets typeMap

case Map.lookup i tm of

Nothing -> return () -- previous error

Just (TypeInfo ok ks sups defn) ->

if any (== t) sups then

addDiags[mkDiag Hint "repeated supertype" t]

else putTypeMap $ Map.insert i

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

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

addDataSubtype (DataPat _ _ _ rt) st =

case st of

TypeName i _ _ -> addSuperType rt 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 dt@(DataPat _ _ rk rt) <- dataPatToType d

let fullKind = typeArgsListToKind nAs k

frk <- anaKind fullKind

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 srt = generalize nAs rt

sc = TypeScheme nAs

(getConstrType srt p tc) []

addOpId c sc [] (ConstructData i)

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

Just s -> do

let selSc = TypeScheme nAs

(getSelType srt pa ts) []

addOpId s selSc []

$ SelectData [ConstrInfo c sc] i

Nothing -> return False) $ concat sels) newAlts

let de = DataEntry Map.empty i genKind (genTypeArgs nAs) rk newAlts

addTypeId True (DatatypeDefn de) inst frk fullKind i

appendSentences $ makeDataSelEqs de rt

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

star 0 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 star 0 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