on e4e8d89 help sign in
elk/compiler/Type/State.hs
195 lines 6.6 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 =
53 case span of
54 NoSpan -> ""
55 Span p1 p2 ->
56 if line p1 == line p2 then "on line " ++ show (line p1)
57 else "between lines " ++ show (line p1) ++ " and " ++ show (line p2)
59 makeError pt1 pt2 =
60 P.vcat [ P.text $ "Type error " ++ location
61 , if null message then empty else P.vcat . map P.text $ lines message
62 , P.text " "
63 , P.text " Expected Type:" <+> pt1
64 , P.text " Actual Type:" <+> pt2 <> P.text "\n"
65 ]
67switchToPool pool = modifyPool (\_ -> pool)
69getPool :: StateT SolverState IO Pool
70getPool = sPool <$> get
72getEnv :: StateT SolverState IO (Map.Map String Variable)
73getEnv = sEnv <$> get
75saveLocalEnv :: StateT SolverState IO ()
76saveLocalEnv = do
77 env <- sEnv <$> get
78 modify $ \state -> state { sSavedEnv = env }
80uniqueMark :: StateT SolverState IO Int
81uniqueMark = do
82 state <- get
83 let mark = sMark state
84 put $ state { sMark = mark + 1 }
85 return mark
87nextRankPool :: StateT SolverState IO Pool
88nextRankPool = do
89 pool <- getPool
90 return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
92register :: Variable -> StateT SolverState IO Variable
93register variable = do
94 modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
95 return variable
97introduce :: Variable -> StateT SolverState IO Variable
98introduce variable = do
99 pool <- getPool
100 liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
101 register variable
103flatten :: Type -> StateT SolverState IO Variable
104flatten term =
105 case term of
106 VarN v -> return v
107 TermN t -> do
108 flatStructure <- traverseTerm flatten t
109 pool <- getPool
110 var <- liftIO . UF.fresh $ Descriptor {
111 structure = Just flatStructure,
112 rank = maxRank pool,
113 flex = Flexible,
114 name = Nothing,
115 copy = Nothing,
116 mark = noMark
117 }
118 register var
120makeInstance :: Variable -> StateT SolverState IO Variable
121makeInstance var = do
122 alreadyCopied <- uniqueMark
123 freshVar <- makeCopy alreadyCopied var
124 restore alreadyCopied var
125 return freshVar
127makeCopy :: Int -> Variable -> StateT SolverState IO Variable
128makeCopy alreadyCopied variable = do
129 desc <- liftIO $ UF.descriptor variable
130 case () of
131 () | mark desc == alreadyCopied ->
132 case copy desc of
133 Just v -> return v
134 Nothing -> error "This should be impossible."
136 | rank desc /= noRank || flex desc == Constant ->
137 return variable
139 | otherwise -> do
140 pool <- getPool
141 newVar <- liftIO $ UF.fresh $ Descriptor {
142 structure = Nothing,
143 rank = maxRank pool,
144 mark = noMark,
145 flex = case flex desc of
146 Is s -> Is s
147 _ -> Flexible,
148 copy = Nothing,
149 name = case flex desc of
150 Rigid -> Nothing
151 _ -> name desc
152 }
153 register newVar
155 -- Link the original variable to the new variable. This lets us
156 -- avoid making multiple copies of the variable we are instantiating.
157 --
158 -- Need to do this before recursively copying the structure of
159 -- the variable to avoid looping on cyclic terms.
160 liftIO $ UF.modifyDescriptor variable $ \desc ->
161 desc { mark = alreadyCopied, copy = Just newVar }
163 -- Now we recursively copy the structure of the variable.
164 -- We have already marked the variable as copied, so we
165 -- will not repeat this work or crawl this variable again.
166 case structure desc of
167 Nothing -> return newVar
168 Just term -> do
169 newTerm <- traverseTerm (makeCopy alreadyCopied) term
170 liftIO $ UF.modifyDescriptor newVar $ \desc ->
171 desc { structure = Just newTerm }
172 return newVar
174restore :: Int -> Variable -> StateT SolverState IO Variable
175restore alreadyCopied variable = do
176 desc <- liftIO $ UF.descriptor variable
177 if mark desc /= alreadyCopied
178 then return variable
179 else do
180 restoredStructure <-
181 Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
182 liftIO $ UF.modifyDescriptor variable $ \desc ->
183 desc { mark = noMark, rank = noRank, structure = restoredStructure }
184 return variable
186traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
187traverseTerm f term =
188 case term of
189 App1 a b -> App1 <$> f a <*> f b
190 Fun1 a b -> Fun1 <$> f a <*> f b
191 Var1 x -> Var1 <$> f x
192 EmptyRecord1 -> return EmptyRecord1
193 Record1 fields ext ->
194 Record1 <$> Traversable.traverse (mapM f) fields <*> f ext