]>
Commit | Line | Data |
---|---|---|
f035d41b XL |
1 | use super::search_graph::DepthFirstNumber; |
2 | use chalk_ir::interner::Interner; | |
3 | use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, Substitution, UCanonical}; | |
4 | use std::fmt; | |
5 | use tracing::debug; | |
6 | ||
7 | pub 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)] | |
12 | pub(super) struct Minimums { | |
13 | pub(super) positive: DepthFirstNumber, | |
14 | } | |
15 | ||
16 | impl 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)] | |
30 | pub 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)] | |
46 | pub 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 | ||
61 | impl<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 | ||
171 | pub struct SolutionDisplay<'a, I: Interner> { | |
172 | solution: &'a Solution<I>, | |
173 | interner: &'a I, | |
174 | } | |
175 | ||
176 | impl<'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 | } |