on 552becc help sign in
elk/src/Type/State.hs
261 lines 7.4 kB history raw
1{-# LANGUAGE FlexibleContexts #-}
2module Type.State where
4import Control.Applicative ( Applicative, (<$>), (<*>), (<|>) )
5import Control.Monad.State
6import Data.Map ((!))
7import qualified Data.Map as Map
8import qualified Data.Traversable as Traversable
9import qualified Data.UnionFind.IO as UF
11import qualified Type.Hint as Hint
12import Type.Type
15-- Pool
16-- Holds a bunch of variables
17-- The rank of each variable is less than or equal to the pool's "maxRank"
18-- The young pool exists to make it possible to identify these vars in constant time.
20data Pool = Pool
21 { maxRank :: Int
22 , inhabitants :: [Variable]
23 }
26emptyPool :: Pool
27emptyPool =
28 Pool
29 { maxRank = outermostRank
30 , inhabitants = []
31 }
34type Env = Map.Map String Variable
37-- Keeps track of the environment, type variable pool, and a list of errors
38data SolverState = SS
39 { sEnv :: Env
40 , sSavedEnv :: Env
41 , sPool :: Pool
42 , sMark :: Int
43 , sHint :: [Hint.Hint]
44 }
47initialState :: SolverState
48initialState =
49 SS
50 { sEnv = Map.empty
51 , sSavedEnv = Map.empty
52 , sPool = emptyPool
53 , sMark = noMark + 1 -- The mark must never be equal to noMark!
54 , sHint = []
55 }
58modifyEnv :: (MonadState SolverState m) => (Env -> Env) -> m ()
59modifyEnv f =
60 modify $ \state -> state { sEnv = f (sEnv state) }
63modifyPool :: (MonadState SolverState m) => (Pool -> Pool) -> m ()
64modifyPool f =
65 modify $ \state -> state { sPool = f (sPool state) }
68addHint :: Hint.Hint -> StateT SolverState IO ()
69addHint hint =
70 modify $ \state -> state { sHint = hint : sHint state }
73switchToPool :: (MonadState SolverState m) => Pool -> m ()
74switchToPool pool =
75 modifyPool (\_ -> pool)
78getPool :: StateT SolverState IO Pool
79getPool =
80 gets sPool
83getEnv :: StateT SolverState IO Env
84getEnv =
85 gets sEnv
88saveLocalEnv :: StateT SolverState IO ()
89saveLocalEnv =
90 do currentEnv <- getEnv
91 modify $ \state -> state { sSavedEnv = currentEnv }
94uniqueMark :: StateT SolverState IO Int
95uniqueMark =
96 do state <- get
97 let mark = sMark state
98 put $ state { sMark = mark + 1 }
99 return mark
102nextRankPool :: StateT SolverState IO Pool
103nextRankPool =
104 do pool <- getPool
105 return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
108register :: Variable -> StateT SolverState IO Variable
109register variable =
110 do modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
111 return variable
114introduce :: Variable -> StateT SolverState IO Variable
115introduce variable =
116 do pool <- getPool
117 liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
118 register variable
121flatten :: Type -> StateT SolverState IO Variable
122flatten term =
123 flattenHelp Map.empty term
126flattenHelp :: Map.Map String Variable -> Type -> StateT SolverState IO Variable
127flattenHelp aliasDict term =
128 case term of
129 PlaceHolder name ->
130 return (aliasDict ! name)
132 VarN maybeAlias v ->
133 do maybeAlias' <- Traversable.traverse flattenAlias maybeAlias
134 liftIO $ UF.modifyDescriptor v $ \desc ->
135 desc { alias = maybeAlias' <|> alias desc }
136 return v
138 TermN maybeAlias subTerm ->
139 do maybeAlias' <- Traversable.traverse flattenAlias maybeAlias
140 let localDict = maybe aliasDict (Map.fromList . snd) maybeAlias'
141 flatStructure <- traverseTerm (flattenHelp localDict) subTerm
142 pool <- getPool
143 var <-
144 liftIO . UF.fresh $ Descriptor
145 { structure = Just flatStructure
146 , rank = maxRank pool
147 , flex = Flexible
148 , name = Nothing
149 , copy = Nothing
150 , mark = noMark
151 , alias = maybeAlias'
152 }
153 register var
154 where
155 flattenAlias (name, args) =
156 let flattenPair (arg, subTerm) =
157 (,) arg <$> flattenHelp aliasDict subTerm
158 in
159 (,) name <$> mapM flattenPair args
164makeInstance :: Variable -> StateT SolverState IO Variable
165makeInstance var =
166 do alreadyCopied <- uniqueMark
167 freshVar <- makeCopy alreadyCopied var
168 restore alreadyCopied var
169 return freshVar
172makeCopy :: Int -> Variable -> StateT SolverState IO Variable
173makeCopy alreadyCopied variable = do
174 desc <- liftIO $ UF.descriptor variable
175 case () of
176 () | mark desc == alreadyCopied ->
177 case copy desc of
178 Just v ->
179 return v
180 Nothing ->
181 error $
182 "Error copying type variable. This should be impossible." ++
183 " Please report an error to the github repo!"
185 | rank desc /= noRank || flex desc == Constant ->
186 return variable
188 | otherwise ->
189 do pool <- getPool
190 newVar <-
191 liftIO $ UF.fresh $ Descriptor
192 { structure = Nothing
193 , rank = maxRank pool
194 , mark = noMark
195 , flex =
196 case flex desc of
197 Is s -> Is s
198 _ -> Flexible
199 , copy = Nothing
200 , name =
201 case flex desc of
202 Rigid -> Nothing
203 _ -> name desc
204 , alias = Nothing
205 }
206 register newVar
208 -- Link the original variable to the new variable. This lets us
209 -- avoid making multiple copies of the variable we are instantiating.
210 --
211 -- Need to do this before recursively copying the structure of
212 -- the variable to avoid looping on cyclic terms.
213 liftIO $ UF.modifyDescriptor variable $ \desc ->
214 desc { mark = alreadyCopied, copy = Just newVar }
216 -- Now we recursively copy the structure of the variable.
217 -- We have already marked the variable as copied, so we
218 -- will not repeat this work or crawl this variable again.
219 case structure desc of
220 Nothing ->
221 return newVar
223 Just term ->
224 do newTerm <- traverseTerm (makeCopy alreadyCopied) term
225 liftIO $ UF.modifyDescriptor newVar $ \desc ->
226 desc { structure = Just newTerm }
227 return newVar
230restore :: Int -> Variable -> StateT SolverState IO Variable
231restore alreadyCopied variable =
232 do desc <- liftIO $ UF.descriptor variable
233 case mark desc /= alreadyCopied of
234 True -> return variable
235 False ->
236 do restoredStructure <-
237 Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
238 liftIO $ UF.modifyDescriptor variable $ \desc ->
239 desc { mark = noMark, rank = noRank, structure = restoredStructure }
240 return variable
243traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
244traverseTerm f term =
245 case term of
246 App1 a b ->
247 App1 <$> f a <*> f b
249 Fun1 a b ->
250 Fun1 <$> f a <*> f b
252 Var1 x ->
253 Var1 <$> f x
255 EmptyRecord1 ->
256 return EmptyRecord1
258 Record1 fields ext ->
259 Record1
260 <$> Traversable.traverse (mapM f) fields
261 <*> f ext