on master help sign in
avoid adding the same constraint to the queue
baad761Ozgur Akgun
src/Idris/Core/Constraints.hs+10−8
@@ -154,7 +154,7 @@ solve maxUniverseLevel inpConstraints =
154 : "Involved constraints: "
154 : "Involved constraints: "
155 : map (("\t"++) . show) (suspect : S.toList suspects)
155 : map (("\t"++) . show) (suspect : S.toList suspects)
156 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
156 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
157− addToQueueRHS (Var var)
157+ addToQueueRHS (fst suspect) (Var var)
158 updateUpperBoundOf _ UVal{} _ = return ()
158 updateUpperBoundOf _ UVal{} _ = return ()
159
159
160 updateLowerBoundOf :: (UConstraint, FC) -> UExp -> Int -> StateT SolverState TC ()
160 updateLowerBoundOf :: (UConstraint, FC) -> UExp -> Int -> StateT SolverState TC ()
@@ -170,30 +170,32 @@ solve maxUniverseLevel inpConstraints =
170 : "Involved constraints: "
170 : "Involved constraints: "
171 : map (("\t"++) . show) (suspect : S.toList suspects)
171 : map (("\t"++) . show) (suspect : S.toList suspects)
172 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
172 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
173− addToQueueLHS (Var var)
173+ addToQueueLHS (fst suspect) (Var var)
174 updateLowerBoundOf _ UVal{} _ = return ()
174 updateLowerBoundOf _ UVal{} _ = return ()
175
175
176 -- | add all constraints (with the given var on the lhs) to the queue
176 -- | add all constraints (with the given var on the lhs) to the queue
177− addToQueueLHS :: MonadState SolverState m => Var -> m ()
177+ addToQueueLHS :: MonadState SolverState m => UConstraint -> Var -> m ()
178− addToQueueLHS var =
178+ addToQueueLHS thisCons var =
179 case M.lookup var constraintsLHS of
179 case M.lookup var constraintsLHS of
180 Nothing -> return ()
180 Nothing -> return ()
181 Just cs -> do
181 Just cs -> do
182 Queue list set <- gets queue
182 Queue list set <- gets queue
183+ let set' = S.insert thisCons set
183− let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set ]
184+ let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set' ]
184 if null newCons
185 if null newCons
185 then return ()
186 then return ()
186 else modify $ \ st -> st { queue = Queue (list ++ newCons)
187 else modify $ \ st -> st { queue = Queue (list ++ newCons)
187 (S.union set (S.fromList (map fst newCons))) }
188 (S.union set (S.fromList (map fst newCons))) }
188
189
189 -- | add all constraints (with the given var on the rhs) to the queue
190 -- | add all constraints (with the given var on the rhs) to the queue
190− addToQueueRHS :: MonadState SolverState m => Var -> m ()
191+ addToQueueRHS :: MonadState SolverState m => UConstraint -> Var -> m ()
191− addToQueueRHS var =
192+ addToQueueRHS thisCons var =
192 case M.lookup var constraintsRHS of
193 case M.lookup var constraintsRHS of
193 Nothing -> return ()
194 Nothing -> return ()
194 Just cs -> do
195 Just cs -> do
195 Queue list set <- gets queue
196 Queue list set <- gets queue
197+ let set' = S.insert thisCons set
196− let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set ]
198+ let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set' ]
197 if null newCons
199 if null newCons
198 then return ()
200 then return ()
199 else modify $ \ st -> st { queue = Queue (list ++ newCons)
201 else modify $ \ st -> st { queue = Queue (list ++ newCons)