vendor/chalk-recursive/src/solve.rs

   1 use super::combine;
   2 use super::fulfill::{Fulfill, RecursiveInferenceTable};
   3 use crate::{Guidance, Minimums, Solution, UCanonicalGoal};
   4 use chalk_ir::fold::Fold;
   5 use chalk_ir::interner::{HasInterner, Interner};
   6 use chalk_ir::visit::Visit;
   7 use chalk_ir::zip::Zip;
   8 use chalk_ir::{
   9     Binders, Canonical, ClausePriority, DomainGoal, Environment, Fallible, Floundered, GenericArg,
  10     Goal, GoalData, InEnvironment, NoSolution, ProgramClause, ProgramClauseData,
  11     ProgramClauseImplication, Substitution, UCanonical, UniverseMap,
  12 };
  13 use chalk_solve::clauses::program_clauses_for_goal;
  14 use chalk_solve::debug_span;
  15 use chalk_solve::infer::{InferenceTable, ParameterEnaVariableExt};
  16 use chalk_solve::{solve::truncate, RustIrDatabase};
  17 use std::fmt::Debug;
  18 use tracing::{debug, instrument};
  19
  20 pub(super) trait SolveDatabase<I: Interner>: Sized {
  21     fn solve_goal(
  22         &mut self,
  23         goal: UCanonical<InEnvironment<Goal<I>>>,
  24         minimums: &mut Minimums,
  25     ) -> Fallible<Solution<I>>;
  26
  27     fn interner(&self) -> &I;
  28
  29     fn db(&self) -> &dyn RustIrDatabase<I>;
  30 }
  31
  32 /// The `solve_iteration` method -- implemented for any type that implements
  33 /// `SolveDb`.
  34 pub(super) trait SolveIteration<I: Interner>: SolveDatabase<I> {
  35     /// Executes one iteration of the recursive solver, computing the current
  36     /// solution to the given canonical goal. This is used as part of a loop in
  37     /// the case of cyclic goals.
  38     #[instrument(level = "debug", skip(self))]
  39     fn solve_iteration(
  40         &mut self,
  41         canonical_goal: &UCanonicalGoal<I>,
  42         minimums: &mut Minimums,
  43     ) -> (Fallible<Solution<I>>, ClausePriority) {
  44         let UCanonical {
  45             universes,
  46             canonical:
  47                 Canonical {
  48                     binders,
  49                     value: InEnvironment { environment, goal },
  50                 },
  51         } = canonical_goal.clone();
  52
  53         match goal.data(self.interner()) {
  54             GoalData::DomainGoal(domain_goal) => {
  55                 let canonical_goal = UCanonical {
  56                     universes,
  57                     canonical: Canonical {
  58                         binders,
  59                         value: InEnvironment {
  60                             environment,
  61                             goal: domain_goal.clone(),
  62                         },
  63                     },
  64                 };
  65
  66                 // "Domain" goals (i.e., leaf goals that are Rust-specific) are
  67                 // always solved via some form of implication. We can either
  68                 // apply assumptions from our environment (i.e. where clauses),
  69                 // or from the lowered program, which includes fallback
  70                 // clauses. We try each approach in turn:
  71
  72                 let (prog_solution, prog_prio) = {
  73                     debug_span!("prog_clauses");
  74
  75                     let prog_clauses = self.program_clauses_for_goal(&canonical_goal);
  76                     match prog_clauses {
  77                         Ok(clauses) => self.solve_from_clauses(&canonical_goal, clauses, minimums),
  78                         Err(Floundered) => {
  79                             (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High)
  80                         }
  81                     }
  82                 };
  83                 debug!(?prog_solution);
  84
  85                 (prog_solution, prog_prio)
  86             }
  87
  88             _ => {
  89                 let canonical_goal = UCanonical {
  90                     universes,
  91                     canonical: Canonical {
  92                         binders,
  93                         value: InEnvironment { environment, goal },
  94                     },
  95                 };
  96
  97                 self.solve_via_simplification(&canonical_goal, minimums)
  98             }
  99         }
 100     }
 101 }
 102
 103 impl<S, I> SolveIteration<I> for S
 104 where
 105     S: SolveDatabase<I>,
 106     I: Interner,
 107 {
 108 }
 109
 110 /// Helper methods for `solve_iteration`, private to this module.
 111 trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
 112     #[instrument(level = "debug", skip(self, minimums))]
 113     fn solve_via_simplification(
 114         &mut self,
 115         canonical_goal: &UCanonicalGoal<I>,
 116         minimums: &mut Minimums,
 117     ) -> (Fallible<Solution<I>>, ClausePriority) {
 118         let (infer, subst, goal) = self.new_inference_table(canonical_goal);
 119         match Fulfill::new_with_simplification(self, infer, subst, goal) {
 120             Ok(fulfill) => (fulfill.solve(minimums), ClausePriority::High),
 121             Err(e) => (Err(e), ClausePriority::High),
 122         }
 123     }
 124
 125     /// See whether we can solve a goal by implication on any of the given
 126     /// clauses. If multiple such solutions are possible, we attempt to combine
 127     /// them.
 128     fn solve_from_clauses<C>(
 129         &mut self,
 130         canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
 131         clauses: C,
 132         minimums: &mut Minimums,
 133     ) -> (Fallible<Solution<I>>, ClausePriority)
 134     where
 135         C: IntoIterator<Item = ProgramClause<I>>,
 136     {
 137         let mut cur_solution = None;
 138         for program_clause in clauses {
 139             debug_span!("solve_from_clauses", clause = ?program_clause);
 140
 141             // If we have a completely ambiguous answer, it's not going to get better, so stop
 142             if cur_solution == Some((Solution::Ambig(Guidance::Unknown), ClausePriority::High)) {
 143                 return (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High);
 144             }
 145
 146             let ProgramClauseData(implication) = program_clause.data(self.interner());
 147             let res = self.solve_via_implication(canonical_goal, implication, minimums);
 148
 149             if let (Ok(solution), priority) = res {
 150                 debug!(?solution, ?priority, "Ok");
 151                 cur_solution = Some(match cur_solution {
 152                     None => (solution, priority),
 153                     Some((cur, cur_priority)) => combine::with_priorities(
 154                         self.interner(),
 155                         &canonical_goal.canonical.value.goal,
 156                         cur,
 157                         cur_priority,
 158                         solution,
 159                         priority,
 160                     ),
 161                 });
 162             } else {
 163                 debug!("Error");
 164             }
 165         }
 166         cur_solution.map_or((Err(NoSolution), ClausePriority::High), |(s, p)| (Ok(s), p))
 167     }
 168
 169     /// Modus ponens! That is: try to apply an implication by proving its premises.
 170     #[instrument(level = "info", skip(self, minimums))]
 171     fn solve_via_implication(
 172         &mut self,
 173         canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
 174         clause: &Binders<ProgramClauseImplication<I>>,
 175         minimums: &mut Minimums,
 176     ) -> (Fallible<Solution<I>>, ClausePriority) {
 177         let (infer, subst, goal) = self.new_inference_table(canonical_goal);
 178         match Fulfill::new_with_clause(self, infer, subst, goal, clause) {
 179             Ok(fulfill) => (fulfill.solve(minimums), clause.skip_binders().priority),
 180             Err(e) => (Err(e), ClausePriority::High),
 181         }
 182     }
 183
 184     fn new_inference_table<T: Fold<I, I, Result = T> + HasInterner<Interner = I> + Clone>(
 185         &self,
 186         ucanonical_goal: &UCanonical<InEnvironment<T>>,
 187     ) -> (
 188         RecursiveInferenceTableImpl<I>,
 189         Substitution<I>,
 190         InEnvironment<T::Result>,
 191     ) {
 192         let (infer, subst, canonical_goal) = InferenceTable::from_canonical(
 193             self.interner(),
 194             ucanonical_goal.universes,
 195             &ucanonical_goal.canonical,
 196         );
 197         let infer = RecursiveInferenceTableImpl { infer };
 198         (infer, subst, canonical_goal)
 199     }
 200
 201     fn program_clauses_for_goal(
 202         &self,
 203         canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
 204     ) -> Result<Vec<ProgramClause<I>>, Floundered> {
 205         program_clauses_for_goal(
 206             self.db(),
 207             &canonical_goal.canonical.value.environment,
 208             &canonical_goal.canonical.value.goal,
 209             &canonical_goal.canonical.binders,
 210         )
 211     }
 212 }
 213
 214 impl<S, I> SolveIterationHelpers<I> for S
 215 where
 216     S: SolveDatabase<I>,
 217     I: Interner,
 218 {
 219 }
 220
 221 struct RecursiveInferenceTableImpl<I: Interner> {
 222     infer: InferenceTable<I>,
 223 }
 224
 225 impl<I: Interner> RecursiveInferenceTable<I> for RecursiveInferenceTableImpl<I> {
 226     fn instantiate_binders_universally<'a, T>(
 227         &mut self,
 228         interner: &'a I,
 229         arg: &'a Binders<T>,
 230     ) -> T::Result
 231     where
 232         T: Fold<I> + HasInterner<Interner = I>,
 233     {
 234         self.infer.instantiate_binders_universally(interner, arg)
 235     }
 236
 237     fn instantiate_binders_existentially<'a, T>(
 238         &mut self,
 239         interner: &'a I,
 240         arg: &'a Binders<T>,
 241     ) -> T::Result
 242     where
 243         T: Fold<I> + HasInterner<Interner = I>,
 244     {
 245         self.infer.instantiate_binders_existentially(interner, arg)
 246     }
 247
 248     fn canonicalize<T>(
 249         &mut self,
 250         interner: &I,
 251         value: &T,
 252     ) -> (Canonical<T::Result>, Vec<GenericArg<I>>)
 253     where
 254         T: Fold<I>,
 255         T::Result: HasInterner<Interner = I>,
 256     {
 257         let res = self.infer.canonicalize(interner, value);
 258         let free_vars = res
 259             .free_vars
 260             .into_iter()
 261             .map(|free_var| free_var.to_generic_arg(interner))
 262             .collect();
 263         (res.quantified, free_vars)
 264     }
 265
 266     fn u_canonicalize<T>(
 267         &mut self,
 268         interner: &I,
 269         value0: &Canonical<T>,
 270     ) -> (UCanonical<T::Result>, UniverseMap)
 271     where
 272         T: HasInterner<Interner = I> + Fold<I> + Visit<I>,
 273         T::Result: HasInterner<Interner = I>,
 274     {
 275         let res = self.infer.u_canonicalize(interner, value0);
 276         (res.quantified, res.universes)
 277     }
 278
 279     fn unify<T>(
 280         &mut self,
 281         interner: &I,
 282         environment: &Environment<I>,
 283         a: &T,
 284         b: &T,
 285     ) -> Fallible<Vec<InEnvironment<Goal<I>>>>
 286     where
 287         T: ?Sized + Zip<I>,
 288     {
 289         let res = self.infer.unify(interner, environment, a, b)?;
 290         Ok(res.goals)
 291     }
 292
 293     fn instantiate_canonical<T>(&mut self, interner: &I, bound: &Canonical<T>) -> T::Result
 294     where
 295         T: HasInterner<Interner = I> + Fold<I> + Debug,
 296     {
 297         self.infer.instantiate_canonical(interner, bound)
 298     }
 299
 300     fn invert_then_canonicalize<T>(
 301         &mut self,
 302         interner: &I,
 303         value: &T,
 304     ) -> Option<Canonical<T::Result>>
 305     where
 306         T: Fold<I, Result = T> + HasInterner<Interner = I>,
 307     {
 308         self.infer.invert_then_canonicalize(interner, value)
 309     }
 310
 311     fn needs_truncation(&mut self, interner: &I, max_size: usize, value: impl Visit<I>) -> bool {
 312         truncate::needs_truncation(interner, &mut self.infer, max_size, value)
 313     }
 314 }