@@ -16,180 +16,186 @@ import qualified AST.Annotation as A
1616-- | Every variable has rank less than or equal to the maxRank of the pool.
1717-- This sorts variables into the young and old pools accordingly.
1818generalize :: TS.Pool -> StateT TS.SolverState IO ()
19−generalize youngPool = do
20− youngMark <- TS.uniqueMark
21− let youngRank = TS.maxRank youngPool
22− insert dict var = do
23− descriptor <- liftIO $ UF.descriptor var
24− liftIO $ UF.modifyDescriptor var (\desc -> desc { mark = youngMark })
25− return $ Map.insertWith (++) (rank descriptor) [var] dict
26−
27− -- Sort the youngPool variables by rank.
28− rankDict <- foldM insert Map.empty (TS.inhabitants youngPool)
29−
30− -- get the ranks right for each entry.
31− -- start at low ranks so that we only have to pass
32− -- over the information once.
33− visitedMark <- TS.uniqueMark
34− forM (Map.toList rankDict) $ \(poolRank, vars) ->
35− mapM (adjustRank youngMark visitedMark poolRank) vars
36−
37− -- For variables that have rank lowerer than youngRank, register them in
38− -- the old pool if they are not redundant.
39− let registerIfNotRedundant var = do
40− isRedundant <- liftIO $ UF.redundant var
41− if isRedundant then return var else TS.register var
42−
43− let rankDict' = Map.delete youngRank rankDict
44− Traversable.traverse (mapM registerIfNotRedundant) rankDict'
45−
46− -- For variables with rank youngRank
47− -- If rank < youngRank: register in oldPool
48− -- otherwise generalize
49− let registerIfLowerRank var = do
50− isRedundant <- liftIO $ UF.redundant var
51− case isRedundant of
52− True -> return ()
53− False -> do
54− desc <- liftIO $ UF.descriptor var
55− case rank desc < youngRank of
56− True -> TS.register var >> return ()
19+generalize youngPool =
20+ do youngMark <- TS.uniqueMark
21+ let youngRank = TS.maxRank youngPool
22+ insert dict var = do
23+ descriptor <- liftIO $ UF.descriptor var
24+ liftIO $ UF.modifyDescriptor var (\desc -> desc { mark = youngMark })
25+ return $ Map.insertWith (++) (rank descriptor) [var] dict
26+
27+ -- Sort the youngPool variables by rank.
28+ rankDict <- foldM insert Map.empty (TS.inhabitants youngPool)
29+
30+ -- get the ranks right for each entry.
31+ -- start at low ranks so that we only have to pass
32+ -- over the information once.
33+ visitedMark <- TS.uniqueMark
34+ forM (Map.toList rankDict) $ \(poolRank, vars) ->
35+ mapM (adjustRank youngMark visitedMark poolRank) vars
36+
37+ -- For variables that have rank lowerer than youngRank, register them in
38+ -- the old pool if they are not redundant.
39+ let registerIfNotRedundant var = do
40+ isRedundant <- liftIO $ UF.redundant var
41+ if isRedundant then return var else TS.register var
42+
43+ let rankDict' = Map.delete youngRank rankDict
44+ Traversable.traverse (mapM registerIfNotRedundant) rankDict'
45+
46+ -- For variables with rank youngRank
47+ -- If rank < youngRank: register in oldPool
48+ -- otherwise generalize
49+ let registerIfLowerRank var = do
50+ isRedundant <- liftIO $ UF.redundant var
51+ case isRedundant of
52+ True -> return ()
5753 False -> do
58− let flex' = case flex desc of { Flexible -> Rigid ; other -> other }
59− liftIO $ UF.setDescriptor var (desc { rank = noRank, flex = flex' })
60−
61− mapM_ registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
54+ desc <- liftIO $ UF.descriptor var
55+ case rank desc < youngRank of
56+ True -> TS.register var >> return ()
57+ False -> do
58+ let flex' = case flex desc of { Flexible -> Rigid ; other -> other }
59+ liftIO $ UF.setDescriptor var (desc { rank = noRank, flex = flex' })
60+
61+ mapM_ registerIfLowerRank (Map.findWithDefault [] youngRank rankDict)
6262
6363
6464-- adjust the ranks of variables such that ranks never increase as you
6565-- move deeper into a variable.
6666adjustRank :: Int -> Int -> Int -> Variable -> StateT TS.SolverState IO Int
6767adjustRank youngMark visitedMark groupRank var =
68− do descriptor <- liftIO $ UF.descriptor var
69− case () of
70− () | mark descriptor == youngMark ->
71− do -- Set the variable as marked first because it may be cyclic.
72− liftIO $ UF.modifyDescriptor var $ \desc ->
73− desc { mark = visitedMark }
74− rank' <- maybe (return groupRank) adjustTerm (structure descriptor)
75− liftIO $ UF.modifyDescriptor var $ \desc ->
76− desc { rank = rank' }
77− return rank'
68+ do descriptor <- liftIO $ UF.descriptor var
69+ case () of
70+ () | mark descriptor == youngMark ->
71+ do -- Set the variable as marked first because it may be cyclic.
72+ liftIO $ UF.modifyDescriptor var $ \desc ->
73+ desc { mark = visitedMark }
74+ rank' <- maybe (return groupRank) adjustTerm (structure descriptor)
75+ liftIO $ UF.modifyDescriptor var $ \desc ->
76+ desc { rank = rank' }
77+ return rank'
7878
7979 | mark descriptor /= visitedMark ->
80− do let rank' = min groupRank (rank descriptor)
81− liftIO $ UF.setDescriptor var (descriptor { mark = visitedMark, rank = rank' })
82− return rank'
83−
84− | otherwise -> return (rank descriptor)
85−
86− where
87− adjust = adjustRank youngMark visitedMark groupRank
88−
89− adjustTerm term =
90− case term of
91− App1 a b -> max `liftM` adjust a `ap` adjust b
92− Fun1 a b -> max `liftM` adjust a `ap` adjust b
93− Var1 x -> adjust x
94− EmptyRecord1 -> return outermostRank
95− Record1 fields extension ->
96− do ranks <- mapM adjust (concat (Map.elems fields))
97− rnk <- adjust extension
98− return . maximum $ rnk : ranks
80+ do let rank' = min groupRank (rank descriptor)
81+ liftIO $ UF.setDescriptor var (descriptor { mark = visitedMark, rank = rank' })
82+ return rank'
83+
84+ | otherwise ->
85+ return (rank descriptor)
86+ where
87+ adjust = adjustRank youngMark visitedMark groupRank
88+
89+ adjustTerm term =
90+ case term of
91+ App1 a b -> max `liftM` adjust a `ap` adjust b
92+ Fun1 a b -> max `liftM` adjust a `ap` adjust b
93+ Var1 x -> adjust x
94+ EmptyRecord1 -> return outermostRank
95+ Record1 fields extension ->
96+ do ranks <- mapM adjust (concat (Map.elems fields))
97+ rnk <- adjust extension
98+ return . maximum $ rnk : ranks
9999
100100
101101solve :: TypeConstraint -> StateT TS.SolverState IO ()
102102solve (A.A region constraint) =
103103 case constraint of
104− CTrue -> return ()
105−
106− CSaveEnv -> TS.saveLocalEnv
107−
108− CEqual term1 term2 -> do
109− t1 <- TS.flatten term1
110− t2 <- TS.flatten term2
111− unify region t1 t2
112−
113− CAnd cs -> mapM_ solve cs
114−
115− CLet [Scheme [] fqs constraint' _] (A.A _ CTrue) -> do
116− oldEnv <- TS.getEnv
117− mapM TS.introduce fqs
118− solve constraint'
119− TS.modifyEnv (\_ -> oldEnv)
120−
121− CLet schemes constraint' -> do
122− oldEnv <- TS.getEnv
123− headers <- Map.unions `fmap` mapM (solveScheme region) schemes
124− TS.modifyEnv $ \env -> Map.union headers env
125− solve constraint'
126− mapM Check.occurs $ Map.toList headers
127− TS.modifyEnv (\_ -> oldEnv)
128−
129− CInstance name term -> do
130− env <- TS.getEnv
131− freshCopy <-
132− case Map.lookup name env of
133− Just tipe -> TS.makeInstance tipe
134− Nothing
135− | List.isPrefixOf "Native." name -> liftIO (variable Flexible)
136− | otherwise ->
137− error ("Could not find '" ++ name ++ "' when solving type constraints.")
138−
139− t <- TS.flatten term
140− unify region freshCopy t
104+ CTrue ->
105+ return ()
106+
107+ CSaveEnv ->
108+ TS.saveLocalEnv
109+
110+ CEqual term1 term2 ->
111+ do t1 <- TS.flatten term1
112+ t2 <- TS.flatten term2
113+ unify region t1 t2
114+
115+ CAnd cs ->
116+ mapM_ solve cs
117+
118+ CLet [Scheme [] fqs constraint' _] (A.A _ CTrue) ->
119+ do oldEnv <- TS.getEnv
120+ mapM TS.introduce fqs
121+ solve constraint'
122+ TS.modifyEnv (\_ -> oldEnv)
123+
124+ CLet schemes constraint' ->
125+ do oldEnv <- TS.getEnv
126+ headers <- Map.unions `fmap` mapM (solveScheme region) schemes
127+ TS.modifyEnv $ \env -> Map.union headers env
128+ solve constraint'
129+ mapM Check.occurs $ Map.toList headers
130+ TS.modifyEnv (\_ -> oldEnv)
131+
132+ CInstance name term ->
133+ do env <- TS.getEnv
134+ freshCopy <-
135+ case Map.lookup name env of
136+ Just tipe -> TS.makeInstance tipe
137+ Nothing
138+ | List.isPrefixOf "Native." name -> liftIO (variable Flexible)
139+ | otherwise ->
140+ error ("Could not find '" ++ name ++ "' when solving type constraints.")
141+
142+ t <- TS.flatten term
143+ unify region freshCopy t
144+
141145
142146solveScheme :: A.Region -> TypeScheme -> StateT TS.SolverState IO (Map.Map String Variable)
143147solveScheme region scheme =
144148 case scheme of
145− Scheme [] [] constraint header -> do
146− solve constraint
147− Traversable.traverse TS.flatten header
149+ Scheme [] [] constraint header ->
150+ do solve constraint
151+ Traversable.traverse TS.flatten header
148152
149− Scheme rigidQuantifiers flexibleQuantifiers constraint header -> do
150− let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
151− oldPool <- TS.getPool
153+ Scheme rigidQuantifiers flexibleQuantifiers constraint header ->
154+ do let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
155+ oldPool <- TS.getPool
152156
153− -- fill in a new pool when working on this scheme's constraints
154− freshPool <- TS.nextRankPool
155− TS.switchToPool freshPool
156− mapM TS.introduce quantifiers
157− header' <- Traversable.traverse TS.flatten header
158− solve constraint
157+ -- fill in a new pool when working on this scheme's constraints
158+ freshPool <- TS.nextRankPool
159+ TS.switchToPool freshPool
160+ mapM TS.introduce quantifiers
161+ header' <- Traversable.traverse TS.flatten header
162+ solve constraint
159163
160− allDistinct region rigidQuantifiers
161− youngPool <- TS.getPool
162− TS.switchToPool oldPool
163− generalize youngPool
164− mapM (isGeneric region) rigidQuantifiers
165− return header'
164+ allDistinct region rigidQuantifiers
165+ youngPool <- TS.getPool
166+ TS.switchToPool oldPool
167+ generalize youngPool
168+ mapM (isGeneric region) rigidQuantifiers
169+ return header'
166170
167171
168172-- Checks that all of the given variables belong to distinct equivalence classes.
169173-- Also checks that their structure is Nothing, so they represent a variable, not
170174-- a more complex term.
171175allDistinct :: A.Region -> [Variable] -> StateT TS.SolverState IO ()
172−allDistinct region vars = do
173− seen <- TS.uniqueMark
174− let check var = do
175− desc <- liftIO $ UF.descriptor var
176− case structure desc of
177− Just _ -> TS.addError region (Just msg) var var
178− where msg = "Cannot generalize something that is not a type variable."
179−
180− Nothing -> do
181− if mark desc == seen
182− then let msg = "Duplicate variable during generalization."
183− in TS.addError region (Just msg) var var
184− else return ()
185− liftIO $ UF.setDescriptor var (desc { mark = seen })
186− mapM_ check vars
176+allDistinct region vars =
177+ do seen <- TS.uniqueMark
178+ let check var = do
179+ desc <- liftIO $ UF.descriptor var
180+ case structure desc of
181+ Just _ -> TS.addError region (Just msg) var var
182+ where msg = "Cannot generalize something that is not a type variable."
183+
184+ Nothing -> do
185+ if mark desc == seen
186+ then let msg = "Duplicate variable during generalization."
187+ in TS.addError region (Just msg) var var
188+ else return ()
189+ liftIO $ UF.setDescriptor var (desc { mark = seen })
190+ mapM_ check vars
191+
187192
188193-- Check that a variable has rank == noRank, meaning that it can be generalized.
189194isGeneric :: A.Region -> Variable -> StateT TS.SolverState IO ()
190−isGeneric region var = do
191− desc <- liftIO $ UF.descriptor var
192− if rank desc == noRank
193− then return ()
194− else let msg = "Unable to generalize a type variable. It is not unranked."
195− in TS.addError region (Just msg) var var
195+isGeneric region var =
196+ do desc <- liftIO $ UF.descriptor var
197+ if rank desc == noRank
198+ then return ()
199+ else
200+ let msg = "Unable to generalize a type variable. It is not unranked."
201+ in TS.addError region (Just msg) var var