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