on 96dfd88 help sign in
elk/src/Type/State.hs
208 lines 6.7 kB history raw
1module Type.State where
3import Control.Applicative ( (<$>), (<*>), Applicative, (<|>) )
4import Control.Monad.State
5import qualified Data.Map as Map
6import qualified Data.Traversable as Traversable
7import qualified Data.UnionFind.IO as UF
9import qualified AST.Annotation as A
10import AST.PrettyPrint
11import Text.PrettyPrint as P
12import 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 }
24emptyPool = Pool { maxRank = outermostRank, inhabitants = [] }
26type Env = Map.Map String Variable
28-- Keeps track of the environment, type variable pool, and a list of errors
29data SolverState = SS {
30 sEnv :: Env,
31 sSavedEnv :: Env,
32 sPool :: Pool,
33 sMark :: Int,
34 sErrors :: [P.Doc]
37initialState = SS {
38 sEnv = Map.empty,
39 sSavedEnv = Map.empty,
40 sPool = emptyPool,
41 sMark = noMark + 1, -- The mark must never be equal to noMark!
42 sErrors = []
45modifyEnv f = modify $ \state -> state { sEnv = f (sEnv state) }
46modifyPool f = modify $ \state -> state { sPool = f (sPool state) }
49addError
50 :: A.Region
51 -> Maybe String
52 -> UF.Point Descriptor
53 -> UF.Point Descriptor
54 -> StateT SolverState IO ()
55addError region hint t1 t2 =
56 do err <- liftIO makeError
57 modify $ \state -> state { sErrors = err : sErrors state }
58 where
59 makeError = do
60 t1' <- pretty <$> toSrcType t1
61 t2' <- pretty <$> toSrcType t2
62 return . foldr ($+$) P.empty $
63 [ P.text "Type mismatch between the following types:"
64 , P.text ""
65 , P.nest 8 t1'
66 , P.text ""
67 , P.nest 8 t2'
68 , P.text ""
69 , maybe P.empty (P.nest 4 . P.text) hint
70 , P.text " It is related to the expression" <+> pretty region
71 , P.text ""
72 , P.nest 8 $ A.getRegionDocs region
73 ]
75switchToPool pool = modifyPool (\_ -> pool)
77getPool :: StateT SolverState IO Pool
78getPool = sPool <$> get
80getEnv :: StateT SolverState IO Env
81getEnv = sEnv <$> get
83saveLocalEnv :: StateT SolverState IO ()
84saveLocalEnv = do
85 env <- sEnv <$> get
86 modify $ \state -> state { sSavedEnv = env }
88uniqueMark :: StateT SolverState IO Int
89uniqueMark = do
90 state <- get
91 let mark = sMark state
92 put $ state { sMark = mark + 1 }
93 return mark
95nextRankPool :: StateT SolverState IO Pool
96nextRankPool = do
97 pool <- getPool
98 return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
100register :: Variable -> StateT SolverState IO Variable
101register variable = do
102 modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
103 return variable
105introduce :: Variable -> StateT SolverState IO Variable
106introduce variable = do
107 pool <- getPool
108 liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
109 register variable
111flatten :: Type -> StateT SolverState IO Variable
112flatten term =
113 case term of
114 VarN maybeAlias v -> do
115 liftIO $ UF.modifyDescriptor v $ \desc -> desc { alias = maybeAlias <|> alias desc }
116 return v
117 TermN maybeAlias t -> do
118 flatStructure <- traverseTerm flatten t
119 pool <- getPool
120 var <- liftIO . UF.fresh $ Descriptor
121 { structure = Just flatStructure
122 , rank = maxRank pool
123 , flex = Flexible
124 , name = Nothing
125 , copy = Nothing
126 , mark = noMark
127 , alias = maybeAlias
128 }
129 register var
131makeInstance :: Variable -> StateT SolverState IO Variable
132makeInstance var = do
133 alreadyCopied <- uniqueMark
134 freshVar <- makeCopy alreadyCopied var
135 restore alreadyCopied var
136 return freshVar
138makeCopy :: Int -> Variable -> StateT SolverState IO Variable
139makeCopy alreadyCopied variable = do
140 desc <- liftIO $ UF.descriptor variable
141 case () of
142 () | mark desc == alreadyCopied ->
143 case copy desc of
144 Just v -> return v
145 Nothing -> error $ "Error copying type variable. This should be impossible." ++
146 " Please report an error to the github repo!"
148 | rank desc /= noRank || flex desc == Constant ->
149 return variable
151 | otherwise -> do
152 pool <- getPool
153 newVar <- liftIO $ UF.fresh $ Descriptor
154 { structure = Nothing
155 , rank = maxRank pool
156 , mark = noMark
157 , flex = case flex desc of
158 Is s -> Is s
159 _ -> Flexible
160 , copy = Nothing
161 , name = case flex desc of
162 Rigid -> Nothing
163 _ -> name desc
164 , alias = Nothing
165 }
166 register newVar
168 -- Link the original variable to the new variable. This lets us
169 -- avoid making multiple copies of the variable we are instantiating.
170 --
171 -- Need to do this before recursively copying the structure of
172 -- the variable to avoid looping on cyclic terms.
173 liftIO $ UF.modifyDescriptor variable $ \desc ->
174 desc { mark = alreadyCopied, copy = Just newVar }
176 -- Now we recursively copy the structure of the variable.
177 -- We have already marked the variable as copied, so we
178 -- will not repeat this work or crawl this variable again.
179 case structure desc of
180 Nothing -> return newVar
181 Just term -> do
182 newTerm <- traverseTerm (makeCopy alreadyCopied) term
183 liftIO $ UF.modifyDescriptor newVar $ \desc ->
184 desc { structure = Just newTerm }
185 return newVar
187restore :: Int -> Variable -> StateT SolverState IO Variable
188restore alreadyCopied variable = do
189 desc <- liftIO $ UF.descriptor variable
190 if mark desc /= alreadyCopied
191 then return variable
192 else do
193 restoredStructure <-
194 Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
195 liftIO $ UF.modifyDescriptor variable $ \desc ->
196 desc { mark = noMark, rank = noRank, structure = restoredStructure }
197 return variable
199traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
200traverseTerm f term =
201 case term of
202 App1 a b -> App1 <$> f a <*> f b
203 Fun1 a b -> Fun1 <$> f a <*> f b
204 Var1 x -> Var1 <$> f x
205 EmptyRecord1 -> return EmptyRecord1
206 Record1 fields ext ->
207 Record1 <$> Traversable.traverse (mapM f) fields <*> f ext