2013-07-09 08:25:50 +00:00
|
|
|
module Type.State where
|
|
|
|
|
|
|
|
import Type.Type
|
2013-07-09 19:52:05 +00:00
|
|
|
import qualified Data.Map as Map
|
2013-07-10 12:31:57 +00:00
|
|
|
import qualified Data.List as List
|
2013-07-09 08:25:50 +00:00
|
|
|
import qualified Type.Environment as Env
|
|
|
|
import qualified Data.UnionFind.IO as UF
|
|
|
|
import Control.Monad.State
|
2013-07-09 19:52:05 +00:00
|
|
|
import Control.Applicative ((<$>),(<*>), Applicative)
|
|
|
|
import qualified Data.Traversable as Traversable
|
2013-07-10 12:31:57 +00:00
|
|
|
import Text.PrettyPrint as P
|
2013-07-09 19:52:05 +00:00
|
|
|
import SourceSyntax.PrettyPrint
|
2013-07-30 23:22:20 +00:00
|
|
|
import SourceSyntax.Location
|
2013-07-09 08:25:50 +00:00
|
|
|
|
|
|
|
-- Pool
|
|
|
|
-- Holds a bunch of variables
|
|
|
|
-- The rank of each variable is less than or equal to the pool's "maxRank"
|
|
|
|
-- The young pool exists to make it possible to identify these vars in constant time.
|
|
|
|
|
|
|
|
data Pool = Pool {
|
|
|
|
maxRank :: Int,
|
|
|
|
inhabitants :: [Variable]
|
2013-07-09 19:52:05 +00:00
|
|
|
} deriving Show
|
|
|
|
|
2013-07-12 09:05:03 +00:00
|
|
|
emptyPool = Pool { maxRank = outermostRank, inhabitants = [] }
|
2013-07-09 08:25:50 +00:00
|
|
|
|
|
|
|
-- Keeps track of the environment, type variable pool, and a list of errors
|
2013-07-19 15:50:16 +00:00
|
|
|
data SolverState = SS {
|
|
|
|
sEnv :: Map.Map String Variable,
|
|
|
|
sSavedEnv :: Map.Map String Variable,
|
|
|
|
sPool :: Pool,
|
|
|
|
sMark :: Int,
|
|
|
|
sErrors :: [IO P.Doc]
|
|
|
|
}
|
2013-07-09 19:52:05 +00:00
|
|
|
|
2013-07-19 15:50:16 +00:00
|
|
|
initialState = SS {
|
|
|
|
sEnv = Map.empty,
|
|
|
|
sSavedEnv = Map.empty,
|
|
|
|
sPool = emptyPool,
|
|
|
|
sMark = noMark + 1, -- The mark must never be equal to noMark!
|
|
|
|
sErrors = []
|
|
|
|
}
|
2013-07-09 08:25:50 +00:00
|
|
|
|
2013-07-19 15:50:16 +00:00
|
|
|
modifyEnv f = modify $ \state -> state { sEnv = f (sEnv state) }
|
|
|
|
modifyPool f = modify $ \state -> state { sPool = f (sPool state) }
|
2013-07-25 13:46:48 +00:00
|
|
|
|
2013-07-30 23:22:20 +00:00
|
|
|
addError span message t1 t2 =
|
2013-07-19 15:50:16 +00:00
|
|
|
modify $ \state -> state { sErrors = err : sErrors state }
|
2013-07-10 12:31:57 +00:00
|
|
|
where
|
2013-07-10 22:31:56 +00:00
|
|
|
err = makeError <$> extraPretty t1 <*> extraPretty t2
|
2013-07-30 23:22:20 +00:00
|
|
|
|
2013-08-03 19:28:59 +00:00
|
|
|
location = case span of
|
|
|
|
NoSpan msg -> ""
|
|
|
|
Span p1 p2 msg ->
|
|
|
|
if line p1 == line p2 then " on line " ++ show (line p1)
|
|
|
|
else " between lines " ++ show (line p1) ++ " and " ++ show (line p2)
|
|
|
|
|
|
|
|
display msg = if null msg then "\n"
|
|
|
|
else "\n" ++ unlines (map (" "++) $ lines msg)
|
|
|
|
|
|
|
|
src = case span of
|
|
|
|
NoSpan msg -> display msg
|
|
|
|
Span _ _ msg -> display msg
|
2013-08-03 18:41:47 +00:00
|
|
|
|
2013-08-07 09:12:11 +00:00
|
|
|
defaultMessage = "Something weird is happening with this value:"
|
2013-08-07 05:12:26 +00:00
|
|
|
|
2013-07-10 22:31:56 +00:00
|
|
|
makeError pt1 pt2 =
|
2013-08-03 19:28:59 +00:00
|
|
|
P.vcat [ P.text $ "Type error" ++ location ++ ":"
|
2013-08-07 05:12:26 +00:00
|
|
|
, P.vcat . map P.text . lines $ if null message then defaultMessage else message
|
2013-08-03 19:28:59 +00:00
|
|
|
, P.text src
|
2013-07-10 22:31:56 +00:00
|
|
|
, P.text " Expected Type:" <+> pt1
|
|
|
|
, P.text " Actual Type:" <+> pt2 <> P.text "\n"
|
|
|
|
]
|
2013-07-09 19:52:05 +00:00
|
|
|
|
|
|
|
switchToPool pool = modifyPool (\_ -> pool)
|
2013-07-09 08:25:50 +00:00
|
|
|
|
|
|
|
getPool :: StateT SolverState IO Pool
|
2013-07-19 15:50:16 +00:00
|
|
|
getPool = sPool <$> get
|
2013-07-09 08:25:50 +00:00
|
|
|
|
2013-07-09 19:52:05 +00:00
|
|
|
getEnv :: StateT SolverState IO (Map.Map String Variable)
|
2013-07-19 15:50:16 +00:00
|
|
|
getEnv = sEnv <$> get
|
|
|
|
|
|
|
|
saveLocalEnv :: StateT SolverState IO ()
|
|
|
|
saveLocalEnv = do
|
|
|
|
env <- sEnv <$> get
|
|
|
|
modify $ \state -> state { sSavedEnv = env }
|
2013-07-09 19:52:05 +00:00
|
|
|
|
|
|
|
uniqueMark :: StateT SolverState IO Int
|
|
|
|
uniqueMark = do
|
2013-07-19 15:50:16 +00:00
|
|
|
state <- get
|
|
|
|
let mark = sMark state
|
|
|
|
put $ state { sMark = mark + 1 }
|
2013-07-09 19:52:05 +00:00
|
|
|
return mark
|
|
|
|
|
|
|
|
nextRankPool :: StateT SolverState IO Pool
|
|
|
|
nextRankPool = do
|
|
|
|
pool <- getPool
|
2013-07-09 08:25:50 +00:00
|
|
|
return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
|
|
|
|
|
|
|
|
register :: Variable -> StateT SolverState IO Variable
|
|
|
|
register variable = do
|
|
|
|
modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
|
|
|
|
return variable
|
|
|
|
|
|
|
|
introduce :: Variable -> StateT SolverState IO Variable
|
|
|
|
introduce variable = do
|
2013-07-09 19:52:05 +00:00
|
|
|
pool <- getPool
|
2013-07-09 08:25:50 +00:00
|
|
|
liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
|
|
|
|
register variable
|
|
|
|
|
|
|
|
flatten :: Type -> StateT SolverState IO Variable
|
|
|
|
flatten term =
|
|
|
|
case term of
|
|
|
|
VarN v -> return v
|
|
|
|
TermN t -> do
|
2013-07-09 19:52:05 +00:00
|
|
|
flatStructure <- traverseTerm flatten t
|
|
|
|
pool <- getPool
|
2013-07-09 08:25:50 +00:00
|
|
|
var <- liftIO . UF.fresh $ Descriptor {
|
|
|
|
structure = Just flatStructure,
|
|
|
|
rank = maxRank pool,
|
|
|
|
flex = Flexible,
|
|
|
|
name = Nothing,
|
2013-07-09 19:52:05 +00:00
|
|
|
copy = Nothing,
|
|
|
|
mark = noMark
|
2013-07-09 08:25:50 +00:00
|
|
|
}
|
2013-07-09 19:52:05 +00:00
|
|
|
register var
|
|
|
|
|
|
|
|
makeInstance :: Variable -> StateT SolverState IO Variable
|
|
|
|
makeInstance var = do
|
|
|
|
alreadyCopied <- uniqueMark
|
|
|
|
freshVar <- makeCopy alreadyCopied var
|
|
|
|
restore alreadyCopied var
|
|
|
|
return freshVar
|
|
|
|
|
|
|
|
makeCopy :: Int -> Variable -> StateT SolverState IO Variable
|
|
|
|
makeCopy alreadyCopied variable = do
|
|
|
|
desc <- liftIO $ UF.descriptor variable
|
2013-07-31 05:57:13 +00:00
|
|
|
case () of
|
|
|
|
() | mark desc == alreadyCopied ->
|
2013-07-09 19:52:05 +00:00
|
|
|
case copy desc of
|
|
|
|
Just v -> return v
|
2013-08-12 21:30:32 +00:00
|
|
|
Nothing -> error $ "Error copying type variable. This should be impossible." ++
|
|
|
|
" Please report an error to the github repo!"
|
2013-07-09 19:52:05 +00:00
|
|
|
|
2013-07-31 05:57:13 +00:00
|
|
|
| rank desc /= noRank || flex desc == Constant ->
|
2013-07-10 12:31:57 +00:00
|
|
|
return variable
|
2013-07-09 19:52:05 +00:00
|
|
|
|
2013-07-31 05:57:13 +00:00
|
|
|
| otherwise -> do
|
|
|
|
pool <- getPool
|
|
|
|
newVar <- liftIO $ UF.fresh $ Descriptor {
|
|
|
|
structure = Nothing,
|
|
|
|
rank = maxRank pool,
|
|
|
|
mark = noMark,
|
|
|
|
flex = case flex desc of
|
|
|
|
Is s -> Is s
|
|
|
|
_ -> Flexible,
|
|
|
|
copy = Nothing,
|
|
|
|
name = case flex desc of
|
|
|
|
Rigid -> Nothing
|
|
|
|
_ -> name desc
|
|
|
|
}
|
|
|
|
register newVar
|
|
|
|
|
|
|
|
-- Link the original variable to the new variable. This lets us
|
|
|
|
-- avoid making multiple copies of the variable we are instantiating.
|
|
|
|
--
|
|
|
|
-- Need to do this before recursively copying the structure of
|
|
|
|
-- the variable to avoid looping on cyclic terms.
|
|
|
|
liftIO $ UF.modifyDescriptor variable $ \desc ->
|
|
|
|
desc { mark = alreadyCopied, copy = Just newVar }
|
|
|
|
|
|
|
|
-- Now we recursively copy the structure of the variable.
|
|
|
|
-- We have already marked the variable as copied, so we
|
|
|
|
-- will not repeat this work or crawl this variable again.
|
|
|
|
case structure desc of
|
|
|
|
Nothing -> return newVar
|
|
|
|
Just term -> do
|
|
|
|
newTerm <- traverseTerm (makeCopy alreadyCopied) term
|
|
|
|
liftIO $ UF.modifyDescriptor newVar $ \desc ->
|
|
|
|
desc { structure = Just newTerm }
|
|
|
|
return newVar
|
2013-07-09 19:52:05 +00:00
|
|
|
|
|
|
|
restore :: Int -> Variable -> StateT SolverState IO Variable
|
|
|
|
restore alreadyCopied variable = do
|
|
|
|
desc <- liftIO $ UF.descriptor variable
|
2013-07-10 12:31:57 +00:00
|
|
|
if mark desc /= alreadyCopied
|
2013-07-12 09:05:03 +00:00
|
|
|
then return variable
|
2013-07-11 10:48:37 +00:00
|
|
|
else do
|
2013-07-09 19:52:05 +00:00
|
|
|
restoredStructure <-
|
2013-07-12 09:05:03 +00:00
|
|
|
Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
|
|
|
|
liftIO $ UF.modifyDescriptor variable $ \desc ->
|
2013-07-09 19:52:05 +00:00
|
|
|
desc { mark = noMark, rank = noRank, structure = restoredStructure }
|
|
|
|
return variable
|
|
|
|
|
|
|
|
traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
|
|
|
|
traverseTerm f term =
|
|
|
|
case term of
|
|
|
|
App1 a b -> App1 <$> f a <*> f b
|
|
|
|
Fun1 a b -> Fun1 <$> f a <*> f b
|
|
|
|
Var1 x -> Var1 <$> f x
|
|
|
|
EmptyRecord1 -> return EmptyRecord1
|
|
|
|
Record1 fields ext ->
|
|
|
|
Record1 <$> Traversable.traverse (mapM f) fields <*> f ext
|
|
|
|
|