git.iko.soy/elk
on 577fc17 help sign in
elk/compiler/Type/Solve.hs
196 lines 7.4 kB history raw
1{-# OPTIONS_GHC -W #-}
2module Type.Solve (solve) where
4import Control.Monad
5import Control.Monad.State
6import qualified Data.List as List
7import qualified Data.Map as Map
8import qualified Data.Traversable as Traversable
9import qualified Data.UnionFind.IO as UF
10import Type.Type
11import Type.Unify
12import qualified Type.ExtraChecks as Check
13import qualified Type.State as TS
14import qualified AST.Annotation as A
17-- | Every variable has rank less than or equal to the maxRank of the pool.
18-- This sorts variables into the young and old pools accordingly.
19generalize :: TS.Pool -> StateT TS.SolverState IO ()
20generalize youngPool = do
21 youngMark <- TS.uniqueMark
22 let youngRank = TS.maxRank youngPool
23 insert dict var = do
24 descriptor <- liftIO $ UF.descriptor var
25 liftIO $ UF.modifyDescriptor var (\desc -> desc { mark = youngMark })
26 return $ Map.insertWith (++) (rank descriptor) [var] dict
28 -- Sort the youngPool variables by rank.
29 rankDict <- foldM insert Map.empty (TS.inhabitants youngPool)
31 -- get the ranks right for each entry.
32 -- start at low ranks so that we only have to pass
33 -- over the information once.
34 visitedMark <- TS.uniqueMark
35 forM (Map.toList rankDict) $ \(poolRank, vars) ->
36 mapM (adjustRank youngMark visitedMark poolRank) vars
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 var =
69 do descriptor <- liftIO $ UF.descriptor var
70 case () of
71 () | mark descriptor == youngMark ->
72 do -- Set the variable as marked first because it may be cyclic.
73 liftIO $ UF.modifyDescriptor var $ \desc ->
74 desc { mark = visitedMark }
75 rank' <- maybe (return groupRank) adjustTerm (structure descriptor)
76 liftIO $ UF.modifyDescriptor var $ \desc ->
77 desc { rank = rank' }
78 return rank'
80 | mark descriptor /= visitedMark ->
81 do let rank' = min groupRank (rank descriptor)
82 liftIO $ UF.setDescriptor var (descriptor { mark = visitedMark, rank = rank' })
83 return rank'
85 | otherwise -> return (rank descriptor)
87 where
88 adjust = adjustRank youngMark visitedMark groupRank
90 adjustTerm term =
91 case term of
92 App1 a b -> max `liftM` adjust a `ap` adjust b
93 Fun1 a b -> max `liftM` adjust a `ap` adjust b
94 Var1 x -> adjust x
95 EmptyRecord1 -> return outermostRank
96 Record1 fields extension ->
97 do ranks <- mapM adjust (concat (Map.elems fields))
98 rnk <- adjust extension
99 return . maximum $ rnk : ranks
102solve :: TypeConstraint -> StateT TS.SolverState IO ()
103solve (A.A region constraint) =
104 case constraint of
105 CTrue -> return ()
107 CSaveEnv -> TS.saveLocalEnv
109 CEqual term1 term2 -> do
110 t1 <- TS.flatten term1
111 t2 <- TS.flatten term2
112 unify region t1 t2
114 CAnd cs -> mapM_ solve cs
116 CLet [Scheme [] fqs constraint' _] (A.A _ CTrue) -> do
117 oldEnv <- TS.getEnv
118 mapM TS.introduce fqs
119 solve constraint'
120 TS.modifyEnv (\_ -> oldEnv)
122 CLet schemes constraint' -> do
123 oldEnv <- TS.getEnv
124 headers <- Map.unions `fmap` mapM (solveScheme region) schemes
125 TS.modifyEnv $ \env -> Map.union headers env
126 solve constraint'
127 mapM Check.occurs $ Map.toList headers
128 TS.modifyEnv (\_ -> oldEnv)
130 CInstance name term -> do
131 env <- TS.getEnv
132 freshCopy <-
133 case Map.lookup name env of
134 Just tipe -> TS.makeInstance tipe
135 Nothing
136 | List.isPrefixOf "Native." name -> liftIO (variable Flexible)
137 | otherwise ->
138 error ("Could not find '" ++ name ++ "' when solving type constraints.")
140 t <- TS.flatten term
141 unify region freshCopy t
143solveScheme :: A.Region -> TypeScheme -> StateT TS.SolverState IO (Map.Map String Variable)
144solveScheme region scheme =
145 case scheme of
146 Scheme [] [] constraint header -> do
147 solve constraint
148 Traversable.traverse TS.flatten header
150 Scheme rigidQuantifiers flexibleQuantifiers constraint header -> do
151 let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
152 oldPool <- TS.getPool
154 -- fill in a new pool when working on this scheme's constraints
155 freshPool <- TS.nextRankPool
156 TS.switchToPool freshPool
157 mapM TS.introduce quantifiers
158 header' <- Traversable.traverse TS.flatten header
159 solve constraint
161 allDistinct region rigidQuantifiers
162 youngPool <- TS.getPool
163 TS.switchToPool oldPool
164 generalize youngPool
165 mapM (isGeneric region) rigidQuantifiers
166 return header'
169-- Checks that all of the given variables belong to distinct equivalence classes.
170-- Also checks that their structure is Nothing, so they represent a variable, not
171-- a more complex term.
172allDistinct :: A.Region -> [Variable] -> StateT TS.SolverState IO ()
173allDistinct region vars = do
174 seen <- TS.uniqueMark
175 let check var = do
176 desc <- liftIO $ UF.descriptor var
177 case structure desc of
178 Just _ -> TS.addError region (Just msg) var var
179 where msg = "Cannot generalize something that is not a type variable."
181 Nothing -> do
182 if mark desc == seen
183 then let msg = "Duplicate variable during generalization."
184 in TS.addError region (Just msg) var var
185 else return ()
186 liftIO $ UF.setDescriptor var (desc { mark = seen })
187 mapM_ check vars
189-- Check that a variable has rank == noRank, meaning that it can be generalized.
190isGeneric :: A.Region -> Variable -> StateT TS.SolverState IO ()
191isGeneric region var = do
192 desc <- liftIO $ UF.descriptor var
193 if rank desc == noRank
194 then return ()
195 else let msg = "Unable to generalize a type variable. It is not unranked."
196 in TS.addError region (Just msg) var var