vendor/chalk-solve-0.25.0/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
   7 pub mod truncate;
   8
   9 /// A (possible) solution for a proposed goal.
  10 #[derive(Clone, Debug, PartialEq, Eq, HasInterner)]
  11 pub enum Solution<I: Interner> {
  12     /// The goal indeed holds, and there is a unique value for all existential
  13     /// variables. In this case, we also record a set of lifetime constraints
  14     /// which must also hold for the goal to be valid.
  15     Unique(Canonical<ConstrainedSubst<I>>),
  16
  17     /// The goal may be provable in multiple ways, but regardless we may have some guidance
  18     /// for type inference. In this case, we don't return any lifetime
  19     /// constraints, since we have not "committed" to any particular solution
  20     /// yet.
  21     Ambig(Guidance<I>),
  22 }
  23
  24 /// When a goal holds ambiguously (e.g., because there are multiple possible
  25 /// solutions), we issue a set of *guidance* back to type inference.
  26 #[derive(Clone, Debug, PartialEq, Eq)]
  27 pub enum Guidance<I: Interner> {
  28     /// The existential variables *must* have the given values if the goal is
  29     /// ever to hold, but that alone isn't enough to guarantee the goal will
  30     /// actually hold.
  31     Definite(Canonical<Substitution<I>>),
  32
  33     /// There are multiple plausible values for the existentials, but the ones
  34     /// here are suggested as the preferred choice heuristically. These should
  35     /// be used for inference fallback only.
  36     Suggested(Canonical<Substitution<I>>),
  37
  38     /// There's no useful information to feed back to type inference
  39     Unknown,
  40 }
  41
  42 impl<I: Interner> Solution<I> {
  43     pub fn is_unique(&self) -> bool {
  44         match *self {
  45             Solution::Unique(..) => true,
  46             _ => false,
  47         }
  48     }
  49
  50     pub fn display<'a>(&'a self, interner: &'a I) -> SolutionDisplay<'a, I> {
  51         SolutionDisplay {
  52             solution: self,
  53             interner,
  54         }
  55     }
  56 }
  57
  58 pub struct SolutionDisplay<'a, I: Interner> {
  59     solution: &'a Solution<I>,
  60     interner: &'a I,
  61 }
  62
  63 impl<'a, I: Interner> fmt::Display for SolutionDisplay<'a, I> {
  64     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> {
  65         let SolutionDisplay { solution, interner } = self;
  66         match solution {
  67             Solution::Unique(constrained) => write!(f, "Unique; {}", constrained.display(interner)),
  68             Solution::Ambig(Guidance::Definite(subst)) => write!(
  69                 f,
  70                 "Ambiguous; definite substitution {}",
  71                 subst.display(interner)
  72             ),
  73             Solution::Ambig(Guidance::Suggested(subst)) => write!(
  74                 f,
  75                 "Ambiguous; suggested substitution {}",
  76                 subst.display(interner)
  77             ),
  78             Solution::Ambig(Guidance::Unknown) => write!(f, "Ambiguous; no inference guidance"),
  79         }
  80     }
  81 }
  82
  83 #[derive(Debug)]
  84 pub enum SubstitutionResult<S> {
  85     Definite(S),
  86     Ambiguous(S),
  87     Floundered,
  88 }
  89
  90 impl<S> SubstitutionResult<S> {
  91     pub fn as_ref(&self) -> SubstitutionResult<&S> {
  92         match self {
  93             SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(subst),
  94             SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(subst),
  95             SubstitutionResult::Floundered => SubstitutionResult::Floundered,
  96         }
  97     }
  98     pub fn map<U, F: FnOnce(S) -> U>(self, f: F) -> SubstitutionResult<U> {
  99         match self {
 100             SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(f(subst)),
 101             SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(f(subst)),
 102             SubstitutionResult::Floundered => SubstitutionResult::Floundered,
 103         }
 104     }
 105 }
 106
 107 impl<S: fmt::Display> fmt::Display for SubstitutionResult<S> {
 108     fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
 109         match self {
 110             SubstitutionResult::Definite(subst) => write!(fmt, "{}", subst),
 111             SubstitutionResult::Ambiguous(subst) => write!(fmt, "Ambiguous({})", subst),
 112             SubstitutionResult::Floundered => write!(fmt, "Floundered"),
 113         }
 114     }
 115 }
 116
 117 /// Finds the solution to "goals", or trait queries -- i.e., figures
 118 /// out what sets of types implement which traits. Also, between
 119 /// queries, this struct stores the cached state from previous solver
 120 /// attempts, which can then be re-used later.
 121 pub trait Solver<I: Interner>
 122 where
 123     Self: fmt::Debug,
 124 {
 125     /// Attempts to solve the given goal, which must be in canonical
 126     /// form. Returns a unique solution (if one exists).  This will do
 127     /// only as much work towards `goal` as it has to (and that work
 128     /// is cached for future attempts).
 129     ///
 130     /// # Parameters
 131     ///
 132     /// - `program` -- defines the program clauses in scope.
 133     ///   - **Important:** You must supply the same set of program clauses
 134     ///     each time you invoke `solve`, as otherwise the cached data may be
 135     ///     invalid.
 136     /// - `goal` the goal to solve
 137     ///
 138     /// # Returns
 139     ///
 140     /// - `None` is the goal cannot be proven.
 141     /// - `Some(solution)` if we succeeded in finding *some* answers,
 142     ///   although `solution` may reflect ambiguity and unknowns.
 143     fn solve(
 144         &mut self,
 145         program: &dyn RustIrDatabase<I>,
 146         goal: &UCanonical<InEnvironment<Goal<I>>>,
 147     ) -> Option<Solution<I>>;
 148
 149     /// Attempts to solve the given goal, which must be in canonical
 150     /// form. Returns a unique solution (if one exists).  This will do
 151     /// only as much work towards `goal` as it has to (and that work
 152     /// is cached for future attempts). In addition, the solving of the
 153     /// goal can be limited by returning `false` from `should_continue`.
 154     ///
 155     /// # Parameters
 156     ///
 157     /// - `program` -- defines the program clauses in scope.
 158     ///   - **Important:** You must supply the same set of program clauses
 159     ///     each time you invoke `solve`, as otherwise the cached data may be
 160     ///     invalid.
 161     /// - `goal` the goal to solve
 162     /// - `should_continue` if `false` is returned, the no further solving
 163     ///   will be done. A `Guidance(Suggested(...))` will be returned a
 164     ///   `Solution`, using any answers that were generated up to that point.
 165     ///
 166     /// # Returns
 167     ///
 168     /// - `None` is the goal cannot be proven.
 169     /// - `Some(solution)` if we succeeded in finding *some* answers,
 170     ///   although `solution` may reflect ambiguity and unknowns.
 171     fn solve_limited(
 172         &mut self,
 173         program: &dyn RustIrDatabase<I>,
 174         goal: &UCanonical<InEnvironment<Goal<I>>>,
 175         should_continue: &dyn std::ops::Fn() -> bool,
 176     ) -> Option<Solution<I>>;
 177
 178     /// Attempts to solve the given goal, which must be in canonical
 179     /// form. Provides multiple solutions to function `f`.  This will do
 180     /// only as much work towards `goal` as it has to (and that work
 181     /// is cached for future attempts).
 182     ///
 183     /// # Parameters
 184     ///
 185     /// - `program` -- defines the program clauses in scope.
 186     ///   - **Important:** You must supply the same set of program clauses
 187     ///     each time you invoke `solve`, as otherwise the cached data may be
 188     ///     invalid.
 189     /// - `goal` the goal to solve
 190     /// - `f` -- function to proceed solution. New solutions will be generated
 191     /// while function returns `true`.
 192     ///   - first argument is solution found
 193     ///   - second argument is ther next solution present
 194     ///   - returns true if next solution should be handled
 195     ///
 196     /// # Returns
 197     ///
 198     /// - `true` all solutions were processed with the function.
 199     /// - `false` the function returned `false` and solutions were interrupted.
 200     fn solve_multiple(
 201         &mut self,
 202         program: &dyn RustIrDatabase<I>,
 203         goal: &UCanonical<InEnvironment<Goal<I>>>,
 204         f: &mut dyn FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool,
 205     ) -> bool;
 206 }