@@ -4,7 +4,6 @@ module Type.Solve where
44import Control.Monad
55import Control.Monad.State
66import qualified Data.UnionFind.IO as UF
7−import qualified Data.Array.IO as Array
87import qualified Data.Map as Map
98import qualified Data.Traversable as Traversable
109import qualified Data.Maybe as Maybe
@@ -13,73 +12,78 @@ import Type.Unify
1312import qualified Type.Environment as Env
1413import qualified Type.State as TS
1514
16−register = undefined
17−
18−generalize :: TS.Pool -> TS.Pool -> IO [Variable]
19−generalize oldPool youngPool = do
20− let young = 0
21− visited = 1
22− youngRank = TS.maxRank youngPool
23−
24− array' <- Array.newArray (0, youngRank) []
25− let array = array' :: Array.IOArray Int [Variable]
26−
27− -- Insert all of the youngPool variables into the array.
28− -- They are placed into a list at the index corresponding
29− -- to their rank.
30− forM (TS.inhabitants youngPool) $ \var -> do
31− desc <- UF.descriptor var
32− vars <- Array.readArray array (rank desc)
33− Array.writeArray array (rank desc) (var : vars)
34−
35− -- get the ranks right for each entry
36− forM [0 .. youngRank] $ \i -> do
37− vars <- Array.readArray array i
38− mapM (traverse young visited i) vars
39−
40− -- do not need to work with variables that have become redundant
41− vars <- Array.readArray array youngRank
42− forM vars $ \var -> do
43− isRedundant <- UF.redundant var
44− if isRedundant then do
45− desc <- UF.descriptor var
46− if rank desc < youngRank
47− then register oldPool var
48− else let flex' = if flex desc == Flexible then Rigid else flex desc
49− in UF.setDescriptor var (desc { rank = noRank, flex = flex' })
50− else return ()
51−
52− return vars
53−
54−traverse :: Int -> Int -> Int -> Variable -> IO Int
55−traverse young visited k variable =
56− let f = traverse young visited k in
57− do desc <- UF.descriptor variable
58− case mark desc == young of
15+
16+-- | Every variable has rank less than or equal to the maxRank of the pool.
17+-- This sorts variables into the young and old pools accordingly.
18+generalize :: TS.Pool -> StateT TS.SolverState IO ()
19+generalize youngPool = do
20+ let youngRank = TS.maxRank youngPool
21+ insert dict var = do
22+ desc <- liftIO $ UF.descriptor var
23+ return $ Map.insertWith (++) (rank desc) [var] dict
24+
25+ -- Sort the youngPool variables by rank.
26+ rankDict <- foldM insert Map.empty (TS.inhabitants youngPool)
27+
28+ -- get the ranks right for each entry.
29+ -- start at low ranks so that we only have to pass
30+ -- over the information once.
31+ youngMark <- TS.uniqueMark
32+ visitedMark <- TS.uniqueMark
33+ Traversable.traverse (mapM (adjustRank youngMark visitedMark youngRank)) rankDict
34+
35+ -- Move variables out of the young pool if they do not have a young rank.
36+ -- We should not generalize things we cannot use.
37+ let youngVars = (Map.!) rankDict youngRank
38+
39+ registerIfNotRedundant var = do
40+ isRedundant <- liftIO $ UF.redundant var
41+ if isRedundant then return var else TS.register var
42+
43+ registerIfHigherRank var = do
44+ isRedundant <- liftIO $ UF.redundant var
45+ if isRedundant then return () else do
46+ desc <- liftIO $ UF.descriptor var
47+ if rank desc < youngRank
48+ then TS.register var >> return ()
49+ else let flex' = if flex desc == Flexible then Rigid else flex desc
50+ in liftIO $ UF.setDescriptor var (desc { rank = noRank, flex = flex' })
51+
52+ Traversable.traverse (mapM registerIfNotRedundant) rankDict
53+ Traversable.traverse (mapM registerIfHigherRank) rankDict
54+
55+ return ()
56+
57+
58+-- adjust the ranks of variables such that ranks never increase as you
59+-- move deeper into a variable. This mean the rank actually represents the
60+-- deepest variable in the whole type, and we can ignore things at a lower
61+-- rank than the current constraints.
62+adjustRank :: Int -> Int -> Int -> Variable -> StateT TS.SolverState IO Int
63+adjustRank youngMark visitedMark groupRank variable =
64+ let adjust = adjustRank youngMark visitedMark groupRank in
65+ do desc <- liftIO $ UF.descriptor variable
66+ case mark desc == youngMark of
5967 True -> do
6068 rank' <- case structure desc of
61− Nothing -> return k
69+ Nothing -> return groupRank
6270 Just term -> case term of
63− App1 a b -> max `liftM` f a `ap` f b
64− Fun1 a b -> max `liftM` f a `ap` f b
65− Var1 x -> f x
71+ App1 a b -> max `liftM` adjust a `ap` adjust b
72+ Fun1 a b -> max `liftM` adjust a `ap` adjust b
73+ Var1 x -> adjust x
6674 EmptyRecord1 -> return outermostRank
6775 Record1 fields extension -> do
68− ranks <- mapM f (concat (Map.elems fields))
69− max (maximum ranks) `liftM` f extension
70− UF.setDescriptor variable (desc { mark = visited, rank = rank' })
76+ ranks <- mapM adjust (concat (Map.elems fields))
77+ max (maximum ranks) `liftM` adjust extension
78+ liftIO $ UF.setDescriptor variable (desc { mark = visitedMark, rank = rank' })
7179 return rank'
7280
7381 False -> do
74− if mark desc /= visited then do
75− let rank' = min k (rank desc)
76− UF.setDescriptor variable (desc { mark = visited, rank = rank' })
82+ if mark desc == visitedMark then return (rank desc) else do
83+ let rank' = min groupRank (rank desc)
84+ liftIO $ UF.setDescriptor variable (desc { mark = visitedMark, rank = rank' })
7785 return rank'
78− else return (rank desc)
7986
80−addTo = undefined
81−newPool = undefined
82−introduce = undefined
8387
8488solve :: TypeConstraint -> StateT TS.SolverState IO ()
8589solve constraint =
@@ -94,41 +98,67 @@ solve constraint =
9498 CAnd cs -> mapM_ solve cs
9599
96100 CLet [Scheme [] fqs constraint' _] CTrue -> do
97− mapM_ introduce fqs
101+ mapM_ TS.introduce fqs
98102 solve constraint'
99103
100104 CLet schemes constraint' -> do
101− mapM solveScheme schemes
105+ headers <- mapM solveScheme schemes
106+ TS.modifyEnv $ \env -> Map.unions (headers ++ [env])
102107 solve constraint'
103108
104109 CInstance name term -> do
105− let instance' = undefined
106− inst = undefined --instance' pool (Env.get env value name)
110+ env <- TS.getEnv
111+ freshCopy <- TS.makeInstance ((Map.!) env name)
107112 t <- TS.flatten term
108− unify inst t
113+ unify freshCopy t
109114
110−solveScheme :: TypeScheme -> StateT TS.SolverState IO ()
115+solveScheme :: TypeScheme -> StateT TS.SolverState IO (Map.Map String Variable)
111116solveScheme scheme =
112117 case scheme of
113118 Scheme [] [] constraint header -> do
114119 solve constraint
115120 Traversable.traverse TS.flatten header
116− return ()
117121
118122 Scheme rigidQuantifiers flexibleQuantifiers constraint header -> do
119123 let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
120− globalPool <- TS.getPool
121− localPool <- TS.newPool
122− TS.modifyPool (\_ -> localPool)
124+ currentPool <- TS.getPool
125+
126+ -- fill in a new pool when working on this scheme's constraints
127+ emptyPool <- TS.nextRankPool
128+ TS.switchToPool emptyPool
123129 mapM TS.introduce quantifiers
124130 header' <- Traversable.traverse TS.flatten header
125131 solve constraint
126− -- distinct variables
127− -- generalize
128− -- generic variables
129− TS.modifyPool (\_ -> globalPool)
130−
131−isGeneric var =
132− do desc <- UF.descriptor var
133− undefined
134132
133+ allDistinct rigidQuantifiers
134+ localPool <- TS.getPool
135+ TS.switchToPool currentPool
136+ generalize localPool
137+ mapM isGeneric rigidQuantifiers
138+ return header'
139+
140+
141+-- Checks that all of the given variables belong to distinct equivalence classes.
142+-- Also checks that their structure is Nothing, so they represent a variable, not
143+-- a more complex term.
144+allDistinct :: [Variable] -> StateT TS.SolverState IO ()
145+allDistinct vars = do
146+ seen <- TS.uniqueMark
147+ let check var = do
148+ desc <- liftIO $ UF.descriptor var
149+ case structure desc of
150+ Just _ -> TS.addError "Cannot generalize something that is not a type variable."
151+ Nothing -> do
152+ if mark desc == seen
153+ then TS.addError "Duplicate variable during generalization"
154+ else return ()
155+ liftIO $ UF.setDescriptor var (desc { mark = seen })
156+ mapM_ check vars
157+
158+-- Check that a variable has rank == noRank, meaning that it can be generalized.
159+isGeneric :: Variable -> StateT TS.SolverState IO ()
160+isGeneric var = do
161+ desc <- liftIO $ UF.descriptor var
162+ if rank desc == noRank
163+ then return ()
164+ else TS.addError "Cannot generalize. Variable must have not have a rank."