{- |

Module : $Header$

Description : infer the kinds of types

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

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : experimental

Portability : portable

analyse types

-}

module HasCASL.TypeAna where

import HasCASL.As

import HasCASL.FoldType

import HasCASL.AsUtils

import HasCASL.Le

import HasCASL.ClassAna

import HasCASL.TypeMixAna

import qualified Data.Map as Map

import qualified Data.Set as Set

import Common.DocUtils

import Common.Id

import Common.Result

import Common.Utils

import Common.Lib.State

import Data.Maybe

import Data.List as List

import Control.Monad

-- * infer kind

-- | extract kinds of type identifier

getIdKind :: Env -> Id -> Result ((Variance, RawKind, Set.Set Kind), Type)

getIdKind te i =

case Map.lookup i $ localTypeVars te of

Nothing -> case Map.lookup i $ typeMap te of

Nothing -> mkError "unknown type" i

Just (TypeInfo rk l _ _) ->

return ((NonVar, rk, l), TypeName i rk 0)

Just (TypeVarDefn v vk rk c) ->

return ((v, rk, Set.singleton $ toKind vk), TypeName i rk c)

-- | extract kinds of co- or invariant type identifiers

getCoVarKind :: Maybe Bool -> Env -> Id

-> Result ((RawKind, Set.Set Kind), Type)

getCoVarKind b te i = do

((v, rk, l), ty) <- getIdKind te i

case (v, b) of

(ContraVar, Just True) -> Result

[mkDiag Hint "wrong contravariance of" i]

$ Just ((rk, Set.empty), ty)

(CoVar, Just False) -> Result

[mkDiag Hint "wrong covariance of" i]

$ Just ((rk, Set.empty), ty)

_ -> return ((rk, l), ty)

-- | check if there is at least one solution

subKinds :: DiagKind -> ClassMap -> Type -> Set.Set Kind -> Set.Set Kind

-> Set.Set Kind -> Result (Set.Set Kind)

subKinds dk cm ty sk ks res =

if Set.null $ Set.filter (flip (newKind cm) ks) sk then return res

else Result [Diag dk

("no kind found for '" ++ showDoc ty "'" ++

if Set.null ks then "" else expected sk ks)

$ getRange ty] $ if dk == Error then Nothing else Just Set.empty

-- | add an analysed type argument (warn on redeclared types)

addTypeVarDecl :: Bool -> TypeArg -> State Env ()

addTypeVarDecl warn (TypeArg i v vk rk c _ _) =

addLocalTypeVar warn (TypeVarDefn v vk rk c) i

addLocalTypeVar :: Bool -> TypeVarDefn -> Id -> State Env ()

addLocalTypeVar warn tvd i = do

e <- get

let tvs = localTypeVars e

when warn $ do

when (Map.member i $ typeMap e)

$ addDiags [mkDiag Warning

"type variable shadows type constructor" i]

when (Map.member i tvs)

$ addDiags [mkDiag Hint "rebound type variable" i]

when (Map.member i $ localVars e)

$ addDiags [mkDiag Warning

"type variable does not shadow normal variable" i]

putLocalTypeVars $ Map.insert i tvd tvs

-- | infer all minimal kinds

inferKinds :: Maybe Bool -> Type -> Env

-> Result ((RawKind, Set.Set Kind), Type)

inferKinds b ty te@Env {classMap = cm} = case ty of

TypeName i _ _ -> getCoVarKind b te i

TypeAppl t1 t2 -> do

((rk, ks), t3) <- inferKinds b t1 te

case rk of

FunKind v _ rr _ -> do

((_, l), t4) <- inferKinds (case v of

ContraVar -> Just $ maybe False not b

CoVar -> Just $ fromMaybe True b

_ -> Nothing) t2 te

kks <- mapM (getFunKinds cm) $ Set.toList ks

rs <- mapM ( \ fk -> case fk of

FunKind _ arg res _ -> subKinds Hint cm t2

(Set.singleton arg) l $ Set.singleton res

_ -> error "inferKinds: no function kind"

) $ Set.toList $ keepMinKinds cm kks

return ((rr, keepMinKinds cm rs), TypeAppl t3 t4)

_ -> mkError "unexpected type argument" t2

TypeAbs ta@(TypeArg _ v k r _ _ q) t ps -> do

let newEnv = execState (addTypeVarDecl False ta) te

((rk, ks), nt) <- inferKinds Nothing t newEnv

return (( FunKind v r rk q

, keepMinKinds cm

[Set.map (\ j -> FunKind v (toKind k) j q) ks])

, TypeAbs ta nt ps)

KindedType kt kind ps -> do

let Result ds _ = mapM (`anaKindM` cm) $ Set.toList kind

sk <- if null ds then return kind else Result ds Nothing

((rk, ks), t) <- inferKinds b kt te

l <- subKinds Hint cm kt sk ks sk

return ((rk, l), KindedType t sk ps)

ExpandedType t1 t2 -> do

((rk1, ks), t4) <- inferKinds b t2 te

((rk2, aks), t3) <- inferKinds b t1 te

rk <- maybe (Result (diffKindDiag ty rk1 rk2) Nothing) return

$ minRawKind "" rk1 rk2

return ((rk, keepMinKinds cm [aks, ks]), ExpandedType t3 t4)

_ -> error "inferKinds"

-- | extract the raw kind from a type term

rawKindOfType :: Type -> RawKind

rawKindOfType = foldType FoldTypeRec

{ foldTypeName = \ _ _ k _ -> k

, foldTypeAppl = \ _ ka _ -> case ka of

FunKind _ _ k _ -> k

_ -> error "rawKindOfType"

, foldExpandedType = \ _ k1 ->

fromMaybe (error "rawKindOfType.foldExpandedType") . minRawKind "" k1

, foldTypeAbs = \ _ (TypeArg _ v _ r _ _ _) -> FunKind v r

, foldKindedType = \ _ k _ _ -> k

, foldTypeToken = \ _ _ -> rStar

, foldBracketType = \ _ _ _ _ -> rStar

, foldMixfixType = \ _ _ -> rStar }

-- | subtyping relation

lesserType :: Env -> Type -> Type -> Bool

lesserType te t1 t2 = case (t1, t2) of

(KindedType t _ _, _) -> lesserType te t t2

(ExpandedType _ t, _) -> lesserType te t t2

(_, KindedType t _ _) -> lesserType te t1 t

(_, ExpandedType _ t) -> lesserType te t1 t

(TypeName {}, TypeAppl (TypeName l _ _) t) | l == lazyTypeId ->

lesserType te t1 t

(TypeAppl c1 a1, TypeAppl c2 a2) ->

let b1 = lesserType te a1 a2

b2 = lesserType te a2 a1

b = b1 && b2

in (case (rawKindOfType c1, rawKindOfType c2) of

(FunKind v1 _ _ _, FunKind v2 _ _ _) ->

if v1 == v2 then case v1 of

CoVar -> b1

ContraVar -> b2

_ -> b

else b

_ -> error "lesserType: no FunKind") && lesserType te c1 c2

|| case c2 of

(TypeName l _ _) | l == lazyTypeId -> lesserType te t1 a2

_ -> False

(TypeName i1 _ _, TypeName i2 _ _) | i1 == i2 -> True

(TypeName i k _, _) -> case Map.lookup i $ localTypeVars te of

Nothing -> case Map.lookup i $ typeMap te of

Nothing -> False

Just ti -> any ( \ j -> lesserType te (TypeName j k 0) t2) $

Set.toList $ superTypes ti

Just (TypeVarDefn _ vk _ _) -> case vk of

Downset t -> lesserType te t t2

_ -> False

(TypeAppl _ _, TypeName {}) -> False

(TypeAppl _ _, TypeAbs {}) -> False

(TypeAbs {}, TypeName {}) -> False

(t3, t4) -> t3 == t4

lesserTypeScheme :: Env -> TypeScheme -> TypeScheme -> Bool

lesserTypeScheme e (TypeScheme args1 t1 _) (TypeScheme args2 t2 _) =

null args1 && null args2 && lesserType e t1 t2

lesserOpInfo :: Env -> OpInfo -> OpInfo -> Bool

lesserOpInfo e o1 = lesserTypeScheme e (opType o1) . opType

-- | get operations by name removing super profiles

getMinAssumps :: Env -> Id -> [OpInfo]

getMinAssumps e i = keepMins (lesserOpInfo e) $ Set.toList

$ Map.findWithDefault Set.empty i $ assumps e

-- | type identifiers of a type

idsOf :: (Int -> Bool) -> Type -> Set.Set Id

idsOf b = Set.fromList . map (fst . snd) . leaves b

-- * super type ids

-- | compute super type ids of one type id

superIds :: TypeMap -> Id -> Set.Set Id

superIds tm = supIds tm Set.empty . Set.singleton

-- | compute all super type ids for several type ids given as second argument

supIds :: TypeMap -> Set.Set Id -> Set.Set Id -> Set.Set Id

supIds tm known new =

if Set.null new then known else

let more = Set.unions $ map ( \ i -> superTypes

$ Map.findWithDefault starTypeInfo i tm)

$ Set.toList new

newKnown = Set.union known new

in supIds tm newKnown (more Set.\\ newKnown)

-- * expand alias types

-- | expand aliases in a type scheme

expand :: TypeMap -> TypeScheme -> TypeScheme

expand = mapTypeOfScheme . expandAliases

filterAliases :: TypeMap -> TypeMap

filterAliases = Map.filter ( \ ti -> case typeDefn ti of

AliasTypeDefn _ -> True

_ -> False)

-- | expand aliases in a type and reduce type map first

expandAlias :: TypeMap -> Type -> Type

expandAlias = expandAliases . filterAliases

-- | expand aliases in a type if type map non-null

expandAliases :: TypeMap -> Type -> Type

expandAliases tm = if Map.null tm then id else expandAux tm

-- | expand aliases in a type

expandAux :: TypeMap -> Type -> Type

expandAux tm = replAlias $ \ i k n -> case Map.lookup i tm of

Just TypeInfo {typeDefn = AliasTypeDefn s} ->

ExpandedType (TypeName i k n) s

_ -> TypeName i k n

-- | find unexpanded alias identifier

hasAlias :: TypeMap -> Type -> [Diagnosis]

hasAlias tm t =

map ( \ i -> mkDiag Error ("unexpanded alias '" ++ showId i "' in") t)

$ Set.toList $ Set.intersection (idsOf (const True) t) $

Map.keysSet $ filterAliases tm

-- * resolve and analyse types

-- | resolve type and infer minimal kinds

anaTypeM :: (Maybe Kind, Type) -> Env -> Result ((RawKind, Set.Set Kind), Type)

anaTypeM (mk, parsedType) te =

do resolvedType <- mkTypeConstrAppl te parsedType

let tm = typeMap te

adj = adjustPos $ getRange parsedType

cm = classMap te

((rk, ks), checkedType) <- adj $ inferKinds Nothing resolvedType te

l <- adj $ case mk of

Nothing -> subKinds Error cm parsedType

(if Set.null ks then Set.singleton universe else ks) ks ks

Just k -> subKinds Error cm parsedType (Set.singleton k) ks $

Set.filter (flip (lesserKind cm) k) ks

let expandedType = expandAlias tm checkedType

Result (hasAlias tm expandedType) $ Just ()

return ((rk, l), expandedType)

-- | resolve the type and check if it is of the universe class

anaStarTypeM :: Type -> Env -> Result ((RawKind, Set.Set Kind), Type)

anaStarTypeM t = anaTypeM (Just universe, t)

-- * misc functions on types

-- | check if an id occurs in a type

cyclicType :: Id -> Type -> Bool

cyclicType i = Set.member i . idsOf (== 0)

-- | check for unbound (or if False for too many) type variables

unboundTypevars :: Bool -> [TypeArg] -> Type -> [Diagnosis]

unboundTypevars b args ty =

let fvs = freeTVarIds ty

argIds = map getTypeVar args

restVars1 = fvs List.\\ argIds

restVars2 = argIds List.\\ fvs

in (if null restVars1 then []

else [mkDiag Error ("unbound type variable(s)\n "

++ showSepList ("," ++) showId

restVars1 " in") ty])

++ if b || null restVars2 then [] else

[mkDiag Warning ("ignoring unused variable(s)\n "

++ showSepList ("," ++) showId

restVars2 " in") ty]

-- | check for proper generalizability (False: warn also for unused types)

generalizable :: Bool -> TypeScheme -> [Diagnosis]

generalizable b (TypeScheme args ty _) =

unboundTypevars b args ty ++ checkUniqueTypevars args

-- | check uniqueness of type variables

checkUniqueTypevars :: [TypeArg] -> [Diagnosis]

checkUniqueTypevars = checkUniqueness . map getTypeVar