7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{- |

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederModule : $Header$

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : hets@tzi.de

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederStability : experimental

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederPortability : portable

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder analyse classes and types

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-}

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule HasCASL.TypeAna where

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.As

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport HasCASL.ClassAna

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.Le

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport HasCASL.Unify

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederimport qualified Common.Lib.Map as Map

8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian Maederimport qualified Common.Lib.Set as Set

f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian Maederimport Common.Id

3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maederimport Common.Result

8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian Maederimport Common.PrettyPrint

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Data.List as List

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder-- --------------------------------------------------------------------------

d42a01c4eb6892fe23ca9eff107bb29f4a229480Christian Maeder-- kind analysis

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder-- --------------------------------------------------------------------------

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederanaKindM :: Kind -> Env -> Result Kind

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaederanaKindM k env =

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder case k of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder MissingKind -> mkError "missing kind" k

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Downset v t _ ps -> do (rk, newT) <- anaType (Nothing, t) (typeMap env)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder let ds = unboundTypevars [] newT

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder if null ds then

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return $ Downset v newT rk ps

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder else Result ds Nothing

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ClassKind ci _ -> anaClassId ci (classMap env)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Intersection ks ps -> do newKs <- mapM ( \ ek -> anaKindM ek env) ks

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder if null newKs then return k

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder else let ds = checkIntersection

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder (rawKind $ head newKs)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder $ tail newKs

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder in if null ds then

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder return $ if isSingle newKs

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder then head newKs

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder else Intersection newKs ps

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder else Result ds Nothing

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder FunKind k1 k2 ps -> do k3 <- anaKindM k1 env

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder k4 <- anaKindM k2 env

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder return $ FunKind k3 k4 ps

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder ExtKind ek v ps -> do nk <- anaKindM ek env

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder return $ ExtKind nk v ps

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederdata ApplMode = OnlyArg | TopLevel

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedergetIdType :: Id -> TypeMap -> Result Type

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian MaedergetIdType i tm = do

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder k <- getIdKind tm i

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder return $ TypeName i k $ case Map.lookup i tm of

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder Just (TypeInfo _ _ _ (TypeVarDefn c)) -> c

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder _ -> 0

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian MaedermkTypeConstrAppls :: ApplMode -> Type -> TypeMap -> Result Type

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian MaedermkTypeConstrAppls m ty tm = case ty of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder TypeName _ _ _ -> return ty

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder TypeAppl t1 t2 -> do

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder t3 <- mkTypeConstrAppls m t1 tm

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder t4 <- mkTypeConstrAppls OnlyArg t2 tm

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return $ TypeAppl t3 t4

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder TypeToken tt -> getIdType (simpleIdToId tt) tm

c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder BracketType b ts ps -> do

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder args <- mapM (\ trm -> mkTypeConstrAppls m trm tm) ts

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder case args of

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder [] -> case b of

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Parens -> return logicalType

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder _ -> let i = Id (mkBracketToken b ps) [] []

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder in getIdType i tm

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder [x] -> case b of

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder Parens -> return x

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder _ -> do let [o,c] = mkBracketToken b ps

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder i = Id [o, Token place $ firstPos args ps

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder , c] [] []

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder t <- getIdType i tm

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder return $ TypeAppl t x

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder _ -> mkError "illegal type" ty

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder MixfixType [] -> error "mkTypeConstrAppl (MixfixType [])"

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder MixfixType (f:a) -> case (f, a) of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (TypeToken t, [BracketType Squares as@(_:_) ps]) -> do

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder mis <- mapM mkTypeCompId as

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder getIdType (Id [t] mis ps) tm

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder _ -> do newF <- mkTypeConstrAppls TopLevel f tm

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder nA <- mapM ( \ t -> mkTypeConstrAppls OnlyArg t tm) a

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return $ foldl1 TypeAppl $ newF : nA

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder KindedType t k p -> do

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder newT <- mkTypeConstrAppls m t tm

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder return $ KindedType newT k p

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder LazyType t p -> do

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder newT <- mkTypeConstrAppls TopLevel t tm

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder return $ LazyType newT p

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder ProductType ts ps -> do

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder mTs <- mapM (\ t -> mkTypeConstrAppls TopLevel t tm) ts

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder return $ mkProductType mTs ps

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder FunType t1 a t2 ps -> do

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder newT1 <- mkTypeConstrAppls TopLevel t1 tm

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder newT2 <- mkTypeConstrAppls TopLevel t2 tm

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder return $ FunType newT1 a newT2 ps

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder ExpandedType _ t2 -> mkTypeConstrAppls m t2 tm

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaedermkTypeCompId :: Type -> Result Id

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaedermkTypeCompId ty = case ty of

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder TypeToken t -> if isPlace t then mkError "unexpected place" t

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder else return $ Id [t] [] []

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder MixfixType [] -> error "mkTypeCompId: MixfixType []"

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder MixfixType (hd:tps) ->

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder if null tps then mkTypeCompId hd

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder else do

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder let (toks, comps) = break ( \ p ->

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder case p of BracketType Squares (_:_) _ -> True

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder _ -> False) tps

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder mts <- mapM mkTypeCompToks (hd:toks)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (mis, ps) <- if null comps then return ([], [])

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder else mkTypeCompIds $ head comps

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder pls <- if null comps then return []

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder else mapM mkTypeIdPlace $ tail comps

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder return $ Id (concat mts ++ pls) mis ps

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder _ -> do ts <- mkTypeCompToks ty

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder return $ Id ts [] []

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermkTypeCompIds :: Type -> Result ([Id], [Pos])

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermkTypeCompIds ty = case ty of

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder BracketType Squares tps@(_:_) ps -> do

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder mis <- mapM mkTypeCompId tps

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder return (mis, ps)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder _ -> mkError "no compound list for type id" ty

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermkTypeCompToks :: Type -> Result [Token]

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermkTypeCompToks ty = case ty of

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder TypeToken t -> return [t]

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder BracketType bk [tp] ps -> case bk of

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Parens -> mkError "no type id" ty

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder _ -> do let [o,c] = mkBracketToken bk ps

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder mts <- mkTypeCompToks tp

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder return (o : mts ++ [c])

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder MixfixType tps -> do

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder mts <- mapM mkTypeCompToks tps

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder return $ concat mts

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder _ -> mkError "no type tokens" ty

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermkTypeIdPlace :: Type -> Result Token

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermkTypeIdPlace ty = case ty of

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder TypeToken t -> if isPlace t then return t

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder else mkError "no place" t

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder _ -> mkError "no place" ty

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- ---------------------------------------------------------------------------

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- compare types

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- ---------------------------------------------------------------------------

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedergetKindAppl :: Kind -> [a] -> [(Kind, [Kind])]

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian MaedergetKindAppl k args = if null args then [(k, [])] else

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder case k of

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder FunKind k1 k2 _ -> let ks = getKindAppl k2 (tail args)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder in map ( \ (rk, kargs) -> (rk, k1 : kargs)) ks

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Intersection l _ ->

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder concatMap (flip getKindAppl args) l

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder ExtKind ek _ _ -> getKindAppl ek args

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder ClassKind _ ck -> getKindAppl ck args

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Downset _ _ dk _ -> getKindAppl dk args

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder _ -> error ("getKindAppl " ++ show k)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedergetTypeAppl :: TypeMap -> Type -> (Type, [Type])

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian MaedergetTypeAppl tm ty = let (t, args) = getTyAppl ty in

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (t, reverse args) where

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder getTyAppl typ = case typ of

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder TypeAppl t1 t2 -> let (t, args) = getTyAppl t1 in (t, t2 : args)

8dcc70ff9afdfe4aff258676718677a4d7076fd0Christian Maeder ExpandedType _ t -> getTyAppl t

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder LazyType t _ -> getTyAppl t

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder KindedType t _ _ -> getTyAppl t

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder ProductType ts ps ->

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder let Result _ mk = getIdKind tm productId

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder in case mk of

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Just k ->

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder let rk = toIntersection (map fst $ getKindAppl k [typ,typ]) ps

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder in case ts of

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder [t1,t2] -> (TypeName productId k 0, [t2, t1])

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder [] -> (TypeName productId rk 0, [])

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder [_] -> error "getTyAppl productType"

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder t:rt -> (TypeName productId k 0, [ProductType rt ps, t])

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder _ -> error "getTyAppl productId"

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder FunType t1 a t2 _ ->

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder let i = arrowId a

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder Result _ mk = getIdKind tm i in

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder case mk of

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder Just k -> (TypeName i k 0, [t2, t1])

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder _ -> error "getTyAppl arrowId"

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder _ -> (typ, [])

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaedermkTypeAppl :: Type -> [Type] -> Type

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaedermkTypeAppl t as =

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder if null as then t else mkTypeAppl (TypeAppl t $ head as) $ tail as

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaedercyclicType :: Id -> Type -> Bool

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian MaedercyclicType i ty = Set.member i $ idsOf (==0) ty

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederlesserType :: TypeMap -> Type -> Type -> Bool

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian MaederlesserType tm t1 t2 = case (t1, t2) of

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder (ExpandedType _ t, _) -> lesserType tm t t2

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (_, ExpandedType _ t) -> lesserType tm t1 t

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (LazyType t _, _) -> lesserType tm t t2

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (_, LazyType t _) -> lesserType tm t1 t

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder (KindedType t _ _, _) -> lesserType tm t t2

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder (_, KindedType t _ _) -> lesserType tm t1 t

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (ProductType ts1 _, ProductType ts2 _) ->

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder if length ts1 == length ts2 then

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder and $ zipWith (lesserType tm) ts1 ts2

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder else False

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (FunType ta1 a1 tr1 _, FunType ta2 a2 tr2 _) ->

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder (case (a1, a2) of

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (ContFunArr, _) -> True

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (_, PFunArr) -> True

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder (PContFunArr, FunArr) -> False

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (FunArr, PContFunArr) -> False

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder _ -> a1 == a2) && lesserType tm tr1 tr2 && lesserType tm ta2 ta1

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder _ -> let (top1, as1) = getTypeAppl tm t1

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (top2, as2) = getTypeAppl tm t2 in

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder case (top1, top2) of

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (TypeName i1 k1 _, TypeName i2 k2 _) ->

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder let rk = rawKind k1

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder kindArgs k as = if null as then []

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder else case k of

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder FunKind ka kr _ -> ka : kindArgs kr (tail as)

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder _ -> []

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder kas = kindArgs rk as1

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder ts1 = filter (not . cyclicType i1) $ superTypes

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder $ Map.findWithDefault starTypeInfo i1 tm

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder l1 = length as1

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder in if i1 == i2 then

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder if rawKind k2 == rk && l1 == length as2

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder && length kas == l1 then

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder and $ zipWith (\ k (ta1, ta2) ->

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder let b1 = lesserType tm ta1 ta2

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder b2 = lesserType tm ta2 ta1

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder in case k of

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder ExtKind _ CoVar _ -> b1

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder ExtKind _ ContraVar _ -> b2

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder _ -> b1 && b2) kas

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder $ zip as1 as2

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder else error ("lesserType: expected length " ++

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder shows l1 " and kind " ++

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder showPretty rk "")

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder else any (\ st -> lesserType tm (mkTypeAppl st as1) t2) ts1

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder _ -> error ("lesserType: " ++ showPretty top1 " < "

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder ++ showPretty top2 "")

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder-- ---------------------------------------------------------------------------

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder-- compare kinds

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder-- ---------------------------------------------------------------------------

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederlesserKind :: TypeMap -> Kind -> Kind -> Bool

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian MaederlesserKind tm k1 k2 =

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder case (k1, k2) of

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder (MissingKind, _) -> error "lesserKind1"

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (_, MissingKind) -> error "lesserKind2"

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (_, Intersection l2@(_:_) _) -> and $ map (lesserKind tm k1) l2

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (Intersection l1@(_:_) _, _) -> or $ map (flip (lesserKind tm) k2) l1

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (ExtKind ek1 v1 _, ExtKind ek2 v2 _) ->

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (v1 == v2) && lesserKind tm ek1 ek2

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (_, ExtKind ek2 _ _) -> lesserKind tm k1 ek2

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (ExtKind _ _ _, _) -> False

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (Intersection [] _, Intersection [] _) -> True

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (Intersection [] _, _) -> False

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (Downset _ t1 k _, Downset _ t2 _ _) -> lesserType tm t1 t2

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder || lesserKind tm k k2

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder (Downset _ _ k _, _) -> lesserKind tm k k2

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder (ClassKind c1 k, ClassKind c2 _) -> c1 == c2 || lesserKind tm k k2

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder (ClassKind _ k, _) -> lesserKind tm k k2

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder (FunKind ek rk _, FunKind ek2 rk2 _) ->

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder lesserKind tm rk rk2 && lesserKind tm ek2 ek

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder (FunKind _ _ _, _) -> False

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder-- ---------------------------------------------------------------------------

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- infer kind

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder-- ---------------------------------------------------------------------------

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder

bb13d067514a3f474166f345e098b81f3de11dbeChristian MaedercheckMaybeKinds :: (PosItem a, PrettyPrint a) =>

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder TypeMap -> a -> Maybe Kind -> Kind -> Result Kind

bb13d067514a3f474166f345e098b81f3de11dbeChristian MaedercheckMaybeKinds tm a mk1 k2 =

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder case mk1 of

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder Nothing -> return k2

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder Just k1 -> if lesserKind tm k1 k2 then return k1

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder else if lesserKind tm k2 k1 then return k2

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder else Result (diffKindDiag a k1 k2) Nothing

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaedercheckFunKind :: Maybe Kind -> Type -> Type -> Kind -> TypeMap -> Result Kind

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaedercheckFunKind mk t1 t2 k1 tm =

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder case k1 of

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder FunKind fk ak _ -> do

inferKind (Just fk) t2 tm

checkMaybeKinds tm (TypeAppl t1 t2) mk ak

Intersection l@(_:_) ps -> do

ml <- mapM ( \ k -> checkFunKind mk t1 t2 k tm) l

return $ toIntersection ml ps

ClassKind _ k -> checkFunKind mk t1 t2 k tm

Downset _ _ k _ -> checkFunKind mk t1 t2 k tm

ExtKind k _ _ -> checkFunKind mk t1 t2 k tm

_ -> mkError "unexpected type argument" t2

inferKind :: Maybe Kind -> Type -> TypeMap -> Result Kind

inferKind mk ty tm = case ty of

TypeName i _ _ -> do

m <- getIdKind tm i

checkMaybeKinds tm i mk m

TypeAppl t1 t2 -> do

k1 <- inferKind Nothing t1 tm

checkFunKind mk t1 t2 k1 tm

ExpandedType _ t1 -> inferKind mk t1 tm

FunType t1 a t2 _ -> do

let i = arrowId a

fk <- getIdKind tm i

let tn = TypeName i fk 0

inferKind mk (TypeAppl (TypeAppl tn t1) t2) tm

ProductType ts _ -> if null ts then checkMaybeKinds tm ty mk star else

do pk <- getIdKind tm productId

let tn = TypeName productId pk 0

mkAppl [t1] = t1

mkAppl (t1:tr) = TypeAppl (TypeAppl tn t1) $ mkAppl tr

mkAppl [] = error "inferKind: mkAppl"

inferKind mk (mkAppl ts) tm

LazyType t _ -> inferKind mk t tm

KindedType t k _ -> do

mk2 <- inferKind (Just k) t tm

checkMaybeKinds tm t mk mk2

_ -> mkError "unresolved type" ty

getIdKind :: TypeMap -> Id -> Result Kind

getIdKind tm i = case Map.lookup i tm of

Nothing -> mkError "unknown type" i

Just (TypeInfo rk l _ _) -> return $

if null l then rk else

if isSingle l then head l else Intersection l []

-- ---------------------------------------------------------------------------

anaType :: (Maybe Kind, Type) -> TypeMap -> Result (Kind, Type)

anaType (mk, t) tm =

do nt <- mkTypeConstrAppls TopLevel t tm

let newTy = expandAlias tm nt

newk <- inferKind mk newTy tm

return (newk, newTy)

anaStarTypeR :: Type -> TypeMap -> Result (Kind, Type)

anaStarTypeR t = anaType (Just star, t)

mkGenVars :: [TypeArg] -> Type -> Type

mkGenVars fvs newTy =

let ts = zipWith ( \ (TypeArg i k _ _) n ->

TypeName i k n) fvs [-1, -2..]

m = Map.fromList $ zip fvs ts

in repl m newTy

generalize :: TypeScheme -> TypeScheme

generalize (TypeScheme args ty p) =

let fvs = leaves (> 0) ty

ts = zipWith ( \ (v, TypeArg i k _ _) n ->

(v, TypeName i k n)) fvs [-1, -2..]

newTy = subst (Map.fromList ts) ty

newArgs = map snd fvs

in if null $ newArgs List.\\ args then TypeScheme args newTy p

else TypeScheme newArgs newTy p

-- | check for unbound type variables

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

unboundTypevars args ty =

let restVars = map snd (leaves (> 0) ty) List.\\ args in

if null restVars then []

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

++ showSepList ("," ++) showPretty

restVars " in") ty]

generalizable :: TypeScheme -> [Diagnosis]

generalizable (TypeScheme args ty _) =

(if null args then [] else unboundTypevars args ty)

++ checkUniqueTypevars args

-- | check uniqueness of type variables

checkUniqueTypevars :: [TypeArg] -> [Diagnosis]

checkUniqueTypevars = checkUniqueness . map getTypeVar

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]