git.iko.soy/elk
on da346ea help sign in
elk/compiler/Type/State.hs
187 lines 6.2 kB history raw
1{-# LANGUAGE MultiWayIf #-}
2module Type.State where
4import Type.Type
5import qualified Data.Map as Map
6import qualified Data.List as List
7import qualified Type.Environment as Env
8import qualified Data.UnionFind.IO as UF
9import Control.Monad.State
10import Control.Applicative ((<$>),(<*>), Applicative)
11import qualified Data.Traversable as Traversable
12import Text.PrettyPrint as P
13import SourceSyntax.PrettyPrint
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 message t1 t2 =
48 modify $ \state -> state { sErrors = err : sErrors state }
49 where
50 err = makeError <$> extraPretty t1 <*> extraPretty t2
51 makeError pt1 pt2 =
52 P.vcat [ P.text $ "Type error on line ???"
53 , if null message then empty else P.fsep . map P.text $ words message
54 , P.text " "
55 , P.text " Expected Type:" <+> pt1
56 , P.text " Actual Type:" <+> pt2 <> P.text "\n"
57 ]
59switchToPool pool = modifyPool (\_ -> pool)
61getPool :: StateT SolverState IO Pool
62getPool = sPool <$> get
64getEnv :: StateT SolverState IO (Map.Map String Variable)
65getEnv = sEnv <$> get
67saveLocalEnv :: StateT SolverState IO ()
68saveLocalEnv = do
69 env <- sEnv <$> get
70 modify $ \state -> state { sSavedEnv = env }
72uniqueMark :: StateT SolverState IO Int
73uniqueMark = do
74 state <- get
75 let mark = sMark state
76 put $ state { sMark = mark + 1 }
77 return mark
79nextRankPool :: StateT SolverState IO Pool
80nextRankPool = do
81 pool <- getPool
82 return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
84register :: Variable -> StateT SolverState IO Variable
85register variable = do
86 modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
87 return variable
89introduce :: Variable -> StateT SolverState IO Variable
90introduce variable = do
91 pool <- getPool
92 liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
93 register variable
95flatten :: Type -> StateT SolverState IO Variable
96flatten term =
97 case term of
98 VarN v -> return v
99 TermN t -> do
100 flatStructure <- traverseTerm flatten t
101 pool <- getPool
102 var <- liftIO . UF.fresh $ Descriptor {
103 structure = Just flatStructure,
104 rank = maxRank pool,
105 flex = Flexible,
106 name = Nothing,
107 copy = Nothing,
108 mark = noMark
109 }
110 register var
112makeInstance :: Variable -> StateT SolverState IO Variable
113makeInstance var = do
114 alreadyCopied <- uniqueMark
115 freshVar <- makeCopy alreadyCopied var
116 restore alreadyCopied var
117 return freshVar
119makeCopy :: Int -> Variable -> StateT SolverState IO Variable
120makeCopy alreadyCopied variable = do
121 desc <- liftIO $ UF.descriptor variable
122 if | mark desc == alreadyCopied ->
123 case copy desc of
124 Just v -> return v
125 Nothing -> error "This should be impossible."
127 | rank desc /= noRank || flex desc == Constant ->
128 return variable
130 | otherwise -> do
131 pool <- getPool
132 newVar <- liftIO $ UF.fresh $ Descriptor {
133 structure = Nothing,
134 rank = maxRank pool,
135 mark = noMark,
136 flex = case flex desc of
137 Is s -> Is s
138 _ -> Flexible,
139 copy = Nothing,
140 name = case flex desc of
141 Rigid -> Nothing
142 _ -> name desc
143 }
145 register newVar
147 -- Link the original variable to the new variable. This lets us
148 -- avoid making multiple copies of the variable we are instantiating.
149 --
150 -- Need to do this before recursively copying the structure of
151 -- the variable to avoid looping on cyclic terms.
152 liftIO $ UF.modifyDescriptor variable $ \desc ->
153 desc { mark = alreadyCopied, copy = Just newVar }
155 -- Now we recursively copy the structure of the variable.
156 -- We have already marked the variable as copied, so we
157 -- will not repeat this work or crawl this variable again.
158 case structure desc of
159 Nothing -> return newVar
160 Just term -> do
161 newTerm <- traverseTerm (makeCopy alreadyCopied) term
162 liftIO $ UF.modifyDescriptor newVar $ \desc ->
163 desc { structure = Just newTerm }
164 return newVar
166restore :: Int -> Variable -> StateT SolverState IO Variable
167restore alreadyCopied variable = do
168 desc <- liftIO $ UF.descriptor variable
169 if mark desc /= alreadyCopied
170 then return variable
171 else do
172 restoredStructure <-
173 Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
174 liftIO $ UF.modifyDescriptor variable $ \desc ->
175 desc { mark = noMark, rank = noRank, structure = restoredStructure }
176 return variable
178traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
179traverseTerm f term =
180 case term of
181 App1 a b -> App1 <$> f a <*> f b
182 Fun1 a b -> Fun1 <$> f a <*> f b
183 Var1 x -> Var1 <$> f x
184 EmptyRecord1 -> return EmptyRecord1
185 Record1 fields ext ->
186 Record1 <$> Traversable.traverse (mapM f) fields <*> f ext