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