@@ -1,3 +1,4 @@
1+{-# LANGUAGE FlexibleContexts #-}
12module Type.State where
23
34import Control.Applicative ( (<$>), (<*>), Applicative, (<|>) )
@@ -21,29 +22,47 @@ data Pool = Pool
2122 , inhabitants :: [Variable]
2223 }
2324
24−emptyPool = Pool { maxRank = outermostRank, inhabitants = [] }
25+
26+emptyPool :: Pool
27+emptyPool =
28+ Pool
29+ { maxRank = outermostRank
30+ , inhabitants = []
31+ }
32+
2533
2634type Env = Map.Map String Variable
2735
36+
2837-- Keeps track of the environment, type variable pool, and a list of errors
29−data SolverState = SS {
30− sEnv :: Env,
31− sSavedEnv :: Env,
32− sPool :: Pool,
33− sMark :: Int,
34− sErrors :: [P.Doc]
35−}
36−
37−initialState = SS {
38− sEnv = Map.empty,
39− sSavedEnv = Map.empty,
40− sPool = emptyPool,
41− sMark = noMark + 1, -- The mark must never be equal to noMark!
42− sErrors = []
43−}
44−
45−modifyEnv f = modify $ \state -> state { sEnv = f (sEnv state) }
46−modifyPool f = modify $ \state -> state { sPool = f (sPool state) }
38+data SolverState = SS
39+ { sEnv :: Env
40+ , sSavedEnv :: Env
41+ , sPool :: Pool
42+ , sMark :: Int
43+ , sErrors :: [P.Doc]
44+ }
45+
46+
47+initialState :: SolverState
48+initialState =
49+ SS
50+ { sEnv = Map.empty
51+ , sSavedEnv = Map.empty
52+ , sPool = emptyPool
53+ , sMark = noMark + 1 -- The mark must never be equal to noMark!
54+ , sErrors = []
55+ }
56+
57+
58+modifyEnv :: (MonadState SolverState m) => (Env -> Env) -> m ()
59+modifyEnv f =
60+ modify $ \state -> state { sEnv = f (sEnv state) }
61+
62+
63+modifyPool :: (MonadState SolverState m) => (Pool -> Pool) -> m ()
64+modifyPool f =
65+ modify $ \state -> state { sPool = f (sPool state) }
4766
4867
4968addError
@@ -72,68 +91,84 @@ addError region hint t1 t2 =
7291 , P.nest 8 $ A.getRegionDocs region
7392 ]
7493
75−switchToPool pool = modifyPool (\_ -> pool)
94+
95+switchToPool :: (MonadState SolverState m) => Pool -> m ()
96+switchToPool pool =
97+ modifyPool (\_ -> pool)
98+
7699
77100getPool :: StateT SolverState IO Pool
78−getPool = sPool <$> get
101+getPool =
102+ gets sPool
103+
79104
80105getEnv :: StateT SolverState IO Env
81−getEnv = sEnv <$> get
106+getEnv =
107+ gets sEnv
108+
82109
83110saveLocalEnv :: StateT SolverState IO ()
84−saveLocalEnv = do
85− env <- sEnv <$> get
86− modify $ \state -> state { sSavedEnv = env }
111+saveLocalEnv =
112+ do env <- sEnv <$> get
113+ modify $ \state -> state { sSavedEnv = env }
114+
87115
88116uniqueMark :: StateT SolverState IO Int
89−uniqueMark = do
90− state <- get
91− let mark = sMark state
92− put $ state { sMark = mark + 1 }
93− return mark
117+uniqueMark =
118+ do state <- get
119+ let mark = sMark state
120+ put $ state { sMark = mark + 1 }
121+ return mark
122+
94123
95124nextRankPool :: StateT SolverState IO Pool
96−nextRankPool = do
97− pool <- getPool
98− return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
125+nextRankPool =
126+ do pool <- getPool
127+ return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
128+
99129
100130register :: Variable -> StateT SolverState IO Variable
101−register variable = do
102− modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
103− return variable
131+register variable =
132+ do modifyPool $ \pool -> pool { inhabitants = variable : inhabitants pool }
133+ return variable
134+
104135
105136introduce :: Variable -> StateT SolverState IO Variable
106−introduce variable = do
107− pool <- getPool
108− liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
109− register variable
137+introduce variable =
138+ do pool <- getPool
139+ liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
140+ register variable
141+
110142
111143flatten :: Type -> StateT SolverState IO Variable
112144flatten term =
113145 case term of
114− VarN maybeAlias v -> do
115− liftIO $ UF.modifyDescriptor v $ \desc -> desc { alias = maybeAlias <|> alias desc }
116− return v
117− TermN maybeAlias t -> do
118− flatStructure <- traverseTerm flatten t
119− pool <- getPool
120− var <- liftIO . UF.fresh $ Descriptor
121− { structure = Just flatStructure
122− , rank = maxRank pool
123− , flex = Flexible
124− , name = Nothing
125− , copy = Nothing
126− , mark = noMark
127− , alias = maybeAlias
128− }
129− register var
146+ VarN maybeAlias v ->
147+ do liftIO $ UF.modifyDescriptor v $ \desc -> desc { alias = maybeAlias <|> alias desc }
148+ return v
149+
150+ TermN maybeAlias t ->
151+ do flatStructure <- traverseTerm flatten t
152+ pool <- getPool
153+ var <- liftIO . UF.fresh $ Descriptor
154+ { structure = Just flatStructure
155+ , rank = maxRank pool
156+ , flex = Flexible
157+ , name = Nothing
158+ , copy = Nothing
159+ , mark = noMark
160+ , alias = maybeAlias
161+ }
162+ register var
163+
130164
131165makeInstance :: Variable -> StateT SolverState IO Variable
132−makeInstance var = do
133− alreadyCopied <- uniqueMark
134− freshVar <- makeCopy alreadyCopied var
135− restore alreadyCopied var
136− return freshVar
166+makeInstance var =
167+ do alreadyCopied <- uniqueMark
168+ freshVar <- makeCopy alreadyCopied var
169+ restore alreadyCopied var
170+ return freshVar
171+
137172
138173makeCopy :: Int -> Variable -> StateT SolverState IO Variable
139174makeCopy alreadyCopied variable = do
@@ -184,17 +219,19 @@ makeCopy alreadyCopied variable = do
184219 desc { structure = Just newTerm }
185220 return newVar
186221
222+
187223restore :: Int -> Variable -> StateT SolverState IO Variable
188−restore alreadyCopied variable = do
189− desc <- liftIO $ UF.descriptor variable
190− if mark desc /= alreadyCopied
191− then return variable
192− else do
193− restoredStructure <-
194− Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
195− liftIO $ UF.modifyDescriptor variable $ \desc ->
196− desc { mark = noMark, rank = noRank, structure = restoredStructure }
197− return variable
224+restore alreadyCopied variable =
225+ do desc <- liftIO $ UF.descriptor variable
226+ case mark desc /= alreadyCopied of
227+ True -> return variable
228+ False ->
229+ do restoredStructure <-
230+ Traversable.traverse (traverseTerm (restore alreadyCopied)) (structure desc)
231+ liftIO $ UF.modifyDescriptor variable $ \desc ->
232+ desc { mark = noMark, rank = noRank, structure = restoredStructure }
233+ return variable
234+
198235
199236traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
200237traverseTerm f term =