module Types.Solver (solver) where
import Context
import Control.Arrow (second)
import Control.Monad (liftM)
import Data.Either (lefts,rights)
import Data.List (foldl')
import Data.Maybe (isJust)
import qualified Data.Set as Set
import qualified Data.Map as Map
import Guid
import Types.Types
import Types.Constrain
import Types.Substitutions
import Types.Alias (dealias)
isSolved ss (C _ _ (t1 :=: t2)) = t1 == t2
isSolved ss (C _ _ (x :<<: _)) = isJust (lookup x ss)
isSolved ss c = False
type Aliases = Map.Map String ([X],Type)
crush :: Aliases -> Scheme -> GuidCounter (Either String Scheme)
crush aliases (Forall xs cs t) =
do subs <- solver aliases Map.empty cs
return $ do ss' <- subs
let ss = Map.toList ss'
cs' = filter (not . isSolved ss) (subst ss cs)
return $ Forall xs cs' (subst ss t)
schemeSubHelp txt span x s t1 rltn t2 = do
(t1',cs1) <- sub t1
(t2',cs2) <- sub t2
return (C txt span (rltn t1' t2') : cs1 ++ cs2)
where sub t | not (occurs x t) = return (t, [])
| otherwise = do (st, cs) <- concretize s
return (subst [(x,st)] t, cs)
schemeSub aliases x s c =
do s' <- crush aliases s
case s' of
Right s'' -> Right `liftM` schemeSub' x s'' c
Left err -> return $ Left err
schemeSub' x s c@(C txt span constraint) =
case constraint of
(t1 :=: t2) -> schemeSubHelp txt span x s t1 (:=:) t2
(t1 :<: t2) -> schemeSubHelp txt span x s t1 (:<:) t2
(y :<<: Forall cxs ccs ctipe)
| not (occurs x c) -> return [c]
| otherwise ->
do Forall xs cs tipe <- rescheme s
let ss = [(x,tipe)]
constraints = subst ss (cs ++ ccs)
c' = y :<<: Forall (cxs ++ xs) constraints (subst ss ctipe)
return [ C txt span c' ]
recordConstraints eq fs t fs' t' =
liftM concat . sequence $
[ constrain fs fs'
, liftM concat . mapM (\(k,ts) -> zipper [] k ts []) . Map.toList $
Map.difference fs fs'
, liftM concat . mapM (\(k,ts) -> zipper [] k [] ts) . Map.toList $
Map.difference fs' fs
]
where constrain :: Map.Map String [Type] -> Map.Map String [Type]
-> GuidCounter [Context Constraint]
constrain as bs = liftM concat . sequence . Map.elems $
Map.intersectionWithKey (zipper []) as bs
zipper :: [Context Constraint] -> String -> [Type] -> [Type]
-> GuidCounter [Context Constraint]
zipper cs k xs ys =
case (xs,ys) of
(a:as, b:bs) -> zipper (eq a b : cs) k as bs
([],[]) -> return cs
(as,[]) -> do x <- guid
let tipe = RecordT (Map.singleton k as) (VarT x)
return (cs ++ [eq t' tipe])
([],bs) -> do x <- guid
let tipe = RecordT (Map.singleton k bs) (VarT x)
return (cs ++ [eq t tipe])
solver :: Aliases
-> Map.Map X Type
-> [Context Constraint]
-> GuidCounter (Either String (Map.Map X Type))
solver _ subs [] = return $ Right subs
solver aliases subs (C txt span c : cs) =
let ctx = C txt span
eq t1 t2 = ctx (t1 :=: t2)
solv = solver aliases subs
uniError' = uniError (\t1 t2 -> solv (eq t1 t2 : cs)) aliases txt span
in case c of
t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2) ->
if n1 == n2 then solv (zipWith eq ts1 ts2 ++ cs)
else uniError' t1 t2
LambdaT t1 t2 :=: LambdaT t1' t2' ->
solv ([ eq t1 t1', eq t2 t2' ] ++ cs)
RecordT fs t :=: RecordT fs' t' ->
do cs' <- recordConstraints eq fs t fs' t'
solv (cs' ++ cs)
VarT x :=: VarT y
| x == y -> solv cs
| otherwise ->
case (Map.lookup x subs, Map.lookup y subs) of
(Just (Super xts), Just (Super yts)) ->
let ts = Set.intersection xts yts
setXY t = Map.insert x t . Map.insert y t
in case Set.toList ts of
[] -> unionError txt span xts yts
[t] -> let cs1 = subst [(x,t),(y,t)] cs in
cs1 `seq` solver aliases (setXY t subs) cs1
_ -> solver aliases (setXY (Super ts) subs) cs
(Just (Super xts), _) ->
let cs2 = subst [(y,VarT x)] cs in
solver aliases (Map.insert y (VarT x) subs) cs2
(_, _) ->
let cs3 = subst [(x,VarT y)] cs in
solver aliases (Map.insert x (VarT y) subs) cs3
VarT x :=: t -> do
if x `occurs` t then occursError txt span (VarT x) t else
(case Map.lookup x subs of
Nothing ->
let cs4 = subst [(x,t)] cs
subs' = Map.map (subst [(x,t)]) $ Map.insert x t subs
in solver aliases subs' cs4
Just (Super ts) ->
let ts' = Set.intersection ts (Set.singleton t) in
case Set.toList ts' of
[] -> solv (ctx (t :<: Super ts) : cs)
[t'] -> let cs5 = subst [(x,t)] cs in
solver aliases (Map.insert x t' subs) cs5
_ -> solver aliases (Map.insert x (Super ts') subs) cs
Just t' -> solv (ctx (t' :=: t) : cs)
)
t :=: VarT x -> solv ((ctx (VarT x :=: t)) : cs)
t1 :=: t2 | t1 == t2 -> solv cs
| otherwise -> uniError' t1 t2
VarT x :<: Super ts ->
case Map.lookup x subs of
Nothing -> solver aliases (Map.insert x (Super ts) subs) cs
Just (Super ts') ->
case Set.toList $ Set.intersection ts ts' of
[] -> unionError txt span ts ts'
[t] -> solver aliases (Map.insert x t subs) (subst [(x,t)] cs)
ts'' -> solver aliases subs' cs
where subs' = Map.insert x (Super $ Set.fromList ts'') subs
ADT "List" [t] :<: Super ts
| any f (Set.toList ts) -> solv cs
| otherwise -> subtypeError txt span (ADT "List" [t]) (Super ts)
where f (ADT "List" [VarT _]) = True
f (ADT "List" [t']) = dealias aliases t == t'
f _ = False
t :<: Super ts
| Set.member t ts -> solv cs
| Set.member (dealias aliases t) ts -> solv cs
| otherwise -> subtypeError txt span t (Super ts)
x :<<: s
| any (occurs x) cs ->
do css <- mapM (schemeSub aliases x s) cs
case lefts css of
err : _ -> return $ Left err
[] -> solv (concat (rights css))
| otherwise ->
do (t,cs7) <- concretize s
solv (cs ++ ctx (VarT x :=: t) : cs7)
showMsg msg = case msg of
Just str -> "\nIn context: " ++ str
Nothing -> ""
occursError msg span t1 t2 =
return . Left $ concat
[ "Type error (" ++ show span ++ "):\n"
, "Occurs check: cannot construct the infinite type:\n"
, show t1, " = ", show t2, showMsg msg ]
uniError solveWith aliases msg span t1 t2 =
let t1' = dealias aliases t1
t2' = dealias aliases t2
in if t1 /= t1' || t2 /= t2'
then solveWith t1' t2'
else return . Left $ concat
[ "Type error (" ++ show span ++ "):\n"
, show t1, " is not equal to ", show t2, showMsg msg ]
unionError msg span ts ts' =
return . Left $ concat
[ "Type error (" ++ show span ++ "):\n"
, "There are no types in both "
, show (Super ts), " and ", show (Super ts'), showMsg msg ]
subtypeError msg span t s =
return . Left $ concat
[ "Type error (" ++ show span ++ "):\n"
, show t, " is not a ", show s, showMsg msg ]