on 4e7ef5f help sign in
elk/compiler/Type/State.hs
192 lines 6.4 kB history raw
1{-# OPTIONS_GHC -XMultiWayIf #-}
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) }
46addError message t1 t2 =
47 modify $ \state -> state { sErrors = err : sErrors state }
48 where
49 wordify = P.fsep . map P.text . words
50 msg = wordify message
51 width = maximum . map length . lines $ render msg
52 spaces = List.replicate (width - 15 - 3) ' '
53 err = makeError <$> extraPretty t1 <*> extraPretty t2
54 makeError pt1 pt2 =
55 P.vcat [ P.text $ "Type error" ++ spaces ++ "line ???"
56 , P.text (List.replicate width '-')
57 , msg <> P.text "\n"
58 , P.text " Expected Type:" <+> pt1
59 , P.text " Actual Type:" <+> pt2 <> P.text "\n"
60 , wordify "The error comes from:" <> P.text "\n"
61 , P.nest 3 (P.text "???")
62 ]
64switchToPool pool = modifyPool (\_ -> pool)
66getPool :: StateT SolverState IO Pool
67getPool = sPool <$> get
69getEnv :: StateT SolverState IO (Map.Map String Variable)
70getEnv = sEnv <$> get
72saveLocalEnv :: StateT SolverState IO ()
73saveLocalEnv = do
74 env <- sEnv <$> get
75 modify $ \state -> state { sSavedEnv = env }
77uniqueMark :: StateT SolverState IO Int
78uniqueMark = do
79 state <- get
80 let mark = sMark state
81 put $ state { sMark = mark + 1 }
82 return mark
84nextRankPool :: StateT SolverState IO Pool
85nextRankPool = do
86 pool <- getPool
87 return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
89register :: Variable -> StateT SolverState IO Variable
90register variable = do
91 modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
92 return variable
94introduce :: Variable -> StateT SolverState IO Variable
95introduce variable = do
96 pool <- getPool
97 liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
98 register variable
100flatten :: Type -> StateT SolverState IO Variable
101flatten term =
102 case term of
103 VarN v -> return v
104 TermN t -> do
105 flatStructure <- traverseTerm flatten t
106 pool <- getPool
107 var <- liftIO . UF.fresh $ Descriptor {
108 structure = Just flatStructure,
109 rank = maxRank pool,
110 flex = Flexible,
111 name = Nothing,
112 copy = Nothing,
113 mark = noMark
114 }
115 register var
117makeInstance :: Variable -> StateT SolverState IO Variable
118makeInstance var = do
119 alreadyCopied <- uniqueMark
120 freshVar <- makeCopy alreadyCopied var
121 restore alreadyCopied var
122 return freshVar
124makeCopy :: Int -> Variable -> StateT SolverState IO Variable
125makeCopy alreadyCopied variable = do
126 desc <- liftIO $ UF.descriptor variable
127 if | mark desc == alreadyCopied ->
128 case copy desc of
129 Just v -> return v
130 Nothing -> error "This should be impossible."
132 | rank desc /= noRank || flex desc == Constant ->
133 return variable
135 | otherwise -> do
136 pool <- getPool
137 newVar <- liftIO $ UF.fresh $ Descriptor {
138 structure = Nothing,
139 rank = maxRank pool,
140 mark = noMark,
141 flex = case flex desc of
142 IsIn s -> IsIn s
143 _ -> Flexible,
144 copy = Nothing,
145 name = case flex desc of
146 Rigid -> Nothing
147 _ -> name desc
148 }
150 register newVar
152 -- Link the original variable to the new variable. This lets us
153 -- avoid making multiple copies of the variable we are instantiating.
154 --
155 -- Need to do this before recursively copying the structure of
156 -- the variable to avoid looping on cyclic terms.
157 liftIO $ UF.modifyDescriptor variable $ \desc ->
158 desc { mark = alreadyCopied, copy = Just newVar }
160 -- Now we recursively copy the structure of the variable.
161 -- We have already marked the variable as copied, so we
162 -- will not repeat this work or crawl this variable again.
163 case structure desc of
164 Nothing -> return newVar
165 Just term -> do
166 newTerm <- traverseTerm (makeCopy alreadyCopied) term
167 liftIO $ UF.modifyDescriptor newVar $ \desc ->
168 desc { structure = Just newTerm }
169 return newVar
171restore :: Int -> Variable -> StateT SolverState IO Variable
172restore alreadyCopied variable = do
173 desc <- liftIO $ UF.descriptor variable
174 if mark desc /= alreadyCopied
175 then return variable
176 else do
177 restoredStructure <-
178 Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
179 liftIO $ UF.modifyDescriptor variable $ \desc ->
180 desc { mark = noMark, rank = noRank, structure = restoredStructure }
181 return variable
183traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
184traverseTerm f term =
185 case term of
186 App1 a b -> App1 <$> f a <*> f b
187 Fun1 a b -> Fun1 <$> f a <*> f b
188 Var1 x -> Var1 <$> f x
189 EmptyRecord1 -> return EmptyRecord1
190 Record1 fields ext ->
191 Record1 <$> Traversable.traverse (mapM f) fields <*> f ext