Create type pools, have an organized model of state to flow through
the State Transformer during constraint solving and variable unification.
This commit is contained in:
parent
0b2b98db65
commit
ca62ee64a9
4 changed files with 115 additions and 106 deletions
|
@ -1,45 +0,0 @@
|
||||||
module Type.Pool where
|
|
||||||
|
|
||||||
import Type.Type
|
|
||||||
import qualified Data.UnionFind.IO as UF
|
|
||||||
import Control.Arrow (first)
|
|
||||||
import Control.Monad.State
|
|
||||||
|
|
||||||
-- 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.
|
|
||||||
|
|
||||||
-- inhabitants :: Pool -> [Variable]
|
|
||||||
|
|
||||||
data Pool = Pool {
|
|
||||||
maxRank :: Int,
|
|
||||||
inhabitants :: [Variable]
|
|
||||||
}
|
|
||||||
|
|
||||||
register :: Variable -> StateT (Pool,[String]) IO Variable
|
|
||||||
register variable = do
|
|
||||||
modify . first $ \pool -> pool { inhabitants = variable : inhabitants pool }
|
|
||||||
return variable
|
|
||||||
|
|
||||||
introduce :: Variable -> StateT (Pool,[String]) IO Variable
|
|
||||||
introduce variable = do
|
|
||||||
(pool, _) <- get
|
|
||||||
liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
|
|
||||||
register variable
|
|
||||||
|
|
||||||
flatten :: Type -> StateT (Pool,[String]) IO Variable
|
|
||||||
flatten term =
|
|
||||||
case term of
|
|
||||||
VarN v -> return v
|
|
||||||
TermN t -> do
|
|
||||||
flatStructure <- undefined -- chop t
|
|
||||||
(pool, _) <- get
|
|
||||||
var <- liftIO . UF.fresh $ Descriptor {
|
|
||||||
structure = Just flatStructure,
|
|
||||||
rank = maxRank pool,
|
|
||||||
flex = Flexible,
|
|
||||||
name = Nothing,
|
|
||||||
mark = 0
|
|
||||||
}
|
|
||||||
register var
|
|
|
@ -2,33 +2,24 @@
|
||||||
module Type.Solve where
|
module Type.Solve where
|
||||||
|
|
||||||
import Control.Monad
|
import Control.Monad
|
||||||
|
import Control.Monad.State
|
||||||
import qualified Data.UnionFind.IO as UF
|
import qualified Data.UnionFind.IO as UF
|
||||||
import qualified Data.Array.IO as Array
|
import qualified Data.Array.IO as Array
|
||||||
import Data.Map as Map
|
import qualified Data.Map as Map
|
||||||
|
import qualified Data.Traversable as Traversable
|
||||||
import qualified Data.Maybe as Maybe
|
import qualified Data.Maybe as Maybe
|
||||||
import Type.Type
|
import Type.Type
|
||||||
import Type.Unify
|
import Type.Unify
|
||||||
import Type.Environment as Env
|
import qualified Type.Environment as Env
|
||||||
|
import qualified Type.State as TS
|
||||||
-- Pool
|
|
||||||
-- Holds a bunch of variables
|
|
||||||
-- The rank of each variable is less than or equal to the pool's "number"
|
|
||||||
-- The young pool exists to make it possible to identify these vars in constant time.
|
|
||||||
|
|
||||||
-- inhabitants :: Pool -> [Variable]
|
|
||||||
|
|
||||||
data Pool = Pool {
|
|
||||||
maxRank :: Int,
|
|
||||||
inhabitants :: [Variable]
|
|
||||||
}
|
|
||||||
|
|
||||||
register = undefined
|
register = undefined
|
||||||
|
|
||||||
generalize :: Pool -> Pool -> IO [Variable]
|
generalize :: TS.Pool -> TS.Pool -> IO [Variable]
|
||||||
generalize oldPool youngPool = do
|
generalize oldPool youngPool = do
|
||||||
let young = 0
|
let young = 0
|
||||||
visited = 1
|
visited = 1
|
||||||
youngRank = maxRank youngPool
|
youngRank = TS.maxRank youngPool
|
||||||
|
|
||||||
array' <- Array.newArray (0, youngRank) []
|
array' <- Array.newArray (0, youngRank) []
|
||||||
let array = array' :: Array.IOArray Int [Variable]
|
let array = array' :: Array.IOArray Int [Variable]
|
||||||
|
@ -36,7 +27,7 @@ generalize oldPool youngPool = do
|
||||||
-- Insert all of the youngPool variables into the array.
|
-- Insert all of the youngPool variables into the array.
|
||||||
-- They are placed into a list at the index corresponding
|
-- They are placed into a list at the index corresponding
|
||||||
-- to their rank.
|
-- to their rank.
|
||||||
forM (inhabitants youngPool) $ \var -> do
|
forM (TS.inhabitants youngPool) $ \var -> do
|
||||||
desc <- UF.descriptor var
|
desc <- UF.descriptor var
|
||||||
vars <- Array.readArray array (rank desc)
|
vars <- Array.readArray array (rank desc)
|
||||||
Array.writeArray array (rank desc) (var : vars)
|
Array.writeArray array (rank desc) (var : vars)
|
||||||
|
@ -86,50 +77,56 @@ traverse young visited k variable =
|
||||||
return rank'
|
return rank'
|
||||||
else return (rank desc)
|
else return (rank desc)
|
||||||
|
|
||||||
success = return []
|
|
||||||
|
|
||||||
chop = undefined
|
|
||||||
addTo = undefined
|
addTo = undefined
|
||||||
newPool = undefined
|
newPool = undefined
|
||||||
introduce = undefined
|
introduce = undefined
|
||||||
|
|
||||||
solve env pool constraint =
|
solve :: TypeConstraint -> StateT TS.SolverState IO ()
|
||||||
case constraint of
|
solve constraint =
|
||||||
CTrue -> success
|
case constraint of
|
||||||
|
CTrue -> return ()
|
||||||
|
|
||||||
CEqual term1 term2 ->
|
CEqual term1 term2 -> do
|
||||||
unify (register pool) term1 term2
|
t1 <- TS.flatten term1
|
||||||
|
t2 <- TS.flatten term2
|
||||||
|
unify t1 t2
|
||||||
|
|
||||||
CAnd cs -> do
|
CAnd cs -> mapM_ solve cs
|
||||||
results <- mapM (solve env pool) cs
|
|
||||||
return (concat results)
|
|
||||||
|
|
||||||
CLet schemes constraint' -> do
|
CLet [Scheme [] fqs constraint' _] CTrue -> do
|
||||||
env' <- foldM (\env' scheme -> addTo env' `liftM` solveScheme env pool scheme) env schemes
|
mapM_ introduce fqs
|
||||||
solve env' pool constraint'
|
solve constraint'
|
||||||
|
|
||||||
CInstance name term -> do
|
CLet schemes constraint' -> do
|
||||||
let instance' = undefined
|
mapM solveScheme schemes
|
||||||
inst = instance' pool (Env.get env value name)
|
solve constraint'
|
||||||
t <- chop pool term
|
|
||||||
unify pool inst t
|
|
||||||
|
|
||||||
solveScheme env pool scheme =
|
CInstance name term -> do
|
||||||
|
let instance' = undefined
|
||||||
|
inst = undefined --instance' pool (Env.get env value name)
|
||||||
|
t <- TS.flatten term
|
||||||
|
unify inst t
|
||||||
|
|
||||||
|
solveScheme :: TypeScheme -> StateT TS.SolverState IO ()
|
||||||
|
solveScheme scheme =
|
||||||
case scheme of
|
case scheme of
|
||||||
Scheme [] [] constraint header -> do
|
Scheme [] [] constraint header -> do
|
||||||
solve env pool constraint
|
solve constraint
|
||||||
mapM (\(n,t) -> (,) n `liftM` chop pool t) (Map.toList header)
|
Traversable.traverse TS.flatten header
|
||||||
|
return ()
|
||||||
|
|
||||||
Scheme rigidQuantifiers flexibleQuantifiers constraint header -> do
|
Scheme rigidQuantifiers flexibleQuantifiers constraint header -> do
|
||||||
let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
|
let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
|
||||||
pool' <- newPool pool
|
globalPool <- TS.getPool
|
||||||
mapM (introduce pool') rigidQuantifiers
|
localPool <- TS.newPool
|
||||||
mapM (introduce pool') flexibleQuantifiers
|
TS.modifyPool (\_ -> localPool)
|
||||||
header' <- mapM (\(n,t) -> (,) n `liftM` chop pool t) (Map.toList header)
|
mapM TS.introduce quantifiers
|
||||||
solve env pool' constraint
|
header' <- Traversable.traverse TS.flatten header
|
||||||
generalize pool pool'
|
solve constraint
|
||||||
mapM isGeneric rigidQuantifiers
|
-- distinct variables
|
||||||
return header'
|
-- generalize
|
||||||
|
-- generic variables
|
||||||
|
TS.modifyPool (\_ -> globalPool)
|
||||||
|
|
||||||
isGeneric var =
|
isGeneric var =
|
||||||
do desc <- UF.descriptor var
|
do desc <- UF.descriptor var
|
||||||
|
|
60
compiler/Type/State.hs
Normal file
60
compiler/Type/State.hs
Normal file
|
@ -0,0 +1,60 @@
|
||||||
|
module Type.State where
|
||||||
|
|
||||||
|
import Type.Type
|
||||||
|
import qualified Type.Environment as Env
|
||||||
|
import qualified Data.UnionFind.IO as UF
|
||||||
|
import Control.Monad.State
|
||||||
|
|
||||||
|
-- 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]
|
||||||
|
}
|
||||||
|
|
||||||
|
-- Keeps track of the environment, type variable pool, and a list of errors
|
||||||
|
type SolverState = (Env.Environment, Pool, [String])
|
||||||
|
|
||||||
|
modifyEnv f = modify $ \(env, pool, errors) -> (f env, pool, errors)
|
||||||
|
modifyPool f = modify $ \(env, pool, errors) -> (env, f pool, errors)
|
||||||
|
addError err = modify $ \(env, pool, errors) -> (env, pool, err:errors)
|
||||||
|
|
||||||
|
getPool :: StateT SolverState IO Pool
|
||||||
|
getPool = do
|
||||||
|
(_, pool, _) <- get
|
||||||
|
return pool
|
||||||
|
|
||||||
|
newPool :: StateT SolverState IO Pool
|
||||||
|
newPool = do
|
||||||
|
(_, pool, _) <- get
|
||||||
|
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
|
||||||
|
(_, pool, _) <- get
|
||||||
|
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
|
||||||
|
flatStructure <- undefined -- chop t
|
||||||
|
(_, pool, _) <- get
|
||||||
|
var <- liftIO . UF.fresh $ Descriptor {
|
||||||
|
structure = Just flatStructure,
|
||||||
|
rank = maxRank pool,
|
||||||
|
flex = Flexible,
|
||||||
|
name = Nothing,
|
||||||
|
mark = 0
|
||||||
|
}
|
||||||
|
register var
|
|
@ -2,17 +2,17 @@ module Type.Unify (unify) where
|
||||||
|
|
||||||
import Type.Type
|
import Type.Type
|
||||||
import qualified Data.UnionFind.IO as UF
|
import qualified Data.UnionFind.IO as UF
|
||||||
import qualified Type.Pool as Pool
|
import qualified Type.State as TS
|
||||||
import Control.Arrow (first,second)
|
import Control.Arrow (first,second)
|
||||||
import Control.Monad.State
|
import Control.Monad.State
|
||||||
|
|
||||||
unify :: Variable -> Variable -> StateT (Pool.Pool, [String]) IO ()
|
unify :: Variable -> Variable -> StateT TS.SolverState IO ()
|
||||||
unify variable1 variable2 = do
|
unify variable1 variable2 = do
|
||||||
equivalent <- liftIO $ UF.equivalent variable1 variable2
|
equivalent <- liftIO $ UF.equivalent variable1 variable2
|
||||||
if equivalent then return ()
|
if equivalent then return ()
|
||||||
else actuallyUnify variable1 variable2
|
else actuallyUnify variable1 variable2
|
||||||
|
|
||||||
actuallyUnify :: Variable -> Variable -> StateT (Pool.Pool, [String]) IO ()
|
actuallyUnify :: Variable -> Variable -> StateT TS.SolverState IO ()
|
||||||
actuallyUnify variable1 variable2 = do
|
actuallyUnify variable1 variable2 = do
|
||||||
desc1 <- liftIO $ UF.descriptor variable1
|
desc1 <- liftIO $ UF.descriptor variable1
|
||||||
desc2 <- liftIO $ UF.descriptor variable2
|
desc2 <- liftIO $ UF.descriptor variable2
|
||||||
|
@ -34,25 +34,22 @@ actuallyUnify variable1 variable2 = do
|
||||||
rank' :: Int
|
rank' :: Int
|
||||||
rank' = min (rank desc1) (rank desc2)
|
rank' = min (rank desc1) (rank desc2)
|
||||||
|
|
||||||
merge1 :: StateT (Pool.Pool, [String]) IO ()
|
merge1 :: StateT TS.SolverState IO ()
|
||||||
merge1 = liftIO $ do
|
merge1 = liftIO $ do
|
||||||
UF.union variable2 variable1
|
UF.union variable2 variable1
|
||||||
UF.setDescriptor variable1 (desc1 { flex = flex', name = name', rank = rank', mark = undefined })
|
UF.setDescriptor variable1 (desc1 { flex = flex', name = name', rank = rank', mark = undefined })
|
||||||
|
|
||||||
merge2 :: StateT (Pool.Pool, [String]) IO ()
|
merge2 :: StateT TS.SolverState IO ()
|
||||||
merge2 = liftIO $ do
|
merge2 = liftIO $ do
|
||||||
UF.union variable1 variable2
|
UF.union variable1 variable2
|
||||||
UF.setDescriptor variable2 (desc2 { flex = flex', name = name', rank = rank', mark = undefined })
|
UF.setDescriptor variable2 (desc2 { flex = flex', name = name', rank = rank', mark = undefined })
|
||||||
|
|
||||||
fresh :: Maybe (Term1 Variable) -> StateT (Pool.Pool, [String]) IO Variable
|
fresh :: Maybe (Term1 Variable) -> StateT TS.SolverState IO Variable
|
||||||
fresh structure = do
|
fresh structure = do
|
||||||
var <- liftIO . UF.fresh $ Descriptor {
|
var <- liftIO . UF.fresh $ Descriptor {
|
||||||
structure = structure, rank = rank', flex = flex', name = name', mark = undefined
|
structure = structure, rank = rank', flex = flex', name = name', mark = undefined
|
||||||
}
|
}
|
||||||
Pool.register var
|
TS.register var
|
||||||
|
|
||||||
mistake :: String -> StateT (Pool.Pool, [String]) IO ()
|
|
||||||
mistake err = modify $ second (err:)
|
|
||||||
|
|
||||||
case (structure desc1, structure desc2) of
|
case (structure desc1, structure desc2) of
|
||||||
(Nothing, _) | flex desc1 == Flexible -> merge2
|
(Nothing, _) | flex desc1 == Flexible -> merge2
|
||||||
|
@ -61,8 +58,8 @@ actuallyUnify variable1 variable2 = do
|
||||||
(Just (Var1 v), _) -> unify v variable2
|
(Just (Var1 v), _) -> unify v variable2
|
||||||
(_, Just (Var1 v)) -> unify v variable1
|
(_, Just (Var1 v)) -> unify v variable1
|
||||||
|
|
||||||
(Nothing, _) -> mistake "Cannot unify rigid type variable."
|
(Nothing, _) -> TS.addError "Cannot unify rigid type variable."
|
||||||
(_, Nothing) -> mistake "Cannot unify rigid type variable."
|
(_, Nothing) -> TS.addError "Cannot unify rigid type variable."
|
||||||
|
|
||||||
(Just type1, Just type2) ->
|
(Just type1, Just type2) ->
|
||||||
case (type1,type2) of
|
case (type1,type2) of
|
||||||
|
@ -79,6 +76,6 @@ actuallyUnify variable1 variable2 = do
|
||||||
return ()
|
return ()
|
||||||
|
|
||||||
(Record1 fields1 ext1, Record1 fields2 ext2) ->
|
(Record1 fields1 ext1, Record1 fields2 ext2) ->
|
||||||
mistake "did not write record unification yet"
|
TS.addError "did not write record unification yet"
|
||||||
|
|
||||||
_ -> mistake "Could not unify types"
|
_ -> TS.addError "Could not unify types"
|
Loading…
Reference in a new issue