vendor/chalk-solve/src/solve.rs

   1 use crate::RustIrDatabase;
   2 use chalk_derive::HasInterner;
   3 use chalk_ir::interner::Interner;
   4 use chalk_ir::*;
   5 use std::fmt;
   6 use tracing::debug;
   7
   8 pub mod truncate;
   9
  10 /// A (possible) solution for a proposed goal.
  11 #[derive(Clone, Debug, PartialEq, Eq, HasInterner)]
  12 pub enum Solution<I: Interner> {
  13     /// The goal indeed holds, and there is a unique value for all existential
  14     /// variables. In this case, we also record a set of lifetime constraints
  15     /// which must also hold for the goal to be valid.
  16     Unique(Canonical<ConstrainedSubst<I>>),
  17
  18     /// The goal may be provable in multiple ways, but regardless we may have some guidance
  19     /// for type inference. In this case, we don't return any lifetime
  20     /// constraints, since we have not "committed" to any particular solution
  21     /// yet.
  22     Ambig(Guidance<I>),
  23 }
  24
  25 /// When a goal holds ambiguously (e.g., because there are multiple possible
  26 /// solutions), we issue a set of *guidance* back to type inference.
  27 #[derive(Clone, Debug, PartialEq, Eq)]
  28 pub enum Guidance<I: Interner> {
  29     /// The existential variables *must* have the given values if the goal is
  30     /// ever to hold, but that alone isn't enough to guarantee the goal will
  31     /// actually hold.
  32     Definite(Canonical<Substitution<I>>),
  33
  34     /// There are multiple plausible values for the existentials, but the ones
  35     /// here are suggested as the preferred choice heuristically. These should
  36     /// be used for inference fallback only.
  37     Suggested(Canonical<Substitution<I>>),
  38
  39     /// There's no useful information to feed back to type inference
  40     Unknown,
  41 }
  42
  43 impl<I: Interner> Solution<I> {
  44     /// There are multiple candidate solutions, which may or may not agree on
  45     /// the values for existential variables; attempt to combine them. This
  46     /// operation does not depend on the order of its arguments.
  47     ///
  48     /// This actually isn't as precise as it could be, in two ways:
  49     ///
  50     /// a. It might be that while there are multiple distinct candidates, they
  51     ///    all agree about *some things*. To be maximally precise, we would
  52     ///    compute the intersection of what they agree on. It's not clear though
  53     ///    that this is actually what we want Rust's inference to do, and it's
  54     ///    certainly not what it does today.
  55     ///
  56     /// b. There might also be an ambiguous candidate and a successful candidate,
  57     ///    both with the same refined-goal. In that case, we could probably claim
  58     ///    success, since if the conditions of the ambiguous candidate were met,
  59     ///    we know the success would apply.  Example: `?0: Clone` yields ambiguous
  60     ///    candidate `Option<?0>: Clone` and successful candidate `Option<?0>:
  61     ///    Clone`.
  62     ///
  63     /// But you get the idea.
  64     pub fn combine(self, other: Solution<I>, interner: I) -> Solution<I> {
  65         use self::Guidance::*;
  66
  67         if self == other {
  68             return self;
  69         }
  70
  71         // Special case hack: if one solution is "true" without any constraints,
  72         // that is always the combined result.
  73         //
  74         // This is not as general as it could be: ideally, if we had one solution
  75         // that is Unique with a simpler substitution than the other one, or region constraints
  76         // which are a subset, we'd combine them.
  77         if self.is_trivial_and_always_true(interner) {
  78             return self;
  79         }
  80         if other.is_trivial_and_always_true(interner) {
  81             return other;
  82         }
  83
  84         debug!(
  85             "combine {} with {}",
  86             self.display(interner),
  87             other.display(interner)
  88         );
  89
  90         // Otherwise, always downgrade to Ambig:
  91
  92         let guidance = match (self.into_guidance(), other.into_guidance()) {
  93             (Definite(ref subst1), Definite(ref subst2)) if subst1 == subst2 => {
  94                 Definite(subst1.clone())
  95             }
  96             (Suggested(ref subst1), Suggested(ref subst2)) if subst1 == subst2 => {
  97                 Suggested(subst1.clone())
  98             }
  99             _ => Unknown,
 100         };
 101         Solution::Ambig(guidance)
 102     }
 103
 104     pub fn is_trivial_and_always_true(&self, interner: I) -> bool {
 105         match self {
 106             Solution::Unique(constrained_subst) => {
 107                 constrained_subst.value.subst.is_identity_subst(interner)
 108                     && constrained_subst.value.constraints.is_empty(interner)
 109             }
 110             Solution::Ambig(_) => false,
 111         }
 112     }
 113
 114     /// View this solution purely in terms of type inference guidance
 115     pub fn into_guidance(self) -> Guidance<I> {
 116         match self {
 117             Solution::Unique(constrained) => Guidance::Definite(Canonical {
 118                 value: constrained.value.subst,
 119                 binders: constrained.binders,
 120             }),
 121             Solution::Ambig(guidance) => guidance,
 122         }
 123     }
 124
 125     /// Extract a constrained substitution from this solution, even if ambiguous.
 126     pub fn constrained_subst(&self, interner: I) -> Option<Canonical<ConstrainedSubst<I>>> {
 127         match *self {
 128             Solution::Unique(ref constrained) => Some(constrained.clone()),
 129             Solution::Ambig(Guidance::Definite(ref canonical))
 130             | Solution::Ambig(Guidance::Suggested(ref canonical)) => {
 131                 let value = ConstrainedSubst {
 132                     subst: canonical.value.clone(),
 133                     constraints: Constraints::empty(interner),
 134                 };
 135                 Some(Canonical {
 136                     value,
 137                     binders: canonical.binders.clone(),
 138                 })
 139             }
 140             Solution::Ambig(_) => None,
 141         }
 142     }
 143
 144     /// Determine whether this solution contains type information that *must*
 145     /// hold, and returns the subst in that case.
 146     pub fn definite_subst(&self, interner: I) -> Option<Canonical<ConstrainedSubst<I>>> {
 147         match self {
 148             Solution::Unique(constrained) => Some(constrained.clone()),
 149             Solution::Ambig(Guidance::Definite(canonical)) => {
 150                 let value = ConstrainedSubst {
 151                     subst: canonical.value.clone(),
 152                     constraints: Constraints::empty(interner),
 153                 };
 154                 Some(Canonical {
 155                     value,
 156                     binders: canonical.binders.clone(),
 157                 })
 158             }
 159             _ => None,
 160         }
 161     }
 162
 163     pub fn is_unique(&self) -> bool {
 164         matches!(*self, Solution::Unique(..))
 165     }
 166
 167     pub fn is_ambig(&self) -> bool {
 168         matches!(*self, Solution::Ambig(_))
 169     }
 170
 171     pub fn display(&self, interner: I) -> SolutionDisplay<'_, I> {
 172         SolutionDisplay {
 173             solution: self,
 174             interner,
 175         }
 176     }
 177 }
 178
 179 pub struct SolutionDisplay<'a, I: Interner> {
 180     solution: &'a Solution<I>,
 181     interner: I,
 182 }
 183
 184 impl<'a, I: Interner> fmt::Display for SolutionDisplay<'a, I> {
 185     #[rustfmt::skip]
 186     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> {
 187         let SolutionDisplay { solution, interner } = self;
 188         match solution {
 189             // If a `Unique` solution has no associated data, omit the trailing semicolon.
 190             // This makes blessed test output nicer to read.
 191             Solution::Unique(Canonical { binders, value: ConstrainedSubst { subst, constraints } } )
 192                 if interner.constraints_data(constraints.interned()).is_empty()
 193                     && interner.substitution_data(subst.interned()).is_empty()
 194                     && interner.canonical_var_kinds_data(binders.interned()).is_empty()
 195                 => write!(f, "Unique"),
 196
 197             Solution::Unique(constrained) => write!(f, "Unique; {}", constrained.display(*interner)),
 198
 199             Solution::Ambig(Guidance::Definite(subst)) => write!(
 200                 f,
 201                 "Ambiguous; definite substitution {}",
 202                 subst.display(*interner)
 203             ),
 204             Solution::Ambig(Guidance::Suggested(subst)) => write!(
 205                 f,
 206                 "Ambiguous; suggested substitution {}",
 207                 subst.display(*interner)
 208             ),
 209             Solution::Ambig(Guidance::Unknown) => write!(f, "Ambiguous; no inference guidance"),
 210         }
 211     }
 212 }
 213
 214 #[derive(Debug)]
 215 pub enum SubstitutionResult<S> {
 216     Definite(S),
 217     Ambiguous(S),
 218     Floundered,
 219 }
 220
 221 impl<S> SubstitutionResult<S> {
 222     pub fn as_ref(&self) -> SubstitutionResult<&S> {
 223         match self {
 224             SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(subst),
 225             SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(subst),
 226             SubstitutionResult::Floundered => SubstitutionResult::Floundered,
 227         }
 228     }
 229     pub fn map<U, F: FnOnce(S) -> U>(self, f: F) -> SubstitutionResult<U> {
 230         match self {
 231             SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(f(subst)),
 232             SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(f(subst)),
 233             SubstitutionResult::Floundered => SubstitutionResult::Floundered,
 234         }
 235     }
 236 }
 237
 238 impl<S: fmt::Display> fmt::Display for SubstitutionResult<S> {
 239     fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
 240         match self {
 241             SubstitutionResult::Definite(subst) => write!(fmt, "{}", subst),
 242             SubstitutionResult::Ambiguous(subst) => write!(fmt, "Ambiguous({})", subst),
 243             SubstitutionResult::Floundered => write!(fmt, "Floundered"),
 244         }
 245     }
 246 }
 247
 248 /// Finds the solution to "goals", or trait queries -- i.e., figures
 249 /// out what sets of types implement which traits. Also, between
 250 /// queries, this struct stores the cached state from previous solver
 251 /// attempts, which can then be re-used later.
 252 pub trait Solver<I: Interner>
 253 where
 254     Self: fmt::Debug,
 255 {
 256     /// Attempts to solve the given goal, which must be in canonical
 257     /// form. Returns a unique solution (if one exists).  This will do
 258     /// only as much work towards `goal` as it has to (and that work
 259     /// is cached for future attempts).
 260     ///
 261     /// # Parameters
 262     ///
 263     /// - `program` -- defines the program clauses in scope.
 264     ///   - **Important:** You must supply the same set of program clauses
 265     ///     each time you invoke `solve`, as otherwise the cached data may be
 266     ///     invalid.
 267     /// - `goal` the goal to solve
 268     ///
 269     /// # Returns
 270     ///
 271     /// - `None` is the goal cannot be proven.
 272     /// - `Some(solution)` if we succeeded in finding *some* answers,
 273     ///   although `solution` may reflect ambiguity and unknowns.
 274     fn solve(
 275         &mut self,
 276         program: &dyn RustIrDatabase<I>,
 277         goal: &UCanonical<InEnvironment<Goal<I>>>,
 278     ) -> Option<Solution<I>>;
 279
 280     /// Attempts to solve the given goal, which must be in canonical
 281     /// form. Returns a unique solution (if one exists).  This will do
 282     /// only as much work towards `goal` as it has to (and that work
 283     /// is cached for future attempts). In addition, the solving of the
 284     /// goal can be limited by returning `false` from `should_continue`.
 285     ///
 286     /// # Parameters
 287     ///
 288     /// - `program` -- defines the program clauses in scope.
 289     ///   - **Important:** You must supply the same set of program clauses
 290     ///     each time you invoke `solve`, as otherwise the cached data may be
 291     ///     invalid.
 292     /// - `goal` the goal to solve
 293     /// - `should_continue` if `false` is returned, the no further solving
 294     ///   will be done. A `Guidance(Suggested(...))` will be returned a
 295     ///   `Solution`, using any answers that were generated up to that point.
 296     ///
 297     /// # Returns
 298     ///
 299     /// - `None` is the goal cannot be proven.
 300     /// - `Some(solution)` if we succeeded in finding *some* answers,
 301     ///   although `solution` may reflect ambiguity and unknowns.
 302     fn solve_limited(
 303         &mut self,
 304         program: &dyn RustIrDatabase<I>,
 305         goal: &UCanonical<InEnvironment<Goal<I>>>,
 306         should_continue: &dyn std::ops::Fn() -> bool,
 307     ) -> Option<Solution<I>>;
 308
 309     /// Attempts to solve the given goal, which must be in canonical
 310     /// form. Provides multiple solutions to function `f`.  This will do
 311     /// only as much work towards `goal` as it has to (and that work
 312     /// is cached for future attempts).
 313     ///
 314     /// # Parameters
 315     ///
 316     /// - `program` -- defines the program clauses in scope.
 317     ///   - **Important:** You must supply the same set of program clauses
 318     ///     each time you invoke `solve`, as otherwise the cached data may be
 319     ///     invalid.
 320     /// - `goal` the goal to solve
 321     /// - `f` -- function to proceed solution. New solutions will be generated
 322     /// while function returns `true`.
 323     ///   - first argument is solution found
 324     ///   - second argument is the next solution present
 325     ///   - returns true if next solution should be handled
 326     ///
 327     /// # Returns
 328     ///
 329     /// - `true` all solutions were processed with the function.
 330     /// - `false` the function returned `false` and solutions were interrupted.
 331     fn solve_multiple(
 332         &mut self,
 333         program: &dyn RustIrDatabase<I>,
 334         goal: &UCanonical<InEnvironment<Goal<I>>>,
 335         f: &mut dyn FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool,
 336     ) -> bool;
 337
 338     /// A convenience method for when one doesn't need the actual solution,
 339     /// only whether or not one exists.
 340     fn has_unique_solution(
 341         &mut self,
 342         program: &dyn RustIrDatabase<I>,
 343         goal: &UCanonical<InEnvironment<Goal<I>>>,
 344     ) -> bool {
 345         match self.solve(program, goal) {
 346             Some(sol) => sol.is_unique(),
 347             None => false,
 348         }
 349     }
 350 }