module CSPM.TypeChecker.Unification (
generaliseGroup, instantiate, unify, unifyAll, evaluateDots,
typeToDotList,
) where
import Control.Monad
import Control.Monad.Trans
import Data.List (nub, (\\), intersect, group, sort)
import Prelude
import CSPM.DataStructures.Names
import CSPM.DataStructures.Types
import CSPM.TypeChecker.Environment
import CSPM.TypeChecker.Exceptions
import CSPM.TypeChecker.Monad
import Util.Exception
import Util.Monad
import Util.PrettyPrint
freeTypeVars :: Type -> TypeCheckMonad [(TypeVar, [Constraint])]
freeTypeVars = liftM nub . freeTypeVars'
freeTypeVars' :: Type -> TypeCheckMonad [(TypeVar, [Constraint])]
freeTypeVars' (TVar tv) = do
typ <- readTypeRef tv
case typ of
Left (tv, cs) -> return [(tv, cs)]
Right t -> freeTypeVars' t
freeTypeVars' (TFunction targs tr) =
liftM concat (mapM freeTypeVars' (tr:targs))
freeTypeVars' (TSeq t) = freeTypeVars' t
freeTypeVars' (TSet t) = freeTypeVars' t
freeTypeVars' (TTuple ts) = liftM concat (mapM freeTypeVars' ts)
freeTypeVars' (TDotable t1 t2) = liftM concat (mapM freeTypeVars' [t1,t2])
freeTypeVars' (TDot t1 t2) = liftM concat (mapM freeTypeVars' [t1,t2])
freeTypeVars' (TDatatype n1) = return []
freeTypeVars' TInt = return []
freeTypeVars' TBool = return []
freeTypeVars' TEvent = return []
freeTypeVars' TEventable = return []
freeTypeVars' TProc = return []
generaliseGroup :: [Name] -> [TypeCheckMonad [(Name, Type)]] ->
TypeCheckMonad [[(Name, TypeScheme)]]
generaliseGroup names tsm = do
ts <- sequence tsm
env <- getEnvironment
envfvs <- (liftM nub . concatMapM freeTypeVars)
[t | (n, SymbolInformation {
typeScheme = ForAll _ t
}) <- toList env, not (n `elem` names)]
mapM (\ nts -> mapM (\ (n,t) -> do
deffvs <- freeTypeVars t
let
unboundVars =
filter (\ (fv, cs) -> not (fv `elem` map fst envfvs)) deffvs
ts = ForAll unboundVars t
setType n ts
return (n, ts)) nts) ts
instantiate :: TypeScheme -> TypeCheckMonad Type
instantiate (ForAll ts t) = do
tvs <- mapM (freshTypeVarWithConstraints . snd) ts
foldM (\ x y -> substituteType y x) t (zip (map fst ts) tvs)
occurs :: TypeVar -> Type -> TypeCheckMonad Bool
occurs a (TVar (tvref @ (TypeVarRef tv _ _))) = do
res <- readTypeRef tvref
case res of
Left (tv,cs)-> return $ a == tv
Right t -> occurs a t
occurs a (TSet t) = occurs a t
occurs a (TSeq t) = occurs a t
occurs a (TDot t1 t2) = liftM or (mapM (occurs a) [t1,t2])
occurs a (TTuple ts) = liftM or (mapM (occurs a) ts)
occurs a (TFunction ts t) = liftM or (mapM (occurs a) (t:ts))
occurs a (TDatatype n) = return False
occurs a (TDotable t1 t2) = liftM or (mapM (occurs a) [t1,t2])
occurs a TInt = return False
occurs a TBool = return False
occurs a TProc = return False
occurs a TEvent = return False
occurs a TEventable = return False
unifyAll :: [Type] -> TypeCheckMonad Type
unifyAll [] = freshTypeVar
unifyAll [t] = return t
unifyAll (t1:ts) = do
t2 <- unifyAll ts
unify t1 t2
unifyConstraint :: Constraint -> Type -> TypeCheckMonad ()
unifyConstraint c (TVar v) = do
res <- readTypeRef v
case res of
Left (tva, cs) ->
if c `elem` cs then return () else do
fv <- freshTypeVarWithConstraints (nub (c:cs))
applySubstitution v fv
return ()
Right t -> unifyConstraint c t
unifyConstraint c TInt = return ()
unifyConstraint Eq TBool = return ()
unifyConstraint Inputable TBool = return ()
unifyConstraint c (TSeq t) = unifyConstraint c t
unifyConstraint Inputable (TDot t1 t2) = do
t <- evaluateDots (TDot t1 t2)
case t of
TDot t1 t2 -> mapM_ (unifyConstraint Inputable) [t1,t2]
_ -> unifyConstraint Inputable t
unifyConstraint c (TDot t1 t2) = mapM_ (unifyConstraint c) [t1,t2]
unifyConstraint c (TSet t) = return ()
unifyConstraint c (TTuple ts) = mapM_ (unifyConstraint c) ts
unifyConstraint Eq TEvent = return ()
unifyConstraint Inputable TEvent = return ()
unifyConstraint Eq TEventable = return ()
unifyConstraint Eq (TDotable a b) =
mapM_ (unifyConstraint Eq) [a,b]
unifyConstraint Eq (TDatatype n) = return ()
unifyConstraint Inputable (TDatatype n) = return ()
unifyConstraint c t =
raiseMessageAsError $ constraintUnificationErrorMessage c t
typeToDotList :: Type -> TypeCheckMonad [Type]
typeToDotList t = compress t >>= \ t ->
case t of
TDot t1 t2 -> do
(t:ts1) <- typeToDotList t1
ts2 <- typeToDotList t2
return (t:ts1++ts2)
_ -> return [t]
reduceDotable :: Type -> ([Type], Type)
reduceDotable (TDotable argt rt) =
let (args, urt) = reduceDotable rt in (argt:args, urt)
reduceDotable x = ([], x)
toNormalForm :: Type -> Type
toNormalForm (TDotable (TDot t1 t2) rt) =
toNormalForm (TDotable t1 (TDotable t2 rt))
toNormalForm (TDotable t1 (TDotable t2 rt)) =
TDotable t1 (toNormalForm (TDotable t2 rt))
toNormalForm x = x
isVar :: Type -> Bool
isVar (TVar _) = True
isVar _ = False
isDotable :: Type -> Bool
isDotable (TDotable _ _) = True
isDotable _ = False
isSimple :: Type -> Bool
isSimple a = not (isDotable a) && not (isVar a)
combineTypeLists :: [Type] -> [Type] -> TypeCheckMonad [Type]
combineTypeLists [] [] = return []
combineTypeLists ((TDot a1 a2):as) bs = do
ts <- typeToDotList (TDot a1 a2)
combineTypeLists (ts++as) bs
combineTypeLists as ((TDot b1 b2):bs) = do
ts <- typeToDotList (TDot b1 b2)
combineTypeLists as (ts++bs)
combineTypeLists (a:as) [b] = do
t <- unify b (foldr1 TDot (a:as))
return [t]
combineTypeLists [a] (b:bs) = do
t <- unify a (foldr1 TDot (b:bs))
return [t]
combineTypeLists (a:as) (b:bs) | not (isDotable a) && not (isDotable b) = do
t <- unify a b
ts <- combineTypeLists as bs
return (t:ts)
combineTypeLists ((a0@(TDotable argt rt)):a:as) (b:bs)
| (isSimple a || (isVar a && as /= [])) = do
unify argt a
combineTypeLists (rt:as) (b:bs)
| isVar a = do
let (args, urt) = reduceDotable (TDotable argt rt)
t:ts <- evalTypeList (b:bs)
t1 <- unify urt t
combineTypeLists (args++ts) [a]
return (t1:ts)
| isDotable a = do
let (argsA, rtA) = reduceDotable a
unify argt rtA
combineTypeLists (foldr TDotable rt argsA : as) (b:bs)
combineTypeLists (a:as) ((TDotable argt rt):b:bs)
| (isSimple b || (isVar b && bs /= [])) = do
unify b argt
combineTypeLists (a:as) (rt:bs)
| isVar b = do
let (args, urt) = reduceDotable (TDotable argt rt)
t:ts <- evalTypeList (a:as)
t1 <- unify t urt
combineTypeLists [b] (args++ts)
return (t1:ts)
| isDotable b = do
let (argsB, rtB) = reduceDotable b
unify rtB argt
combineTypeLists (a:as) (foldr TDotable rt argsB : bs)
combineTypeLists as bs = raiseUnificationError True
unify :: Type -> Type -> TypeCheckMonad Type
unify texp tact = do
text <- compress texp
tact <- compress tact
addUnificationPair (texp, tact) (unifyNoStk texp tact)
unifyNoStk :: Type -> Type -> TypeCheckMonad Type
unifyNoStk (TVar t1) (TVar t2) | t1 == t2 =
return (TVar t1)
unifyNoStk (TVar t1) (TVar t2) = do
res1 <- readTypeRef t1
res2 <- readTypeRef t2
case (res1, res2) of
(Left (tv1, cs1), Left (tv2,cs2)) -> do
fv <- freshTypeVarWithConstraints (nub (cs1 ++ cs2))
applySubstitution t1 fv
applySubstitution t2 fv
return fv
(Left _, Right t) -> unify (TVar t1) t
(Right t, Left _) -> unify t (TVar t2)
(Right t1, Right t2) -> unify t1 t2
unifyNoStk (TVar a) b = do
res <- readTypeRef a
case res of
Left (tva, cs) -> do
mapM_ (\ c -> unifyConstraint c b) cs
applySubstitution a b
Right t -> unify t b
unifyNoStk a (TVar b) = do
res <- readTypeRef b
case res of
Left (tvb, cs) -> do
mapM_ (\ c -> unifyConstraint c a) cs
applySubstitution b a
Right t -> unify a t
unifyNoStk TInt TInt = return TInt
unifyNoStk TBool TBool = return TBool
unifyNoStk TProc TProc = return TProc
unifyNoStk TEvent TEvent = return TEvent
unifyNoStk TEventable TEventable = return TEventable
unifyNoStk TEvent TEventable = return TEvent
unifyNoStk TEventable TEvent = return TEvent
unifyNoStk (TDatatype n1) (TDatatype n2)
| n1 == n2 = return $ TDatatype n1
unifyNoStk (TFunction ts1 rt1) (TFunction ts2 rt2) | length ts1 == length ts2 = do
ts <- zipWithM unify ts1 ts2
rt <- unify rt1 rt2
return $ TFunction ts rt
unifyNoStk (TSeq t1) (TSeq t2) = do
t <- unify t1 t2
return $ TSeq t
unifyNoStk (TSet t1) (TSet t2) = do
t <- unify t1 t2
return $ TSet t
unifyNoStk (TTuple ts1) (TTuple ts2) | length ts1 == length ts2 = do
ts <- zipWithM unify ts1 ts2
return $ TTuple ts
unifyNoStk (a@(TDotable _ _)) (b@(TDotable _ _)) = do
a <- compress a
b <- compress b
let
(argsA, rtA) = (reduceDotable . toNormalForm) a
(argsB, rtB) = (reduceDotable . toNormalForm) b
rt <- unify rtA rtB
case (rtA, rtB) of
(TEventable, TEventable) -> panic "TC: double eventable"
(TEventable, _) -> do
as <- evalTypeList argsA
bs <- evalTypeList argsB
let as' = map (snd . reduceDotable . toNormalForm) as
zipWithM unify as' bs
return $ TDotable (foldl1 TDot bs) rt
(_, TEventable) -> do
as <- evalTypeList argsA
bs <- evalTypeList argsB
let bs' = map (snd . reduceDotable . toNormalForm) bs
zipWithM unify as bs'
return $ TDotable (foldl1 TDot as) rt
(_, _) -> do
args <- combineTypeLists argsA argsB
return $ TDotable (foldl1 TDot args) rt
unifyNoStk (TDot t1 t2) (TDot t1' t2') = do
a0 <- typeToDotList (TDot t1 t2)
b0 <- typeToDotList (TDot t1' t2')
let a = map toNormalForm a0
let b = map toNormalForm b0
ts <- combineTypeLists a b
return $ foldl1 TDot ts
unifyNoStk (TDot t1 t2) (TDatatype n) = do
b <- symmetricUnificationAllowed
if not b then raiseUnificationError False else return ()
unify (TDotable t2 (TDatatype n)) t1
return $ TDatatype n
unifyNoStk (TDatatype n) (TDot t1 t2) = do
unify (TDotable t2 (TDatatype n)) t1
return $ TDatatype n
unifyNoStk (TDot t1 t2) TEvent = do
b <- symmetricUnificationAllowed
if not b then raiseUnificationError False else return ()
unify (TDotable t2 TEvent) t1
return TEvent
unifyNoStk TEvent (TDot t1 t2) = do
unify (TDotable t2 TEvent) t1
return TEvent
unifyNoStk (TDot t1 t2) TEventable = do
b <- symmetricUnificationAllowed
if not b then raiseUnificationError False else return ()
tl <- unify (TDotable t2 TEventable) t1
return $ TDot tl t2
unifyNoStk TEventable (TDot t1 t2) = do
tl <- unify (TDotable t2 TEventable) t1
return $ TDot tl t2
unifyNoStk (TDot t1 t2) (TDotable argt rt) = do
b <- symmetricUnificationAllowed
if not b then raiseUnificationError False else return ()
unify t1 (TDotable t2 (TDotable argt rt))
return $ TDotable argt rt
unifyNoStk (TDotable argt rt) (TDot t1 t2) = do
unify (TDotable t2 (TDotable argt rt)) t1
return $ TDotable argt rt
unifyNoStk (TDotable argt rt) TEventable = do
unify TEventable rt
return $ TDotable argt rt
unifyNoStk TEventable (TDotable argt rt) = do
unify TEventable rt
return $ TDotable argt rt
unifyNoStk t1 t2 = raiseUnificationError False
raiseUnificationError :: Bool -> TypeCheckMonad a
raiseUnificationError isDotError = do
b <- getInError
if b then throwException $ UserError else setInError True $ do
ts <- getUnificationStack
cts <- mapM (\ (t1, t2) -> do
t1 <- compress t1
t2 <- compress t2
(t1, t2) <- tryAndRecover (do
t1 <- evaluateDots t1
t2 <- evaluateDots t2
return (t1, t2)) (return (t1,t2))
return (t1, t2)) ts
raiseMessageAsError $ unificationErrorMessage cts
applySubstitution :: TypeVarRef -> Type -> TypeCheckMonad Type
applySubstitution (tvref @ (TypeVarRef tv _ _)) typ = do
t' <- compress typ
b <- occurs tv typ
(b, t) <- if b then do
t <- evaluateDots t'
b <- occurs tv t
return (b,t)
else return (b, typ)
errorIfFalse (not b)
(infiniteUnificationMessage (TVar tvref) t')
writeTypeRef tvref t
return typ
substituteType :: (TypeVar, Type) -> Type -> TypeCheckMonad Type
substituteType (tv, t) (b @ (TVar (a @ (TypeVarRef tv' cs ioref)))) = do
res <- readTypeRef a
case res of
Left tva -> if tv == tv' then return t else return b
Right t' -> substituteType (tv, t) t'
substituteType sub (TFunction targs tr) = do
targs' <- mapM (substituteType sub) targs
tr' <- substituteType sub tr
return $ TFunction targs' tr'
substituteType sub (TSeq t) = substituteType sub t >>= return . TSeq
substituteType sub (TDot t1 t2) = do
t1' <- substituteType sub t1
t2' <- substituteType sub t2
return $ TDot t1' t2'
substituteType sub (TSet t) = substituteType sub t >>= return . TSet
substituteType sub (TDotable t1 t2) = do
t1' <- substituteType sub t1
t2' <- substituteType sub t2
return $ TDotable t1' t2'
substituteType sub (TTuple ts) =
mapM (substituteType sub) ts >>= return . TTuple
substituteType sub (TDatatype n) = return $ TDatatype n
substituteType sub TInt = return TInt
substituteType sub TBool = return TBool
substituteType sub TProc = return TProc
substituteType sub TEvent = return TEvent
substituteType sub TEventable = return TEventable
evaluateDots :: Type -> TypeCheckMonad Type
evaluateDots (TVar t) = do
res <- readTypeRef t
case res of
Left (tv, cs) -> return $ TVar t
Right t -> evaluateDots t
evaluateDots (TSet t) = evaluateDots t >>= return . TSet
evaluateDots (TSeq t) = evaluateDots t >>= return . TSeq
evaluateDots (TTuple ts) = mapM evaluateDots ts >>= return . TTuple
evaluateDots t = do
ts <- typeToDotList t
ts <- mapM (\t -> compress t >>= return . toNormalForm) ts
ts <- evalTypeList ts
return $ foldr1 TDot ts
evalTypeList :: [Type] -> TypeCheckMonad [Type]
evalTypeList (t:[]) = return [t]
evalTypeList ((TDot t1 t2):ts) = evalTypeList (t1:t2:ts)
evalTypeList (TDotable argt rt : arg : args)
| isVar arg && args == [] = do
let (args, urt) = reduceDotable (TDotable argt rt)
unify arg (foldr1 TDot args)
return [urt]
| not (isDotable arg) = do
t <- unify argt arg
evalTypeList (rt:args)
| isDotable arg = do
let (argsA, rtA) = reduceDotable arg
t <- unify argt rtA
evalTypeList (foldr TDotable rt argsA : args)
evalTypeList (t:ts) = do
ts <- evalTypeList ts
return $ t:ts