vendor/chalk-recursive/src/lib.rs

   1 use crate::search_graph::DepthFirstNumber;
   2 use chalk_ir::interner::Interner;
   3 use chalk_ir::{
   4     Canonical, ConstrainedSubst, Constraints, Goal, InEnvironment, Substitution, UCanonical,
   5 };
   6 use std::fmt;
   7 use tracing::debug;
   8
   9 pub type UCanonicalGoal<I> = UCanonical<InEnvironment<Goal<I>>>;
  10
  11 mod combine;
  12 mod fulfill;
  13 mod recursive;
  14 mod search_graph;
  15 pub mod solve;
  16 mod stack;
  17
  18 pub use recursive::RecursiveSolver;
  19
  20 /// The `minimums` struct is used while solving to track whether we encountered
  21 /// any cycles in the process.
  22 #[derive(Copy, Clone, Debug)]
  23 pub(crate) struct Minimums {
  24     pub(crate) positive: DepthFirstNumber,
  25 }
  26
  27 impl Minimums {
  28     pub fn new() -> Self {
  29         Minimums {
  30             positive: DepthFirstNumber::MAX,
  31         }
  32     }
  33
  34     pub fn update_from(&mut self, minimums: Minimums) {
  35         self.positive = ::std::cmp::min(self.positive, minimums.positive);
  36     }
  37 }
  38
  39 /// A (possible) solution for a proposed goal.
  40 #[derive(Clone, Debug, PartialEq, Eq)]
  41 pub enum Solution<I: Interner> {
  42     /// The goal indeed holds, and there is a unique value for all existential
  43     /// variables. In this case, we also record a set of lifetime constraints
  44     /// which must also hold for the goal to be valid.
  45     Unique(Canonical<ConstrainedSubst<I>>),
  46
  47     /// The goal may be provable in multiple ways, but regardless we may have some guidance
  48     /// for type inference. In this case, we don't return any lifetime
  49     /// constraints, since we have not "committed" to any particular solution
  50     /// yet.
  51     Ambig(Guidance<I>),
  52 }
  53
  54 /// When a goal holds ambiguously (e.g., because there are multiple possible
  55 /// solutions), we issue a set of *guidance* back to type inference.
  56 #[derive(Clone, Debug, PartialEq, Eq)]
  57 pub enum Guidance<I: Interner> {
  58     /// The existential variables *must* have the given values if the goal is
  59     /// ever to hold, but that alone isn't enough to guarantee the goal will
  60     /// actually hold.
  61     Definite(Canonical<Substitution<I>>),
  62
  63     /// There are multiple plausible values for the existentials, but the ones
  64     /// here are suggested as the preferred choice heuristically. These should
  65     /// be used for inference fallback only.
  66     Suggested(Canonical<Substitution<I>>),
  67
  68     /// There's no useful information to feed back to type inference
  69     Unknown,
  70 }
  71
  72 impl<I: Interner> Solution<I> {
  73     /// There are multiple candidate solutions, which may or may not agree on
  74     /// the values for existential variables; attempt to combine them. This
  75     /// operation does not depend on the order of its arguments.
  76     //
  77     // This actually isn't as precise as it could be, in two ways:
  78     //
  79     // a. It might be that while there are multiple distinct candidates, they
  80     //    all agree about *some things*. To be maximally precise, we would
  81     //    compute the intersection of what they agree on. It's not clear though
  82     //    that this is actually what we want Rust's inference to do, and it's
  83     //    certainly not what it does today.
  84     //
  85     // b. There might also be an ambiguous candidate and a successful candidate,
  86     //    both with the same refined-goal. In that case, we could probably claim
  87     //    success, since if the conditions of the ambiguous candidate were met,
  88     //    we know the success would apply.  Example: `?0: Clone` yields ambiguous
  89     //    candidate `Option<?0>: Clone` and successful candidate `Option<?0>:
  90     //    Clone`.
  91     //
  92     // But you get the idea.
  93     pub(crate) fn combine(self, other: Solution<I>, interner: &I) -> Solution<I> {
  94         use self::Guidance::*;
  95
  96         if self == other {
  97             return self;
  98         }
  99
 100         debug!(
 101             "combine {} with {}",
 102             self.display(interner),
 103             other.display(interner)
 104         );
 105
 106         // Otherwise, always downgrade to Ambig:
 107
 108         let guidance = match (self.into_guidance(), other.into_guidance()) {
 109             (Definite(ref subst1), Definite(ref subst2)) if subst1 == subst2 => {
 110                 Definite(subst1.clone())
 111             }
 112             (Suggested(ref subst1), Suggested(ref subst2)) if subst1 == subst2 => {
 113                 Suggested(subst1.clone())
 114             }
 115             _ => Unknown,
 116         };
 117         Solution::Ambig(guidance)
 118     }
 119
 120     /// View this solution purely in terms of type inference guidance
 121     pub(crate) fn into_guidance(self) -> Guidance<I> {
 122         match self {
 123             Solution::Unique(constrained) => Guidance::Definite(Canonical {
 124                 value: constrained.value.subst,
 125                 binders: constrained.binders,
 126             }),
 127             Solution::Ambig(guidance) => guidance,
 128         }
 129     }
 130
 131     /// Extract a constrained substitution from this solution, even if ambiguous.
 132     pub(crate) fn constrained_subst(&self, interner: &I) -> Option<Canonical<ConstrainedSubst<I>>> {
 133         match *self {
 134             Solution::Unique(ref constrained) => Some(constrained.clone()),
 135             Solution::Ambig(Guidance::Definite(ref canonical))
 136             | Solution::Ambig(Guidance::Suggested(ref canonical)) => {
 137                 let value = ConstrainedSubst {
 138                     subst: canonical.value.clone(),
 139                     constraints: Constraints::empty(interner),
 140                 };
 141                 Some(Canonical {
 142                     value,
 143                     binders: canonical.binders.clone(),
 144                 })
 145             }
 146             Solution::Ambig(_) => None,
 147         }
 148     }
 149
 150     /// Determine whether this solution contains type information that *must*
 151     /// hold, and returns the subst in that case.
 152     pub(crate) fn definite_subst(&self, interner: &I) -> Option<Canonical<ConstrainedSubst<I>>> {
 153         match self {
 154             Solution::Unique(constrained) => Some(constrained.clone()),
 155             Solution::Ambig(Guidance::Definite(canonical)) => {
 156                 let value = ConstrainedSubst {
 157                     subst: canonical.value.clone(),
 158                     constraints: Constraints::empty(interner),
 159                 };
 160                 Some(Canonical {
 161                     value,
 162                     binders: canonical.binders.clone(),
 163                 })
 164             }
 165             _ => None,
 166         }
 167     }
 168
 169     pub fn is_unique(&self) -> bool {
 170         match *self {
 171             Solution::Unique(..) => true,
 172             _ => false,
 173         }
 174     }
 175
 176     pub(crate) fn is_ambig(&self) -> bool {
 177         match *self {
 178             Solution::Ambig(_) => true,
 179             _ => false,
 180         }
 181     }
 182
 183     pub fn display<'a>(&'a self, interner: &'a I) -> SolutionDisplay<'a, I> {
 184         SolutionDisplay {
 185             solution: self,
 186             interner,
 187         }
 188     }
 189 }
 190
 191 pub struct SolutionDisplay<'a, I: Interner> {
 192     solution: &'a Solution<I>,
 193     interner: &'a I,
 194 }
 195
 196 impl<'a, I: Interner> fmt::Display for SolutionDisplay<'a, I> {
 197     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> {
 198         let SolutionDisplay { solution, interner } = self;
 199         match solution {
 200             Solution::Unique(constrained) => write!(f, "Unique; {}", constrained.display(interner)),
 201             Solution::Ambig(Guidance::Definite(subst)) => write!(
 202                 f,
 203                 "Ambiguous; definite substitution {}",
 204                 subst.display(interner)
 205             ),
 206             Solution::Ambig(Guidance::Suggested(subst)) => write!(
 207                 f,
 208                 "Ambiguous; suggested substitution {}",
 209                 subst.display(interner)
 210             ),
 211             Solution::Ambig(Guidance::Unknown) => write!(f, "Ambiguous; no inference guidance"),
 212         }
 213     }
 214 }