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
isSolved ss (C _ _ (t1 :=: t2)) = t1 == t2
isSolved ss (C _ _ (x :<<: _)) = isJust (lookup x ss)
isSolved ss c = False
crush :: Scheme -> GuidCounter (Either String Scheme)
crush (Forall xs cs t) =
do subs <- solver cs Map.empty
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 x s c = do s' <- crush 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 :: [Context Constraint]
-> Map.Map X Type
-> GuidCounter (Either String (Map.Map X Type))
solver [] subs = return $ Right subs
solver (C txt span c : cs) subs =
let ctx = C txt span in
let eq t1 t2 = ctx (t1 :=: t2) in
case c of
t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2) ->
if n1 /= n2 then uniError txt span t1 t2 else
solver (zipWith eq ts1 ts2 ++ cs) subs
LambdaT t1 t2 :=: LambdaT t1' t2' ->
solver ([ eq t1 t1', eq t2 t2' ] ++ cs) subs
RecordT fs t :=: RecordT fs' t' ->
do cs' <- recordConstraints eq fs t fs' t'
solver (cs' ++ cs) subs
VarT x :=: VarT y
| x == y -> solver cs subs
| 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 cs1 (setXY t subs)
_ -> solver cs $ setXY (Super ts) subs
(Just (Super xts), _) ->
let cs2 = subst [(y,VarT x)] cs in
solver cs2 $ Map.insert y (VarT x) subs
(_, _) ->
let cs3 = subst [(x,VarT y)] cs in
solver cs3 $ Map.insert x (VarT y) subs
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 in
solver cs4 . Map.map (subst [(x,t)]) $
Map.insert x t subs
Just (Super ts) ->
let ts' = Set.intersection ts (Set.singleton t) in
case Set.toList ts' of
[] -> solver (ctx (t :<: Super ts) : cs) subs
[t'] -> let cs5 = subst [(x,t)] cs in
solver cs5 $ Map.insert x t' subs
_ -> solver cs $ Map.insert x (Super ts') subs
Just t' -> solver (ctx (t' :=: t) : cs) subs
)
t :=: VarT x -> solver ((ctx (VarT x :=: t)) : cs) subs
t1 :=: t2 | t1 == t2 -> solver cs subs
| otherwise -> uniError txt span t1 t2
VarT x :<: Super ts ->
case Map.lookup x subs of
Nothing -> solver cs $ Map.insert x (Super ts) subs
Just (Super ts') ->
case Set.toList $ Set.intersection ts ts' of
[] -> unionError txt span ts ts'
[t] -> solver (subst [(x,t)] cs) $ Map.insert x t subs
ts'' -> solver cs $
Map.insert x (Super $ Set.fromList ts'') subs
ADT "List" [t] :<: Super ts
| any f (Set.toList ts) -> solver cs subs
| otherwise -> subtypeError txt span (ADT "List" [t]) (Super ts)
where f (ADT "List" [VarT _]) = True
f (ADT "List" [t']) = t == t'
f _ = False
t :<: Super ts
| Set.member t ts -> solver cs subs
| otherwise -> subtypeError txt span t (Super ts)
x :<<: s
| any (occurs x) cs ->
do css <- mapM (schemeSub x s) cs
case lefts css of
err : _ -> return $ Left err
[] -> solver (concat (rights css)) subs
| otherwise ->
do (t,cs7) <- concretize s
let cs'' = (cs ++ ctx (VarT x :=: t) : cs7)
solver cs'' subs
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 msg span t1 t2 =
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 ]