TypeAna.hs revision 81946e2b3f6dde6167f48769bd02c7a634736856
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian MaederModule : $Header$
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiMaintainer : maeder@tzi.de
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederStability : experimental
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederPortability : portable
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport qualified Common.Lib.Map as Map
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport qualified Common.Lib.Set as Set
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder-- * infer kind
cf31aaf25d0fe96b0578755e7ee18b732e337343Christian Maeder-- | inspect types and classes only
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedertype TypeEnv = Env
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | extract kinds of type identifier
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskigetIdKind :: TypeEnv -> Id -> Result ((Variance, RawKind, [Kind]), Type)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskigetIdKind te i =
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski case Map.lookup i $ localTypeVars te of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Nothing -> case Map.lookup i $ typeMap te of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Nothing -> mkError "unknown type" i
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Just (TypeInfo rk l _ _) -> return ((InVar, rk, l), TypeName i rk 0)
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder Just (TypeVarDefn v vk rk c) -> assert (c > 0) $
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder return ((v, rk, [toKind vk]), TypeName i rk c)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | extract kinds of co- or invariant type identifiers
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedergetCoVarKind :: Maybe Bool -> TypeEnv -> Id -> Result ((RawKind, [Kind]), Type)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedergetCoVarKind b te i = do
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ((v, rk, l), ty) <- getIdKind te i
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder case (v, b) of
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (ContraVar, Just True) -> Result
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder [mkDiag Hint "wrong contravariance of" i] $ Just ((rk, []), ty)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (CoVar, Just False) -> Result
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder [mkDiag Hint "wrong covariance of" i] $ Just ((rk, []), ty)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski _ -> return ((rk, keepMinKinds (classMap te) l), ty)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | check if there is at least one solution
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskisubKinds :: DiagKind -> ClassMap -> Type -> Kind -> [Kind] -> [Kind]
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -> Result [Kind]
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskisubKinds dk cm ty sk ks res =
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski if any ( \ k -> lesserKind cm k sk) ks then return res
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski else Result [Diag dk
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski ("no kind found for '" ++ showPretty ty "'" ++
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder if null ks then "" else expected sk $ head ks)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder $ posOfType ty] $ Just []
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder-- | infer all minimal kinds
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiinferKinds :: Maybe Bool -> Type -> TypeEnv -> Result ((RawKind, [Kind]), Type)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiinferKinds b ty te@Env{classMap = cm} = let
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder resu = case ty of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski TypeName i _ _ -> getCoVarKind b te i
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder TypeAppl t1 t2 -> do
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski ((rk, ks), t3) <- inferKinds b t1 te
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski FunKind v _ rr _ -> do
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski ((_, l), t4) <- case v of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski inferKinds (fmap not b) t2 te
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder inferKinds b t2 te
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski InVar -> inferKinds Nothing t2 te
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski kks <- mapM (getFunKinds cm) ks
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder rs <- mapM ( \ fk -> case fk of
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder FunKind _ arg res _ -> do
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder subKinds Hint cm t2 arg l [res]
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski _ -> error "inferKinds: no function kind"
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski ) $ keepMinKinds cm $ concat kks
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski return ((rr, keepMinKinds cm $ concat rs), TypeAppl t3 t4)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder _ -> mkError "unexpected type argument" t2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski KindedType kt kind ps -> do
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder let Result ds _ = anaKindM kind cm
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder k <- if null ds then return kind else Result ds Nothing
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder ((rk, ks), t) <- inferKinds b kt te
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder l <- subKinds Hint cm kt k ks [k]
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski return ((rk, l), KindedType t k ps)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski ProductType ts ps -> do
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski l <- mapM ( \ t -> inferKinds b t te) ts
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let res@(Result _ mk) = inferKinds b (convertType ty) te
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Just (kp, _) -> return (kp, ProductType (map snd l) ps)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Nothing -> res
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder LazyType t ps -> do
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski (kp, nt) <- inferKinds b t te
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski return (kp, LazyType nt ps)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder FunType t1 a t2 ps -> do
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski (_, t3) <- inferKinds (fmap not b) t1 te
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski (_, t4) <- inferKinds b t2 te
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski let res@(Result _ mk) = inferKinds b (convertType ty) te
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Just (kp, _) -> return (kp, FunType t3 a t4 ps)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu Nothing -> res
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu ExpandedType t1 t2 -> do
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu let Result _ mk = inferKinds b t1 te
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski (kp, t4) <- inferKinds b t2 te
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski return (kp, case mk of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Just (_, t3) -> ExpandedType t3 t4
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Nothing -> t4)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski _ -> error "inferKinds"
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski in -- trace (showPretty ty " : " ++ showPretty resu "")
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- * converting type terms
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | change lazy, product and fun types to type constructor name with arguments
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskigetTypeAppl :: Type -> (Type, [Type])
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedergetTypeAppl ty = let (t, args) = getTyAppl ty in
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski (t, reverse args) where
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski getTyAppl typ = case typ of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder TypeName _ _ _ -> (typ, [])
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski TypeAppl t1 t2 -> let (t, args) = getTyAppl t1 in (t, t2 : args)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ExpandedType _ t -> getTyAppl t
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski LazyType t ps -> getTyAppl $ liftType t ps
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski KindedType t _ _ -> getTyAppl t
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski ProductType ts _ -> let n = length ts in
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski (TypeName (productId n) (toRaw $ prodKind n) 0, reverse ts)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder FunType t1 a t2 _ -> (TypeName (arrowId a) (toRaw funKind) 0, [t2, t1])
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder _ -> error "getTypeAppl: unresolved type"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | change lazy, product and fun types to uniform applications
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederconvertType :: Type -> Type
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederconvertType ty = let (c, args) = getTypeAppl ty in mkTypeAppl c args
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * subtyping relation
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | extract the raw kind from a type term
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederrawKindOfType :: Type -> RawKind
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederrawKindOfType ty = case ty of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder TypeName _ k _ -> k
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder TypeAppl t1 _ -> case rawKindOfType t1 of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder FunKind _ _ rk _ -> rk
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ -> error "rawKindOfType"
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ -> rawKindOfType $ convertType ty
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | subtyping relation
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederlesserType :: TypeEnv -> Type -> Type -> Bool
a98fd29a06e80e447af26d898044c23497adbc73Mihai CodesculesserType te t1 t2 = case (t1, t2) of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (TypeAppl c1 a1, TypeAppl c2 a2) ->
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let b1 = lesserType te a1 a2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder b2 = lesserType te a2 a1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder in (case (rawKindOfType c1, rawKindOfType c2) of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (FunKind v1 _ _ _, FunKind v2 _ _ _) ->
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder if v1 == v2 then case v1 of
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ContraVar -> b2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder _ -> error "lesserType: no FunKind") && lesserType te c1 c2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (TypeName i1 _ _, TypeName i2 _ _) | i1 == i2 -> True
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (TypeName i _ _, _) -> case Map.lookup i $ localTypeVars te of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Nothing -> case Map.lookup i $ typeMap te of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Nothing -> False
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Just ti -> any ( \ t -> lesserType te t t2) $ superTypes ti
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Just (TypeVarDefn _ vk _ _) -> case vk of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Downset t -> lesserType te t t2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (TypeAppl _ _, TypeName _ _ _) -> False
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder _ -> lesserType te (convertType t1) $ convertType t2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- * leaves of types and substitution
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | the type name components of a type
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maederleaves :: (Int -> Bool) -> Type -> [(Int, (Id, RawKind))]
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu TypeName j k i -> if b(i)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu then [(i, (j, k))]
da955132262baab309a50fdffe228c9efe68251dCui Jian TypeAppl t1 t2 -> leaves b t1 `List.union` leaves b t2
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu ExpandedType _ t2 -> leaves b t2
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu KindedType tk _ _ -> leaves b tk
da955132262baab309a50fdffe228c9efe68251dCui Jian LazyType tl _ -> leaves b tl
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu ProductType l _ -> foldl List.union [] $ map (leaves b) l
da955132262baab309a50fdffe228c9efe68251dCui Jian FunType t1 _ t2 _ -> leaves b t1 `List.union` leaves b t2
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu _ -> error ("leaves: " ++ show t)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | type identifiers of a type
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederidsOf :: (Int -> Bool) -> Type -> Set.Set TypeId
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederidsOf b = Set.fromList . map (fst . snd) . leaves b
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | replace some type names with types
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederrepl :: Map.Map Id Type -> Type -> Type
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettichrepl m = rename ( \ i k n ->
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Nothing -> TypeName i k n)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * super type ids
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | compute super type ids of one type id
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedersuperIds :: TypeMap -> Id -> Set.Set Id
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedersuperIds tm = supIds tm Set.empty . Set.singleton
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | compute all super type ids for several type ids given as second argument
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedersupIds :: TypeMap -> Set.Set Id -> Set.Set Id -> Set.Set Id
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedersupIds tm known new =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder if Set.null new then known else
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let more = Set.unions $ map superTypeToId $
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder concatMap ( \ i -> superTypes
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder $ Map.findWithDefault starTypeInfo i tm)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder newKnown = Set.union known new
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder in supIds tm newKnown (more Set.\\ newKnown)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | extract super type ids from a type
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedersuperTypeToId :: Type -> Set.Set Id
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedersuperTypeToId t =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder TypeName i _ _ -> Set.singleton i
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * expand alias types
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich-- | expand aliases in a type scheme
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederexpand :: TypeMap -> TypeScheme -> TypeScheme
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederexpand = mapTypeOfScheme . expandAlias
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | expand aliases in a type
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederexpandAlias :: TypeMap -> Type -> Type
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederexpandAlias tm t =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let (ps, ts, ta, b) = expandAliases tm t in
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder if b && length ps == length ts then
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ExpandedType t $ repl (Map.fromList (zip
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (map getTypeVar ps) $ reverse ts)) ta
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- | Collect formal and actual parameters of the first argument of a
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedertype application. -}
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederexpandAliases :: TypeMap -> Type -> ([TypeArg], [Type], Type, Bool)
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederexpandAliases tm t = case t of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder TypeName i _ _ -> case Map.lookup i tm of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Just ti -> case typeDefn ti of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder AliasTypeDefn (TypeScheme l ty _) ->
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (l, [], ty, True)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Supertype _ (TypeScheme l ty _) _ ->
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder TypeName _ _ _ -> wrap t
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder _ -> (l, [], ty, True)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder TypeAppl t1 t2 ->
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let (ps, ts, ta, b) = expandAliases tm t1
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu t3 = expandAlias tm t2
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu (ps, t3 : ts, ta, b) -- reverse later on
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder else wrap $ TypeAppl t1 t3
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder FunType t1 a t2 ps ->
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder wrap $ FunType (expandAlias tm t1) a (expandAlias tm t2) ps
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ProductType ts ps -> wrap $ ProductType (map (expandAlias tm) ts) ps
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder LazyType ty ps -> wrap $ LazyType (expandAlias tm ty) ps
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ExpandedType t1 t2 -> wrap $ ExpandedType t1 $ expandAlias tm t2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder KindedType ty k ps -> wrap $ KindedType (expandAlias tm ty) k ps
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu where wrap ty = ([], [], ty, False)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu-- | find unexpanded alias identifier
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederhasAlias :: TypeMap -> Type -> [Diagnosis]
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederhasAlias tm t =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder map ( \ i -> mkDiag Error ("unexpanded alias '" ++ showId i "' in") t)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder $ filter ( \ i -> case Map.lookup i tm of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Just ti -> case typeDefn ti of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder AliasTypeDefn _ -> True
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder _ -> False) $ Set.toList $ idsOf (const True) t
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * resolve and analyse types
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | resolve type and infer minimal kinds
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederanaTypeM :: (Maybe Kind, Type) -> TypeEnv -> Result ((RawKind, [Kind]), Type)
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederanaTypeM (mk, parsedType) te =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder do resolvedType <- mkTypeConstrAppl parsedType
da955132262baab309a50fdffe228c9efe68251dCui Jian let tm = typeMap te
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu expandedType = expandAlias tm resolvedType
da955132262baab309a50fdffe228c9efe68251dCui Jian cm = classMap te
da955132262baab309a50fdffe228c9efe68251dCui Jian ((rk, ks), checkedType) <- inferKinds (Just True) expandedType te
da955132262baab309a50fdffe228c9efe68251dCui Jian l <- case mk of
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu Nothing -> subKinds Error cm parsedType
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu (if null ks then universe else head ks)
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder Just k -> subKinds Error cm parsedType k ks $
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder filter ( \ j -> lesserKind cm j k) ks
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder Result (hasAlias tm checkedType) $ Just ()
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder return ((rk, l), checkedType)
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder-- | resolve the type and check if it is of the universe class
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian MaederanaStarTypeM :: Type -> TypeEnv -> Result ((RawKind, [Kind]), Type)
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederanaStarTypeM t = anaTypeM (Just universe, t)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * misc functions on types
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | check if an id occurs in a type
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedercyclicType :: Id -> Type -> Bool
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedercyclicType i ty = Set.member i $ idsOf (==0) ty
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | check for unbound (or too many) type variables
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederunboundTypevars :: Bool -> [TypeArg] -> Type -> [Diagnosis]
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian MaederunboundTypevars b args ty =
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder let fvs = map (fst . snd) (leaves (> 0) ty)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder argIds = map getTypeVar args
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder restVars1 = fvs List.\\ argIds
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder restVars2 = argIds List.\\ fvs
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder in (if null restVars1 then []
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder else [mkDiag Error ("unbound type variable(s)\n "
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ++ showSepList ("," ++) showId
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder restVars1 " in") ty])
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich ++ if b || null restVars2 then [] else
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich [mkDiag Warning ("ignoring unused variable(s)\n "
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich ++ showSepList ("," ++) showId
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich restVars2 " in") ty]
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedergeneralizable :: TypeScheme -> [Diagnosis]
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedergeneralizable (TypeScheme args ty _) =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (if null args then [] else unboundTypevars False args ty)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ++ checkUniqueTypevars args
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | check uniqueness of type variables
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedercheckUniqueTypevars :: [TypeArg] -> [Diagnosis]
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedercheckUniqueTypevars = checkUniqueness . map getTypeVar