git.iko.soy/elk
on 63243ca help sign in
elk/compiler/Type/Solve.hs
192 lines 7.5 kB history raw
1{-# OPTIONS_GHC -W #-}
2module Type.Solve (solve) where
4import Control.Monad
5import Control.Monad.State
6import qualified Data.UnionFind.IO as UF
7import qualified Data.Map as Map
8import qualified Data.Traversable as Traversable
9import qualified Data.List as List
10import Type.Type
11import Type.Unify
12import qualified Type.ExtraChecks as Check
13import qualified Type.State as TS
14import SourceSyntax.Location (Located(L), SrcSpan)
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 desc <- liftIO $ UF.descriptor var
25 liftIO $ UF.modifyDescriptor var (\desc -> desc { mark = youngMark })
26 return $ Map.insertWith (++) (rank desc) [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 mapM (\(poolRank, vars) -> mapM (adjustRank youngMark visitedMark poolRank) vars) (Map.toList rankDict)
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 variable =
68 let adjust = adjustRank youngMark visitedMark groupRank in
69 do desc <- liftIO $ UF.descriptor variable
70 case () of
71 () | mark desc == youngMark ->
72 do -- Set the variable as marked first because it may be cyclic.
73 liftIO $ UF.modifyDescriptor variable $ \desc -> desc { mark = visitedMark }
74 rank' <- case structure desc of
75 Nothing -> return groupRank
76 Just term ->
77 case term of
78 App1 a b -> max `liftM` adjust a `ap` adjust b
79 Fun1 a b -> max `liftM` adjust a `ap` adjust b
80 Var1 x -> adjust x
81 EmptyRecord1 -> return outermostRank
82 Record1 fields extension ->
83 do ranks <- mapM adjust (concat (Map.elems fields))
84 rnk <- adjust extension
85 return . maximum $ rnk : ranks
86 liftIO $ UF.modifyDescriptor variable $ \desc -> desc { rank = rank' }
87 return rank'
89 | mark desc /= visitedMark ->
90 do let rank' = min groupRank (rank desc)
91 liftIO $ UF.setDescriptor variable (desc { mark = visitedMark, rank = rank' })
92 return rank'
94 | otherwise -> return (rank desc)
98solve :: TypeConstraint -> StateT TS.SolverState IO ()
99solve (L span constraint) =
100 case constraint of
101 CTrue -> return ()
103 CSaveEnv -> TS.saveLocalEnv
105 CEqual term1 term2 -> do
106 t1 <- TS.flatten term1
107 t2 <- TS.flatten term2
108 unify span t1 t2
110 CAnd cs -> mapM_ solve cs
112 CLet [Scheme [] fqs constraint' _] (L _ CTrue) -> do
113 oldEnv <- TS.getEnv
114 mapM TS.introduce fqs
115 solve constraint'
116 TS.modifyEnv (\_ -> oldEnv)
118 CLet schemes constraint' -> do
119 oldEnv <- TS.getEnv
120 headers <- Map.unions `fmap` mapM (solveScheme span) schemes
121 TS.modifyEnv $ \env -> Map.union headers env
122 solve constraint'
123 mapM Check.occurs $ Map.toList headers
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 _ -> TS.addError span (Just msg) var var
175 where msg = "Cannot generalize something that is not a type variable."
177 Nothing -> do
178 if mark desc == seen
179 then let msg = "Duplicate variable during generalization."
180 in TS.addError span (Just msg) var var
181 else return ()
182 liftIO $ UF.setDescriptor var (desc { mark = seen })
183 mapM_ check vars
185-- Check that a variable has rank == noRank, meaning that it can be generalized.
186isGeneric :: SrcSpan -> Variable -> StateT TS.SolverState IO ()
187isGeneric span var = do
188 desc <- liftIO $ UF.descriptor var
189 if rank desc == noRank
190 then return ()
191 else let msg = "Unable to generalize a type variable. It is not unranked."
192 in TS.addError span (Just msg) var var