module CSPM.TypeChecker.Unification (
generaliseGroup, instantiate, unify, unifyAll, evaluateDots,
typeToDotList, dotableToDotList, substituteTypes, instantiate',
) where
import Control.Monad
import Data.List (nub, 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
freeTypeVars :: Type -> TypeCheckMonad [(TypeVar, [Constraint])]
freeTypeVars = liftM (nub . sort) . 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' (TMap t1 t2) = liftM concat (mapM freeTypeVars' [t1,t2])
freeTypeVars' (TDatatype n1) = return []
freeTypeVars' TInt = return []
freeTypeVars' TBool = return []
freeTypeVars' TEvent = return []
freeTypeVars' TChar = return []
freeTypeVars' (TExtendable t pt) = do
fvs1 <- freeTypeVars' t
res <- readTypeRef pt
case res of
Left (tv, cs) -> do
return $ (tv, cs):fvs1
Right t -> do
fvs2 <- freeTypeVars' t
return $ fvs1 ++ fvs2
freeTypeVars' TProc = return []
freeTypeVars' TExtendableEmptyDotList = 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 ts = instantiate' ts >>= return . fst
instantiate' :: TypeScheme -> TypeCheckMonad (Type, [(TypeVar, Type)])
instantiate' (ForAll ts t) = do
tvs <- mapM (freshTypeVarWithConstraints . snd) ts
let sub = (zip (map fst ts) tvs)
t <- substituteTypes sub t
return (t, sub)
occurs :: TypeVar -> Type -> TypeCheckMonad Bool
occurs a (TVar tvref) = 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 (TMap 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 TChar = return False
occurs a (TExtendable t pt) = do
b <- occurs a t
if b then return True else do
res <- readTypeRef pt
case res of
Left (tv, cs) | a == tv -> return True
Left _ -> return False
Right t -> occurs a t
occurs a TExtendableEmptyDotList = 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) | isRigid v = do
when (not (or (map (constraintImpliedBy c) (constraints v)))) $ do
raiseMessageAsError $ constraintUnificationErrorMessage c (TVar v)
unifyConstraint c (TVar v) = do
res <- readTypeRef v
case res of
Left (tva, cs) ->
when (not (or (map (constraintImpliedBy c) cs))) $ do
fv <- freshTypeVarWithConstraints (nub (sort (c:cs)))
applySubstitution v fv
return ()
Right t -> unifyConstraint c t
unifyConstraint c (TExtendable t pt) = do
res <- readTypeRef pt
case res of
Left _ ->
if c == CYieldable then
safeWriteTypeRef pt TExtendableEmptyDotList
else if c == CInputable then do
unifyConstraint c t
safeWriteTypeRef pt TExtendableEmptyDotList
else
when (c /= CEq && c /= CSet) $ raiseMessageAsError $
constraintUnificationErrorMessage c (TExtendable t pt)
Right t -> do
t' <- compress (TExtendable t pt)
unifyConstraint c t'
unifyConstraint CYieldable (TDatatype n) = return ()
unifyConstraint CYieldable TEvent = return ()
unifyConstraint CYieldable (TDot t1 t2) = do
t <- evaluateDots (TDot t1 t2)
case t of
TDot _ _ -> raiseMessageAsError $
constraintUnificationErrorMessage CYieldable t
_ -> unifyConstraint CYieldable t
unifyConstraint CYieldable t =
raiseMessageAsError $ constraintUnificationErrorMessage CYieldable t
unifyConstraint CSet TProc = return ()
unifyConstraint c TInt = return ()
unifyConstraint c TChar = return ()
unifyConstraint c TBool | c /= COrd = return ()
unifyConstraint CEq (TDatatype n) = do
b <- datatypeIsComparableForEquality n
if b then return ()
else raiseMessageAsError $ constraintUnificationErrorMessage CEq (TDatatype n)
unifyConstraint c (TDatatype n) | c /= COrd = return ()
unifyConstraint c TEvent | c /= COrd = return ()
unifyConstraint CInputable (TSeq _) = return ()
unifyConstraint CSet (TSeq t) = unifyConstraint CSet t
unifyConstraint CEq (TSeq t) = unifyConstraint CEq t
unifyConstraint COrd (TSeq t) = unifyConstraint CEq t
unifyConstraint CInputable (TTuple _) = return ()
unifyConstraint c (TTuple ts) = mapM_ (unifyConstraint c) ts
unifyConstraint CEq (TDotable a b) = unifyConstraint CEq a >> unifyConstraint CEq b
unifyConstraint CSet (TDotable a b) = unifyConstraint CSet a >> unifyConstraint CSet b
unifyConstraint CInputable (TDot t1 t2) = do
t <- evaluateDots (TDot t1 t2)
case t of
TDot t1 t2 -> mapM_ (unifyConstraint CInputable) [t1,t2]
_ -> unifyConstraint CInputable t
unifyConstraint c (TDot t1 t2) | c /= COrd =
unifyConstraint c t1 >> unifyConstraint c t2
unifyConstraint CSet (TSet t) = unifyConstraint CSet t
unifyConstraint CInputable (TSet t) = return ()
unifyConstraint CEq (TSet t) = unifyConstraint CEq t
unifyConstraint COrd (TSet t) = unifyConstraint CEq t
unifyConstraint CInputable (TMap _ _) = return ()
unifyConstraint c (TMap k v) = unifyConstraint c k >> unifyConstraint c v
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]
dotableToDotList :: Type -> TypeCheckMonad ([Type], Type)
dotableToDotList t = compress t >>= return . reduceDotable
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
isExtendable :: Type -> Bool
isExtendable (TExtendable _ _) = True
isExtendable _ = 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)
| isDotable argt = do
unify argt a
combineTypeLists (rt: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 LongestMatch (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)
| isDotable argt = do
unify argt b
combineTypeLists (a:as) (rt: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 LongestMatch (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
texp <- 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
let cs = nub $ sort $ cs1++cs2
if isRigid t1 && isRigid t2 then do
when (t1 /= t2) $ raiseUnificationError False
return $ TVar t1
else if isRigid t1 then do
mapM_ (flip unifyConstraint (TVar t1)) cs
applySubstitution t2 (TVar t1)
else if isRigid t2 then do
mapM_ (flip unifyConstraint (TVar t2)) cs
applySubstitution t1 (TVar t2)
else do
fv <- freshTypeVarWithConstraints cs
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 TChar TChar = return TChar
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 (TMap k1 v1) (TMap k2 v2) = do
k <- unify k1 k2
v <- unify v1 v2
return $ TMap k v
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
case (rtA, rtB) of
(TExtendable _ _, TExtendable _ _) -> do
rt <- unify rtA rtB
as <- evalTypeList LongestMatch argsA
bs <- evalTypeList LongestMatch argsB
let as' = map (snd . reduceDotable . toNormalForm) as
bs' = map (snd . reduceDotable . toNormalForm) bs
ts <- zipWithM unify as' bs'
let ts' = drop (length ts) (if length as == length ts then bs else as)
return $ TDotable (foldl1 TDot (ts++ts')) rtA
(TExtendable _ _, _) -> do
as <- evalTypeList LongestMatch argsA
bs <- evalTypeList LongestMatch argsB
let as' = map (snd . reduceDotable . toNormalForm) as
ts <- zipWithM unify as' bs
let remainingArgs = drop (length as') bs
unify rtA (foldr TDotable rtB remainingArgs)
let ts' = drop (length ts) (if length as' == length ts then bs else as')
args = ts ++ ts'
return $ TDotable (foldl1 TDot args) rtB
(_, TExtendable _ _) -> do
rt <- unify rtA rtB
as <- evalTypeList LongestMatch argsA
bs <- evalTypeList LongestMatch argsB
let bs' = map (snd . reduceDotable . toNormalForm) bs
ts <- zipWithM unify as bs'
let remainingArgs = drop (length bs') as
unify (foldr TDotable rtA remainingArgs) rtB
let ts' = drop (length ts) (if length bs' == length ts then as else bs')
args = ts ++ ts'
return $ TDotable (foldl1 TDot args) rtA
(_, _) -> do
rt <- unify rtA rtB
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) (TExtendable t pt) = do
b <- symmetricUnificationAllowed
if not b then raiseUnificationError False else return ()
tl <- unify (TDotable t2 (TExtendable t pt)) t1
return $ TDot tl t2
unifyNoStk (TExtendable t pt) (TDot t1 t2) = do
tl <- typeToDotList (TDot t1 t2)
tl <- mapM (\x -> compress x >>= return . toNormalForm) tl
tl <- evalTypeList ShortestMatch tl
case foldr1 TDot tl of
TDot t1 t2 -> do
t1' <- unify (TDotable t2 (TExtendable t pt)) t1
return $ TDot t1' t2
tl -> unify (TExtendable t pt) tl
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) (TExtendable t pt) = do
pt' <- freshTypeVarRef []
rt' <- unify (TExtendable t pt') rt
safeWriteTypeRef pt $! TDotable argt (TVar pt')
return $! TDotable argt (TExtendable t pt')
unifyNoStk (TExtendable t pt) (TDotable argt rt) = do
pt' <- freshTypeVarRef []
rt' <- unify (TExtendable t pt') rt
safeWriteTypeRef pt $! TDotable argt (TVar pt')
return $! TDotable argt (TExtendable t pt')
unifyNoStk (TExtendable t1 pt1) (TExtendable t2 pt2) | pt1 == pt2 = do
t <- unify t1 t2
return $ TExtendable t pt1
unifyNoStk (TExtendable t1 pt1) (TExtendable t2 pt2) = do
t <- unify t1 t2
if isRigid pt2 then safeWriteTypeRef pt1 (TVar pt2)
else safeWriteTypeRef pt2 (TVar pt1)
return $ TExtendable t pt1
unifyNoStk (TExtendable t1 pt) t2 = do
t <- unify t1 t2
safeWriteTypeRef pt TExtendableEmptyDotList
return t
unifyNoStk t1 (TExtendable t2 pt) = do
t <- unify t1 t2
safeWriteTypeRef pt TExtendableEmptyDotList
return t
unifyNoStk t1 t2 = raiseUnificationError False
safeWriteTypeRef :: TypeVarRef -> Type -> TypeCheckMonad ()
safeWriteTypeRef (RigidTypeVarRef tv cs n) t = raiseUnificationError False
safeWriteTypeRef tvref t = writeTypeRef tvref t
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 False (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 typ = do
t' <- compress typ
b <- occurs (typeVar tvref) typ
if b then do
t <- evaluateDots t'
if t == TVar tvref then return t else do
b <- occurs (typeVar tvref) t
errorIfFalse (not b) (infiniteUnificationMessage (TVar tvref) typ)
safeWriteTypeRef tvref t
return t
else do
safeWriteTypeRef tvref typ
return typ
substituteTypes :: [(TypeVar, Type)] -> Type -> TypeCheckMonad Type
substituteTypes sub t = foldM (\ x y -> substituteType y x) t sub
substituteType :: (TypeVar, Type) -> Type -> TypeCheckMonad Type
substituteType (tv, t) (b @ (TVar tvref)) = do
res <- readTypeRef tvref
case res of
Left (tv', _) -> 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 (TMap t1 t2) =
return TMap $$ substituteType sub t1 $$ substituteType sub t2
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 TChar = return TChar
substituteType sub TExtendableEmptyDotList = return TExtendableEmptyDotList
substituteType (sub@(tv, TVar spt)) (TExtendable t tvref) = do
t' <- substituteType sub t
res <- readTypeRef tvref
case res of
Left (tv', _) -> do
let pt' = if tv == tv' then spt else tvref
return $ TExtendable t' pt'
Right t' -> do
substituteType sub t'
return $ TExtendable t' tvref
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 (TMap t1 t2) = return TMap $$ evaluateDots t1 $$ evaluateDots t2
evaluateDots (TSeq t) = evaluateDots t >>= return . TSeq
evaluateDots (TTuple ts) = mapM evaluateDots ts >>= return . TTuple
evaluateDots (TExtendable t pt) = compress (TExtendable t pt) >>= \ t -> do
case t of
TExtendable t pt -> return $! TExtendable t pt
t -> evaluateDots t
evaluateDots (TFunction t1 t2) = do
t1' <- mapM evaluateDots t1
t2' <- evaluateDots t2
return $ TFunction t1' t2'
evaluateDots t = do
ts <- typeToDotList t
ts <- mapM (\t -> compress t >>= return . toNormalForm) ts
ts <- evalTypeList LongestMatch ts
return $ foldr1 TDot ts
data TypeListMode = ShortestMatch | LongestMatch deriving Eq
evalTypeList m ts = mapM compress ts >>= \ ts -> evalTypeList' m ts
evalTypeList' :: TypeListMode -> [Type] -> TypeCheckMonad [Type]
evalTypeList' _ (t:[]) = return [t]
evalTypeList' m ((TDot t1 t2):ts) = evalTypeList m (t1:t2:ts)
evalTypeList' m (TDotable argt rt : arg : args)
| isVar arg && args == [] && m == LongestMatch = do
let (args, urt) = reduceDotable (TDotable argt rt)
unify arg (foldr1 TDot args)
return [urt]
| isVar arg && args == [] && m == ShortestMatch = do
let (arg':args, urt) = reduceDotable (TDotable argt rt)
unify arg' arg
return [foldr TDotable urt args]
| isExtendable arg = do
let TExtendable rtA ptref = arg
t <- unify argt rtA
evalTypeList m (TExtendable rt ptref : args)
| not (isDotable arg) = do
t <- unify argt arg
evalTypeList m (rt:args)
| isDotable argt && isDotable arg = do
unify argt arg
evalTypeList m (rt:args)
| isDotable arg = do
let (argsA, rtA) = reduceDotable arg
t <- unify argt rtA
evalTypeList m (foldr TDotable rt argsA : args)
evalTypeList' LongestMatch (TExtendable urt pt : args) = do
args <- evalTypeList LongestMatch args
safeWriteTypeRef pt $! foldr TDotable TExtendableEmptyDotList args
return [urt]
evalTypeList' ShortestMatch (TExtendable urt pt : arg : args) = do
res <- readTypeRef pt
safeWriteTypeRef pt $! TDotable arg TExtendableEmptyDotList
evalTypeList ShortestMatch (urt : args)
evalTypeList' m (t:ts) = do
ts <- evalTypeList m ts
return $ t:ts