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