TypeAna.hs revision 3bffe0f10ad93403e36288a1a4a92d50356956b5
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{- |
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannModule : $Header$
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannDescription : infer the kinds of types
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannMaintainer : Christian.Maeder@dfki.de
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannStability : experimental
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannPortability : portable
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannanalyse types
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-}
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannmodule HasCASL.TypeAna where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HasCASL.As
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HasCASL.FoldType
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HasCASL.AsUtils
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HasCASL.Le
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HasCASL.ClassAna
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HasCASL.TypeMixAna
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport qualified Data.Map as Map
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport qualified Data.Set as Set
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.DocUtils
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Id
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Result
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Lib.State
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Data.List as List
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Data.Maybe
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Control.Monad
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- * infer kind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | extract kinds of type identifier
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetIdKind :: Env -> Id -> Result ((Variance, RawKind, Set.Set Kind), Type)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetIdKind te i =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann case Map.lookup i $ localTypeVars te of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> case Map.lookup i $ typeMap te of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> mkError "unknown type" i
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just (TypeInfo rk l _ _) ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann return ((NonVar, rk, l), TypeName i rk 0)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just (TypeVarDefn v vk rk c) ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann return ((v, rk, Set.singleton $ toKind vk), TypeName i rk c)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | extract kinds of co- or invariant type identifiers
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetCoVarKind :: Maybe Bool -> Env -> Id
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -> Result ((RawKind, Set.Set Kind), Type)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanngetCoVarKind b te i = do
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ((v, rk, l), ty) <- getIdKind te i
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann case (v, b) of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (ContraVar, Just True) -> Result
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann [mkDiag Hint "wrong contravariance of" i]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ Just ((rk, Set.empty), ty)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (CoVar, Just False) -> Result
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann [mkDiag Hint "wrong covariance of" i]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ Just ((rk, Set.empty), ty)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> return ((rk, l), ty)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | check if there is at least one solution
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsubKinds :: DiagKind -> ClassMap -> Type -> Set.Set Kind -> Set.Set Kind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -> Set.Set Kind -> Result (Set.Set Kind)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsubKinds dk cm ty sk ks res =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann if Set.null $ Set.filter (flip (newKind cm) ks) sk then return res
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann else Result [Diag dk
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ("no kind found for '" ++ showDoc ty "'" ++
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann if Set.null ks then "" else expected sk ks)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ getRange ty] $ Just Set.empty
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | add an analysed type argument (warn on redeclared types)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannaddTypeVarDecl :: Bool -> TypeArg -> State Env ()
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannaddTypeVarDecl warn (TypeArg i v vk rk c _ _) =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann addLocalTypeVar warn (TypeVarDefn v vk rk c) i
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannaddLocalTypeVar :: Bool -> TypeVarDefn -> Id -> State Env ()
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannaddLocalTypeVar warn tvd i = do
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann e <- get
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let tvs = localTypeVars e
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann when warn $ do
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann when (Map.member i $ typeMap e)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ addDiags [mkDiag Warning
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann "type variable shadows type constructor" i]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann when (Map.member i tvs)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ addDiags [mkDiag Hint "rebound type variable" i]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann when (Map.member i $ localVars e)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ addDiags [mkDiag Warning
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann "type variable does not shadow normal variable" i]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann putLocalTypeVars $ Map.insert i tvd tvs
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | infer all minimal kinds
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanninferKinds :: Maybe Bool -> Type -> Env
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -> Result ((RawKind, Set.Set Kind), Type)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanninferKinds b ty te@Env{classMap = cm} = case ty of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann TypeName i _ _ -> getCoVarKind b te i
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann TypeAppl t1 t2 -> do
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ((rk, ks), t3) <- inferKinds b t1 te
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann case rk of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann FunKind v _ rr _ -> do
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ((_, l), t4) <- inferKinds (case v of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ContraVar -> Just $ maybe False not b
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann CoVar -> Just $ maybe True id b
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> Nothing) t2 te
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann kks <- mapM (getFunKinds cm) $ Set.toList ks
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann rs <- mapM ( \ fk -> case fk of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann FunKind _ arg res _ -> subKinds Hint cm t2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (Set.singleton arg) l $ Set.singleton res
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> error "inferKinds: no function kind"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ) $ Set.toList $ keepMinKinds cm kks
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann return ((rr, keepMinKinds cm rs), TypeAppl t3 t4)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> mkError "unexpected type argument" t2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann TypeAbs ta@(TypeArg _ v k r _ _ q) t ps -> do
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let newEnv = execState (addTypeVarDecl False ta) te
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ((rk, ks), nt) <- inferKinds Nothing t newEnv
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann return (( FunKind v r rk q
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , keepMinKinds cm
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann [Set.map (\ j -> FunKind v (toKind k) j q) ks])
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , TypeAbs ta nt ps)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann KindedType kt kind ps -> do
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let Result ds _ = mapM (flip anaKindM cm) $ Set.toList kind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sk <- if null ds then return kind else Result ds Nothing
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ((rk, ks), t) <- inferKinds b kt te
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann l <- subKinds Hint cm kt sk ks sk
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann return ((rk, l), KindedType t sk ps)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ExpandedType t1 t2 -> do
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ((rk1, ks), t4) <- inferKinds b t2 te
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ((rk2, aks), t3) <- inferKinds b t1 te
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann rk <- maybe (Result (diffKindDiag ty rk1 rk2) Nothing) return
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ minRawKind "" rk1 rk2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann return ((rk, keepMinKinds cm [aks, ks]), ExpandedType t3 t4)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> error "inferKinds"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | extract the raw kind from a type term
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannrawKindOfType :: Type -> RawKind
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannrawKindOfType = foldType FoldTypeRec
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann { foldTypeName = \ _ _ k _ -> k
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , foldTypeAppl = \ _ ka _ -> case ka of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann FunKind _ _ k _ -> k
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> error "rawKindOfType"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , foldExpandedType = \ _ k1 k2 ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann maybe (error "rawKindOfType.foldExpandedType") id $ minRawKind "" k1 k2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , foldTypeAbs = \ _ (TypeArg _ v _ r _ _ _) k p ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann FunKind v r k p
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , foldKindedType = \ _ k _ _ -> k
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , foldTypeToken = \ _ _ -> error "rawKindOfType.foldTypeToken"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , foldBracketType = \ _ _ _ _ -> error "rawKindOfType.foldBracketType"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , foldMixfixType = \ _ -> error "rawKindOfType.foldMixfixType" }
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | subtyping relation
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannlesserType :: Env -> Type -> Type -> Bool
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannlesserType te t1 t2 = case (t1, t2) of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (KindedType t _ _, _) -> lesserType te t t2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (ExpandedType _ t, _) -> lesserType te t t2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (_, KindedType t _ _) -> lesserType te t1 t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (_, ExpandedType _ t) -> lesserType te t1 t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (TypeName _ _ _, TypeAppl (TypeName l _ _) t) | l == lazyTypeId ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann lesserType te t1 t
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (TypeAppl c1 a1, TypeAppl c2 a2) ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let b1 = lesserType te a1 a2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann b2 = lesserType te a2 a1
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann b = b1 && b2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in (case (rawKindOfType c1, rawKindOfType c2) of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (FunKind v1 _ _ _, FunKind v2 _ _ _) ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann if v1 == v2 then case v1 of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann CoVar -> b1
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ContraVar -> b2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> b
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann else b
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> error "lesserType: no FunKind") && lesserType te c1 c2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann || case c2 of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (TypeName l _ _) | l == lazyTypeId -> lesserType te t1 a2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> False
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (TypeName i1 _ _, TypeName i2 _ _) | i1 == i2 -> True
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (TypeName i k _, _) -> case Map.lookup i $ localTypeVars te of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> case Map.lookup i $ typeMap te of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> False
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just ti -> any ( \ j -> lesserType te (TypeName j k 0) t2) $
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Set.toList $ superTypes ti
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just (TypeVarDefn _ vk _ _) -> case vk of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Downset t -> lesserType te t t2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> False
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (TypeAppl _ _, TypeName _ _ _) -> False
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (TypeAppl _ _, TypeAbs _ _ _) -> False
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (TypeAbs _ _ _, TypeName _ _ _) -> False
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (t3, t4) -> t3 == t4
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | type identifiers of a type
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannidsOf :: (Int -> Bool) -> Type -> Set.Set Id
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannidsOf b = Set.fromList . map (fst . snd) . leaves b
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- * super type ids
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | compute super type ids of one type id
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsuperIds :: TypeMap -> Id -> Set.Set Id
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsuperIds tm = supIds tm Set.empty . Set.singleton
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | compute all super type ids for several type ids given as second argument
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsupIds :: TypeMap -> Set.Set Id -> Set.Set Id -> Set.Set Id
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannsupIds tm known new =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann if Set.null new then known else
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let more = Set.unions $ map ( \ i -> superTypes
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ Map.findWithDefault starTypeInfo i tm)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ Set.toList new
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann newKnown = Set.union known new
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in supIds tm newKnown (more Set.\\ newKnown)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- * expand alias types
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | expand aliases in a type scheme
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannexpand :: TypeMap -> TypeScheme -> TypeScheme
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannexpand = mapTypeOfScheme . expandAliases
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannfilterAliases :: TypeMap -> TypeMap
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannfilterAliases = Map.filter ( \ ti -> case typeDefn ti of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann AliasTypeDefn _ -> True
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> False)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | expand aliases in a type and reduce type map first
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannexpandAlias :: TypeMap -> Type -> Type
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannexpandAlias = expandAliases . filterAliases
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | expand aliases in a type if type map non-null
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannexpandAliases :: TypeMap -> Type -> Type
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannexpandAliases tm = if Map.null tm then id else expandAux tm
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | expand aliases in a type
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannexpandAux :: TypeMap -> Type -> Type
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannexpandAux tm ty = replAlias ( \ i k n ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann case Map.lookup i tm of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just TypeInfo {typeDefn = AliasTypeDefn s} ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ExpandedType (TypeName i k n) s
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> TypeName i k n) ty
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | find unexpanded alias identifier
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannhasAlias :: TypeMap -> Type -> [Diagnosis]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannhasAlias tm t =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map ( \ i -> mkDiag Error ("unexpanded alias '" ++ showId i "' in") t)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ Set.toList $ Set.intersection (idsOf (const True) t) $
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Map.keysSet $ filterAliases tm
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- * resolve and analyse types
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | resolve type and infer minimal kinds
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannanaTypeM :: (Maybe Kind, Type) -> Env -> Result ((RawKind, Set.Set Kind), Type)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannanaTypeM (mk, parsedType) te =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann do resolvedType <- mkTypeConstrAppl te parsedType
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let tm = typeMap te
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann adj = adjustPos $ getRange parsedType
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann cm = classMap te
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ((rk, ks), checkedType) <- adj $ inferKinds Nothing resolvedType te
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann l <- adj $ case mk of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Nothing -> subKinds Error cm parsedType
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (if Set.null ks then Set.singleton universe else ks) ks ks
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just k -> subKinds Error cm parsedType (Set.singleton k) ks $
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Set.filter (flip (lesserKind cm) k) ks
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let expandedType = expandAlias tm checkedType
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Result (hasAlias tm expandedType) $ Just ()
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann return ((rk, l), expandedType)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | resolve the type and check if it is of the universe class
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannanaStarTypeM :: Type -> Env -> Result ((RawKind, Set.Set Kind), Type)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannanaStarTypeM t = anaTypeM (Just universe, t)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- * misc functions on types
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | check if an id occurs in a type
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanncyclicType :: Id -> Type -> Bool
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanncyclicType i ty = Set.member i $ idsOf (==0) ty
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | check for unbound (or if False for too many) type variables
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannunboundTypevars :: Bool -> [TypeArg] -> Type -> [Diagnosis]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannunboundTypevars b args ty =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let fvs = freeTVarIds ty
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann argIds = map getTypeVar args
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann restVars1 = fvs List.\\ argIds
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann restVars2 = argIds List.\\ fvs
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann in (if null restVars1 then []
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann else [mkDiag Error ("unbound type variable(s)\n "
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ showSepList ("," ++) showId
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann restVars1 " in") ty])
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ if b || null restVars2 then [] else
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann [mkDiag Warning ("ignoring unused variable(s)\n "
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ showSepList ("," ++) showId
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann restVars2 " in") ty]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | check for proper generalizability (False: warn also for unused types)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanngeneralizable :: Bool -> TypeScheme -> [Diagnosis]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanngeneralizable b (TypeScheme args ty _) =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann unboundTypevars b args ty ++ checkUniqueTypevars args
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- | check uniqueness of type variables
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanncheckUniqueTypevars :: [TypeArg] -> [Diagnosis]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanncheckUniqueTypevars = checkUniqueness . map getTypeVar
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann