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