on 77ff8ca help sign in
elk/compiler/Type/State.hs
203 lines 7.0 kB history raw
1module Type.State where
3import Type.Type
4import qualified Data.Map as Map
5import qualified Data.List as List
6import qualified Type.Environment as Env
7import qualified Data.UnionFind.IO as UF
8import Control.Monad.State
9import Control.Applicative ((<$>),(<*>), Applicative)
10import qualified Data.Traversable as Traversable
11import Text.PrettyPrint as P
12import SourceSyntax.PrettyPrint
13import SourceSyntax.Location
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 = [] }
27-- Keeps track of the environment, type variable pool, and a list of errors
28data SolverState = SS {
29 sEnv :: Map.Map String Variable,
30 sSavedEnv :: Map.Map String Variable,
31 sPool :: Pool,
32 sMark :: Int,
33 sErrors :: [IO P.Doc]
36initialState = SS {
37 sEnv = Map.empty,
38 sSavedEnv = Map.empty,
39 sPool = emptyPool,
40 sMark = noMark + 1, -- The mark must never be equal to noMark!
41 sErrors = []
44modifyEnv f = modify $ \state -> state { sEnv = f (sEnv state) }
45modifyPool f = modify $ \state -> state { sPool = f (sPool state) }
47addError span message t1 t2 =
48 modify $ \state -> state { sErrors = err : sErrors state }
49 where
50 err = makeError <$> extraPretty t1 <*> extraPretty t2
52 location = case span of
53 NoSpan msg -> ""
54 Span p1 p2 msg ->
55 if line p1 == line p2 then " on line " ++ show (line p1)
56 else " between lines " ++ show (line p1) ++ " and " ++ show (line p2)
58 display msg = if null msg then "\n"
59 else "\n" ++ unlines (map (" "++) $ lines msg)
61 src = case span of
62 NoSpan msg -> display msg
63 Span _ _ msg -> display msg
65 defaultMessage = "Something weird is happening with this value:"
67 makeError pt1 pt2 =
68 P.vcat [ P.text $ "Type error" ++ location ++ ":"
69 , P.vcat . map P.text . lines $ if null message then defaultMessage else message
70 , P.text src
71 , P.text " Expected Type:" <+> pt1
72 , P.text " Actual Type:" <+> pt2 <> P.text "\n"
73 ]
75switchToPool pool = modifyPool (\_ -> pool)
77getPool :: StateT SolverState IO Pool
78getPool = sPool <$> get
80getEnv :: StateT SolverState IO (Map.Map String Variable)
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 v -> return v
115 TermN t -> do
116 flatStructure <- traverseTerm flatten t
117 pool <- getPool
118 var <- liftIO . UF.fresh $ Descriptor {
119 structure = Just flatStructure,
120 rank = maxRank pool,
121 flex = Flexible,
122 name = Nothing,
123 copy = Nothing,
124 mark = noMark
125 }
126 register var
128makeInstance :: Variable -> StateT SolverState IO Variable
129makeInstance var = do
130 alreadyCopied <- uniqueMark
131 freshVar <- makeCopy alreadyCopied var
132 restore alreadyCopied var
133 return freshVar
135makeCopy :: Int -> Variable -> StateT SolverState IO Variable
136makeCopy alreadyCopied variable = do
137 desc <- liftIO $ UF.descriptor variable
138 case () of
139 () | mark desc == alreadyCopied ->
140 case copy desc of
141 Just v -> return v
142 Nothing -> error "This should be impossible."
144 | rank desc /= noRank || flex desc == Constant ->
145 return variable
147 | otherwise -> do
148 pool <- getPool
149 newVar <- liftIO $ UF.fresh $ Descriptor {
150 structure = Nothing,
151 rank = maxRank pool,
152 mark = noMark,
153 flex = case flex desc of
154 Is s -> Is s
155 _ -> Flexible,
156 copy = Nothing,
157 name = case flex desc of
158 Rigid -> Nothing
159 _ -> name desc
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