diff --git a/chalk-engine/src/forest.rs b/chalk-engine/src/forest.rs index 493d2ac569a..907ee632324 100644 --- a/chalk-engine/src/forest.rs +++ b/chalk-engine/src/forest.rs @@ -77,6 +77,7 @@ impl<C: Context> Forest<C> { &'f mut self, context: &'f impl ContextOps<C>, goal: &C::UCanonicalGoalInEnvironment, + fuel: Option<usize>, ) -> impl AnswerStream<C> + 'f { let table = self.get_or_create_table_for_ucanonical_goal(context, goal.clone()); let answer = AnswerIndex::ZERO; @@ -85,6 +86,7 @@ impl<C: Context> Forest<C> { context, table, answer, + fuel, } } @@ -95,8 +97,9 @@ impl<C: Context> Forest<C> { &mut self, context: &impl ContextOps<C>, goal: &C::UCanonicalGoalInEnvironment, + fuel: Option<usize>, ) -> Option<C::Solution> { - context.make_solution(C::canonical(&goal), self.iter_answers(context, goal)) + context.make_solution(C::canonical(&goal), self.iter_answers(context, goal, fuel)) } /// True if all the tables on the stack starting from `depth` and @@ -148,6 +151,7 @@ struct ForestSolver<'me, C: Context + 'me, CO: ContextOps<C> + 'me> { context: &'me CO, table: TableIndex, answer: AnswerIndex, + fuel: Option<usize>, } impl<'me, C, CO> AnswerStream<C> for ForestSolver<'me, C, CO> @@ -157,6 +161,13 @@ where { fn peek_answer(&mut self) -> Option<SimplifiedAnswer<C>> { loop { + if let Some(fuel) = &mut self.fuel { + if *fuel == 0 { + // TODO: would it be better to return an ambiguous answer? + return None; + } + *fuel -= 1; + } match self .forest .ensure_root_answer(self.context, self.table, self.answer) diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index 901181bf7d2..411a4e06234 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -113,19 +113,47 @@ impl Solver { /// each time you invoke `solve`, as otherwise the cached data may be /// invalid. /// - `goal` the goal to solve + /// - `fuel` if `Some`, this limits how much time the solver spends before giving up. /// /// # Returns /// /// - `None` is the goal cannot be proven. /// - `Some(solution)` if we succeeded in finding *some* answers, /// although `solution` may reflect ambiguity and unknowns. - pub fn solve( + pub fn solve_with_fuel( &mut self, program: &dyn RustIrDatabase, goal: &UCanonical<InEnvironment<Goal>>, + fuel: Option<usize>, ) -> Option<Solution> { let ops = self.forest.context().ops(program); - self.forest.solve(&ops, goal) + self.forest.solve(&ops, goal, fuel) + } + + /// Attempts to solve the given goal, which must be in canonical + /// form. Returns a unique solution (if one exists). This will do + /// only as much work towards `goal` as it has to (and that work + /// is cached for future attempts). + /// + /// # Parameters + /// + /// - `program` -- defines the program clauses in scope. + /// - **Important:** You must supply the same set of program clauses + /// each time you invoke `solve`, as otherwise the cached data may be + /// invalid. + /// - `goal` the goal to solve + /// + /// # Returns + /// + /// - `None` is the goal cannot be proven. + /// - `Some(solution)` if we succeeded in finding *some* answers, + /// although `solution` may reflect ambiguity and unknowns. + pub fn solve( + &mut self, + program: &dyn RustIrDatabase, + goal: &UCanonical<InEnvironment<Goal>>, + ) -> Option<Solution> { + self.solve_with_fuel(program, goal, None) } pub fn into_test(self) -> TestSolver {