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