]>
Commit | Line | Data |
---|---|---|
f035d41b XL |
1 | use super::combine; |
2 | use super::fulfill::{Fulfill, RecursiveInferenceTable}; | |
3 | use super::lib::{Guidance, Minimums, Solution, UCanonicalGoal}; | |
4 | use crate::clauses::program_clauses_for_goal; | |
5 | use crate::debug_span; | |
6 | use crate::infer::{InferenceTable, ParameterEnaVariableExt}; | |
7 | use crate::{solve::truncate, RustIrDatabase}; | |
8 | use chalk_ir::fold::Fold; | |
9 | use chalk_ir::interner::{HasInterner, Interner}; | |
10 | use chalk_ir::visit::Visit; | |
11 | use chalk_ir::zip::Zip; | |
12 | use chalk_ir::{ | |
13 | Binders, Canonical, ClausePriority, Constraint, DomainGoal, Environment, Fallible, Floundered, | |
14 | GenericArg, Goal, GoalData, InEnvironment, NoSolution, ProgramClause, ProgramClauseData, | |
15 | ProgramClauseImplication, Substitution, UCanonical, UniverseMap, | |
16 | }; | |
17 | use std::fmt::Debug; | |
18 | use tracing::{debug, instrument}; | |
19 | ||
20 | pub(super) trait SolveDatabase<I: Interner>: Sized { | |
21 | fn solve_goal( | |
22 | &mut self, | |
23 | goal: UCanonical<InEnvironment<Goal<I>>>, | |
24 | minimums: &mut Minimums, | |
25 | ) -> Fallible<Solution<I>>; | |
26 | ||
27 | fn interner(&self) -> &I; | |
28 | ||
29 | fn db(&self) -> &dyn RustIrDatabase<I>; | |
30 | } | |
31 | ||
32 | /// The `solve_iteration` method -- implemented for any type that implements | |
33 | /// `SolveDb`. | |
34 | pub(super) trait SolveIteration<I: Interner>: SolveDatabase<I> { | |
35 | /// Executes one iteration of the recursive solver, computing the current | |
36 | /// solution to the given canonical goal. This is used as part of a loop in | |
37 | /// the case of cyclic goals. | |
38 | fn solve_iteration( | |
39 | &mut self, | |
40 | canonical_goal: &UCanonicalGoal<I>, | |
41 | minimums: &mut Minimums, | |
42 | ) -> (Fallible<Solution<I>>, ClausePriority) { | |
43 | let UCanonical { | |
44 | universes, | |
45 | canonical: | |
46 | Canonical { | |
47 | binders, | |
48 | value: InEnvironment { environment, goal }, | |
49 | }, | |
50 | } = canonical_goal.clone(); | |
51 | ||
52 | match goal.data(self.interner()) { | |
53 | GoalData::DomainGoal(domain_goal) => { | |
54 | let canonical_goal = UCanonical { | |
55 | universes, | |
56 | canonical: Canonical { | |
57 | binders, | |
58 | value: InEnvironment { | |
59 | environment, | |
60 | goal: domain_goal.clone(), | |
61 | }, | |
62 | }, | |
63 | }; | |
64 | ||
65 | // "Domain" goals (i.e., leaf goals that are Rust-specific) are | |
66 | // always solved via some form of implication. We can either | |
67 | // apply assumptions from our environment (i.e. where clauses), | |
68 | // or from the lowered program, which includes fallback | |
69 | // clauses. We try each approach in turn: | |
70 | ||
71 | let InEnvironment { environment, goal } = &canonical_goal.canonical.value; | |
72 | ||
73 | let (prog_solution, prog_prio) = { | |
74 | debug_span!("prog_clauses"); | |
75 | ||
76 | let prog_clauses = self.program_clauses_for_goal(environment, &goal); | |
77 | match prog_clauses { | |
78 | Ok(clauses) => self.solve_from_clauses(&canonical_goal, clauses, minimums), | |
79 | Err(Floundered) => { | |
80 | (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High) | |
81 | } | |
82 | } | |
83 | }; | |
84 | debug!("prog_solution={:?}", prog_solution); | |
85 | ||
86 | (prog_solution, prog_prio) | |
87 | } | |
88 | ||
89 | _ => { | |
90 | let canonical_goal = UCanonical { | |
91 | universes, | |
92 | canonical: Canonical { | |
93 | binders, | |
94 | value: InEnvironment { environment, goal }, | |
95 | }, | |
96 | }; | |
97 | ||
98 | self.solve_via_simplification(&canonical_goal, minimums) | |
99 | } | |
100 | } | |
101 | } | |
102 | } | |
103 | ||
104 | impl<S, I> SolveIteration<I> for S | |
105 | where | |
106 | S: SolveDatabase<I>, | |
107 | I: Interner, | |
108 | { | |
109 | } | |
110 | ||
111 | /// Helper methods for `solve_iteration`, private to this module. | |
112 | trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> { | |
113 | #[instrument(level = "debug", skip(self, minimums))] | |
114 | fn solve_via_simplification( | |
115 | &mut self, | |
116 | canonical_goal: &UCanonicalGoal<I>, | |
117 | minimums: &mut Minimums, | |
118 | ) -> (Fallible<Solution<I>>, ClausePriority) { | |
119 | let (infer, subst, goal) = self.new_inference_table(canonical_goal); | |
120 | match Fulfill::new_with_simplification(self, infer, subst, goal) { | |
121 | Ok(fulfill) => (fulfill.solve(minimums), ClausePriority::High), | |
122 | Err(e) => (Err(e), ClausePriority::High), | |
123 | } | |
124 | } | |
125 | ||
126 | /// See whether we can solve a goal by implication on any of the given | |
127 | /// clauses. If multiple such solutions are possible, we attempt to combine | |
128 | /// them. | |
129 | fn solve_from_clauses<C>( | |
130 | &mut self, | |
131 | canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>, | |
132 | clauses: C, | |
133 | minimums: &mut Minimums, | |
134 | ) -> (Fallible<Solution<I>>, ClausePriority) | |
135 | where | |
136 | C: IntoIterator<Item = ProgramClause<I>>, | |
137 | { | |
138 | let mut cur_solution = None; | |
139 | for program_clause in clauses { | |
140 | debug_span!("solve_from_clauses", clause = ?program_clause); | |
141 | ||
142 | // If we have a completely ambiguous answer, it's not going to get better, so stop | |
143 | if cur_solution == Some((Solution::Ambig(Guidance::Unknown), ClausePriority::High)) { | |
144 | return (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High); | |
145 | } | |
146 | ||
147 | let ProgramClauseData(implication) = program_clause.data(self.interner()); | |
148 | let res = self.solve_via_implication(canonical_goal, implication, minimums); | |
149 | ||
150 | if let (Ok(solution), priority) = res { | |
151 | debug!("ok: solution={:?} prio={:?}", solution, priority); | |
152 | cur_solution = Some(match cur_solution { | |
153 | None => (solution, priority), | |
154 | Some((cur, cur_priority)) => combine::with_priorities( | |
155 | self.interner(), | |
156 | &canonical_goal.canonical.value.goal, | |
157 | cur, | |
158 | cur_priority, | |
159 | solution, | |
160 | priority, | |
161 | ), | |
162 | }); | |
163 | } else { | |
164 | debug!("error"); | |
165 | } | |
166 | } | |
167 | cur_solution.map_or((Err(NoSolution), ClausePriority::High), |(s, p)| (Ok(s), p)) | |
168 | } | |
169 | ||
170 | /// Modus ponens! That is: try to apply an implication by proving its premises. | |
171 | #[instrument(level = "info", skip(self, minimums))] | |
172 | fn solve_via_implication( | |
173 | &mut self, | |
174 | canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>, | |
175 | clause: &Binders<ProgramClauseImplication<I>>, | |
176 | minimums: &mut Minimums, | |
177 | ) -> (Fallible<Solution<I>>, ClausePriority) { | |
178 | let (infer, subst, goal) = self.new_inference_table(canonical_goal); | |
179 | match Fulfill::new_with_clause(self, infer, subst, goal, clause) { | |
180 | Ok(fulfill) => (fulfill.solve(minimums), clause.skip_binders().priority), | |
181 | Err(e) => (Err(e), ClausePriority::High), | |
182 | } | |
183 | } | |
184 | ||
185 | fn new_inference_table<T: Fold<I, I, Result = T> + HasInterner<Interner = I> + Clone>( | |
186 | &self, | |
187 | ucanonical_goal: &UCanonical<InEnvironment<T>>, | |
188 | ) -> ( | |
189 | RecursiveInferenceTableImpl<I>, | |
190 | Substitution<I>, | |
191 | InEnvironment<T::Result>, | |
192 | ) { | |
193 | let (infer, subst, canonical_goal) = InferenceTable::from_canonical( | |
194 | self.interner(), | |
195 | ucanonical_goal.universes, | |
196 | &ucanonical_goal.canonical, | |
197 | ); | |
198 | let infer = RecursiveInferenceTableImpl { infer }; | |
199 | (infer, subst, canonical_goal) | |
200 | } | |
201 | ||
202 | fn program_clauses_for_goal( | |
203 | &self, | |
204 | environment: &Environment<I>, | |
205 | goal: &DomainGoal<I>, | |
206 | ) -> Result<Vec<ProgramClause<I>>, Floundered> { | |
207 | program_clauses_for_goal(self.db(), environment, goal) | |
208 | } | |
209 | } | |
210 | ||
211 | impl<S, I> SolveIterationHelpers<I> for S | |
212 | where | |
213 | S: SolveDatabase<I>, | |
214 | I: Interner, | |
215 | { | |
216 | } | |
217 | ||
218 | struct RecursiveInferenceTableImpl<I: Interner> { | |
219 | infer: InferenceTable<I>, | |
220 | } | |
221 | ||
222 | impl<I: Interner> RecursiveInferenceTable<I> for RecursiveInferenceTableImpl<I> { | |
223 | fn instantiate_binders_universally<'a, T>( | |
224 | &mut self, | |
225 | interner: &'a I, | |
226 | arg: &'a Binders<T>, | |
227 | ) -> T::Result | |
228 | where | |
229 | T: Fold<I> + HasInterner<Interner = I>, | |
230 | { | |
231 | self.infer.instantiate_binders_universally(interner, arg) | |
232 | } | |
233 | ||
234 | fn instantiate_binders_existentially<'a, T>( | |
235 | &mut self, | |
236 | interner: &'a I, | |
237 | arg: &'a Binders<T>, | |
238 | ) -> T::Result | |
239 | where | |
240 | T: Fold<I> + HasInterner<Interner = I>, | |
241 | { | |
242 | self.infer.instantiate_binders_existentially(interner, arg) | |
243 | } | |
244 | ||
245 | fn canonicalize<T>( | |
246 | &mut self, | |
247 | interner: &I, | |
248 | value: &T, | |
249 | ) -> (Canonical<T::Result>, Vec<GenericArg<I>>) | |
250 | where | |
251 | T: Fold<I>, | |
252 | T::Result: HasInterner<Interner = I>, | |
253 | { | |
254 | let res = self.infer.canonicalize(interner, value); | |
255 | let free_vars = res | |
256 | .free_vars | |
257 | .into_iter() | |
258 | .map(|free_var| free_var.to_generic_arg(interner)) | |
259 | .collect(); | |
260 | (res.quantified, free_vars) | |
261 | } | |
262 | ||
263 | fn u_canonicalize<T>( | |
264 | &mut self, | |
265 | interner: &I, | |
266 | value0: &Canonical<T>, | |
267 | ) -> (UCanonical<T::Result>, UniverseMap) | |
268 | where | |
269 | T: HasInterner<Interner = I> + Fold<I> + Visit<I>, | |
270 | T::Result: HasInterner<Interner = I>, | |
271 | { | |
272 | let res = self.infer.u_canonicalize(interner, value0); | |
273 | (res.quantified, res.universes) | |
274 | } | |
275 | ||
276 | fn unify<T>( | |
277 | &mut self, | |
278 | interner: &I, | |
279 | environment: &Environment<I>, | |
280 | a: &T, | |
281 | b: &T, | |
282 | ) -> Fallible<( | |
283 | Vec<InEnvironment<DomainGoal<I>>>, | |
284 | Vec<InEnvironment<Constraint<I>>>, | |
285 | )> | |
286 | where | |
287 | T: ?Sized + Zip<I>, | |
288 | { | |
289 | let res = self.infer.unify(interner, environment, a, b)?; | |
290 | Ok((res.goals, res.constraints)) | |
291 | } | |
292 | ||
293 | fn instantiate_canonical<T>(&mut self, interner: &I, bound: &Canonical<T>) -> T::Result | |
294 | where | |
295 | T: HasInterner<Interner = I> + Fold<I> + Debug, | |
296 | { | |
297 | self.infer.instantiate_canonical(interner, bound) | |
298 | } | |
299 | ||
300 | fn invert_then_canonicalize<T>( | |
301 | &mut self, | |
302 | interner: &I, | |
303 | value: &T, | |
304 | ) -> Option<Canonical<T::Result>> | |
305 | where | |
306 | T: Fold<I, Result = T> + HasInterner<Interner = I>, | |
307 | { | |
308 | self.infer.invert_then_canonicalize(interner, value) | |
309 | } | |
310 | ||
311 | fn needs_truncation(&mut self, interner: &I, max_size: usize, value: impl Visit<I>) -> bool { | |
312 | truncate::needs_truncation(interner, &mut self.infer, max_size, value) | |
313 | } | |
314 | } |