git.iko.soy/elk
on 564fd4d help sign in
elk/src/Type/Solve.hs
201 lines 7.7 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 =
20 do 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 ->
85 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 ->
105 return ()
107 CSaveEnv ->
108 TS.saveLocalEnv
110 CEqual term1 term2 ->
111 do t1 <- TS.flatten term1
112 t2 <- TS.flatten term2
113 unify region t1 t2
115 CAnd cs ->
116 mapM_ solve cs
118 CLet [Scheme [] fqs constraint' _] (A.A _ CTrue) ->
119 do oldEnv <- TS.getEnv
120 mapM TS.introduce fqs
121 solve constraint'
122 TS.modifyEnv (\_ -> oldEnv)
124 CLet schemes constraint' ->
125 do oldEnv <- TS.getEnv
126 headers <- Map.unions `fmap` mapM (solveScheme region) schemes
127 TS.modifyEnv $ \env -> Map.union headers env
128 solve constraint'
129 mapM Check.occurs $ Map.toList headers
130 TS.modifyEnv (\_ -> oldEnv)
132 CInstance name term ->
133 do env <- TS.getEnv
134 freshCopy <-
135 case Map.lookup name env of
136 Just tipe -> TS.makeInstance tipe
137 Nothing
138 | List.isPrefixOf "Native." name -> liftIO (variable Flexible)
139 | otherwise ->
140 error ("Could not find '" ++ name ++ "' when solving type constraints.")
142 t <- TS.flatten term
143 unify region freshCopy t
146solveScheme :: A.Region -> TypeScheme -> StateT TS.SolverState IO (Map.Map String Variable)
147solveScheme region scheme =
148 case scheme of
149 Scheme [] [] constraint header ->
150 do solve constraint
151 Traversable.traverse TS.flatten header
153 Scheme rigidQuantifiers flexibleQuantifiers constraint header ->
154 do let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
155 oldPool <- TS.getPool
157 -- fill in a new pool when working on this scheme's constraints
158 freshPool <- TS.nextRankPool
159 TS.switchToPool freshPool
160 mapM TS.introduce quantifiers
161 header' <- Traversable.traverse TS.flatten header
162 solve constraint
164 allDistinct region rigidQuantifiers
165 youngPool <- TS.getPool
166 TS.switchToPool oldPool
167 generalize youngPool
168 mapM (isGeneric region) rigidQuantifiers
169 return header'
172-- Checks that all of the given variables belong to distinct equivalence classes.
173-- Also checks that their structure is Nothing, so they represent a variable, not
174-- a more complex term.
175allDistinct :: A.Region -> [Variable] -> StateT TS.SolverState IO ()
176allDistinct region vars =
177 do seen <- TS.uniqueMark
178 let check var = do
179 desc <- liftIO $ UF.descriptor var
180 case structure desc of
181 Just _ -> TS.addError region (Just msg) var var
182 where msg = "Cannot generalize something that is not a type variable."
184 Nothing -> do
185 if mark desc == seen
186 then let msg = "Duplicate variable during generalization."
187 in TS.addError region (Just msg) var var
188 else return ()
189 liftIO $ UF.setDescriptor var (desc { mark = seen })
190 mapM_ check vars
193-- Check that a variable has rank == noRank, meaning that it can be generalized.
194isGeneric :: A.Region -> Variable -> StateT TS.SolverState IO ()
195isGeneric region var =
196 do desc <- liftIO $ UF.descriptor var
197 if rank desc == noRank
198 then return ()
199 else
200 let msg = "Unable to generalize a type variable. It is not unranked."
201 in TS.addError region (Just msg) var var