diff --git a/chalk-solve/src/recursive.rs b/chalk-solve/src/recursive.rs index e26bb74bf63..8659751062f 100644 --- a/chalk-solve/src/recursive.rs +++ b/chalk-solve/src/recursive.rs @@ -16,10 +16,37 @@ use rustc_hash::FxHashMap; type UCanonicalGoal = UCanonical>>; +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Answer { + pub solution: Solution, + pub delayed_goals: Vec>, +} + +impl Answer { + pub fn new(solution: Solution, delayed_goals: Vec>) -> Self { + Self { + solution, + delayed_goals, + } + } + + pub fn needs_refinement(&self) -> bool { + !self.delayed_goals.is_empty() + } + + pub fn combine(self, other: Answer, interner: &I) -> Self { + let mut goals = vec![]; + let combined_solution = self.solution.combine(other.solution, interner); + goals.extend(self.delayed_goals); + goals.extend(other.delayed_goals); + Answer::new(combined_solution, goals) + } +} + pub(crate) struct RecursiveContext { stack: Stack, search_graph: SearchGraph, - cache: FxHashMap, Fallible>>, + cache: FxHashMap, Fallible>>, caching_enabled: bool, } @@ -105,7 +132,35 @@ impl<'me, I: Interner> Solver<'me, I> { debug!("solve_root_goal(canonical_goal={:?})", canonical_goal); assert!(self.context.stack.is_empty()); let minimums = &mut Minimums::new(); - self.solve_goal(canonical_goal.clone(), minimums) + self.solve_goal(canonical_goal.clone(), minimums).map(|a| { + assert!(a.delayed_goals.is_empty()); // at this point there should be no delayed goals + a.solution + }) + } + + fn refine_answer( + &mut self, + goal: UCanonicalGoal, + answer: Answer, + minimums: &mut Minimums, + ) -> Fallible> { + debug_heading!("refine_answer(goal = {:?}, answer = {:?})", goal, answer); + let mut cur_solution = answer.solution.clone(); + let mut delayed_goals = vec![]; + + for subgoal in answer.delayed_goals { + if goal == subgoal { + debug!("encountered trivial cycle"); + } else { + debug!("solving delayed goal(subgoal={:?})", subgoal); + let answer = self.solve_goal(subgoal, minimums)?; + cur_solution = cur_solution.combine(answer.solution, self.program.interner()); + delayed_goals.extend(answer.delayed_goals); + } + } + let refined_answer = Answer::new(cur_solution, delayed_goals); + debug!("refined_answer={:?}", refined_answer); + Ok(refined_answer) } /// Attempt to solve a goal that has been fully broken down into leaf form @@ -115,13 +170,19 @@ impl<'me, I: Interner> Solver<'me, I> { &mut self, goal: UCanonicalGoal, minimums: &mut Minimums, - ) -> Fallible> { + ) -> Fallible> { info_heading!("solve_goal({:?})", goal); // First check the cache. if let Some(value) = self.context.cache.get(&goal) { debug!("solve_reduced_goal: cache hit, value={:?}", value); - return value.clone(); + return value.clone().and_then(|a| { + if a.needs_refinement() { + self.refine_answer(goal.clone(), a, minimums) + } else { + Ok(a) + } + }); } // Next, check if the goal is in the search tree already. @@ -138,11 +199,15 @@ impl<'me, I: Interner> Solver<'me, I> { subst: goal.trivial_substitution(self.program.interner()), constraints: vec![], }; + debug!("applying coinductive semantics"); - return Ok(Solution::Unique(Canonical { - value, - binders: goal.canonical.binders, - })); + return Ok(Answer::new( + Solution::Unique(Canonical { + value, + binders: goal.clone().canonical.binders, + }), + vec![goal], + )); } self.context.stack[depth].flag_cycle(); @@ -163,7 +228,7 @@ impl<'me, I: Interner> Solver<'me, I> { // The initial result for this table is error. let depth = self.context.stack.push(self.program, &goal); let dfn = self.context.search_graph.insert(&goal, depth); - let subgoal_minimums = self.solve_new_subgoal(goal, depth, dfn); + let subgoal_minimums = self.solve_new_subgoal(goal.clone(), depth, dfn); self.context.search_graph[dfn].links = subgoal_minimums; self.context.search_graph[dfn].stack_depth = None; self.context.stack.pop(depth); @@ -191,7 +256,21 @@ impl<'me, I: Interner> Solver<'me, I> { } } - info!("solve_goal: solution = {:?} prio {:?}", result, priority); + info!( + "solve_goal: goal ={:?} solution_unrefined ={:?} prio ={:?}", + goal, result, priority + ); + let result = result.and_then(|a| { + if a.needs_refinement() { + self.refine_answer(goal.clone(), a, minimums) + } else { + Ok(a) + } + }); + info!( + "solve_goal: goal={:?} solution_refined={:?} prio={:?}", + goal, result, priority + ); result } } @@ -258,9 +337,10 @@ impl<'me, I: Interner> Solver<'me, I> { Ok(clauses) => { self.solve_from_clauses(&canonical_goal, clauses, minimums) } - Err(Floundered) => { - (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High) - } + Err(Floundered) => ( + Ok(Answer::new(Solution::Ambig(Guidance::Unknown), vec![])), + ClausePriority::High, + ), } }; debug!("prog_solution={:?}", prog_solution); @@ -314,7 +394,7 @@ impl<'me, I: Interner> Solver<'me, I> { } let current_answer_is_ambig = match ¤t_answer { - Ok(s) => s.is_ambig(), + Ok(s) => s.solution.is_ambig(), Err(_) => false, }; @@ -337,7 +417,7 @@ impl<'me, I: Interner> Solver<'me, I> { &mut self, canonical_goal: &UCanonicalGoal, minimums: &mut Minimums, - ) -> (Fallible>, ClausePriority) { + ) -> (Fallible>, ClausePriority) { debug_heading!("solve_via_simplification({:?})", canonical_goal); let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal); if let Err(e) = fulfill.push_goal(&goal.environment, goal.goal) { @@ -354,7 +434,7 @@ impl<'me, I: Interner> Solver<'me, I> { canonical_goal: &UCanonical>>, clauses: C, minimums: &mut Minimums, - ) -> (Fallible>, ClausePriority) + ) -> (Fallible>, ClausePriority) where C: IntoIterator>, { @@ -363,8 +443,18 @@ impl<'me, I: Interner> Solver<'me, I> { debug_heading!("clause={:?}", program_clause); // If we have a completely ambiguous answer, it's not going to get better, so stop - if cur_solution == Some((Solution::Ambig(Guidance::Unknown), ClausePriority::High)) { - return (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High); + if let Some(( + Answer { + solution: Solution::Ambig(Guidance::Unknown), + .. + }, + ClausePriority::High, + )) = cur_solution + { + return ( + Ok(Answer::new(Solution::Ambig(Guidance::Unknown), vec![])), + ClausePriority::High, + ); } match program_clause.data(self.program.interner()) { @@ -424,7 +514,7 @@ impl<'me, I: Interner> Solver<'me, I> { canonical_goal: &UCanonical>>, clause: &Binders>, minimums: &mut Minimums, - ) -> (Fallible>, ClausePriority) { + ) -> (Fallible>, ClausePriority) { info_heading!( "solve_via_implication(\ \n canonical_goal={:?},\ @@ -485,11 +575,11 @@ fn calculate_inputs( fn combine_with_priorities_for_goal( interner: &I, goal: &Goal, - a: Fallible>, + a: Fallible>, prio_a: ClausePriority, - b: Fallible>, + b: Fallible>, prio_b: ClausePriority, -) -> (Fallible>, ClausePriority) { +) -> (Fallible>, ClausePriority) { let domain_goal = match goal.data(interner) { GoalData::DomainGoal(domain_goal) => domain_goal, _ => { @@ -512,11 +602,11 @@ fn combine_with_priorities_for_goal( fn combine_with_priorities( interner: &I, domain_goal: &DomainGoal, - a: Solution, + a: Answer, prio_a: ClausePriority, - b: Solution, + b: Answer, prio_b: ClausePriority, -) -> (Solution, ClausePriority) { +) -> (Answer, ClausePriority) { match (prio_a, prio_b, a, b) { (ClausePriority::High, ClausePriority::Low, higher, lower) | (ClausePriority::Low, ClausePriority::High, lower, higher) => { @@ -526,8 +616,8 @@ fn combine_with_priorities( // solution overriding a general low-priority one. Currently inputs // only matter for projections; in a goal like `AliasEq(::Type = ?1)`, ?0 is the input. - let inputs_higher = calculate_inputs(interner, domain_goal, &higher); - let inputs_lower = calculate_inputs(interner, domain_goal, &lower); + let inputs_higher = calculate_inputs(interner, domain_goal, &higher.solution); + let inputs_lower = calculate_inputs(interner, domain_goal, &lower.solution); if inputs_higher == inputs_lower { debug!( "preferring solution: {:?} over {:?} because of higher prio", diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index 69696e53494..3225e4d4f53 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -15,20 +15,11 @@ use rustc_hash::FxHashSet; use std::fmt::Debug; use zip::Zip; -enum Outcome { - Complete, +enum Outcome { + Complete(Vec>), Incomplete, } -impl Outcome { - fn is_complete(&self) -> bool { - match *self { - Outcome::Complete => true, - _ => false, - } - } -} - /// A goal that must be resolved #[derive(Clone, Debug, PartialEq, Eq)] enum Obligation { @@ -48,7 +39,7 @@ enum Obligation { struct PositiveSolution { free_vars: Vec>, universes: UniverseMap, - solution: Solution, + answer: Answer, } /// When refuting a goal, there's no impact on inference state. @@ -239,7 +230,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { Ok(PositiveSolution { free_vars, universes, - solution: result?, + answer: result?, }) } @@ -265,7 +256,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { .u_canonicalize(self.solver.program.interner(), &canonicalized); let mut minimums = Minimums::new(); // FIXME -- minimums here seems wrong if let Ok(solution) = self.solver.solve_goal(quantified, &mut minimums) { - if solution.is_unique() { + if solution.solution.is_unique() { Err(NoSolution) } else { Ok(NegativeSolution::Ambiguous) @@ -318,7 +309,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { } } - fn fulfill(&mut self, minimums: &mut Minimums) -> Fallible { + fn fulfill(&mut self, minimums: &mut Minimums) -> Fallible> { debug_heading!("fulfill(obligations={:#?})", self.obligations); // Try to solve all the obligations. We do this via a fixed-point @@ -327,6 +318,8 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { // `obligations` array. This process is repeated so long as we are // learning new things about our inference state. let mut obligations = Vec::with_capacity(self.obligations.len()); + let mut delayed_goals = Vec::new(); + let mut progress = true; while progress { @@ -346,17 +339,17 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { let PositiveSolution { free_vars, universes, - solution, + answer, } = self.prove(wc, minimums)?; - if solution.has_definite() { - if let Some(constrained_subst) = solution.constrained_subst() { + if answer.solution.has_definite() { + if let Some(constrained_subst) = answer.solution.constrained_subst() { self.apply_solution(free_vars, universes, constrained_subst); progress = true; } } - - solution.is_ambig() + delayed_goals.extend(answer.delayed_goals); + answer.solution.is_ambig() } Obligation::Refute(ref goal) => { let answer = self.refute(goal)?; @@ -380,7 +373,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { assert!(obligations.is_empty()); if self.obligations.is_empty() { - Ok(Outcome::Complete) + Ok(Outcome::Complete(delayed_goals)) } else { Ok(Outcome::Incomplete) } @@ -393,17 +386,17 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { mut self, subst: Substitution, minimums: &mut Minimums, - ) -> Fallible> { + ) -> Fallible> { let outcome = match self.fulfill(minimums) { Ok(o) => o, Err(e) => return Err(e), }; if self.cannot_prove { - return Ok(Solution::Ambig(Guidance::Unknown)); + return Ok(Answer::new(Solution::Ambig(Guidance::Unknown), vec![])); } - if outcome.is_complete() { + if let Outcome::Complete(delayed_goals) = outcome { // No obligations remain, so we have definitively solved our goals, // and the current inference state is the unique way to solve them. @@ -412,7 +405,10 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { self.solver.program.interner(), &ConstrainedSubst { subst, constraints }, ); - return Ok(Solution::Unique(constrained.quantified)); + return Ok(Answer::new( + Solution::Unique(constrained.quantified), + delayed_goals, + )); } // Otherwise, we have (positive or negative) obligations remaining, but @@ -435,19 +431,22 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { let PositiveSolution { free_vars, universes, - solution, + answer, } = self.prove(&goal, minimums).unwrap(); - if let Some(constrained_subst) = solution.constrained_subst() { + if let Some(constrained_subst) = answer.solution.constrained_subst() { self.apply_solution(free_vars, universes, constrained_subst); let subst = self .infer .canonicalize(self.solver.program.interner(), &subst); - return Ok(Solution::Ambig(Guidance::Suggested(subst.quantified))); + return Ok(Answer::new( + Solution::Ambig(Guidance::Suggested(subst.quantified)), + answer.delayed_goals, + )); } } } - Ok(Solution::Ambig(Guidance::Unknown)) + Ok(Answer::new(Solution::Ambig(Guidance::Unknown), vec![])) } else { // While we failed to prove the goal, we still learned that // something had to hold. Here's an example where this happens: @@ -472,7 +471,10 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { let subst = self .infer .canonicalize(self.solver.program.interner(), &subst); - Ok(Solution::Ambig(Guidance::Definite(subst.quantified))) + Ok(Answer::new( + Solution::Ambig(Guidance::Definite(subst.quantified)), + vec![], + )) } } diff --git a/chalk-solve/src/recursive/search_graph.rs b/chalk-solve/src/recursive/search_graph.rs index 801c4fdaf94..2ab24b5e9db 100644 --- a/chalk-solve/src/recursive/search_graph.rs +++ b/chalk-solve/src/recursive/search_graph.rs @@ -4,8 +4,7 @@ use std::ops::IndexMut; use std::usize; use super::stack::StackDepth; -use super::{Minimums, UCanonicalGoal}; -use crate::Solution; +use super::{Answer, Minimums, UCanonicalGoal}; use chalk_engine::fallible::{Fallible, NoSolution}; use chalk_ir::{interner::Interner, ClausePriority}; use rustc_hash::FxHashMap; @@ -23,7 +22,7 @@ pub(super) struct DepthFirstNumber { pub(super) struct Node { pub(crate) goal: UCanonicalGoal, - pub(crate) solution: Fallible>, + pub(crate) solution: Fallible>, pub(crate) solution_priority: ClausePriority, /// This is `Some(X)` if we are actively exploring this node, or @@ -88,7 +87,7 @@ impl SearchGraph { pub(crate) fn move_to_cache( &mut self, dfn: DepthFirstNumber, - cache: &mut FxHashMap, Fallible>>, + cache: &mut FxHashMap, Fallible>>, ) { debug!("move_to_cache(dfn={:?})", dfn); self.indices.retain(|_key, value| *value < dfn); diff --git a/tests/test/coinduction.rs b/tests/test/coinduction.rs index 27cb65b5ec7..24b86395664 100644 --- a/tests/test/coinduction.rs +++ b/tests/test/coinduction.rs @@ -210,16 +210,9 @@ fn coinductive_unsound1() { goal { forall { X: C1orC2 } - } yields[SolverChoice::slg(3, None)] { + } yields { "No possible solution" } - - goal { - forall { X: C1orC2 } - } yields[SolverChoice::recursive()] { - // FIXME(chalk#399) recursive solver doesn't handle coinduction correctly - "Unique; substitution [], lifetime constraints []" - } } } @@ -447,14 +440,8 @@ fn coinductive_multicycle4() { goal { forall { X: Any } - } yields_all[SolverChoice::slg(3, None)] { - } - - goal { - forall { X: Any } - } yields[SolverChoice::recursive()] { - // FIXME(chalk#399) recursive solver doesn't handle coinduction correctly - "Unique; substitution [], lifetime constraints []" + } yields { + "No possible solution" } } }