80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major{- |

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajorModule : $Header$

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajorCopyright : (c) Christian Maeder and Uni Bremen 2003

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajorLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajorMaintainer : hets@tzi.de

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajorStability : experimental

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajorPortability : portable

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major analyse types

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major-}

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majormodule HasCASL.TypeAna where

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majorimport HasCASL.As

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majorimport HasCASL.AsUtils

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majorimport HasCASL.ClassAna

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majorimport HasCASL.Le

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majorimport HasCASL.Unify

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majorimport Data.List

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majorimport Data.Maybe

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majorimport qualified Common.Lib.Map as Map

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majorimport qualified Common.Lib.Set as Set

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majorimport Common.Id

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majorimport Common.Result

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majorimport Common.Lib.State

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Majordata ApplMode = OnlyArg | TopLevel

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajormkTypeConstrAppls :: ApplMode -> Type -> State Env (Maybe Type)

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajormkTypeConstrAppls _ t@(TypeName _ _ _) =

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major return $ Just t

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajormkTypeConstrAppls m (TypeAppl t1 t2) =

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major do mt3 <- mkTypeConstrAppls m t1

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major mt4 <- mkTypeConstrAppls OnlyArg t2

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major case (mt3, mt4) of

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major (Just t3, Just t4) -> return $ Just $ TypeAppl t3 t4

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major _ -> return Nothing

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajormkTypeConstrAppls _ (TypeToken t) =

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major do let i = simpleIdToId t

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major tk <- gets typeMap

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major let m = getKind tk i

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major c = if isTypeVar tk i then 1 else 0

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major case m of

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major Just k -> return $ Just $ TypeName i k c

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major _ -> do addDiags [mkDiag Error "unknown type" t]

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major return Nothing

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajormkTypeConstrAppls m t@(BracketType b ts ps) =

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major do mArgs <- mapM (mkTypeConstrAppls m) ts

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major if all isJust mArgs then

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major do let err = do addDiags [mkDiag Error "illegal type" t]

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major return Nothing

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major case catMaybes mArgs of

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major [x] -> case b of

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major Parens -> return $ Just x

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major _ -> do let [o,c] = mkBracketToken b ps

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major i = Id [o, Token place $ posOfType

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major $ head ts, c] [] []

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major tk <- gets typeMap

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major case getKind tk i of

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major Nothing -> err

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major Just k -> return $ Just $ TypeAppl

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major (TypeName i k 0) x

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major _ -> err

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major else return Nothing

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajormkTypeConstrAppls _ (MixfixType []) = error "mkTypeConstrAppl (MixfixType [])"

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajormkTypeConstrAppls _ (MixfixType (f:a)) =

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major do mF <- mkTypeConstrAppls TopLevel f

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major case mF of

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major Nothing -> return Nothing

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major Just newF ->

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major do mA <- mapM (mkTypeConstrAppls OnlyArg) a

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major if all isJust mA then

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major return $ Just $ foldl1 TypeAppl $ newF : catMaybes mA

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major else return Nothing

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajormkTypeConstrAppls m (KindedType t k p) =

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major do mT <- mkTypeConstrAppls m t

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major return $ fmap ( \ newT -> KindedType newT k p ) mT

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajormkTypeConstrAppls _ (LazyType t p) =

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major do mT <- mkTypeConstrAppls TopLevel t

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major return $ fmap ( \ newT -> LazyType newT p ) mT

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajormkTypeConstrAppls _ (ProductType ts ps) =

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major do mTs <- mapM (mkTypeConstrAppls TopLevel) ts

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major if all isJust mTs then

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major return $ Just $ ProductType (catMaybes mTs) ps

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major else return Nothing

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajormkTypeConstrAppls _ (FunType t1 a t2 ps) =

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major do mT1 <- mkTypeConstrAppls TopLevel t1

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major mT2 <- mkTypeConstrAppls TopLevel t2

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major case (mT1, mT2) of

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major (Just newT1, Just newT2) ->

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major return $ Just $ FunType newT1 a newT2 ps

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major _ -> return Nothing

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajorexpandApplKind :: Class -> State Env Kind

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajorexpandApplKind c =

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major case c of

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major Intersection s _ -> if Set.isEmpty s then return star else

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major do mk <- anaClassId $ Set.findMin s

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major case mk of

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major Just k -> case k of

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major ExtClass c2 _ _ -> expandApplKind c2

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major _ -> return k

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major Nothing -> error "expandApplKind"

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major _ -> return star

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajorinferKind :: Type -> State Env Kind

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajorinferKind (TypeName i _ _) = do j <- getIdKind i

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major return j

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter MajorinferKind (TypeAppl t1 t2) =

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major do mk1 <- inferKind t1

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major case mk1 of

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major KindAppl k1 k2 _ -> do checkTypeKind t2 k1

80ca0b9f5ad61b2335af25d4dcf25a04ebfcbc91Peter Major return k2

ExtClass c _ _ ->

do k <- expandApplKind c

case k of

KindAppl k1 k2 _ -> do checkTypeKind t2 k1

return k2

_ -> do addDiags

[mkDiag Error

"incompatible kind of type"

t1]

return star

inferKind (FunType t1 _ t2 _) =

do checkTypeKind t1 star

checkTypeKind t2 star

return star

inferKind (ProductType ts _) =

do mapM_ ( \ t -> checkTypeKind t star) ts

return star

inferKind (LazyType t _) =

do checkTypeKind t star

return star

inferKind (TypeToken t) = getIdKind $ simpleIdToId t

inferKind (KindedType t k _) =

do checkTypeKind t k

return k

inferKind t =

do addDiags [mkDiag Error "unresolved type" t]

return star

checkTypeKind :: Type -> Kind -> State Env ()

checkTypeKind t j = do k <- inferKind t

checkKinds t j k

getIdKind :: Id -> State Env Kind

getIdKind i =

do tk <- gets typeMap

let m = getKind tk i

case m of

Nothing -> do addDiags [mkDiag Error "undeclared type" i]

return star

Just k -> return k

getKind :: TypeMap -> Id -> Maybe Kind

getKind tk i =

case Map.lookup i tk of

Nothing -> Nothing

Just (TypeInfo k _ _ _) -> Just k

isTypeVar :: TypeMap -> Id -> Bool

isTypeVar tk i =

case Map.lookup i tk of

Just (TypeInfo _ _ _ TypeVarDefn) -> True

_ -> False

anaType :: (Kind, Type) -> State Env (Kind, Maybe Type)

anaType (k, t) =

do mT <- mkTypeConstrAppls TopLevel t

tm <- gets typeMap

case mT of

Nothing -> return (star, mT)

Just nt -> do let (newT,_) = expandAlias tm nt

newK <- inferKind newT

checkKinds newT newK k

return (newK, Just newT)

anaStarType :: Type -> State Env (Maybe Type)

anaStarType t = fmap snd $ anaType (star, t)

mkBracketToken :: BracketKind -> [Pos] -> [Token]

mkBracketToken k ps =

if null ps then mkBracketToken k [nullPos]

else zipWith Token ((\ (o,c) -> [o,c]) $ getBrackets k)

[head ps, last ps]