e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- |

c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel CalinModule : $Header$

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel CalinCopyright : (c) Christian Maeder and Uni Bremen 2003

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel CalinMaintainer : hets@tzi.de

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel CalinStability : experimental

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel CalinPortability : portable

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin analyse classes and types

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin-}

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin

c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calinmodule HasCASL.TypeAna where

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calinimport HasCASL.As

edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calinimport HasCASL.AsUtils

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinimport HasCASL.ClassAna

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calinimport HasCASL.Le

edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calinimport HasCASL.Unify

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.List

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.Maybe

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport qualified Common.Lib.Map as Map

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinimport Common.Id

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calinimport Common.Result

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calinimport Common.PrettyPrint

9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- --------------------------------------------------------------------------

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin-- kind analysis

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin-- --------------------------------------------------------------------------

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalinanaKindM :: Kind -> Env -> Result Kind

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederanaKindM k env =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case k of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder MissingKind -> mkError "missing kind" k

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin Downset v t _ ps -> do (rk, newT) <- anaType (Nothing, t) (typeMap env)

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin return $ Downset v newT rk ps

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin ClassKind ci _ -> anaClassId ci (classMap env)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Intersection ks ps -> do newKs <- mapM ( \ ek -> anaKindM ek env) ks

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if null newKs then return k

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else let ds = checkIntersection

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (rawKind $ head newKs)

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin $ tail newKs

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin in if null ds then

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin return $ if isSingle newKs

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin then head newKs

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else Intersection newKs ps

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin else Result ds Nothing

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin FunKind k1 k2 ps -> do k3 <- anaKindM k1 env

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin k4 <- anaKindM k2 env

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin return $ FunKind k3 k4 ps

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin ExtKind ek v ps -> do nk <- anaKindM ek env

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin return $ ExtKind nk v ps

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calindata ApplMode = OnlyArg | TopLevel

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalingetIdType :: Id -> TypeMap -> Result Type

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalingetIdType i tm = do

edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin k <- getIdKind tm i

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return $ TypeName i k $ case Map.lookup i tm of

f00edd94c598adc73dc4f6005d79d2295e463da5Georgel Calin Just (TypeInfo _ _ _ (TypeVarDefn c)) -> c

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> 0

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermkTypeConstrAppls :: ApplMode -> Type -> TypeMap -> Result Type

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermkTypeConstrAppls m ty tm = case ty of

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin TypeName _ _ _ -> return ty

9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder TypeAppl t1 t2 -> do

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder t3 <- mkTypeConstrAppls m t1 tm

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder t4 <- mkTypeConstrAppls OnlyArg t2 tm

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin return $ TypeAppl t3 t4

c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin TypeToken tt -> getIdType (simpleIdToId tt) tm

c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin BracketType b ts ps -> do

9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder args <- mapM (\ trm -> mkTypeConstrAppls m trm tm) ts

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin case args of

c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin [] -> case b of

edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin Parens -> return logicalType

edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin _ -> let i = Id (mkBracketToken b ps) [] []

edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin in getIdType i tm

edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin [x] -> case b of

edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin Parens -> return x

edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin _ -> do let [o,c] = mkBracketToken b ps

edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin i = Id [o, Token place $ posOfType

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin $ head ts, c] [] []

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin t <- getIdType i tm

edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin return $ TypeAppl t x

edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin _ -> mkError "illegal type" ty

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder MixfixType [] -> error "mkTypeConstrAppl (MixfixType [])"

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin MixfixType (f:a) -> case (f, a) of

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin (TypeToken t, [BracketType Squares as@(_:_) ps]) -> do

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mis <- mapM mkTypeCompId as

ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin getIdType (Id [t] mis ps) tm

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> do newF <- mkTypeConstrAppls TopLevel f tm

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nA <- mapM ( \ t -> mkTypeConstrAppls OnlyArg t tm) a

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return $ foldl1 TypeAppl $ newF : nA

c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin KindedType t k p -> do

c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin newT <- mkTypeConstrAppls m t tm

c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin return $ KindedType newT k p

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin LazyType t p -> do

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin newT <- mkTypeConstrAppls TopLevel t tm

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin return $ LazyType newT p

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ProductType ts ps -> do

2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin mTs <- mapM (\ t -> mkTypeConstrAppls TopLevel t tm) ts

edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin return $ mkProductType mTs ps

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder FunType t1 a t2 ps -> do

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder newT1 <- mkTypeConstrAppls TopLevel t1 tm

newT2 <- mkTypeConstrAppls TopLevel t2 tm

return $ FunType newT1 a newT2 ps

ExpandedType _ t2 -> mkTypeConstrAppls m t2 tm

mkTypeCompId :: Type -> Result Id

mkTypeCompId ty = case ty of

TypeToken t -> if isPlace t then mkError "unexpected place" t

else return $ Id [t] [] []

MixfixType [] -> error "mkTypeCompId: MixfixType []"

MixfixType (hd:tps) ->

if null tps then mkTypeCompId hd

else do

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

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

_ -> False) tps

mts <- mapM mkTypeCompToks (hd:toks)

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

else mkTypeCompIds $ head comps

pls <- if null comps then return []

else mapM mkTypeIdPlace $ tail comps

return $ Id (concat mts ++ pls) mis ps

_ -> do ts <- mkTypeCompToks ty

return $ Id ts [] []

mkTypeCompIds :: Type -> Result ([Id], [Pos])

mkTypeCompIds ty = case ty of

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

mis <- mapM mkTypeCompId tps

return (mis, ps)

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

mkTypeCompToks :: Type -> Result [Token]

mkTypeCompToks ty = case ty of

TypeToken t -> return [t]

BracketType bk [tp] ps -> case bk of

Parens -> mkError "no type id" ty

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

mts <- mkTypeCompToks tp

return (o : mts ++ [c])

MixfixType tps -> do

mts <- mapM mkTypeCompToks tps

return $ concat mts

_ -> mkError "no type tokens" ty

mkTypeIdPlace :: Type -> Result Token

mkTypeIdPlace ty = case ty of

TypeToken t -> if isPlace t then return t

else mkError "no place" t

_ -> mkError "no place" ty

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

-- compare kinds

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

lesserKind :: Kind -> Kind -> Bool

lesserKind k1 k2 =

case (k1, k2) of

(MissingKind, _) -> error "lesserKind1"

(_, MissingKind) -> error "lesserKind2"

(_, Intersection l2@(_:_) _) -> and $ map (lesserKind k1) l2

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

(ExtKind ek1 v1 _, ExtKind ek2 v2 _) ->

(v1 == v2) && lesserKind ek1 ek2

(_, ExtKind ek2 _ _) -> lesserKind k1 ek2

(ExtKind _ _ _, _) -> False

(Intersection [] _, Intersection [] _) -> True

(Intersection [] _, _) -> False

(Downset _ t1 k _, Downset _ t2 _ _) -> t1 == t2 || lesserKind k k2

(Downset _ _ k _, _) -> lesserKind k k2

(ClassKind c1 k, ClassKind c2 _) -> c1 == c2 || lesserKind k k2

(ClassKind _ k, _) -> lesserKind k k2

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

lesserKind rk rk2 && lesserKind ek2 ek

(FunKind _ _ _, _) -> False

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

-- infer kind

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

checkMaybeKinds :: (PosItem a, PrettyPrint a) =>

a -> Maybe Kind -> Kind -> Result Kind

checkMaybeKinds a mk1 k2 =

case mk1 of

Nothing -> return k2

Just k1 -> if lesserKind k1 k2 then return k1

else if lesserKind k2 k1 then return k2

else Result (diffKindDiag a k1 k2) Nothing

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

checkFunKind mk t1 t2 k1 tm =

case k1 of

FunKind fk ak _ -> do

inferKind (Just fk) t2 tm

checkMaybeKinds (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 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 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 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)

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 -> Result TypeScheme

generalize (TypeScheme newArgs newTy p) = do

let fvs = varsOf newTy

qTy = mkGenVars fvs newTy

ds = unboundTypevars newArgs newTy

if null ds then

return $ TypeScheme newArgs qTy p

else if null newArgs then

return $ TypeScheme fvs qTy p

else Result ds Nothing

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]