8888 skip(
8989 self ,
9090 minimums,
91+ is_coinductive_goal,
9192 initial_value,
9293 solve_iteration,
9394 reached_fixed_point,
9899 & mut self ,
99100 goal : & K ,
100101 minimums : & mut Minimums ,
101- initial_value : impl Fn ( & K ) -> ( bool , V ) ,
102+ is_coinductive_goal : impl Fn ( & K ) -> bool ,
103+ initial_value : impl Fn ( & K , bool ) -> V ,
102104 solve_iteration : impl FnMut ( & mut Self , & K , & mut Minimums ) -> V ,
103105 reached_fixed_point : impl Fn ( & V , & V ) -> bool ,
104106 error_value : impl Fn ( ) -> V ,
@@ -136,7 +138,8 @@ where
136138 } else {
137139 // Otherwise, push the goal onto the stack and create a table.
138140 // The initial result for this table depends on whether the goal is coinductive.
139- let ( coinductive_goal, initial_solution) = initial_value ( goal) ;
141+ let coinductive_goal = is_coinductive_goal ( goal) ;
142+ let initial_solution = initial_value ( goal, coinductive_goal) ;
140143 let depth = self . stack . push ( coinductive_goal) ;
141144 let dfn = self . search_graph . insert ( & goal, depth, initial_solution) ;
142145
@@ -264,9 +267,9 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
264267 self . context . solve_goal (
265268 & goal,
266269 minimums,
267- |goal| {
268- let coinductive_goal = goal . is_coinductive ( program ) ;
269- let initial_solution = if coinductive_goal {
270+ |goal| goal . is_coinductive ( program ) ,
271+ |goal , coinductive_goal| {
272+ if coinductive_goal {
270273 Ok ( Solution :: Unique ( Canonical {
271274 value : ConstrainedSubst {
272275 subst : goal. trivial_substitution ( interner) ,
@@ -276,8 +279,7 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
276279 } ) )
277280 } else {
278281 Err ( NoSolution )
279- } ;
280- ( coinductive_goal, initial_solution)
282+ }
281283 } ,
282284 |context, goal, minimums| Solver :: new ( context, program) . solve_iteration ( goal, minimums) ,
283285 |old_answer, current_answer| {
0 commit comments