git.iko.soy/elk
on 62bed13 help sign in
elk/src/Type/Solve.hs
270 lines 9.3 kB history raw
1module Type.Solve (solve) where
3import Control.Applicative ((<$>), (<*>))
4import Control.Monad
5import Control.Monad.State (StateT, execStateT, liftIO)
6import Control.Monad.Except (ExceptT, throwError)
7import qualified Data.List as List
8import qualified Data.Map as Map
9import qualified Data.Traversable as Traversable
10import qualified Data.UnionFind.IO as UF
12import qualified Reporting.Annotation as A
13import qualified Reporting.Error.Type as Error
14import qualified Type.State as TS
15import Type.Type
16import Type.Unify
19{-| Every variable has rank less than or equal to the maxRank of the pool.
20This sorts variables into the young and old pools accordingly.
21-}
22generalize :: TS.Pool -> StateT TS.SolverState IO ()
23generalize youngPool =
24 do youngMark <- TS.uniqueMark
25 let youngRank = TS.maxRank youngPool
26 let insert dict var =
27 do descriptor <- liftIO $ UF.descriptor var
28 liftIO $ UF.modifyDescriptor var (\desc -> desc { mark = youngMark })
29 return $ Map.insertWith (++) (rank descriptor) [var] dict
31 -- Sort the youngPool variables by rank.
32 rankDict <- foldM insert Map.empty (TS.inhabitants youngPool)
34 -- get the ranks right for each entry.
35 -- start at low ranks so that we only have to pass
36 -- over the information once.
37 visitedMark <- TS.uniqueMark
38 forM (Map.toList rankDict) $ \(poolRank, vars) ->
39 mapM (adjustRank youngMark visitedMark poolRank) vars
41 -- For variables that have rank lowerer than youngRank, register them in
42 -- the old pool if they are not redundant.
43 let registerIfNotRedundant var =
44 do isRedundant <- liftIO $ UF.redundant var
45 if isRedundant then return var else TS.register var
47 let rankDict' = Map.delete youngRank rankDict
48 Traversable.traverse (mapM registerIfNotRedundant) rankDict'
50 -- For variables with rank youngRank
51 -- If rank < youngRank: register in oldPool
52 -- otherwise generalize
53 let registerIfLowerRank var = do
54 isRedundant <- liftIO $ UF.redundant var
55 case isRedundant of
56 True -> return ()
57 False -> do
58 desc <- liftIO $ UF.descriptor var
59 case rank desc < youngRank of
60 True -> TS.register var >> return ()
61 False -> do
62 let flex' = case flex desc of { Flexible -> Rigid ; other -> other }
63 liftIO $ UF.setDescriptor var (desc { rank = noRank, flex = flex' })
65 mapM_ registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
68-- adjust the ranks of variables such that ranks never increase as you
69-- move deeper into a variable.
70adjustRank :: Int -> Int -> Int -> Variable -> StateT TS.SolverState IO Int
71adjustRank youngMark visitedMark groupRank var =
72 do descriptor <- liftIO $ UF.descriptor var
73 case () of
74 () | mark descriptor == youngMark ->
75 do -- Set the variable as marked first because it may be cyclic.
76 liftIO $ UF.modifyDescriptor var $ \desc ->
77 desc { mark = visitedMark }
78 rank' <- maybe (return groupRank) adjustTerm (structure descriptor)
79 liftIO $ UF.modifyDescriptor var $ \desc ->
80 desc { rank = rank' }
81 return rank'
83 | mark descriptor /= visitedMark ->
84 do let rank' = min groupRank (rank descriptor)
85 liftIO $ UF.setDescriptor var (descriptor { mark = visitedMark, rank = rank' })
86 return rank'
88 | otherwise ->
89 return (rank descriptor)
90 where
91 adjust =
92 adjustRank youngMark visitedMark groupRank
94 adjustTerm term =
95 case term of
96 App1 a b ->
97 max `liftM` adjust a `ap` adjust b
99 Fun1 a b ->
100 max `liftM` adjust a `ap` adjust b
102 Var1 x ->
103 adjust x
105 EmptyRecord1 ->
106 return outermostRank
108 Record1 fields extension ->
109 do ranks <- mapM adjust (concat (Map.elems fields))
110 rnk <- adjust extension
111 return . maximum $ rnk : ranks
114-- SOLVER
116solve :: TypeConstraint -> ExceptT [A.Located Error.Error] IO TS.SolverState
117solve constraint =
118 do state <-
119 liftIO (execStateT (actuallySolve constraint) TS.initialState)
120 case TS.sError state of
121 [] ->
122 return state
123 errors ->
124 throwError errors
127actuallySolve :: TypeConstraint -> StateT TS.SolverState IO ()
128actuallySolve constraint =
129 case constraint of
130 CTrue ->
131 return ()
133 CSaveEnv ->
134 TS.saveLocalEnv
136 CEqual region term1 term2 ->
137 do t1 <- TS.flatten term1
138 t2 <- TS.flatten term2
139 unify region t1 t2
141 CAnd cs ->
142 mapM_ actuallySolve cs
144 CLet [Scheme [] fqs constraint' _] CTrue ->
145 do oldEnv <- TS.getEnv
146 mapM TS.introduce fqs
147 actuallySolve constraint'
148 TS.modifyEnv (\_ -> oldEnv)
150 CLet schemes constraint' ->
151 do oldEnv <- TS.getEnv
152 headers <- Map.unions `fmap` mapM solveScheme schemes
153 TS.modifyEnv $ \env -> Map.union headers env
154 actuallySolve constraint'
155 mapM occurs $ Map.toList headers
156 TS.modifyEnv (\_ -> oldEnv)
158 CInstance region name term ->
159 do env <- TS.getEnv
160 freshCopy <-
161 case Map.lookup name env of
162 Just tipe ->
163 TS.makeInstance tipe
164 Nothing ->
165 if List.isPrefixOf "Native." name
166 then liftIO (variable Flexible)
167 else error ("Could not find '" ++ name ++ "' when solving type constraints.")
169 t <- TS.flatten term
170 unify region freshCopy t
173solveScheme :: TypeScheme -> StateT TS.SolverState IO (Map.Map String Variable)
174solveScheme scheme =
175 case scheme of
176 Scheme [] [] constraint header ->
177 do actuallySolve constraint
178 Traversable.traverse TS.flatten header
180 Scheme rigidQuantifiers flexibleQuantifiers constraint header ->
181 do let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
182 oldPool <- TS.getPool
184 -- fill in a new pool when working on this scheme's constraints
185 freshPool <- TS.nextRankPool
186 TS.switchToPool freshPool
187 mapM TS.introduce quantifiers
188 header' <- Traversable.traverse TS.flatten header
189 actuallySolve constraint
191 allDistinct rigidQuantifiers
192 youngPool <- TS.getPool
193 TS.switchToPool oldPool
194 generalize youngPool
195 mapM isGeneric rigidQuantifiers
196 return header'
199-- ADDITIONAL CHECKS
201-- Checks that all of the given variables belong to distinct equivalence classes.
202-- Also checks that their structure is Nothing, so they represent a variable, not
203-- a more complex term.
204allDistinct :: [Variable] -> StateT TS.SolverState IO ()
205allDistinct vars =
206 do seen <- TS.uniqueMark
207 forM_ vars $ \var ->
208 do desc <- liftIO $ UF.descriptor var
209 case structure desc of
210 Just _ ->
211 TS.addError (error "Cannot generalize something that is not a type variable.") undefined
213 Nothing ->
214 do when (mark desc == seen) $
215 TS.addError (error "Duplicate variable during generalization.") undefined
216 liftIO $ UF.setDescriptor var (desc { mark = seen })
219-- Check that a variable has rank == noRank, meaning that it can be generalized.
220isGeneric :: Variable -> StateT TS.SolverState IO ()
221isGeneric var =
222 do desc <- liftIO $ UF.descriptor var
223 if rank desc == noRank
224 then return ()
225 else
226 TS.addError (error "Unable to generalize a type variable. It is not unranked.") undefined
229occurs :: (String, Variable) -> StateT TS.SolverState IO ()
230occurs (_name, variable) =
231 do vars <- liftIO $ infiniteVars [] variable
232 case vars of
233 [] ->
234 return ()
236 var : _ ->
237 do desc <- liftIO $ UF.descriptor var
238 case structure desc of
239 Nothing ->
240 error "occurs check triggered"
242 Just _ ->
243 error "occurs check triggered"
244 where
245 infiniteVars :: [Variable] -> Variable -> IO [Variable]
246 infiniteVars seen var =
247 let go = infiniteVars (var:seen)
248 in
249 if var `elem` seen
250 then return [var]
251 else do
252 desc <- UF.descriptor var
253 case structure desc of
254 Nothing -> return []
255 Just struct ->
256 case struct of
257 App1 a b ->
258 (++) <$> go a <*> go b
260 Fun1 a b ->
261 (++) <$> go a <*> go b
263 Var1 a ->
264 go a
266 EmptyRecord1 ->
267 return []
269 Record1 fields ext ->
270 concat <$> mapM go (ext : concat (Map.elems fields))