1{-# LANGUAGE FlexibleContexts #-}
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
12import Text.PrettyPrint as P
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.
22 , inhabitants :: [Variable]
29 { maxRank = outermostRank
34type Env = Map.Map String Variable
37-- Keeps track of the environment, type variable pool, and a list of errors
47initialState :: SolverState
51 , sSavedEnv = Map.empty
53 , sMark = noMark + 1 -- The mark must never be equal to noMark!
58modifyEnv :: (MonadState SolverState m) => (Env -> Env) -> m ()
60 modify $ \state -> state { sEnv = f (sEnv state) }
63modifyPool :: (MonadState SolverState m) => (Pool -> Pool) -> m ()
65 modify $ \state -> state { sPool = f (sPool state) }
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 }
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 ":"
88 , maybe P.empty (P.nest 4 . P.text) hint
89 , P.text " It is related to the following expression:"
91 , P.nest 8 $ A.getRegionDocs region
95switchToPool :: (MonadState SolverState m) => Pool -> m ()
97 modifyPool (\_ -> pool)
100getPool :: StateT SolverState IO Pool
105getEnv :: StateT SolverState IO Env
110saveLocalEnv :: StateT SolverState IO ()
112 do env <- sEnv <$> get
113 modify $ \state -> state { sSavedEnv = env }
116uniqueMark :: StateT SolverState IO Int
119 let mark = sMark state
120 put $ state { sMark = mark + 1 }
124nextRankPool :: StateT SolverState IO Pool
127 return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
130register :: Variable -> StateT SolverState IO Variable
132 do modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
136introduce :: Variable -> StateT SolverState IO Variable
139 liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
143flatten :: Type -> StateT SolverState IO Variable
147 do liftIO $ UF.modifyDescriptor v $ \desc -> desc { alias = maybeAlias <|> alias desc }
150 TermN maybeAlias t ->
151 do flatStructure <- traverseTerm flatten t
153 var <- liftIO . UF.fresh $ Descriptor
154 { structure = Just flatStructure
155 , rank = maxRank pool
165makeInstance :: Variable -> StateT SolverState IO Variable
167 do alreadyCopied <- uniqueMark
168 freshVar <- makeCopy alreadyCopied var
169 restore alreadyCopied var
173makeCopy :: Int -> Variable -> StateT SolverState IO Variable
174makeCopy alreadyCopied variable = do
175 desc <- liftIO $ UF.descriptor variable
177 () | mark desc == alreadyCopied ->
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 ->
188 newVar <- liftIO $ UF.fresh $ Descriptor
189 { structure = Nothing
190 , rank = maxRank pool
192 , flex = case flex desc of
196 , name = case flex desc of
203 -- Link the original variable to the new variable. This lets us
204 -- avoid making multiple copies of the variable we are instantiating.
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
217 newTerm <- traverseTerm (makeCopy alreadyCopied) term
218 liftIO $ UF.modifyDescriptor newVar $ \desc ->
219 desc { structure = Just newTerm }
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
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 }
236traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
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
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list