git.iko.soy/elk
on fcdbe58 help sign in
elk/src/Type/Solve.hs
195 lines 7.4 kB history raw
1module Type.Solve (solve) where
3import Control.Monad
4import Control.Monad.State
5import qualified Data.List as List
6import qualified Data.Map as Map
7import qualified Data.Traversable as Traversable
8import qualified Data.UnionFind.IO as UF
9import Type.Type
10import Type.Unify
11import qualified Type.ExtraChecks as Check
12import qualified Type.State as TS
13import qualified AST.Annotation as A
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.
18generalize :: TS.Pool -> StateT TS.SolverState IO ()
19generalize youngPool = do
20 youngMark <- TS.uniqueMark
21 let youngRank = TS.maxRank youngPool
22 insert dict var = do
23 descriptor <- liftIO $ UF.descriptor var
24 liftIO $ UF.modifyDescriptor var (\desc -> desc { mark = youngMark })
25 return $ Map.insertWith (++) (rank descriptor) [var] dict
27 -- Sort the youngPool variables by rank.
28 rankDict <- foldM insert Map.empty (TS.inhabitants youngPool)
30 -- get the ranks right for each entry.
31 -- start at low ranks so that we only have to pass
32 -- over the information once.
33 visitedMark <- TS.uniqueMark
34 forM (Map.toList rankDict) $ \(poolRank, vars) ->
35 mapM (adjustRank youngMark visitedMark poolRank) vars
37 -- For variables that have rank lowerer than youngRank, register them in
38 -- the old pool if they are not redundant.
39 let registerIfNotRedundant var = do
40 isRedundant <- liftIO $ UF.redundant var
41 if isRedundant then return var else TS.register var
43 let rankDict' = Map.delete youngRank rankDict
44 Traversable.traverse (mapM registerIfNotRedundant) rankDict'
46 -- For variables with rank youngRank
47 -- If rank < youngRank: register in oldPool
48 -- otherwise generalize
49 let registerIfLowerRank var = do
50 isRedundant <- liftIO $ UF.redundant var
51 case isRedundant of
52 True -> return ()
53 False -> do
54 desc <- liftIO $ UF.descriptor var
55 case rank desc < youngRank of
56 True -> TS.register var >> return ()
57 False -> do
58 let flex' = case flex desc of { Flexible -> Rigid ; other -> other }
59 liftIO $ UF.setDescriptor var (desc { rank = noRank, flex = flex' })
61 mapM_ registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
64-- adjust the ranks of variables such that ranks never increase as you
65-- move deeper into a variable.
66adjustRank :: Int -> Int -> Int -> Variable -> StateT TS.SolverState IO Int
67adjustRank youngMark visitedMark groupRank var =
68 do descriptor <- liftIO $ UF.descriptor var
69 case () of
70 () | mark descriptor == youngMark ->
71 do -- Set the variable as marked first because it may be cyclic.
72 liftIO $ UF.modifyDescriptor var $ \desc ->
73 desc { mark = visitedMark }
74 rank' <- maybe (return groupRank) adjustTerm (structure descriptor)
75 liftIO $ UF.modifyDescriptor var $ \desc ->
76 desc { rank = rank' }
77 return rank'
79 | mark descriptor /= visitedMark ->
80 do let rank' = min groupRank (rank descriptor)
81 liftIO $ UF.setDescriptor var (descriptor { mark = visitedMark, rank = rank' })
82 return rank'
84 | otherwise -> return (rank descriptor)
86 where
87 adjust = adjustRank youngMark visitedMark groupRank
89 adjustTerm term =
90 case term of
91 App1 a b -> max `liftM` adjust a `ap` adjust b
92 Fun1 a b -> max `liftM` adjust a `ap` adjust b
93 Var1 x -> adjust x
94 EmptyRecord1 -> return outermostRank
95 Record1 fields extension ->
96 do ranks <- mapM adjust (concat (Map.elems fields))
97 rnk <- adjust extension
98 return . maximum $ rnk : ranks
101solve :: TypeConstraint -> StateT TS.SolverState IO ()
102solve (A.A region constraint) =
103 case constraint of
104 CTrue -> return ()
106 CSaveEnv -> TS.saveLocalEnv
108 CEqual term1 term2 -> do
109 t1 <- TS.flatten term1
110 t2 <- TS.flatten term2
111 unify region t1 t2
113 CAnd cs -> mapM_ solve cs
115 CLet [Scheme [] fqs constraint' _] (A.A _ CTrue) -> do
116 oldEnv <- TS.getEnv
117 mapM TS.introduce fqs
118 solve constraint'
119 TS.modifyEnv (\_ -> oldEnv)
121 CLet schemes constraint' -> do
122 oldEnv <- TS.getEnv
123 headers <- Map.unions `fmap` mapM (solveScheme region) schemes
124 TS.modifyEnv $ \env -> Map.union headers env
125 solve constraint'
126 mapM Check.occurs $ Map.toList headers
127 TS.modifyEnv (\_ -> oldEnv)
129 CInstance name term -> do
130 env <- TS.getEnv
131 freshCopy <-
132 case Map.lookup name env of
133 Just tipe -> TS.makeInstance tipe
134 Nothing
135 | List.isPrefixOf "Native." name -> liftIO (variable Flexible)
136 | otherwise ->
137 error ("Could not find '" ++ name ++ "' when solving type constraints.")
139 t <- TS.flatten term
140 unify region freshCopy t
142solveScheme :: A.Region -> TypeScheme -> StateT TS.SolverState IO (Map.Map String Variable)
143solveScheme region scheme =
144 case scheme of
145 Scheme [] [] constraint header -> do
146 solve constraint
147 Traversable.traverse TS.flatten header
149 Scheme rigidQuantifiers flexibleQuantifiers constraint header -> do
150 let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
151 oldPool <- TS.getPool
153 -- fill in a new pool when working on this scheme's constraints
154 freshPool <- TS.nextRankPool
155 TS.switchToPool freshPool
156 mapM TS.introduce quantifiers
157 header' <- Traversable.traverse TS.flatten header
158 solve constraint
160 allDistinct region rigidQuantifiers
161 youngPool <- TS.getPool
162 TS.switchToPool oldPool
163 generalize youngPool
164 mapM (isGeneric region) rigidQuantifiers
165 return header'
168-- Checks that all of the given variables belong to distinct equivalence classes.
169-- Also checks that their structure is Nothing, so they represent a variable, not
170-- a more complex term.
171allDistinct :: A.Region -> [Variable] -> StateT TS.SolverState IO ()
172allDistinct region vars = do
173 seen <- TS.uniqueMark
174 let check var = do
175 desc <- liftIO $ UF.descriptor var
176 case structure desc of
177 Just _ -> TS.addError region (Just msg) var var
178 where msg = "Cannot generalize something that is not a type variable."
180 Nothing -> do
181 if mark desc == seen
182 then let msg = "Duplicate variable during generalization."
183 in TS.addError region (Just msg) var var
184 else return ()
185 liftIO $ UF.setDescriptor var (desc { mark = seen })
186 mapM_ check vars
188-- Check that a variable has rank == noRank, meaning that it can be generalized.
189isGeneric :: A.Region -> Variable -> StateT TS.SolverState IO ()
190isGeneric region var = do
191 desc <- liftIO $ UF.descriptor var
192 if rank desc == noRank
193 then return ()
194 else let msg = "Unable to generalize a type variable. It is not unranked."
195 in TS.addError region (Just msg) var var