git.iko.soy/elk
on abb9633 help sign in
elk/src/Type/State.hs
240 lines 6.8 kB history raw
1{-# LANGUAGE FlexibleContexts #-}
2module Type.State where
4import Control.Applicative ( (<$>), (<*>), Applicative, (<|>) )
5import Control.Monad.State
6import qualified Data.Map as Map
7import qualified Data.Traversable as Traversable
8import qualified Data.UnionFind.IO as UF
10import qualified Type.Hint as Hint
11import Type.Type
14-- Pool
15-- Holds a bunch of variables
16-- The rank of each variable is less than or equal to the pool's "maxRank"
17-- The young pool exists to make it possible to identify these vars in constant time.
19data Pool = Pool
20 { maxRank :: Int
21 , inhabitants :: [Variable]
22 }
25emptyPool :: Pool
26emptyPool =
27 Pool
28 { maxRank = outermostRank
29 , inhabitants = []
30 }
33type Env = Map.Map String Variable
36-- Keeps track of the environment, type variable pool, and a list of errors
37data SolverState = SS
38 { sEnv :: Env
39 , sSavedEnv :: Env
40 , sPool :: Pool
41 , sMark :: Int
42 , sHint :: [Hint.Hint]
43 }
46initialState :: SolverState
47initialState =
48 SS
49 { sEnv = Map.empty
50 , sSavedEnv = Map.empty
51 , sPool = emptyPool
52 , sMark = noMark + 1 -- The mark must never be equal to noMark!
53 , sHint = []
54 }
57modifyEnv :: (MonadState SolverState m) => (Env -> Env) -> m ()
58modifyEnv f =
59 modify $ \state -> state { sEnv = f (sEnv state) }
62modifyPool :: (MonadState SolverState m) => (Pool -> Pool) -> m ()
63modifyPool f =
64 modify $ \state -> state { sPool = f (sPool state) }
67addHint :: Hint.Hint -> StateT SolverState IO ()
68addHint hint =
69 modify $ \state -> state { sHint = hint : sHint state }
72switchToPool :: (MonadState SolverState m) => Pool -> m ()
73switchToPool pool =
74 modifyPool (\_ -> pool)
77getPool :: StateT SolverState IO Pool
78getPool =
79 gets sPool
82getEnv :: StateT SolverState IO Env
83getEnv =
84 gets sEnv
87saveLocalEnv :: StateT SolverState IO ()
88saveLocalEnv =
89 do currentEnv <- getEnv
90 modify $ \state -> state { sSavedEnv = currentEnv }
93uniqueMark :: StateT SolverState IO Int
94uniqueMark =
95 do state <- get
96 let mark = sMark state
97 put $ state { sMark = mark + 1 }
98 return mark
101nextRankPool :: StateT SolverState IO Pool
102nextRankPool =
103 do pool <- getPool
104 return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
107register :: Variable -> StateT SolverState IO Variable
108register variable =
109 do modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
110 return variable
113introduce :: Variable -> StateT SolverState IO Variable
114introduce variable =
115 do pool <- getPool
116 liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
117 register variable
120flatten :: Type -> StateT SolverState IO Variable
121flatten term =
122 case term of
123 VarN maybeAlias v ->
124 do liftIO $ UF.modifyDescriptor v $ \desc -> desc { alias = maybeAlias <|> alias desc }
125 return v
127 TermN maybeAlias t ->
128 do flatStructure <- traverseTerm flatten t
129 pool <- getPool
130 var <-
131 liftIO . UF.fresh $ Descriptor
132 { structure = Just flatStructure
133 , rank = maxRank pool
134 , flex = Flexible
135 , name = Nothing
136 , copy = Nothing
137 , mark = noMark
138 , alias = maybeAlias
139 }
140 register var
143makeInstance :: Variable -> StateT SolverState IO Variable
144makeInstance var =
145 do alreadyCopied <- uniqueMark
146 freshVar <- makeCopy alreadyCopied var
147 restore alreadyCopied var
148 return freshVar
151makeCopy :: Int -> Variable -> StateT SolverState IO Variable
152makeCopy alreadyCopied variable = do
153 desc <- liftIO $ UF.descriptor variable
154 case () of
155 () | mark desc == alreadyCopied ->
156 case copy desc of
157 Just v ->
158 return v
159 Nothing ->
160 error $
161 "Error copying type variable. This should be impossible." ++
162 " Please report an error to the github repo!"
164 | rank desc /= noRank || flex desc == Constant ->
165 return variable
167 | otherwise ->
168 do pool <- getPool
169 newVar <-
170 liftIO $ UF.fresh $ Descriptor
171 { structure = Nothing
172 , rank = maxRank pool
173 , mark = noMark
174 , flex =
175 case flex desc of
176 Is s -> Is s
177 _ -> Flexible
178 , copy = Nothing
179 , name =
180 case flex desc of
181 Rigid -> Nothing
182 _ -> name desc
183 , alias = Nothing
184 }
185 register newVar
187 -- Link the original variable to the new variable. This lets us
188 -- avoid making multiple copies of the variable we are instantiating.
189 --
190 -- Need to do this before recursively copying the structure of
191 -- the variable to avoid looping on cyclic terms.
192 liftIO $ UF.modifyDescriptor variable $ \desc ->
193 desc { mark = alreadyCopied, copy = Just newVar }
195 -- Now we recursively copy the structure of the variable.
196 -- We have already marked the variable as copied, so we
197 -- will not repeat this work or crawl this variable again.
198 case structure desc of
199 Nothing ->
200 return newVar
202 Just term ->
203 do newTerm <- traverseTerm (makeCopy alreadyCopied) term
204 liftIO $ UF.modifyDescriptor newVar $ \desc ->
205 desc { structure = Just newTerm }
206 return newVar
209restore :: Int -> Variable -> StateT SolverState IO Variable
210restore alreadyCopied variable =
211 do desc <- liftIO $ UF.descriptor variable
212 case mark desc /= alreadyCopied of
213 True -> return variable
214 False ->
215 do restoredStructure <-
216 Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
217 liftIO $ UF.modifyDescriptor variable $ \desc ->
218 desc { mark = noMark, rank = noRank, structure = restoredStructure }
219 return variable
222traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
223traverseTerm f term =
224 case term of
225 App1 a b ->
226 App1 <$> f a <*> f b
228 Fun1 a b ->
229 Fun1 <$> f a <*> f b
231 Var1 x ->
232 Var1 <$> f x
234 EmptyRecord1 ->
235 return EmptyRecord1
237 Record1 fields ext ->
238 Record1
239 <$> Traversable.traverse (mapM f) fields
240 <*> f ext