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
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.
22 inhabitants :: [Variable]
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,
38 sSavedEnv = Map.empty,
40 sMark = noMark + 1, -- The mark must never be equal to noMark!
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 }
50 err = makeError <$> extraPretty t1 <*> extraPretty t2
56 if line p1 == line p2 then "on line " ++ show (line p1)
57 else "between lines " ++ show (line p1) ++ " and " ++ show (line p2)
60 P.vcat [ P.text $ "Type error " ++ location
61 , if null message then empty else P.vcat . map P.text $ lines message
63 , P.text " Expected Type:" <+> pt1
64 , P.text " Actual Type:" <+> pt2 <> P.text "\n"
67switchToPool pool = modifyPool (\_ -> pool)
69getPool :: StateT SolverState IO Pool
70getPool = sPool <$> get
72getEnv :: StateT SolverState IO (Map.Map String Variable)
75saveLocalEnv :: StateT SolverState IO ()
78 modify $ \state -> state { sSavedEnv = env }
80uniqueMark :: StateT SolverState IO Int
83 let mark = sMark state
84 put $ state { sMark = mark + 1 }
87nextRankPool :: StateT SolverState IO Pool
90 return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
92register :: Variable -> StateT SolverState IO Variable
94 modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
97introduce :: Variable -> StateT SolverState IO Variable
98introduce variable = do
100 liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
103flatten :: Type -> StateT SolverState IO Variable
108 flatStructure <- traverseTerm flatten t
110 var <- liftIO . UF.fresh $ Descriptor {
111 structure = Just flatStructure,
120makeInstance :: Variable -> StateT SolverState IO Variable
122 alreadyCopied <- uniqueMark
123 freshVar <- makeCopy alreadyCopied var
124 restore alreadyCopied var
127makeCopy :: Int -> Variable -> StateT SolverState IO Variable
128makeCopy alreadyCopied variable = do
129 desc <- liftIO $ UF.descriptor variable
131 () | mark desc == alreadyCopied ->
134 Nothing -> error "This should be impossible."
136 | rank desc /= noRank || flex desc == Constant ->
141 newVar <- liftIO $ UF.fresh $ Descriptor {
145 flex = case flex desc of
149 name = case flex desc of
155 -- Link the original variable to the new variable. This lets us
156 -- avoid making multiple copies of the variable we are instantiating.
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
169 newTerm <- traverseTerm (makeCopy alreadyCopied) term
170 liftIO $ UF.modifyDescriptor newVar $ \desc ->
171 desc { structure = Just newTerm }
174restore :: Int -> Variable -> StateT SolverState IO Variable
175restore alreadyCopied variable = do
176 desc <- liftIO $ UF.descriptor variable
177 if mark desc /= alreadyCopied
181 Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
182 liftIO $ UF.modifyDescriptor variable $ \desc ->
183 desc { mark = noMark, rank = noRank, structure = restoredStructure }
186traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
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
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list