1 use crate::fixed_point::{Cache, Minimums, RecursiveContext, SolverStuff}; 2 use crate::solve::{SolveDatabase, SolveIteration}; 3 use crate::UCanonicalGoal; 4 use chalk_ir::{interner::Interner, NoSolution}; 5 use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, UCanonical}; 6 use chalk_ir::{Constraints, Fallible}; 7 use chalk_solve::{coinductive_goal::IsCoinductive, RustIrDatabase, Solution}; 8 use std::fmt; 9 10 /// A Solver is the basic context in which you can propose goals for a given 11 /// program. **All questions posed to the solver are in canonical, closed form, 12 /// so that each question is answered with effectively a "clean slate"**. This 13 /// allows for better caching, and simplifies management of the inference 14 /// context. 15 struct Solver<'me, I: Interner> { 16 program: &'me dyn RustIrDatabase<I>, 17 context: &'me mut RecursiveContext<UCanonicalGoal<I>, Fallible<Solution<I>>>, 18 } 19 20 pub struct RecursiveSolver<I: Interner> { 21 ctx: Box<RecursiveContext<UCanonicalGoal<I>, Fallible<Solution<I>>>>, 22 } 23 24 impl<I: Interner> RecursiveSolver<I> { new( overflow_depth: usize, max_size: usize, cache: Option<Cache<UCanonicalGoal<I>, Fallible<Solution<I>>>>, ) -> Self25 pub fn new( 26 overflow_depth: usize, 27 max_size: usize, 28 cache: Option<Cache<UCanonicalGoal<I>, Fallible<Solution<I>>>>, 29 ) -> Self { 30 Self { 31 ctx: Box::new(RecursiveContext::new(overflow_depth, max_size, cache)), 32 } 33 } 34 } 35 36 impl<I: Interner> fmt::Debug for RecursiveSolver<I> { fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result37 fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result { 38 write!(fmt, "RecursiveSolver") 39 } 40 } 41 42 impl<'me, I: Interner> Solver<'me, I> { new( context: &'me mut RecursiveContext<UCanonicalGoal<I>, Fallible<Solution<I>>>, program: &'me dyn RustIrDatabase<I>, ) -> Self43 pub(crate) fn new( 44 context: &'me mut RecursiveContext<UCanonicalGoal<I>, Fallible<Solution<I>>>, 45 program: &'me dyn RustIrDatabase<I>, 46 ) -> Self { 47 Self { program, context } 48 } 49 } 50 51 impl<I: Interner> SolverStuff<UCanonicalGoal<I>, Fallible<Solution<I>>> for &dyn RustIrDatabase<I> { is_coinductive_goal(self, goal: &UCanonicalGoal<I>) -> bool52 fn is_coinductive_goal(self, goal: &UCanonicalGoal<I>) -> bool { 53 goal.is_coinductive(self) 54 } 55 initial_value( self, goal: &UCanonicalGoal<I>, coinductive_goal: bool, ) -> Fallible<Solution<I>>56 fn initial_value( 57 self, 58 goal: &UCanonicalGoal<I>, 59 coinductive_goal: bool, 60 ) -> Fallible<Solution<I>> { 61 if coinductive_goal { 62 Ok(Solution::Unique(Canonical { 63 value: ConstrainedSubst { 64 subst: goal.trivial_substitution(self.interner()), 65 constraints: Constraints::empty(self.interner()), 66 }, 67 binders: goal.canonical.binders.clone(), 68 })) 69 } else { 70 Err(NoSolution) 71 } 72 } 73 solve_iteration( self, context: &mut RecursiveContext<UCanonicalGoal<I>, Fallible<Solution<I>>>, goal: &UCanonicalGoal<I>, minimums: &mut Minimums, ) -> Fallible<Solution<I>>74 fn solve_iteration( 75 self, 76 context: &mut RecursiveContext<UCanonicalGoal<I>, Fallible<Solution<I>>>, 77 goal: &UCanonicalGoal<I>, 78 minimums: &mut Minimums, 79 ) -> Fallible<Solution<I>> { 80 Solver::new(context, self).solve_iteration(goal, minimums) 81 } 82 reached_fixed_point( self, old_answer: &Fallible<Solution<I>>, current_answer: &Fallible<Solution<I>>, ) -> bool83 fn reached_fixed_point( 84 self, 85 old_answer: &Fallible<Solution<I>>, 86 current_answer: &Fallible<Solution<I>>, 87 ) -> bool { 88 // Some of our subgoals depended on us. We need to re-run 89 // with the current answer. 90 old_answer == current_answer || { 91 // Subtle: if our current answer is ambiguous, we can just stop, and 92 // in fact we *must* -- otherwise, we sometimes fail to reach a 93 // fixed point. See `multiple_ambiguous_cycles` for more. 94 match ¤t_answer { 95 Ok(s) => s.is_ambig(), 96 Err(_) => false, 97 } 98 } 99 } 100 error_value(self) -> Fallible<Solution<I>>101 fn error_value(self) -> Fallible<Solution<I>> { 102 Err(NoSolution) 103 } 104 } 105 106 impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> { solve_goal( &mut self, goal: UCanonicalGoal<I>, minimums: &mut Minimums, ) -> Fallible<Solution<I>>107 fn solve_goal( 108 &mut self, 109 goal: UCanonicalGoal<I>, 110 minimums: &mut Minimums, 111 ) -> Fallible<Solution<I>> { 112 self.context.solve_goal(&goal, minimums, self.program) 113 } 114 interner(&self) -> &I115 fn interner(&self) -> &I { 116 &self.program.interner() 117 } 118 db(&self) -> &dyn RustIrDatabase<I>119 fn db(&self) -> &dyn RustIrDatabase<I> { 120 self.program 121 } 122 max_size(&self) -> usize123 fn max_size(&self) -> usize { 124 self.context.max_size() 125 } 126 } 127 128 impl<I: Interner> chalk_solve::Solver<I> for RecursiveSolver<I> { solve( &mut self, program: &dyn RustIrDatabase<I>, goal: &UCanonical<InEnvironment<Goal<I>>>, ) -> Option<chalk_solve::Solution<I>>129 fn solve( 130 &mut self, 131 program: &dyn RustIrDatabase<I>, 132 goal: &UCanonical<InEnvironment<Goal<I>>>, 133 ) -> Option<chalk_solve::Solution<I>> { 134 self.ctx.solve_root_goal(goal, program).ok() 135 } 136 solve_limited( &mut self, program: &dyn RustIrDatabase<I>, goal: &UCanonical<InEnvironment<Goal<I>>>, _should_continue: &dyn std::ops::Fn() -> bool, ) -> Option<chalk_solve::Solution<I>>137 fn solve_limited( 138 &mut self, 139 program: &dyn RustIrDatabase<I>, 140 goal: &UCanonical<InEnvironment<Goal<I>>>, 141 _should_continue: &dyn std::ops::Fn() -> bool, 142 ) -> Option<chalk_solve::Solution<I>> { 143 // TODO support should_continue in recursive solver 144 self.ctx.solve_root_goal(goal, program).ok() 145 } 146 solve_multiple( &mut self, _program: &dyn RustIrDatabase<I>, _goal: &UCanonical<InEnvironment<Goal<I>>>, _f: &mut dyn FnMut( chalk_solve::SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool, ) -> bool, ) -> bool147 fn solve_multiple( 148 &mut self, 149 _program: &dyn RustIrDatabase<I>, 150 _goal: &UCanonical<InEnvironment<Goal<I>>>, 151 _f: &mut dyn FnMut( 152 chalk_solve::SubstitutionResult<Canonical<ConstrainedSubst<I>>>, 153 bool, 154 ) -> bool, 155 ) -> bool { 156 unimplemented!("Recursive solver doesn't support multiple answers") 157 } 158 } 159