on cfaeff9 help sign in
elk/src/Type/State.hs
245 lines 7.3 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 AST.Annotation as A
11import AST.PrettyPrint
12import Text.PrettyPrint as P
13import 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 , sErrors :: [P.Doc]
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 , sErrors = []
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) }
68addError
69 :: A.Region
70 -> Maybe String
71 -> UF.Point Descriptor
72 -> UF.Point Descriptor
73 -> StateT SolverState IO ()
74addError region hint t1 t2 =
75 do err <- liftIO makeError
76 modify $ \state -> state { sErrors = err : sErrors state }
77 where
78 makeError = do
79 t1' <- pretty <$> toSrcType t1
80 t2' <- pretty <$> toSrcType t2
81 return . foldr ($+$) P.empty $
82 [ P.text "Type mismatch between the following types" <+> pretty region <> P.text ":"
83 , P.text ""
84 , P.nest 8 t1'
85 , P.text ""
86 , P.nest 8 t2'
87 , P.text ""
88 , maybe P.empty (P.nest 4 . P.text) hint
89 , P.text " It is related to the following expression:"
90 , P.text ""
91 , P.nest 8 $ A.getRegionDocs region
92 ]
95switchToPool :: (MonadState SolverState m) => Pool -> m ()
96switchToPool pool =
97 modifyPool (\_ -> pool)
100getPool :: StateT SolverState IO Pool
101getPool =
102 gets sPool
105getEnv :: StateT SolverState IO Env
106getEnv =
107 gets sEnv
110saveLocalEnv :: StateT SolverState IO ()
111saveLocalEnv =
112 do env <- sEnv <$> get
113 modify $ \state -> state { sSavedEnv = env }
116uniqueMark :: StateT SolverState IO Int
117uniqueMark =
118 do state <- get
119 let mark = sMark state
120 put $ state { sMark = mark + 1 }
121 return mark
124nextRankPool :: StateT SolverState IO Pool
125nextRankPool =
126 do pool <- getPool
127 return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
130register :: Variable -> StateT SolverState IO Variable
131register variable =
132 do modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
133 return variable
136introduce :: Variable -> StateT SolverState IO Variable
137introduce variable =
138 do pool <- getPool
139 liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
140 register variable
143flatten :: Type -> StateT SolverState IO Variable
144flatten term =
145 case term of
146 VarN maybeAlias v ->
147 do liftIO $ UF.modifyDescriptor v $ \desc -> desc { alias = maybeAlias <|> alias desc }
148 return v
150 TermN maybeAlias t ->
151 do flatStructure <- traverseTerm flatten t
152 pool <- getPool
153 var <- liftIO . UF.fresh $ Descriptor
154 { structure = Just flatStructure
155 , rank = maxRank pool
156 , flex = Flexible
157 , name = Nothing
158 , copy = Nothing
159 , mark = noMark
160 , alias = maybeAlias
161 }
162 register var
165makeInstance :: Variable -> StateT SolverState IO Variable
166makeInstance var =
167 do alreadyCopied <- uniqueMark
168 freshVar <- makeCopy alreadyCopied var
169 restore alreadyCopied var
170 return freshVar
173makeCopy :: Int -> Variable -> StateT SolverState IO Variable
174makeCopy alreadyCopied variable = do
175 desc <- liftIO $ UF.descriptor variable
176 case () of
177 () | mark desc == alreadyCopied ->
178 case copy desc of
179 Just v -> return v
180 Nothing -> error $ "Error copying type variable. This should be impossible." ++
181 " Please report an error to the github repo!"
183 | rank desc /= noRank || flex desc == Constant ->
184 return variable
186 | otherwise -> do
187 pool <- getPool
188 newVar <- liftIO $ UF.fresh $ Descriptor
189 { structure = Nothing
190 , rank = maxRank pool
191 , mark = noMark
192 , flex = case flex desc of
193 Is s -> Is s
194 _ -> Flexible
195 , copy = Nothing
196 , name = case flex desc of
197 Rigid -> Nothing
198 _ -> name desc
199 , alias = Nothing
200 }
201 register newVar
203 -- Link the original variable to the new variable. This lets us
204 -- avoid making multiple copies of the variable we are instantiating.
205 --
206 -- Need to do this before recursively copying the structure of
207 -- the variable to avoid looping on cyclic terms.
208 liftIO $ UF.modifyDescriptor variable $ \desc ->
209 desc { mark = alreadyCopied, copy = Just newVar }
211 -- Now we recursively copy the structure of the variable.
212 -- We have already marked the variable as copied, so we
213 -- will not repeat this work or crawl this variable again.
214 case structure desc of
215 Nothing -> return newVar
216 Just term -> do
217 newTerm <- traverseTerm (makeCopy alreadyCopied) term
218 liftIO $ UF.modifyDescriptor newVar $ \desc ->
219 desc { structure = Just newTerm }
220 return newVar
223restore :: Int -> Variable -> StateT SolverState IO Variable
224restore alreadyCopied variable =
225 do desc <- liftIO $ UF.descriptor variable
226 case mark desc /= alreadyCopied of
227 True -> return variable
228 False ->
229 do restoredStructure <-
230 Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
231 liftIO $ UF.modifyDescriptor variable $ \desc ->
232 desc { mark = noMark, rank = noRank, structure = restoredStructure }
233 return variable
236traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
237traverseTerm f term =
238 case term of
239 App1 a b -> App1 <$> f a <*> f b
240 Fun1 a b -> Fun1 <$> f a <*> f b
241 Var1 x -> Var1 <$> f x
242 EmptyRecord1 -> return EmptyRecord1
243 Record1 fields ext ->
244 Record1 <$> Traversable.traverse (mapM f) fields <*> f ext