git.iko.soy/elk
on edfca84 help sign in
elk/src/Type/State.hs
222 lines 6.5 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 <- liftIO . UF.fresh $ Descriptor
131 { structure = Just flatStructure
132 , rank = maxRank pool
133 , flex = Flexible
134 , name = Nothing
135 , copy = Nothing
136 , mark = noMark
137 , alias = maybeAlias
138 }
139 register var
142makeInstance :: Variable -> StateT SolverState IO Variable
143makeInstance var =
144 do alreadyCopied <- uniqueMark
145 freshVar <- makeCopy alreadyCopied var
146 restore alreadyCopied var
147 return freshVar
150makeCopy :: Int -> Variable -> StateT SolverState IO Variable
151makeCopy alreadyCopied variable = do
152 desc <- liftIO $ UF.descriptor variable
153 case () of
154 () | mark desc == alreadyCopied ->
155 case copy desc of
156 Just v -> return v
157 Nothing -> error $ "Error copying type variable. This should be impossible." ++
158 " Please report an error to the github repo!"
160 | rank desc /= noRank || flex desc == Constant ->
161 return variable
163 | otherwise -> do
164 pool <- getPool
165 newVar <- liftIO $ UF.fresh $ Descriptor
166 { structure = Nothing
167 , rank = maxRank pool
168 , mark = noMark
169 , flex = case flex desc of
170 Is s -> Is s
171 _ -> Flexible
172 , copy = Nothing
173 , name = case flex desc of
174 Rigid -> Nothing
175 _ -> name desc
176 , alias = Nothing
177 }
178 register newVar
180 -- Link the original variable to the new variable. This lets us
181 -- avoid making multiple copies of the variable we are instantiating.
182 --
183 -- Need to do this before recursively copying the structure of
184 -- the variable to avoid looping on cyclic terms.
185 liftIO $ UF.modifyDescriptor variable $ \desc ->
186 desc { mark = alreadyCopied, copy = Just newVar }
188 -- Now we recursively copy the structure of the variable.
189 -- We have already marked the variable as copied, so we
190 -- will not repeat this work or crawl this variable again.
191 case structure desc of
192 Nothing -> return newVar
193 Just term -> do
194 newTerm <- traverseTerm (makeCopy alreadyCopied) term
195 liftIO $ UF.modifyDescriptor newVar $ \desc ->
196 desc { structure = Just newTerm }
197 return newVar
200restore :: Int -> Variable -> StateT SolverState IO Variable
201restore alreadyCopied variable =
202 do desc <- liftIO $ UF.descriptor variable
203 case mark desc /= alreadyCopied of
204 True -> return variable
205 False ->
206 do restoredStructure <-
207 Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
208 liftIO $ UF.modifyDescriptor variable $ \desc ->
209 desc { mark = noMark, rank = noRank, structure = restoredStructure }
210 return variable
213traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
214traverseTerm f term =
215 case term of
216 App1 a b -> App1 <$> f a <*> f b
217 Fun1 a b -> Fun1 <$> f a <*> f b
218 Var1 x -> Var1 <$> f x
219 EmptyRecord1 -> return EmptyRecord1
220 Record1 fields ext ->
221 Record1 <$> Traversable.traverse (mapM f) fields <*> f ext