git.iko.soy/elk
on c19ccfe help sign in
elk/compiler/Type/Solve.hs
183 lines 6.9 kB history raw
1{-# LANGUAGE MultiWayIf #-}
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.Maybe as Maybe
10import qualified Data.List as List
11import Type.Type
12import Type.Unify
13import qualified Type.Environment as Env
14import qualified Type.State as TS
15import qualified Text.PrettyPrint as P
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 if isRedundant then return () else do
53 desc <- liftIO $ UF.descriptor var
54 if rank desc < youngRank
55 then TS.register var >> return ()
56 else let flex' = if flex desc == Flexible then Rigid else flex desc
57 in liftIO $ UF.setDescriptor var (desc { rank = noRank, flex = flex' })
59 mapM registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
61 return ()
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 if | mark desc == youngMark -> do
71 rank' <- case structure desc of
72 Nothing -> return groupRank
73 Just term -> case term of
74 App1 a b -> max `liftM` adjust a `ap` adjust b
75 Fun1 a b -> max `liftM` adjust a `ap` adjust b
76 Var1 x -> adjust x
77 EmptyRecord1 -> return outermostRank
78 Record1 fields extension -> do
79 ranks <- mapM adjust (concat (Map.elems fields))
80 max (maximum ranks) `liftM` adjust extension
81 liftIO $ UF.setDescriptor variable (desc { mark = visitedMark, rank = rank' })
82 return rank'
84 | mark desc /= visitedMark -> do
85 let rank' = min groupRank (rank desc)
86 liftIO $ UF.setDescriptor variable (desc { mark = visitedMark, rank = rank' })
87 return rank'
89 | otherwise -> return (rank desc)
93solve :: TypeConstraint -> StateT TS.SolverState IO ()
94solve constraint =
95 case constraint of
96 CTrue -> return ()
98 CSaveEnv -> TS.saveLocalEnv
100 CEqual term1 term2 -> do
101 t1 <- TS.flatten term1
102 t2 <- TS.flatten term2
103 unify t1 t2
105 CAnd cs -> mapM_ solve cs
107 CLet [Scheme [] fqs constraint' _] CTrue -> do
108 oldEnv <- TS.getEnv
109 mapM TS.introduce fqs
110 solve constraint'
111 TS.modifyEnv (\_ -> oldEnv)
113 CLet schemes constraint' -> do
114 oldEnv <- TS.getEnv
115 headers <- mapM solveScheme schemes
116 TS.modifyEnv $ \env -> Map.unions (headers ++ [env])
117 solve constraint'
118 TS.modifyEnv (\_ -> oldEnv)
120 CInstance name term -> do
121 env <- TS.getEnv
122 freshCopy <-
123 case Map.lookup name env of
124 Just tipe -> TS.makeInstance tipe
125 Nothing
126 | List.isPrefixOf "Native." name -> liftIO (var Flexible)
127 | otherwise ->
128 error ("Could not find '" ++ name ++ "' when solving type constraints.")
130 t <- TS.flatten term
131 unify freshCopy t
133solveScheme :: TypeScheme -> StateT TS.SolverState IO (Map.Map String Variable)
134solveScheme scheme =
135 case scheme of
136 Scheme [] [] constraint header -> do
137 solve constraint
138 Traversable.traverse TS.flatten header
140 Scheme rigidQuantifiers flexibleQuantifiers constraint header -> do
141 let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
142 oldPool <- TS.getPool
144 -- fill in a new pool when working on this scheme's constraints
145 freshPool <- TS.nextRankPool
146 TS.switchToPool freshPool
147 mapM TS.introduce quantifiers
148 header' <- Traversable.traverse TS.flatten header
149 solve constraint
151 allDistinct rigidQuantifiers
152 youngPool <- TS.getPool
153 TS.switchToPool oldPool
154 generalize youngPool
155 mapM isGeneric rigidQuantifiers
156 return header'
159-- Checks that all of the given variables belong to distinct equivalence classes.
160-- Also checks that their structure is Nothing, so they represent a variable, not
161-- a more complex term.
162allDistinct :: [Variable] -> StateT TS.SolverState IO ()
163allDistinct vars = do
164 seen <- TS.uniqueMark
165 let check var = do
166 desc <- liftIO $ UF.descriptor var
167 case structure desc of
168 Just _ ->
169 TS.addError "Cannot generalize something that is not a type variable" var var
170 Nothing -> do
171 if mark desc == seen
172 then TS.addError "Duplicate variable during generalization" var var
173 else return ()
174 liftIO $ UF.setDescriptor var (desc { mark = seen })
175 mapM_ check vars
177-- Check that a variable has rank == noRank, meaning that it can be generalized.
178isGeneric :: Variable -> StateT TS.SolverState IO ()
179isGeneric var = do
180 desc <- liftIO $ UF.descriptor var
181 if rank desc == noRank
182 then return ()
183 else TS.addError "Cannot generalize. Variable must have not have a rank." var var