on f71cbfa help sign in
elk/compiler/Type/State.hs
211 lines 7.3 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
14import qualified SourceSyntax.Type as Src
15import qualified Type.Alias as Alias
17-- Pool
18-- Holds a bunch of variables
19-- The rank of each variable is less than or equal to the pool's "maxRank"
20-- The young pool exists to make it possible to identify these vars in constant time.
22data Pool = Pool {
23 maxRank :: Int,
24 inhabitants :: [Variable]
25} deriving Show
27emptyPool = Pool { maxRank = outermostRank, inhabitants = [] }
29type Env = Map.Map String Variable
31-- Keeps track of the environment, type variable pool, and a list of errors
32data SolverState = SS {
33 sEnv :: Env,
34 sSavedEnv :: Env,
35 sPool :: Pool,
36 sMark :: Int,
37 sErrors :: [Alias.Rules -> IO P.Doc]
40initialState = SS {
41 sEnv = Map.empty,
42 sSavedEnv = Map.empty,
43 sPool = emptyPool,
44 sMark = noMark + 1, -- The mark must never be equal to noMark!
45 sErrors = []
48modifyEnv f = modify $ \state -> state { sEnv = f (sEnv state) }
49modifyPool f = modify $ \state -> state { sPool = f (sPool state) }
51addError span hint t1 t2 =
52 modify $ \state -> state { sErrors = makeError : sErrors state }
53 where
54 makeError rules = do
55 let prettiest = pretty . Alias.realias rules
56 t1' <- prettiest <$> toSrcType t1
57 t2' <- prettiest <$> toSrcType t2
58 return . P.vcat $
59 [ display $ case span of { NoSpan msg -> msg ; Span _ _ msg -> msg }
60 , case hint of
61 Nothing -> P.text " Could not match the following types:"
62 Just msg -> P.text $ eightyCharLines 2 $
63 msg ++ ", so I could not match the following types:"
64 , P.text " " <> t1'
65 , P.text " " <> t2'
66 ]
68 location = case span of
69 NoSpan msg -> ""
70 Span p1 p2 msg ->
71 if line p1 == line p2 then " on line " ++ show (line p1)
72 else " between lines " ++ show (line p1) ++ " and " ++ show (line p2)
74 display msg =
75 case lines msg of
76 [] -> P.text $ "Type error" ++ location ++ ":"
77 lines' ->
78 P.vcat [ P.text $ "Type error" ++ location ++ ", in or near this expression:"
79 , P.text $ " " ++ List.intercalate "\n " lines' ]
82switchToPool pool = modifyPool (\_ -> pool)
84getPool :: StateT SolverState IO Pool
85getPool = sPool <$> get
87getEnv :: StateT SolverState IO Env
88getEnv = sEnv <$> get
90saveLocalEnv :: StateT SolverState IO ()
91saveLocalEnv = do
92 env <- sEnv <$> get
93 modify $ \state -> state { sSavedEnv = env }
95uniqueMark :: StateT SolverState IO Int
96uniqueMark = do
97 state <- get
98 let mark = sMark state
99 put $ state { sMark = mark + 1 }
100 return mark
102nextRankPool :: StateT SolverState IO Pool
103nextRankPool = do
104 pool <- getPool
105 return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
107register :: Variable -> StateT SolverState IO Variable
108register variable = do
109 modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
110 return variable
112introduce :: Variable -> StateT SolverState IO Variable
113introduce variable = do
114 pool <- getPool
115 liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
116 register variable
118flatten :: Type -> StateT SolverState IO Variable
119flatten term =
120 case term of
121 VarN v -> return v
122 TermN t -> do
123 flatStructure <- traverseTerm flatten t
124 pool <- getPool
125 var <- liftIO . UF.fresh $ Descriptor {
126 structure = Just flatStructure,
127 rank = maxRank pool,
128 flex = Flexible,
129 name = Nothing,
130 copy = Nothing,
131 mark = noMark
132 }
133 register var
135makeInstance :: Variable -> StateT SolverState IO Variable
136makeInstance var = do
137 alreadyCopied <- uniqueMark
138 freshVar <- makeCopy alreadyCopied var
139 restore alreadyCopied var
140 return freshVar
142makeCopy :: Int -> Variable -> StateT SolverState IO Variable
143makeCopy alreadyCopied variable = do
144 desc <- liftIO $ UF.descriptor variable
145 case () of
146 () | mark desc == alreadyCopied ->
147 case copy desc of
148 Just v -> return v
149 Nothing -> error $ "Error copying type variable. This should be impossible." ++
150 " Please report an error to the github repo!"
152 | rank desc /= noRank || flex desc == Constant ->
153 return variable
155 | otherwise -> do
156 pool <- getPool
157 newVar <- liftIO $ UF.fresh $ Descriptor {
158 structure = Nothing,
159 rank = maxRank pool,
160 mark = noMark,
161 flex = case flex desc of
162 Is s -> Is s
163 _ -> Flexible,
164 copy = Nothing,
165 name = case flex desc of
166 Rigid -> Nothing
167 _ -> name desc
168 }
169 register newVar
171 -- Link the original variable to the new variable. This lets us
172 -- avoid making multiple copies of the variable we are instantiating.
173 --
174 -- Need to do this before recursively copying the structure of
175 -- the variable to avoid looping on cyclic terms.
176 liftIO $ UF.modifyDescriptor variable $ \desc ->
177 desc { mark = alreadyCopied, copy = Just newVar }
179 -- Now we recursively copy the structure of the variable.
180 -- We have already marked the variable as copied, so we
181 -- will not repeat this work or crawl this variable again.
182 case structure desc of
183 Nothing -> return newVar
184 Just term -> do
185 newTerm <- traverseTerm (makeCopy alreadyCopied) term
186 liftIO $ UF.modifyDescriptor newVar $ \desc ->
187 desc { structure = Just newTerm }
188 return newVar
190restore :: Int -> Variable -> StateT SolverState IO Variable
191restore alreadyCopied variable = do
192 desc <- liftIO $ UF.descriptor variable
193 if mark desc /= alreadyCopied
194 then return variable
195 else do
196 restoredStructure <-
197 Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
198 liftIO $ UF.modifyDescriptor variable $ \desc ->
199 desc { mark = noMark, rank = noRank, structure = restoredStructure }
200 return variable
202traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
203traverseTerm f term =
204 case term of
205 App1 a b -> App1 <$> f a <*> f b
206 Fun1 a b -> Fun1 <$> f a <*> f b
207 Var1 x -> Var1 <$> f x
208 EmptyRecord1 -> return EmptyRecord1
209 Record1 fields ext ->
210 Record1 <$> Traversable.traverse (mapM f) fields <*> f ext