Skip to content

Commit 1c651e3

Browse files
committed
Move is_coinductive call to recursive
1 parent 37b95f4 commit 1c651e3

File tree

4 files changed

+6
-14
lines changed

4 files changed

+6
-14
lines changed

chalk-solve/src/recursive.rs

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ use self::stack::{Stack, StackDepth};
1010
use crate::clauses::program_clauses_for_goal;
1111
use crate::infer::{InferenceTable, ParameterEnaVariableExt};
1212
use crate::solve::truncate;
13-
use crate::RustIrDatabase;
13+
use crate::{coinductive_goal::IsCoinductive, RustIrDatabase};
1414
use chalk_ir::fold::Fold;
1515
use chalk_ir::interner::{HasInterner, Interner};
1616
use chalk_ir::visit::Visit;
@@ -516,7 +516,8 @@ impl<'me, I: Interner> RecursiveSolver<I> for Solver<'me, I> {
516516
} else {
517517
// Otherwise, push the goal onto the stack and create a table.
518518
// The initial result for this table is error.
519-
let depth = self.context.stack.push(self.program, &goal);
519+
let coinductive_goal = goal.is_coinductive(self.program);
520+
let depth = self.context.stack.push(coinductive_goal);
520521
let dfn = self.context.search_graph.insert(&goal, depth);
521522
let subgoal_minimums = self.solve_new_subgoal(goal, depth, dfn);
522523
self.context.search_graph[dfn].links = subgoal_minimums;

chalk-solve/src/recursive/fulfill.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
1-
use super::lib::{Guidance, Solution};
2-
use crate::recursive::Minimums;
1+
use super::lib::{Guidance, Minimums, Solution};
32
use chalk_ir::cast::Cast;
43
use chalk_ir::fold::Fold;
54
use chalk_ir::interner::{HasInterner, Interner};

chalk-solve/src/recursive/search_graph.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ use std::ops::Index;
33
use std::ops::IndexMut;
44
use std::usize;
55

6+
use super::lib::{Minimums, Solution, UCanonicalGoal};
67
use super::stack::StackDepth;
7-
use super::{Minimums, UCanonicalGoal, Solution};
88
use chalk_ir::debug;
99
use chalk_ir::{interner::Interner, ClausePriority, Fallible, NoSolution};
1010
use rustc_hash::FxHashMap;

chalk-solve/src/recursive/stack.rs

Lines changed: 1 addition & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,3 @@
1-
use super::UCanonicalGoal;
2-
use crate::{coinductive_goal::IsCoinductive, RustIrDatabase};
3-
use chalk_ir::interner::Interner;
41
use std::mem;
52
use std::ops::Index;
63
use std::ops::IndexMut;
@@ -42,11 +39,7 @@ impl Stack {
4239
self.entries.is_empty()
4340
}
4441

45-
pub(crate) fn push<I: Interner>(
46-
&mut self,
47-
program: &dyn RustIrDatabase<I>,
48-
goal: &UCanonicalGoal<I>,
49-
) -> StackDepth {
42+
pub(crate) fn push(&mut self, coinductive_goal: bool) -> StackDepth {
5043
let depth = StackDepth {
5144
depth: self.entries.len(),
5245
};
@@ -58,7 +51,6 @@ impl Stack {
5851
panic!("overflow depth reached")
5952
}
6053

61-
let coinductive_goal = goal.is_coinductive(program);
6254
self.entries.push(StackEntry {
6355
coinductive_goal,
6456
cycle: false,

0 commit comments

Comments
 (0)