git.iko.soy/elk
on c1ce03a help sign in
elk/src/Type/State.hs
203 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 } deriving Show
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) }
48addError :: A.Region -> Maybe String -> UF.Point Descriptor -> UF.Point Descriptor
49 -> StateT SolverState IO ()
50addError region hint t1 t2 =
51 do err <- liftIO makeError
52 modify $ \state -> state { sErrors = err : sErrors state }
53 where
54 makeError = do
55 t1' <- pretty <$> toSrcType t1
56 t2' <- pretty <$> toSrcType t2
57 return . foldr ($+$) P.empty $
58 [ P.text "Type mismatch" <+> pretty region <> P.text "."
59 , maybe P.empty P.text hint
60 , P.text ""
61 , P.nest 8 $ A.getRegionDocs region
62 , P.text ""
63 , P.text " Something is causing a mismatch between the following types:"
64 , P.text ""
65 , P.nest 8 t1'
66 , P.text ""
67 , P.nest 8 t2'
68 ]
70switchToPool pool = modifyPool (\_ -> pool)
72getPool :: StateT SolverState IO Pool
73getPool = sPool <$> get
75getEnv :: StateT SolverState IO Env
76getEnv = sEnv <$> get
78saveLocalEnv :: StateT SolverState IO ()
79saveLocalEnv = do
80 env <- sEnv <$> get
81 modify $ \state -> state { sSavedEnv = env }
83uniqueMark :: StateT SolverState IO Int
84uniqueMark = do
85 state <- get
86 let mark = sMark state
87 put $ state { sMark = mark + 1 }
88 return mark
90nextRankPool :: StateT SolverState IO Pool
91nextRankPool = do
92 pool <- getPool
93 return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
95register :: Variable -> StateT SolverState IO Variable
96register variable = do
97 modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
98 return variable
100introduce :: Variable -> StateT SolverState IO Variable
101introduce variable = do
102 pool <- getPool
103 liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
104 register variable
106flatten :: Type -> StateT SolverState IO Variable
107flatten term =
108 case term of
109 VarN maybeAlias v -> do
110 liftIO $ UF.modifyDescriptor v $ \desc -> desc { alias = maybeAlias <|> alias desc }
111 return v
112 TermN maybeAlias t -> do
113 flatStructure <- traverseTerm flatten t
114 pool <- getPool
115 var <- liftIO . UF.fresh $ Descriptor
116 { structure = Just flatStructure
117 , rank = maxRank pool
118 , flex = Flexible
119 , name = Nothing
120 , copy = Nothing
121 , mark = noMark
122 , alias = maybeAlias
123 }
124 register var
126makeInstance :: Variable -> StateT SolverState IO Variable
127makeInstance var = do
128 alreadyCopied <- uniqueMark
129 freshVar <- makeCopy alreadyCopied var
130 restore alreadyCopied var
131 return freshVar
133makeCopy :: Int -> Variable -> StateT SolverState IO Variable
134makeCopy alreadyCopied variable = do
135 desc <- liftIO $ UF.descriptor variable
136 case () of
137 () | mark desc == alreadyCopied ->
138 case copy desc of
139 Just v -> return v
140 Nothing -> error $ "Error copying type variable. This should be impossible." ++
141 " Please report an error to the github repo!"
143 | rank desc /= noRank || flex desc == Constant ->
144 return variable
146 | otherwise -> do
147 pool <- getPool
148 newVar <- liftIO $ UF.fresh $ Descriptor
149 { structure = Nothing
150 , rank = maxRank pool
151 , mark = noMark
152 , flex = case flex desc of
153 Is s -> Is s
154 _ -> Flexible
155 , copy = Nothing
156 , name = case flex desc of
157 Rigid -> Nothing
158 _ -> name desc
159 , alias = Nothing
160 }
161 register newVar
163 -- Link the original variable to the new variable. This lets us
164 -- avoid making multiple copies of the variable we are instantiating.
165 --
166 -- Need to do this before recursively copying the structure of
167 -- the variable to avoid looping on cyclic terms.
168 liftIO $ UF.modifyDescriptor variable $ \desc ->
169 desc { mark = alreadyCopied, copy = Just newVar }
171 -- Now we recursively copy the structure of the variable.
172 -- We have already marked the variable as copied, so we
173 -- will not repeat this work or crawl this variable again.
174 case structure desc of
175 Nothing -> return newVar
176 Just term -> do
177 newTerm <- traverseTerm (makeCopy alreadyCopied) term
178 liftIO $ UF.modifyDescriptor newVar $ \desc ->
179 desc { structure = Just newTerm }
180 return newVar
182restore :: Int -> Variable -> StateT SolverState IO Variable
183restore alreadyCopied variable = do
184 desc <- liftIO $ UF.descriptor variable
185 if mark desc /= alreadyCopied
186 then return variable
187 else do
188 restoredStructure <-
189 Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
190 liftIO $ UF.modifyDescriptor variable $ \desc ->
191 desc { mark = noMark, rank = noRank, structure = restoredStructure }
192 return variable
194traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
195traverseTerm f term =
196 case term of
197 App1 a b -> App1 <$> f a <*> f b
198 Fun1 a b -> Fun1 <$> f a <*> f b
199 Var1 x -> Var1 <$> f x
200 EmptyRecord1 -> return EmptyRecord1
201 Record1 fields ext ->
202 Record1 <$> Traversable.traverse (mapM f) fields <*> f ext