{- --------------------------------------------------------------------------- Various functions for type checking: - error messages ... -} module Type.Lib (typeUnify,typeUnifyMany,typeUnifyApply,typePatCon,typeExpCon ,typeIdentDict,getIdent,getTypeErrors,typeError ,typeNewTVar,typeIdentDef,checkExist,funType,extendEnv,getEnv ,msgFun,msgPat,msgLit,msgBool,msgGdExps,msgAltExps,msgCase ,msgAltPats,msgIf,msgApply,msgList,msgExpType,msgAs,msgNK ,newIdent,getState,setState,typeOfMain ,msgPatGdExps,msgPatGd) where import NT import Type.Env(lookupEnv) import Util.Extra(assocDef,strPos,snub,mapSnd) import Id(Id) import Syntax import IdKind import TokenId(t_Arrow,tmain,tIO,t_Tuple) import Flags import SyntaxPos import Type.Subst import Type.Unify import Type.Data import IntState import Type.Util import Info import IO import Error import Nice msgPat :: Pat id -> String -> String msgPat pat err = "Type error " ++ err ++ "\nwhen unifying pattern at " ++ strPos (getPos pat) ++ " with its expression.\n" msgFun :: Rhs id -> String -> String msgFun gdexps err = "Type error " ++ err ++ "\nwhen binding final type to function at " ++ strPos (getPos gdexps) ++ ".\n" msgExpType :: Pos -> String -> String msgExpType pos err = "Type error " ++ err ++ "\nwhen unifying explicit type at " ++ strPos pos ++ ".\n" msgGdExps :: [(Exp id, Exp id)] -> String -> String msgGdExps gdexps err = "Type error " ++ err ++ "\nwhen unifying multiple guarded expressions at " ++ (strPos . getPos . head) gdexps ++ ".\n" msgPatGdExps gdexps err = "Type error " ++ err ++ "\nwhen unifying pattern guarded expressions at " ++ (strPos . getPos . head) gdexps ++ ".\n" msgBool :: Exp id -> String -> String msgBool exp err = "Type error " ++ err ++ "\nwhen trying to unify expressions at " ++ strPos (getPos exp) ++ " with Bool.\n" msgPatGd pat exp err = "Type error " ++ err ++ "\nwhen trying to unify expression at " ++ strPos (getPos exp) ++ "\nwith pattern at "++ strPos (getPos pat) ++ "\nin pattern guard.\n" msgAltPats :: [Alt id] -> String -> String msgAltPats alts err = "Type error " ++ err ++ "\nwhen trying to unify pattern part of alternatives at " ++ (strPos . getPos . head) alts ++ ".\n" msgAltExps :: [Alt id] -> String -> String msgAltExps alts err = "Type error " ++ err ++ "\nwhen trying to unify expression part of alternatives at " ++ (strPos . getPos . head) alts ++ ".\n" msgCase :: Exp id -> String -> String msgCase exp err = "Type error " ++ err ++ "\nwhen trying to unify expression at " ++ strPos (getPos exp) ++ " with patterns.\n" msgIf :: Exp id -> Exp id -> String -> String msgIf exp1 exp2 err = "Type error " ++ err ++ "\nwhen trying to unify then-expressions at " ++ strPos (getPos exp1) ++ " and else-expression at " ++ strPos (getPos exp2) ++ ".\n" msgLit :: Pos -> String -> String -> a -> String msgLit pos typ err no = "Type error " ++ err ++ "\nwhen processing overloaded " ++ typ ++ " at " ++ strPos pos ++ ".\n" msgApply :: HasPos a => [a] -> String -> Int -> String msgApply es err no = "Type error " ++ err ++ "\nwhen trying to apply function at " ++ (strPos . getPos . head) es ++ " to its " ++ showEnum no ++ " argument at " ++ (strPos . getPos . (es !!)) no ++ ".\n" showEnum :: Int -> String showEnum 1 = "1st" showEnum 2 = "2nd" showEnum 3 = "3rd" showEnum n = show n ++ "th" msgList :: [Exp id] -> String -> String msgList es err = "Type error " ++ err ++ "\nwhen trying to unify items in a list at " ++ (strPos . getPos . head) es ++ ".\n" msgAs :: Pos -> String -> String msgAs pos err = "Type error " ++ err ++ "\nwhen trying to unify variable at " ++ strPos pos ++ " with pattern.\n" msgNK :: Pos -> String -> String msgNK pos err = "Type error " ++ err ++ "\nwhen trying to check (n+k) pattern at " ++ strPos pos ++ ".\n" typeOfMain :: Flags -> ((TokenId, IdKind) -> Id) -> Decls Id -> IntState -> IO IntState typeOfMain flags tidFun (DeclsScc depends) state = case findMain (concatMap stripDepend depends) of Nothing -> hPutStr stderr "Warning: Can not find main in module Main.\n" >> return state Just imain -> if sShowType flags then case ntIS state imain of (NewType free [] [] [nt],state) -> do hPutStr stderr (niceNT Nothing state (mkAL free) nt++"\n") exit (nt,state) -> do hPutStr stderr (niceNewType state nt++"\n") exit else case ntIS state imain of (NewType free [] [] [nt],state) -> let mainType = mkNTcons (tidFun (tIO,TCon)) [mkNTvar (tidFun (t_Tuple 0,TCon))] in case unify state idSubst (nt, mainType) of Right phi -> return state Left (phi,str) -> hPutStr stderr ("Function main has the type "++ niceNT Nothing state (mkAL free) nt ++ " instead of IO ().\n") >> exit (nt,state) -> hPutStr stderr ("Function main has the type "++ niceNewType state nt ++ " instead of IO ().\n") >> exit where stripDepend (DeclsNoRec d) = [d] stripDepend (DeclsRec ds) = ds findMain [] = Nothing findMain (DeclFun pos i funs:ds) = if tidIS state i == tmain then Just i else findMain ds findMain (d:ds) = findMain ds typeUnify :: ShowS -> NT -> NT -> TypeDown -> TypeState -> (NT,TypeState) typeUnify errFun t1 t2 down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs ectxsi) = {- trace ("\n\n1: " ++ niceNT Nothing state (map (\x -> (x, 'a':show x)) [1..]) t1) $ trace ("\n\n2: " ++ niceNT Nothing state (map (\x -> (x, 'a':show x)) [1..]) t2) $ -} case unify state phi (t1,t2) of Right phi' -> let t1' = subst phi t1 in {- trace ("\n\n3: " ++ niceNT Nothing state (map (\x -> (x, 'a':show x)) [1..]) t1') $ -} seq t1' (t1',TypeState state phi' ctxs ectxsi) Left (phi',str) -> case uniqueIS state of (unique,state) -> (NTany unique -- new type variable as result to continue -- despite error ,TypeState (addError state (errFun str)) phi' ctxs ectxsi) typeUnifyMany :: ShowS -> [NT] -> TypeDown -> TypeState -> (NT,TypeState) typeUnifyMany errFun [] down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs ectxsi) = case uniqueIS state of (unique,state) -> (NTany unique,TypeState state phi ctxs ectxsi) typeUnifyMany errFun ts@(t:_) down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs ectxsi) = case unifyr state phi ts of Right phi -> let t' = subst phi t in seq t' (t',TypeState state phi ctxs ectxsi) Left (phi,str) -> case uniqueIS state of (unique,state) -> (NTany unique,TypeState (addError state (errFun str)) phi ctxs ectxsi) typeUnifyApply :: (String -> Int -> String) -> [NT] -> TypeDown -> TypeState -> (NT,TypeState) typeUnifyApply errFun (f:xs) down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs ectxsi) = seq nextTvar (unifyApply state phi f (zip [1 .. ] xs)) where (nextTvar,_) = uniqueIS state arrow = tidFun (t_Arrow,TCon) unifyApply state phi f [] = let f' = subst phi f in seq f' (f',TypeState state phi ctxs ectxsi) unifyApply state phi f ((no,x):xs) = case subst phi f of NTcons c _ [a,r] | c == arrow -> case unify state phi (a,x) of Right phi -> unifyApply state phi r xs Left (phi,str) -> case uniqueIS state of (unique,state) -> (NTany unique,TypeState (addError state (errFun str no)) phi ctxs ectxsi) phif -> case uniqueIS state of (a,state) -> case uniqueIS state of (r,state) -> case unify state phi (phif,mkNTcons arrow [NTany a,NTany r]) of Right phi -> case unify state phi (NTany a,x) of Right phi -> unifyApply state phi (NTany r) xs Left (phi,str) -> case uniqueIS state of (unique,state) -> (NTany unique,TypeState (addError state (errFun str no)) phi ctxs ectxsi) Left (phi,str) -> case uniqueIS state of (unique,state) -> (NTany unique,TypeState (addError state (errFun str no)) phi ctxs ectxsi) typeNewTVar :: t -> Type.Data.TypeState -> (NT.NT, Type.Data.TypeState) typeNewTVar down up@(TypeState state phi ctxs ectxsi) = case uniqueIS state of (unique,state) -> (NTany unique,TypeState state phi ctxs ectxsi) newIdent :: t -> Type.Data.TypeState -> (Id.Id, Type.Data.TypeState) newIdent down up@(TypeState state phi ctxs ectxsi) = case uniqueIS state of (unique,state) -> (unique,TypeState state phi ctxs ectxsi) getState :: t -> Type.Data.TypeState -> (IntState.IntState, Type.Data.TypeState) getState down up@(TypeState state phi ctxs ectxsi) = (state,up) setState :: IntState.IntState -> t -> Type.Data.TypeState -> Type.Data.TypeState setState state down up@(TypeState _ phi ctxs ectxsi) = TypeState state phi ctxs ectxsi extendEnv :: [(Id, NT)] -> TypeDown -> b -> (TypeDown, b) extendEnv ext down@(TypeDown env tidFun defaults ctxDict envDict) up = (TypeDown (ext++env) tidFun defaults ctxDict envDict,up) getEnv :: TypeDown -> b -> ([(Id, NT)], b) getEnv down@(TypeDown env tidFun defaults ctxDict envDict) up = (env,up) getIdent :: (TokenId, IdKind) -> TypeDown -> b -> (Id, b) getIdent key down@(TypeDown env tidFun defaults ctxDict envDict) up = (tidFun key,up) -- Drop dictionaries if it is seq, this is used in PrimCode qDict :: t -> Exp id -> [Exp id] -> Exp id qDict state exp [] = exp qDict state exp dict = ExpApplication (getPos exp) (exp:map ExpDict dict) -- Dictionaries done at call site! typeIdentDef :: (Id -> a) -> t -> Id -> TypeDown -> TypeState -> ((a, NT), TypeState) typeIdentDef convar pos ident down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs ectxsi) = case lookupEnv ident env of Just t -> -- Type under construction let t' = subst phi t in seq t' ((convar ident,t'),up) -- Only let-bound identifiers in envDict -- Otherwise internal error! typeExpCon :: Pos -> Id -> TypeDown -> TypeState -> ((Exp Id, NT), TypeState) typeExpCon pos ident down up@(TypeState state phi ctxs ectxsi) = case typeExpCon' pos ident down up of ((exp,expT,ctxs,eTVar),up) -> ((qDict state exp ctxs,expT),up) typeExpCon' :: Pos -> Id -> TypeDown -> TypeState -> ((Exp Id, NT, [Exp Id], [Id]), TypeState) typeExpCon' pos ident down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs ectxsi) = case ntIS state ident of -- Be strict! (NoType,state) -> -- Not possible for constructors! case uniqueIS state of -- Fake answer, there should be an error reported somewhere else (u,state) -> ((ExpCon pos ident,mkNTvar u,[],[]),TypeState state phi ctxs ectxsi) (nt''@(NewType _ eTVar _ _),state) -> case extractCtxs nt'' of (nt',ctxs'') -> case dictAndArrows (tidFun (t_Arrow,TCon)) pos state ctxs'' nt' of (ictxs,nt,state) -> let ctxsStripped' = map snd ictxs is = map fst $ filter ((`elem` eTVar) . ( \ (TypeDict i nt intpos) -> stripNT nt) . snd) ictxs ctxs' = map ( \ (TypeDict i nt intpos) -> TypeDict i (mkNTvar (stripNT nt)) intpos) ctxsStripped' nt' = subst phi nt in seq nt' ((ExpCon pos ident,nt',map (\ i -> assocDef ctxDict (error "TypeLib:204") i) is,eTVar),TypeState state phi (ctxs'++ctxs) ectxsi) typePatCon :: Pos -> Id -> TypeDown -> TypeState -> ((Exp Id, NT, [Id]), TypeState) typePatCon pos ident down up@(TypeState state phi ctxs ectxsi) = case typePatCon' pos ident down up of ((exp,expT,ctxs,eTVar),up) -> ((qDict state exp ctxs,existNT eTVar expT,eTVar),up) typePatCon' :: Pos -> Id -> TypeDown -> TypeState -> ((Exp Id, NT, [Exp Id], [Id]), TypeState) typePatCon' pos ident down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs inEctxsi) = case ntIS state ident of -- Be strict! (NoType,state) -> -- Not possible for constructors! case uniqueIS state of -- Fake answer, there should be an error reported somewhere else (u,state) -> ((ExpCon pos ident,mkNTvar u,[],[]),TypeState state phi ctxs inEctxsi) (nt''@(NewType _ exist _ _),state) -> case extractCtxs nt'' of (nt',ectxs') -> case uniqueISs state (map (mapSnd ( \ v -> if v `elem` exist then mkNTexist v else mkNTvar v)) ectxs') of (ectxsi,state) -> let eictxs = cvi2typedict pos exist ectxsi in case dictAndArrows (tidFun (t_Arrow,TCon)) pos state [] nt' of (ictxs,nt,state) -> let (_,ctxs') = unzip (ictxs ++ eictxs) nt' = subst phi nt in seq nt' ((ExpCon pos ident,nt',map (ExpVar pos . fst) eictxs,exist),TypeState state phi (ctxs'++ctxs) (ectxsi ++ inEctxsi)) existNT :: [Id] -> NT -> NT existNT tv t@(NTany a) = t existNT tv t@(NTvar a k) = if a `elem` tv then NTexist a k else t existNT tv t@(NTexist a _) = t existNT tv (NTstrict t) = NTstrict (existNT tv t) existNT tv (NTapp t1 t2) = NTapp (existNT tv t1) (existNT tv t2) existNT tv (NTcons a k tas) = NTcons a k (map (existNT tv) tas) typeIdentDict :: (Id -> Exp Id) -> Pos -> Id -> TypeDown -> TypeState -> ((Exp Id, NT), TypeState) typeIdentDict convar pos ident down up@(TypeState state phi ctxs ectxsi) = case typeIdentDict' convar pos ident down up of ((exp,expT,ctxs,eTVar),up) -> ((qDict state exp ctxs,expT),up) typeIdentDict' :: (Id -> Exp Id) -> Pos -> Id -> TypeDown -> TypeState -> ((Exp Id, NT, [Exp Id], [Id]), TypeState) typeIdentDict' convar pos ident down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs ectxsi) = case ntIS state ident of -- Be strict! (NoType,state) -> case lookupEnv ident env of Just t -> -- Type still under construction let t' = subst phi t in seq t' ((convar ident,t',assocDef envDict [] ident,[]),up) -- Only let-bound identifiers in envDict Nothing -> -- This is an identifier bound inside a pattern that need dictionaries, i.e, an error reported elsewhere case uniqueIS state of (u,state) -> ((convar ident,mkNTvar u,[],[]),TypeState state phi ctxs ectxsi) (nt'@(NewType _ eTVar _ _),state) -> case dictAndArrows (tidFun (t_Arrow,TCon)) pos state [] nt' of (ictxs,nt,state) -> let (is,ctxs') = unzip ictxs nt' = subst phi nt in seq nt' ((convar ident,nt',map (\ i -> assocDef ctxDict (error "TypeLib:162") i) is,eTVar),TypeState state phi (ctxs'++ctxs) ectxsi) checkExist :: [(Id, NT)] -> [Id] -> t -> TypeState -> TypeState checkExist oldEnv eTVars down up@(TypeState state phi ctxs ectxsi) = case foldr (cE phi eTVars) state oldEnv of state -> TypeState state phi ctxs ectxsi where cE phi eTVars (v,nt) state = let tvars = (snub . freeNT . subst phi) nt in case filter (`elem` eTVars) tvars of [] -> state _ -> case lookupIS state v of Just info -> addError state ("Existential type escaped with " ++ show (tidI info)) Nothing -> addError state ("Existential type escaped (internal name " ++ show v ++ ")") ---- ====== extractCtxs :: NewType -> (NewType, [(Id, Id)]) extractCtxs (NewType free exist ctxs nts) = (NewType free exist ctxs (filter (not . contextNT) nts), map ntContext2Pair (filter contextNT nts)) dictAndArrows :: Id -> Pos -> IntState -> [(Id, Id)] -> NewType -> ([(Id, TypeDict)], NT, IntState) dictAndArrows arrow pos state ectxs (NewType free exist ctxs nts) = case uniqueISs state (map (mapSnd ( \ v -> if v `elem` exist then mkNTexist v else mkNTvar v)) (ctxs ++ ectxs)) of (ctxsi,state) -> (cvi2typedict pos exist ctxsi ,funType arrow nts ,state ) funType :: Id -> [NT] -> NT funType arrow [x] = x funType arrow (x:xs) = mkNTcons arrow [x , funType arrow xs] typeError :: [Char] -> t -> TypeState -> a typeError err down up@(TypeState state phi ctxs ectxsi) = error err -- (PatWildcard noPos,TypeState (addError state err) phi ctxs ectxsi) getTypeErrors :: t -> TypeState -> ([String], TypeState) getTypeErrors down up@(TypeState state phi ctxs ectxsi) = let (st,errs) = getErrors state in (errs, TypeState st phi ctxs ectxsi)