88
88
skip(
89
89
self ,
90
90
minimums,
91
+ is_coinductive_goal,
91
92
initial_value,
92
93
solve_iteration,
93
94
reached_fixed_point,
98
99
& mut self ,
99
100
goal : & K ,
100
101
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 ,
102
104
solve_iteration : impl FnMut ( & mut Self , & K , & mut Minimums ) -> V ,
103
105
reached_fixed_point : impl Fn ( & V , & V ) -> bool ,
104
106
error_value : impl Fn ( ) -> V ,
@@ -136,7 +138,8 @@ where
136
138
} else {
137
139
// Otherwise, push the goal onto the stack and create a table.
138
140
// 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) ;
140
143
let depth = self . stack . push ( coinductive_goal) ;
141
144
let dfn = self . search_graph . insert ( & goal, depth, initial_solution) ;
142
145
@@ -264,9 +267,9 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
264
267
self . context . solve_goal (
265
268
& goal,
266
269
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 {
270
273
Ok ( Solution :: Unique ( Canonical {
271
274
value : ConstrainedSubst {
272
275
subst : goal. trivial_substitution ( interner) ,
@@ -276,8 +279,7 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
276
279
} ) )
277
280
} else {
278
281
Err ( NoSolution )
279
- } ;
280
- ( coinductive_goal, initial_solution)
282
+ }
281
283
} ,
282
284
|context, goal, minimums| Solver :: new ( context, program) . solve_iteration ( goal, minimums) ,
283
285
|old_answer, current_answer| {
0 commit comments