]>
Commit | Line | Data |
---|---|---|
f9f354fc | 1 | use crate::context::{ |
f035d41b | 2 | Context, ContextOps, InferenceTable, ResolventOps, TruncateOps, UnificationOps, |
f9f354fc | 3 | }; |
f9f354fc | 4 | use crate::forest::Forest; |
f9f354fc XL |
5 | use crate::stack::{Stack, StackIndex}; |
6 | use crate::strand::{CanonicalStrand, SelectedSubgoal, Strand}; | |
f035d41b | 7 | use crate::table::{AnswerIndex, Table}; |
f9f354fc | 8 | use crate::{ |
f035d41b XL |
9 | Answer, AnswerMode, CompleteAnswer, ExClause, FlounderedSubgoal, Literal, Minimums, TableIndex, |
10 | TimeStamp, | |
f9f354fc XL |
11 | }; |
12 | ||
f035d41b XL |
13 | use chalk_ir::interner::Interner; |
14 | use chalk_ir::{ | |
1b1a35ee XL |
15 | Canonical, ConstrainedSubst, Floundered, Goal, GoalData, InEnvironment, NoSolution, |
16 | Substitution, UCanonical, UniverseMap, | |
f035d41b XL |
17 | }; |
18 | use tracing::{debug, debug_span, info, instrument}; | |
19 | ||
f9f354fc XL |
20 | type RootSearchResult<T> = Result<T, RootSearchFail>; |
21 | ||
22 | /// The different ways that a *root* search (which potentially pursues | |
23 | /// many strands) can fail. A root search is one that begins with an | |
24 | /// empty stack. | |
25 | #[derive(Debug)] | |
26 | pub(super) enum RootSearchFail { | |
27 | /// The table we were trying to solve cannot succeed. | |
28 | NoMoreSolutions, | |
29 | ||
30 | /// The table cannot be solved without more type information. | |
31 | Floundered, | |
32 | ||
33 | /// We did not find a solution, but we still have things to try. | |
34 | /// Repeat the request, and we'll give one of those a spin. | |
35 | /// | |
36 | /// (In a purely depth-first-based solver, like Prolog, this | |
37 | /// doesn't appear.) | |
38 | QuantumExceeded, | |
39 | ||
40 | /// A negative cycle was found. This is fail-fast, so even if there was | |
41 | /// possibly a solution (ambiguous or not), it may not have been found. | |
42 | NegativeCycle, | |
43 | ||
44 | /// The current answer index is not useful. Currently, this is returned | |
45 | /// because the current answer needs refining. | |
46 | InvalidAnswer, | |
47 | } | |
48 | ||
49 | /// This is returned when we try to select a subgoal for a strand. | |
f035d41b | 50 | #[derive(PartialEq)] |
f9f354fc XL |
51 | enum SubGoalSelection { |
52 | /// A subgoal was successfully selected. It has already been checked | |
53 | /// to not be floundering. However, it may have an answer already, be | |
54 | /// coinductive, or create a cycle. | |
55 | Selected, | |
56 | ||
f035d41b XL |
57 | /// This strand has no remaining subgoals, but there may still be |
58 | /// floundered subgoals. | |
59 | NotSelected, | |
f9f354fc XL |
60 | } |
61 | ||
62 | /// This is returned `on_no_remaining_subgoals` | |
63 | enum NoRemainingSubgoalsResult { | |
64 | /// There is an answer available for the root table | |
65 | RootAnswerAvailable, | |
66 | ||
67 | /// There was a `RootSearchFail` | |
68 | RootSearchFail(RootSearchFail), | |
69 | ||
70 | // This was a success | |
71 | Success, | |
72 | } | |
73 | ||
f035d41b | 74 | impl<I: Interner, C: Context<I>> Forest<I, C> { |
f9f354fc XL |
75 | /// Returns an answer with a given index for the given table. This |
76 | /// may require activating a strand and following it. It returns | |
77 | /// `Ok(answer)` if they answer is available and otherwise a | |
78 | /// `RootSearchFail` result. | |
79 | pub(super) fn root_answer( | |
80 | &mut self, | |
f035d41b | 81 | context: &impl ContextOps<I, C>, |
f9f354fc XL |
82 | table: TableIndex, |
83 | answer_index: AnswerIndex, | |
f035d41b | 84 | ) -> RootSearchResult<CompleteAnswer<I>> { |
f9f354fc XL |
85 | let stack = Stack::default(); |
86 | ||
87 | let mut state = SolveState { | |
88 | forest: self, | |
89 | context, | |
90 | stack, | |
91 | }; | |
92 | ||
93 | match state.ensure_root_answer(table, answer_index) { | |
94 | Ok(()) => { | |
95 | assert!(state.stack.is_empty()); | |
96 | let answer = state.forest.answer(table, answer_index); | |
f035d41b | 97 | if !answer.subst.value.delayed_subgoals.is_empty() { |
f9f354fc XL |
98 | return Err(RootSearchFail::InvalidAnswer); |
99 | } | |
100 | Ok(CompleteAnswer { | |
f035d41b XL |
101 | subst: Canonical { |
102 | binders: answer.subst.binders.clone(), | |
103 | value: ConstrainedSubst { | |
104 | subst: answer.subst.value.subst.clone(), | |
105 | constraints: answer.subst.value.constraints.clone(), | |
106 | }, | |
107 | }, | |
f9f354fc XL |
108 | ambiguous: answer.ambiguous, |
109 | }) | |
110 | } | |
111 | Err(err) => Err(err), | |
112 | } | |
113 | } | |
114 | ||
115 | pub(super) fn any_future_answer( | |
116 | &self, | |
117 | table: TableIndex, | |
118 | answer: AnswerIndex, | |
f035d41b | 119 | mut test: impl FnMut(&Substitution<I>) -> bool, |
f9f354fc XL |
120 | ) -> bool { |
121 | if let Some(answer) = self.tables[table].answer(answer) { | |
122 | info!("answer cached = {:?}", answer); | |
f035d41b | 123 | return test(&answer.subst.value.subst); |
f9f354fc XL |
124 | } |
125 | ||
f035d41b XL |
126 | self.tables[table] |
127 | .strands() | |
128 | .any(|strand| test(&strand.canonical_ex_clause.value.subst)) | |
f9f354fc XL |
129 | } |
130 | ||
f035d41b | 131 | pub(crate) fn answer(&self, table: TableIndex, answer: AnswerIndex) -> &Answer<I> { |
f9f354fc XL |
132 | self.tables[table].answer(answer).unwrap() |
133 | } | |
134 | ||
f035d41b XL |
135 | fn canonicalize_strand( |
136 | context: &impl ContextOps<I, C>, | |
137 | strand: Strand<I, C>, | |
138 | ) -> CanonicalStrand<I> { | |
f9f354fc XL |
139 | let Strand { |
140 | mut infer, | |
141 | ex_clause, | |
142 | selected_subgoal, | |
143 | last_pursued_time, | |
144 | } = strand; | |
145 | Forest::canonicalize_strand_from( | |
146 | context, | |
147 | &mut infer, | |
148 | &ex_clause, | |
149 | selected_subgoal, | |
150 | last_pursued_time, | |
151 | ) | |
152 | } | |
153 | ||
154 | fn canonicalize_strand_from( | |
f035d41b XL |
155 | context: &impl ContextOps<I, C>, |
156 | infer: &mut dyn InferenceTable<I, C>, | |
157 | ex_clause: &ExClause<I>, | |
158 | selected_subgoal: Option<SelectedSubgoal>, | |
f9f354fc | 159 | last_pursued_time: TimeStamp, |
f035d41b | 160 | ) -> CanonicalStrand<I> { |
f9f354fc XL |
161 | let canonical_ex_clause = infer.canonicalize_ex_clause(context.interner(), &ex_clause); |
162 | CanonicalStrand { | |
163 | canonical_ex_clause, | |
164 | selected_subgoal, | |
165 | last_pursued_time, | |
166 | } | |
167 | } | |
168 | ||
169 | /// Given a subgoal, converts the literal into u-canonical form | |
170 | /// and searches for an existing table. If one is found, it is | |
171 | /// returned, but otherwise a new table is created (and populated | |
172 | /// with its initial set of strands). | |
173 | /// | |
174 | /// Returns `None` if the literal cannot be converted into a table | |
175 | /// -- for example, this can occur when we have selected a | |
176 | /// negative literal with free existential variables, in which | |
177 | /// case the execution is said to "flounder". | |
178 | /// | |
179 | /// In terms of the NFTD paper, creating a new table corresponds | |
180 | /// to the *New Subgoal* step as well as the *Program Clause | |
181 | /// Resolution* steps. | |
f035d41b | 182 | #[instrument(level = "debug", skip(self, context, infer))] |
f9f354fc XL |
183 | fn get_or_create_table_for_subgoal( |
184 | &mut self, | |
f035d41b XL |
185 | context: &impl ContextOps<I, C>, |
186 | infer: &mut dyn InferenceTable<I, C>, | |
187 | subgoal: &Literal<I>, | |
188 | ) -> Option<(TableIndex, UniverseMap)> { | |
f9f354fc XL |
189 | // Subgoal abstraction: |
190 | let (ucanonical_subgoal, universe_map) = match subgoal { | |
191 | Literal::Positive(subgoal) => { | |
192 | Forest::abstract_positive_literal(context, infer, subgoal)? | |
193 | } | |
194 | Literal::Negative(subgoal) => { | |
195 | Forest::abstract_negative_literal(context, infer, subgoal)? | |
196 | } | |
197 | }; | |
198 | ||
1b1a35ee | 199 | debug!(?ucanonical_subgoal, ?universe_map); |
f9f354fc XL |
200 | |
201 | let table = self.get_or_create_table_for_ucanonical_goal(context, ucanonical_subgoal); | |
202 | ||
203 | Some((table, universe_map)) | |
204 | } | |
205 | ||
206 | /// Given a u-canonical goal, searches for an existing table. If | |
207 | /// one is found, it is returned, but otherwise a new table is | |
208 | /// created (and populated with its initial set of strands). | |
209 | /// | |
210 | /// In terms of the NFTD paper, creating a new table corresponds | |
211 | /// to the *New Subgoal* step as well as the *Program Clause | |
212 | /// Resolution* steps. | |
f035d41b | 213 | #[instrument(level = "debug", skip(self, context))] |
f9f354fc XL |
214 | pub(crate) fn get_or_create_table_for_ucanonical_goal( |
215 | &mut self, | |
f035d41b XL |
216 | context: &impl ContextOps<I, C>, |
217 | goal: UCanonical<InEnvironment<Goal<I>>>, | |
f9f354fc | 218 | ) -> TableIndex { |
f9f354fc | 219 | if let Some(table) = self.tables.index_of(&goal) { |
1b1a35ee | 220 | debug!(?table, "found existing table"); |
f9f354fc XL |
221 | return table; |
222 | } | |
223 | ||
f035d41b | 224 | info!( |
1b1a35ee XL |
225 | table = ?self.tables.next_index(), |
226 | "creating new table with goal = {:#?}", | |
227 | goal, | |
f9f354fc | 228 | ); |
f035d41b XL |
229 | let table = Self::build_table(context, self.tables.next_index(), goal); |
230 | self.tables.insert(table) | |
f9f354fc XL |
231 | } |
232 | ||
233 | /// When a table is first created, this function is invoked to | |
234 | /// create the initial set of strands. If the table represents a | |
235 | /// domain goal, these strands are created from the program | |
236 | /// clauses as well as the clauses found in the environment. If | |
237 | /// the table represents a non-domain goal, such as `for<T> G` | |
f035d41b | 238 | /// etc, then `simplify_goal` is invoked to create a strand |
f9f354fc XL |
239 | /// that breaks the goal down. |
240 | /// | |
241 | /// In terms of the NFTD paper, this corresponds to the *Program | |
242 | /// Clause Resolution* step being applied eagerly, as many times | |
243 | /// as possible. | |
f035d41b XL |
244 | fn build_table( |
245 | context: &impl ContextOps<I, C>, | |
246 | table_idx: TableIndex, | |
247 | goal: UCanonical<InEnvironment<Goal<I>>>, | |
248 | ) -> Table<I> { | |
249 | let mut table = Table::new(goal.clone(), context.is_coinductive(&goal)); | |
250 | let (mut infer, subst, environment, goal) = context.instantiate_ucanonical_goal(&goal); | |
251 | let goal_data = goal.data(context.interner()); | |
252 | ||
253 | match goal_data { | |
1b1a35ee | 254 | GoalData::DomainGoal(domain_goal) => { |
f9f354fc XL |
255 | match context.program_clauses(&environment, &domain_goal, &mut infer) { |
256 | Ok(clauses) => { | |
257 | for clause in clauses { | |
258 | info!("program clause = {:#?}", clause); | |
259 | let mut infer = infer.clone(); | |
260 | if let Ok(resolvent) = infer.resolvent_clause( | |
261 | context.interner(), | |
262 | &environment, | |
263 | &domain_goal, | |
264 | &subst, | |
265 | &clause, | |
266 | ) { | |
267 | info!("pushing initial strand with ex-clause: {:#?}", &resolvent,); | |
268 | let strand = Strand { | |
269 | infer, | |
270 | ex_clause: resolvent, | |
271 | selected_subgoal: None, | |
272 | last_pursued_time: TimeStamp::default(), | |
273 | }; | |
274 | let canonical_strand = Self::canonicalize_strand(context, strand); | |
f035d41b | 275 | table.enqueue_strand(canonical_strand); |
f9f354fc XL |
276 | } |
277 | } | |
278 | } | |
279 | Err(Floundered) => { | |
f035d41b | 280 | debug!( |
1b1a35ee | 281 | table = ?table_idx, |
f035d41b XL |
282 | "Marking table {:?} as floundered! (failed to create program clauses)", |
283 | table_idx | |
284 | ); | |
285 | table.mark_floundered(); | |
f9f354fc XL |
286 | } |
287 | } | |
288 | } | |
289 | ||
f035d41b XL |
290 | _ => { |
291 | // `canonical_goal` is a goal. We can simplify it | |
f9f354fc XL |
292 | // into a series of *literals*, all of which must be |
293 | // true. Thus, in EWFS terms, we are effectively | |
294 | // creating a single child of the `A :- A` goal that | |
295 | // is like `A :- B, C, D` where B, C, and D are the | |
296 | // simplified subgoals. You can think of this as | |
297 | // applying built-in "meta program clauses" that | |
f035d41b | 298 | // reduce goals into Domain goals. |
f9f354fc | 299 | if let Ok(ex_clause) = |
f035d41b | 300 | Self::simplify_goal(context, &mut infer, subst, environment, goal) |
f9f354fc XL |
301 | { |
302 | info!( | |
1b1a35ee XL |
303 | ex_clause = ?infer.debug_ex_clause(context.interner(), &ex_clause), |
304 | "pushing initial strand" | |
f9f354fc XL |
305 | ); |
306 | let strand = Strand { | |
307 | infer, | |
308 | ex_clause, | |
309 | selected_subgoal: None, | |
310 | last_pursued_time: TimeStamp::default(), | |
311 | }; | |
312 | let canonical_strand = Self::canonicalize_strand(context, strand); | |
f035d41b | 313 | table.enqueue_strand(canonical_strand); |
f9f354fc XL |
314 | } |
315 | } | |
316 | } | |
f035d41b XL |
317 | |
318 | table | |
f9f354fc XL |
319 | } |
320 | ||
321 | /// Given a selected positive subgoal, applies the subgoal | |
322 | /// abstraction function to yield the canonical form that will be | |
323 | /// used to pick a table. Typically, this abstraction has no | |
324 | /// effect, and hence we are simply returning the canonical form | |
325 | /// of `subgoal`; but if the subgoal is getting too big, we return | |
326 | /// `None`, which causes the subgoal to flounder. | |
327 | fn abstract_positive_literal( | |
f035d41b XL |
328 | context: &impl ContextOps<I, C>, |
329 | infer: &mut dyn InferenceTable<I, C>, | |
330 | subgoal: &InEnvironment<Goal<I>>, | |
331 | ) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)> { | |
f9f354fc XL |
332 | if infer.goal_needs_truncation(context.interner(), subgoal) { |
333 | None | |
334 | } else { | |
335 | Some(infer.fully_canonicalize_goal(context.interner(), subgoal)) | |
336 | } | |
337 | } | |
338 | ||
339 | /// Given a selected negative subgoal, the subgoal is "inverted" | |
f035d41b | 340 | /// (see `InferenceTable<I, C>::invert`) and then potentially truncated |
f9f354fc XL |
341 | /// (see `abstract_positive_literal`). The result subgoal is |
342 | /// canonicalized. In some cases, this may return `None` and hence | |
343 | /// fail to yield a useful result, for example if free existential | |
344 | /// variables appear in `subgoal` (in which case the execution is | |
345 | /// said to "flounder"). | |
346 | fn abstract_negative_literal( | |
f035d41b XL |
347 | context: &impl ContextOps<I, C>, |
348 | infer: &mut dyn InferenceTable<I, C>, | |
349 | subgoal: &InEnvironment<Goal<I>>, | |
350 | ) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)> { | |
f9f354fc XL |
351 | // First, we have to check that the selected negative literal |
352 | // is ground, and invert any universally quantified variables. | |
353 | // | |
354 | // DIVERGENCE -- In the RR paper, to ensure completeness, they | |
355 | // permit non-ground negative literals, but only consider | |
356 | // them to succeed when the target table has no answers at | |
357 | // all. This is equivalent inverting those free existentials | |
358 | // into universals, as discussed in the comments of | |
359 | // `invert`. This is clearly *sound*, but the completeness is | |
360 | // a subtle point. In particular, it can cause **us** to reach | |
361 | // false conclusions, because e.g. given a program like | |
362 | // (selected left-to-right): | |
363 | // | |
364 | // not { ?T: Copy }, ?T = Vec<u32> | |
365 | // | |
366 | // we would select `not { ?T: Copy }` first. For this goal to | |
367 | // succeed we would require that -- effectively -- `forall<T> | |
368 | // { not { T: Copy } }`, which clearly doesn't hold. (In the | |
369 | // terms of RR, we would require that the table for `?T: Copy` | |
370 | // has failed before we can continue.) | |
371 | // | |
372 | // In the RR paper, this is acceptable because they assume all | |
373 | // of their input programs are both **normal** (negative | |
374 | // literals are selected after positive ones) and **safe** | |
375 | // (all free variables in negative literals occur in positive | |
376 | // literals). It is plausible for us to guarantee "normal" | |
377 | // form, we can reorder clauses as we need. I suspect we can | |
378 | // guarantee safety too, but I have to think about it. | |
379 | // | |
380 | // For now, we opt for the safer route of terming such | |
381 | // executions as floundering, because I think our use of | |
382 | // negative goals is sufficiently limited we can get away with | |
383 | // it. The practical effect is that we will judge more | |
384 | // executions as floundering than we ought to (i.e., where we | |
385 | // could instead generate an (imprecise) result). As you can | |
386 | // see a bit later, we also diverge in some other aspects that | |
387 | // affect completeness when it comes to subgoal abstraction. | |
388 | let inverted_subgoal = infer.invert_goal(context.interner(), subgoal)?; | |
389 | ||
390 | if infer.goal_needs_truncation(context.interner(), &inverted_subgoal) { | |
391 | None | |
392 | } else { | |
393 | Some(infer.fully_canonicalize_goal(context.interner(), &inverted_subgoal)) | |
394 | } | |
395 | } | |
396 | } | |
397 | ||
f035d41b XL |
398 | pub(crate) struct SolveState<'forest, I: Interner, C: Context<I>, CO: ContextOps<I, C>> { |
399 | forest: &'forest mut Forest<I, C>, | |
f9f354fc | 400 | context: &'forest CO, |
f035d41b | 401 | stack: Stack<I, C>, |
f9f354fc XL |
402 | } |
403 | ||
f035d41b XL |
404 | impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'forest> Drop |
405 | for SolveState<'forest, I, C, CO> | |
f9f354fc XL |
406 | { |
407 | fn drop(&mut self) { | |
408 | if !self.stack.is_empty() { | |
409 | if let Some(active_strand) = self.stack.top().active_strand.take() { | |
410 | let table = self.stack.top().table; | |
411 | let canonical_active_strand = | |
412 | Forest::canonicalize_strand(self.context, active_strand); | |
413 | self.forest.tables[table].enqueue_strand(canonical_active_strand); | |
414 | } | |
415 | self.unwind_stack(); | |
416 | } | |
417 | } | |
418 | } | |
419 | ||
f035d41b XL |
420 | impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'forest> |
421 | SolveState<'forest, I, C, CO> | |
422 | { | |
f9f354fc XL |
423 | /// Ensures that answer with the given index is available from the |
424 | /// given table. Returns `Ok` if there is an answer. | |
425 | /// | |
426 | /// This function first attempts to fetch answer that is cached in | |
427 | /// the table. If none is found, then it will recursively search | |
428 | /// to find an answer. | |
f035d41b | 429 | #[instrument(level = "info", skip(self))] |
f9f354fc XL |
430 | fn ensure_root_answer( |
431 | &mut self, | |
432 | initial_table: TableIndex, | |
433 | initial_answer: AnswerIndex, | |
434 | ) -> RootSearchResult<()> { | |
f9f354fc XL |
435 | info!( |
436 | "table goal = {:#?}", | |
437 | self.forest.tables[initial_table].table_goal | |
438 | ); | |
439 | // Check if this table has floundered. | |
440 | if self.forest.tables[initial_table].is_floundered() { | |
441 | return Err(RootSearchFail::Floundered); | |
442 | } | |
443 | // Check for a tabled answer. | |
444 | if let Some(answer) = self.forest.tables[initial_table].answer(initial_answer) { | |
445 | info!("answer cached = {:?}", answer); | |
446 | return Ok(()); | |
447 | } | |
448 | ||
449 | // If no tabled answer is present, we ought to be requesting | |
450 | // the next available index. | |
451 | assert_eq!( | |
452 | self.forest.tables[initial_table].next_answer_index(), | |
453 | initial_answer | |
454 | ); | |
455 | ||
456 | self.stack | |
457 | .push(initial_table, Minimums::MAX, self.forest.increment_clock()); | |
458 | loop { | |
f9f354fc XL |
459 | let clock = self.stack.top().clock; |
460 | // If we had an active strand, continue to pursue it | |
461 | let table = self.stack.top().table; | |
f035d41b | 462 | let table_answer_mode = self.forest.tables[table].answer_mode; |
f9f354fc XL |
463 | |
464 | // We track when we last pursued each strand. If all the strands have been | |
465 | // pursued at this depth, then that means they all encountered a cycle. | |
466 | // We also know that if the first strand has been pursued at this depth, | |
467 | // then all have. Otherwise, an answer to any strand would have provided an | |
468 | // answer for the table. | |
f035d41b XL |
469 | let num_universes = self.forest.tables[table].table_goal.universes; |
470 | let forest = &mut self.forest; | |
471 | let context = &self.context; | |
f9f354fc | 472 | let next_strand = self.stack.top().active_strand.take().or_else(|| { |
f035d41b XL |
473 | forest.tables[table] |
474 | .dequeue_next_strand_that(|strand| { | |
475 | let (_, ex_clause) = context | |
476 | .instantiate_ex_clause(num_universes, &strand.canonical_ex_clause); | |
477 | let time_eligble = strand.last_pursued_time < clock; | |
478 | let mode_eligble = match (table_answer_mode, ex_clause.ambiguous) { | |
479 | (AnswerMode::Complete, false) => true, | |
480 | (AnswerMode::Complete, true) => false, | |
481 | (AnswerMode::Ambiguous, _) => true, | |
482 | }; | |
483 | time_eligble && mode_eligble | |
484 | }) | |
f9f354fc | 485 | .map(|canonical_strand| { |
f9f354fc XL |
486 | let CanonicalStrand { |
487 | canonical_ex_clause, | |
488 | selected_subgoal, | |
489 | last_pursued_time, | |
490 | } = canonical_strand; | |
f035d41b XL |
491 | let (infer, ex_clause) = |
492 | context.instantiate_ex_clause(num_universes, &canonical_ex_clause); | |
1b1a35ee | 493 | Strand { |
f9f354fc XL |
494 | infer, |
495 | ex_clause, | |
1b1a35ee | 496 | selected_subgoal, |
f9f354fc | 497 | last_pursued_time, |
1b1a35ee | 498 | } |
f9f354fc XL |
499 | }) |
500 | }); | |
501 | match next_strand { | |
502 | Some(mut strand) => { | |
1b1a35ee | 503 | debug!("starting next strand = {:#?}", strand); |
f9f354fc XL |
504 | |
505 | strand.last_pursued_time = clock; | |
506 | match self.select_subgoal(&mut strand) { | |
507 | SubGoalSelection::Selected => { | |
508 | // A subgoal has been selected. We now check this subgoal | |
509 | // table for an existing answer or if it's in a cycle. | |
510 | // If neither of those are the case, a strand is selected | |
511 | // and the next loop iteration happens. | |
512 | self.on_subgoal_selected(strand)?; | |
513 | continue; | |
514 | } | |
f035d41b | 515 | SubGoalSelection::NotSelected => { |
f9f354fc XL |
516 | match self.on_no_remaining_subgoals(strand) { |
517 | NoRemainingSubgoalsResult::RootAnswerAvailable => return Ok(()), | |
518 | NoRemainingSubgoalsResult::RootSearchFail(e) => return Err(e), | |
f035d41b | 519 | NoRemainingSubgoalsResult::Success => continue, |
f9f354fc | 520 | }; |
f9f354fc XL |
521 | } |
522 | } | |
523 | } | |
524 | None => { | |
525 | self.on_no_strands_left()?; | |
526 | continue; | |
527 | } | |
528 | } | |
529 | } | |
530 | } | |
531 | ||
532 | /// This is called when an answer is available for the selected subgoal | |
533 | /// of the strand. First, if the selected subgoal is a `Positive` subgoal, | |
534 | /// it first clones the strand pursuing the next answer. Then, it merges the | |
535 | /// answer into the provided `Strand`. | |
536 | /// On success, `Ok` is returned and the `Strand` can be continued to process | |
537 | /// On failure, `Err` is returned and the `Strand` should be discarded | |
f035d41b | 538 | fn merge_answer_into_strand(&mut self, strand: &mut Strand<I, C>) -> RootSearchResult<()> { |
f9f354fc XL |
539 | // At this point, we know we have an answer for |
540 | // the selected subgoal of the strand. | |
541 | // Now, we have to unify that answer onto the strand. | |
542 | ||
f035d41b XL |
543 | // If this answer is ambiguous and we don't want ambiguous answers |
544 | // yet, then we act like this is a floundered subgoal. | |
545 | let ambiguous = { | |
546 | let selected_subgoal = strand.selected_subgoal.as_ref().unwrap(); | |
547 | let answer = self.forest.answer( | |
548 | selected_subgoal.subgoal_table, | |
549 | selected_subgoal.answer_index, | |
550 | ); | |
551 | answer.ambiguous | |
552 | }; | |
553 | if let AnswerMode::Complete = self.forest.tables[self.stack.top().table].answer_mode { | |
554 | if ambiguous { | |
555 | // FIXME: we could try to be a little bit smarter here. This can | |
556 | // really be split into cases: | |
557 | // 1) Cases where no amount of solving will cause this ambiguity to change. | |
558 | // (e.g. `CannnotProve`) | |
559 | // 2) Cases where we may be able to get a better answer if we | |
560 | // solve other subgoals first. | |
561 | // (e.g. the `non_enumerable_traits_reorder` test) | |
562 | // We really only need to delay merging an ambiguous answer for | |
563 | // case 2. Do note, though, that even if we *do* merge the answer | |
564 | // case 1, we should stop solving this strand when in | |
565 | // `AnswerMode::Complete` since we wouldn't use this answer yet | |
566 | // *anyways*. | |
567 | ||
568 | // The selected subgoal returned an ambiguous answer, but we don't want that. | |
569 | // So, we treat this subgoal as floundered. | |
570 | let selected_subgoal = strand.selected_subgoal.take().unwrap(); | |
571 | self.flounder_subgoal(&mut strand.ex_clause, selected_subgoal.subgoal_index); | |
572 | return Ok(()); | |
573 | } | |
574 | } | |
575 | ||
f9f354fc | 576 | // If this subgoal was a `Positive` one, whichever way this |
f035d41b XL |
577 | // particular answer turns out, there may yet be *more* answers, |
578 | // if this isn't a trivial substitution. | |
f9f354fc XL |
579 | // Enqueue that alternative for later. |
580 | // NOTE: this is separate from the match below because we `take` the selected_subgoal | |
581 | // below, but here we keep it for the new `Strand`. | |
582 | let selected_subgoal = strand.selected_subgoal.as_ref().unwrap(); | |
583 | if let Literal::Positive(_) = strand.ex_clause.subgoals[selected_subgoal.subgoal_index] { | |
f035d41b XL |
584 | let answer = self.forest.answer( |
585 | selected_subgoal.subgoal_table, | |
586 | selected_subgoal.answer_index, | |
587 | ); | |
588 | if !self.context.is_trivial_substitution( | |
589 | &self.forest.tables[selected_subgoal.subgoal_table].table_goal, | |
590 | &answer.subst, | |
591 | ) { | |
592 | let mut next_subgoal = selected_subgoal.clone(); | |
593 | next_subgoal.answer_index.increment(); | |
594 | let next_strand = Strand { | |
595 | infer: strand.infer.clone(), | |
596 | ex_clause: strand.ex_clause.clone(), | |
597 | selected_subgoal: Some(next_subgoal), | |
1b1a35ee | 598 | last_pursued_time: strand.last_pursued_time, |
f035d41b XL |
599 | }; |
600 | let table = self.stack.top().table; | |
601 | let canonical_next_strand = Forest::canonicalize_strand(self.context, next_strand); | |
602 | self.forest.tables[table].enqueue_strand(canonical_next_strand); | |
603 | } | |
f9f354fc XL |
604 | } |
605 | ||
606 | // Deselect and remove the selected subgoal, now that we have an answer for it. | |
607 | let selected_subgoal = strand.selected_subgoal.take().unwrap(); | |
608 | let subgoal = strand | |
609 | .ex_clause | |
610 | .subgoals | |
611 | .remove(selected_subgoal.subgoal_index); | |
612 | match subgoal { | |
613 | Literal::Positive(subgoal) => { | |
614 | let SelectedSubgoal { | |
615 | subgoal_index: _, | |
616 | subgoal_table, | |
617 | answer_index, | |
618 | ref universe_map, | |
619 | } = selected_subgoal; | |
620 | let table_goal = &self.context.map_goal_from_canonical( | |
621 | &universe_map, | |
f035d41b | 622 | &self.forest.tables[subgoal_table].table_goal.canonical, |
f9f354fc XL |
623 | ); |
624 | let answer_subst = &self.context.map_subst_from_canonical( | |
625 | &universe_map, | |
626 | &self.forest.answer(subgoal_table, answer_index).subst, | |
627 | ); | |
628 | match strand.infer.apply_answer_subst( | |
629 | self.context.interner(), | |
630 | &mut strand.ex_clause, | |
631 | &subgoal, | |
632 | table_goal, | |
633 | answer_subst, | |
634 | ) { | |
635 | Ok(()) => { | |
636 | let Strand { | |
637 | infer: _, | |
638 | ex_clause, | |
639 | selected_subgoal: _, | |
640 | last_pursued_time: _, | |
641 | } = strand; | |
642 | ||
643 | // If the answer had was ambiguous, we have to | |
644 | // ensure that `ex_clause` is also ambiguous. This is | |
645 | // the SLG FACTOR operation, though NFTD just makes it | |
646 | // part of computing the SLG resolvent. | |
647 | if self.forest.answer(subgoal_table, answer_index).ambiguous { | |
f035d41b | 648 | debug!("Marking Strand as ambiguous because answer to (positive) subgoal was ambiguous"); |
f9f354fc XL |
649 | ex_clause.ambiguous = true; |
650 | } | |
651 | ||
652 | // Increment the answer time for the `ex_clause`. Floundered | |
653 | // subgoals may be eligble to be pursued again. | |
654 | ex_clause.answer_time.increment(); | |
655 | ||
656 | // Ok, we've applied the answer to this Strand. | |
657 | return Ok(()); | |
658 | } | |
659 | ||
660 | // This answer led nowhere. Give up for now, but of course | |
661 | // there may still be other strands to pursue, so return | |
662 | // `QuantumExceeded`. | |
663 | Err(NoSolution) => { | |
664 | info!("answer not unifiable -> NoSolution"); | |
665 | // This strand as no solution. It is no longer active, | |
666 | // so it dropped at the end of this scope. | |
667 | ||
668 | // Now we want to propogate back to the up with `QuantumExceeded` | |
669 | self.unwind_stack(); | |
670 | return Err(RootSearchFail::QuantumExceeded); | |
671 | } | |
672 | } | |
673 | } | |
674 | Literal::Negative(_) => { | |
675 | let SelectedSubgoal { | |
676 | subgoal_index: _, | |
677 | subgoal_table, | |
678 | answer_index, | |
679 | universe_map: _, | |
680 | } = selected_subgoal; | |
681 | // We got back an answer. This is bad, because we want | |
682 | // to disprove the subgoal, but it may be | |
683 | // "conditional" (maybe true, maybe not). | |
684 | let answer = self.forest.answer(subgoal_table, answer_index); | |
685 | ||
686 | // By construction, we do not expect negative subgoals | |
687 | // to have delayed subgoals. This is because we do not | |
688 | // need to permit `not { L }` where `L` is a | |
689 | // coinductive goal. We could improve this if needed, | |
690 | // but it keeps things simple. | |
f035d41b | 691 | if !answer.subst.value.delayed_subgoals.is_empty() { |
f9f354fc XL |
692 | panic!("Negative subgoal had delayed_subgoals"); |
693 | } | |
694 | ||
695 | if !answer.ambiguous { | |
696 | // We want to disproval the subgoal, but we | |
697 | // have an unconditional answer for the subgoal, | |
698 | // therefore we have failed to disprove it. | |
699 | info!("found unconditional answer to neg literal -> NoSolution"); | |
700 | ||
701 | // This strand as no solution. By returning an Err, | |
702 | // the caller should discard this `Strand`. | |
703 | ||
704 | // Now we want to propogate back to the up with `QuantumExceeded` | |
705 | self.unwind_stack(); | |
706 | return Err(RootSearchFail::QuantumExceeded); | |
707 | } | |
708 | ||
709 | // Otherwise, the answer is ambiguous. We can keep going, | |
710 | // but we have to mark our strand, too, as ambiguous. | |
711 | // | |
712 | // We want to disproval the subgoal, but we | |
713 | // have an unconditional answer for the subgoal, | |
714 | // therefore we have failed to disprove it. | |
1b1a35ee | 715 | debug!(?strand, "Marking Strand as ambiguous because answer to (negative) subgoal was ambiguous"); |
f9f354fc XL |
716 | strand.ex_clause.ambiguous = true; |
717 | ||
718 | // Strand is ambigious. | |
719 | return Ok(()); | |
720 | } | |
721 | }; | |
722 | } | |
723 | ||
724 | /// This is called when the selected subgoal for a strand has floundered. | |
725 | /// We have to decide what this means for the strand. | |
726 | /// - If the strand was positively dependent on the subgoal, we flounder, | |
727 | /// the subgoal, then return `false`. This strand may be able to be | |
728 | /// retried later. | |
729 | /// - If the strand was negatively dependent on the subgoal, then strand | |
730 | /// has led nowhere of interest and we return `true`. This strand should | |
731 | /// be discarded. | |
732 | /// | |
733 | /// In other words, we return whether this strand flounders. | |
f035d41b | 734 | fn propagate_floundered_subgoal(&mut self, strand: &mut Strand<I, C>) -> bool { |
f9f354fc XL |
735 | // This subgoal selection for the strand is finished, so take it |
736 | let selected_subgoal = strand.selected_subgoal.take().unwrap(); | |
737 | match strand.ex_clause.subgoals[selected_subgoal.subgoal_index] { | |
738 | Literal::Positive(_) => { | |
739 | // If this strand depends on this positively, then we can | |
740 | // come back to it later. So, we mark that subgoal as | |
741 | // floundered and yield `QuantumExceeded` up the stack | |
742 | ||
743 | // If this subgoal floundered, push it onto the | |
744 | // floundered list, along with the time that it | |
745 | // floundered. We'll try to solve some other subgoals | |
746 | // and maybe come back to it. | |
747 | self.flounder_subgoal(&mut strand.ex_clause, selected_subgoal.subgoal_index); | |
748 | ||
1b1a35ee | 749 | false |
f9f354fc XL |
750 | } |
751 | Literal::Negative(_) => { | |
752 | // Floundering on a negative literal isn't like a | |
753 | // positive search: we only pursue negative literals | |
754 | // when we already know precisely the type we are | |
755 | // looking for. So there's no point waiting for other | |
756 | // subgoals, we'll never recover more information. | |
757 | // | |
758 | // In fact, floundering on negative searches shouldn't | |
759 | // normally happen, since there are no uninferred | |
760 | // variables in the goal, but it can with forall | |
761 | // goals: | |
762 | // | |
763 | // forall<T> { not { T: Debug } } | |
764 | // | |
765 | // Here, the table we will be searching for answers is | |
766 | // `?T: Debug`, so it could well flounder. | |
767 | ||
768 | // This strand has no solution. It is no longer active, | |
769 | // so it dropped at the end of this scope. | |
770 | ||
1b1a35ee | 771 | true |
f9f354fc XL |
772 | } |
773 | } | |
774 | } | |
775 | ||
776 | /// This is called if the selected subgoal for a `Strand` is | |
777 | /// a coinductive cycle. | |
f035d41b | 778 | fn on_coinductive_subgoal(&mut self, mut strand: Strand<I, C>) -> Result<(), RootSearchFail> { |
f9f354fc XL |
779 | // This is a co-inductive cycle. That is, this table |
780 | // appears somewhere higher on the stack, and has now | |
781 | // recursively requested an answer for itself. This | |
782 | // means that we have to delay this subgoal until we | |
783 | // reach a trivial self-cycle. | |
784 | ||
785 | // This subgoal selection for the strand is finished, so take it | |
786 | let selected_subgoal = strand.selected_subgoal.take().unwrap(); | |
787 | match strand | |
788 | .ex_clause | |
789 | .subgoals | |
790 | .remove(selected_subgoal.subgoal_index) | |
791 | { | |
792 | Literal::Positive(subgoal) => { | |
793 | // We delay this subgoal | |
794 | let table = self.stack.top().table; | |
795 | assert!( | |
796 | self.forest.tables[table].coinductive_goal | |
797 | && self.forest.tables[selected_subgoal.subgoal_table].coinductive_goal | |
798 | ); | |
799 | ||
800 | strand.ex_clause.delayed_subgoals.push(subgoal); | |
801 | ||
802 | self.stack.top().active_strand = Some(strand); | |
1b1a35ee | 803 | Ok(()) |
f9f354fc XL |
804 | } |
805 | Literal::Negative(_) => { | |
806 | // We don't allow coinduction for negative literals | |
807 | info!("found coinductive answer to negative literal"); | |
808 | panic!("Coinductive cycle with negative literal"); | |
809 | } | |
810 | } | |
811 | } | |
812 | ||
813 | /// This is called if the selected subgoal for `strand` is | |
814 | /// a positive, non-coinductive cycle. | |
815 | /// | |
816 | /// # Parameters | |
817 | /// | |
818 | /// * `strand` the strand from the top of the stack we are pursuing | |
819 | /// * `minimums` is the collected minimum clock times | |
820 | fn on_positive_cycle( | |
821 | &mut self, | |
f035d41b | 822 | strand: Strand<I, C>, |
f9f354fc XL |
823 | minimums: Minimums, |
824 | ) -> Result<(), RootSearchFail> { | |
825 | // We can't take this because we might need it later to clear the cycle | |
826 | let selected_subgoal = strand.selected_subgoal.as_ref().unwrap(); | |
827 | ||
828 | match strand.ex_clause.subgoals[selected_subgoal.subgoal_index] { | |
829 | Literal::Positive(_) => { | |
830 | self.stack.top().cyclic_minimums.take_minimums(&minimums); | |
831 | } | |
832 | Literal::Negative(_) => { | |
833 | // We depend on `not(subgoal)`. For us to continue, | |
834 | // `subgoal` must be completely evaluated. Therefore, | |
835 | // we depend (negatively) on the minimum link of | |
836 | // `subgoal` as a whole -- it doesn't matter whether | |
837 | // it's pos or neg. | |
838 | let mins = Minimums { | |
839 | positive: self.stack.top().clock, | |
840 | negative: minimums.minimum_of_pos_and_neg(), | |
841 | }; | |
842 | self.stack.top().cyclic_minimums.take_minimums(&mins); | |
843 | } | |
844 | } | |
845 | ||
846 | // Ok, we've taken the minimums from this cycle above. Now, | |
847 | // we just return the strand to the table. The table only | |
848 | // pulls strands if they have not been checked at this | |
849 | // depth. | |
850 | // | |
851 | // We also can't mark these and return early from this | |
852 | // because the stack above us might change. | |
853 | let table = self.stack.top().table; | |
854 | let canonical_strand = Forest::canonicalize_strand(self.context, strand); | |
855 | self.forest.tables[table].enqueue_strand(canonical_strand); | |
856 | ||
857 | // The strand isn't active, but the table is, so just continue | |
858 | Ok(()) | |
859 | } | |
860 | ||
861 | /// Invoked after we've selected a (new) subgoal for the top-most | |
862 | /// strand. Attempts to pursue this selected subgoal. | |
863 | /// | |
864 | /// Returns: | |
865 | /// | |
866 | /// * `Ok` if we should keep searching. | |
867 | /// * `Err` if the subgoal failed in some way such that the strand can be abandoned. | |
f035d41b | 868 | fn on_subgoal_selected(&mut self, mut strand: Strand<I, C>) -> Result<(), RootSearchFail> { |
f9f354fc XL |
869 | // This may be a newly selected subgoal or an existing selected subgoal. |
870 | ||
871 | let SelectedSubgoal { | |
872 | subgoal_index: _, | |
873 | subgoal_table, | |
874 | answer_index, | |
875 | universe_map: _, | |
876 | } = *strand.selected_subgoal.as_ref().unwrap(); | |
877 | ||
878 | debug!( | |
1b1a35ee XL |
879 | ?subgoal_table, |
880 | goal = ?self.forest.tables[subgoal_table].table_goal, | |
881 | "table selection {:?} with goal: {:?}", | |
f9f354fc XL |
882 | subgoal_table, self.forest.tables[subgoal_table].table_goal |
883 | ); | |
884 | ||
885 | // This is checked inside select_subgoal | |
886 | assert!(!self.forest.tables[subgoal_table].is_floundered()); | |
887 | ||
888 | // Check for a tabled answer. | |
889 | if let Some(answer) = self.forest.tables[subgoal_table].answer(answer_index) { | |
890 | info!("answer cached = {:?}", answer); | |
891 | ||
892 | // There was a previous answer available for this table | |
893 | // We need to check if we can merge it into the current `Strand`. | |
894 | match self.merge_answer_into_strand(&mut strand) { | |
895 | Err(e) => { | |
1b1a35ee | 896 | debug!(?strand, "could not merge into current strand"); |
f9f354fc XL |
897 | drop(strand); |
898 | return Err(e); | |
899 | } | |
900 | Ok(_) => { | |
1b1a35ee | 901 | debug!(?strand, "merged answer into current strand"); |
f9f354fc XL |
902 | self.stack.top().active_strand = Some(strand); |
903 | return Ok(()); | |
904 | } | |
905 | } | |
906 | } | |
907 | ||
908 | // If no tabled answer is present, we ought to be requesting | |
909 | // the next available index. | |
910 | assert_eq!( | |
911 | self.forest.tables[subgoal_table].next_answer_index(), | |
912 | answer_index | |
913 | ); | |
914 | ||
915 | // Next, check if the table is already active. If so, then we | |
916 | // have a recursive attempt. | |
917 | if let Some(cyclic_depth) = self.stack.is_active(subgoal_table) { | |
918 | info!("cycle detected at depth {:?}", cyclic_depth); | |
919 | let minimums = Minimums { | |
920 | positive: self.stack[cyclic_depth].clock, | |
921 | negative: TimeStamp::MAX, | |
922 | }; | |
923 | ||
924 | if self.top_of_stack_is_coinductive_from(cyclic_depth) { | |
925 | debug!("table is coinductive"); | |
926 | return self.on_coinductive_subgoal(strand); | |
927 | } | |
928 | ||
929 | debug!("table encountered a positive cycle"); | |
930 | return self.on_positive_cycle(strand, minimums); | |
931 | } | |
932 | ||
933 | // We don't know anything about the selected subgoal table. | |
934 | // Set this strand as active and push it onto the stack. | |
935 | self.stack.top().active_strand = Some(strand); | |
936 | ||
937 | let cyclic_minimums = Minimums::MAX; | |
938 | self.stack.push( | |
939 | subgoal_table, | |
940 | cyclic_minimums, | |
941 | self.forest.increment_clock(), | |
942 | ); | |
943 | Ok(()) | |
944 | } | |
945 | ||
f035d41b XL |
946 | /// This is called when there are no remaining subgoals for a strand, so |
947 | /// it represents an answer. If the strand is ambiguous and we don't want | |
948 | /// it yet, we just enqueue it again to pick it up later. Otherwise, we | |
949 | /// add the answer from the strand onto the table. | |
950 | fn on_no_remaining_subgoals(&mut self, strand: Strand<I, C>) -> NoRemainingSubgoalsResult { | |
951 | let ambiguous = strand.ex_clause.ambiguous; | |
952 | if let AnswerMode::Complete = self.forest.tables[self.stack.top().table].answer_mode { | |
953 | if ambiguous { | |
954 | // The strand can only return an ambiguous answer, but we don't | |
955 | // want that right now, so requeue and we'll deal with it later. | |
956 | let canonical_strand = Forest::canonicalize_strand(self.context, strand); | |
957 | self.forest.tables[self.stack.top().table].enqueue_strand(canonical_strand); | |
958 | return NoRemainingSubgoalsResult::RootSearchFail(RootSearchFail::QuantumExceeded); | |
959 | } | |
960 | } | |
1b1a35ee | 961 | let floundered = !strand.ex_clause.floundered_subgoals.is_empty(); |
f035d41b XL |
962 | if floundered { |
963 | debug!("all remaining subgoals floundered for the table"); | |
964 | } else { | |
965 | debug!("no remaining subgoals for the table"); | |
966 | }; | |
f9f354fc XL |
967 | match self.pursue_answer(strand) { |
968 | Some(answer_index) => { | |
969 | debug!("answer is available"); | |
970 | ||
971 | // We found an answer for this strand, and therefore an | |
972 | // answer for this table. Now, this table was either a | |
973 | // subgoal for another strand, or was the root table. | |
974 | let table = self.stack.top().table; | |
f035d41b XL |
975 | match self.stack.pop_and_take_caller_strand() { |
976 | Some(caller_strand) => { | |
977 | self.stack.top().active_strand = Some(caller_strand); | |
1b1a35ee | 978 | NoRemainingSubgoalsResult::Success |
f035d41b | 979 | } |
f9f354fc XL |
980 | None => { |
981 | // That was the root table, so we are done -- | |
982 | // *well*, unless there were delayed | |
983 | // subgoals. In that case, we want to evaluate | |
984 | // those delayed subgoals to completion, so we | |
985 | // have to create a fresh strand that will | |
986 | // take them as goals. Note that we *still | |
987 | // need the original answer in place*, because | |
988 | // we might have to build on it (see the | |
989 | // Delayed Trivial Self Cycle, Variant 3 | |
990 | // example). | |
f9f354fc XL |
991 | |
992 | let answer = self.forest.answer(table, answer_index); | |
f035d41b | 993 | if let Some(strand) = self.create_refinement_strand(table, answer) { |
f9f354fc XL |
994 | self.forest.tables[table].enqueue_strand(strand); |
995 | } | |
996 | ||
1b1a35ee | 997 | NoRemainingSubgoalsResult::RootAnswerAvailable |
f9f354fc | 998 | } |
1b1a35ee | 999 | } |
f9f354fc XL |
1000 | } |
1001 | None => { | |
1002 | debug!("answer is not available (or not new)"); | |
1003 | ||
f035d41b XL |
1004 | // This strand led nowhere of interest. There might be *other* |
1005 | // answers on this table, but we don't care right now, we'll | |
1006 | // try again at another time. | |
f9f354fc XL |
1007 | |
1008 | // Now we yield with `QuantumExceeded` | |
1009 | self.unwind_stack(); | |
1b1a35ee | 1010 | NoRemainingSubgoalsResult::RootSearchFail(RootSearchFail::QuantumExceeded) |
f9f354fc | 1011 | } |
1b1a35ee | 1012 | } |
f9f354fc XL |
1013 | } |
1014 | ||
1015 | /// A "refinement" strand is used in coinduction. When the root | |
1016 | /// table on the stack publishes an answer has delayed subgoals, | |
1017 | /// we create a new strand that will attempt to prove out those | |
1018 | /// delayed subgoals (the root answer here is not *special* except | |
1019 | /// in so far as that there is nothing above it, and hence we know | |
1020 | /// that the delayed subgoals (which resulted in some cycle) must | |
1021 | /// be referring to a table that now has completed). | |
1022 | /// | |
1023 | /// Note that it is important for this to be a *refinement* strand | |
1024 | /// -- meaning that the answer with delayed subgoals has been | |
1025 | /// published. This is necessary because sometimes the strand must | |
1026 | /// build on that very answer that it is refining. See Delayed | |
1027 | /// Trivial Self Cycle, Variant 3. | |
1028 | fn create_refinement_strand( | |
1029 | &self, | |
1030 | table: TableIndex, | |
f035d41b XL |
1031 | answer: &Answer<I>, |
1032 | ) -> Option<CanonicalStrand<I>> { | |
f9f354fc XL |
1033 | // If there are no delayed subgoals, then there is no need for |
1034 | // a refinement strand. | |
f035d41b | 1035 | if answer.subst.value.delayed_subgoals.is_empty() { |
f9f354fc XL |
1036 | return None; |
1037 | } | |
1038 | ||
f035d41b | 1039 | let num_universes = self.forest.tables[table].table_goal.universes; |
f9f354fc XL |
1040 | let (table, subst, constraints, delayed_subgoals) = self |
1041 | .context | |
1042 | .instantiate_answer_subst(num_universes, &answer.subst); | |
1043 | ||
f035d41b | 1044 | let delayed_subgoals = delayed_subgoals |
f9f354fc | 1045 | .into_iter() |
f9f354fc XL |
1046 | .map(Literal::Positive) |
1047 | .collect(); | |
1048 | ||
1049 | let strand = Strand { | |
1050 | infer: table, | |
1051 | ex_clause: ExClause { | |
1052 | subst, | |
1053 | ambiguous: answer.ambiguous, | |
1054 | constraints, | |
f035d41b | 1055 | subgoals: delayed_subgoals, |
f9f354fc XL |
1056 | delayed_subgoals: Vec::new(), |
1057 | answer_time: TimeStamp::default(), | |
1058 | floundered_subgoals: Vec::new(), | |
1059 | }, | |
1060 | selected_subgoal: None, | |
1061 | last_pursued_time: TimeStamp::default(), | |
1062 | }; | |
1063 | ||
1064 | Some(Forest::canonicalize_strand(self.context, strand)) | |
1065 | } | |
1066 | ||
f9f354fc | 1067 | fn on_no_strands_left(&mut self) -> Result<(), RootSearchFail> { |
1b1a35ee XL |
1068 | let table = self.stack.top().table; |
1069 | debug!("no more strands available (or all cycles) for {:?}", table); | |
f9f354fc XL |
1070 | |
1071 | // No more strands left to try! This is either because all | |
f035d41b XL |
1072 | // strands have failed, because all strands encountered a |
1073 | // cycle, or all strands have would give ambiguous answers. | |
f9f354fc | 1074 | |
f9f354fc XL |
1075 | if self.forest.tables[table].strands_mut().count() == 0 { |
1076 | // All strands for the table T on the top of the stack | |
1077 | // have **failed**. Hence we can pop it off the stack and | |
1078 | // check what this means for the table T' that was just | |
1079 | // below T on the stack (if any). | |
1080 | debug!("no more strands available"); | |
1081 | let caller_strand = match self.stack.pop_and_borrow_caller_strand() { | |
1082 | Some(s) => s, | |
1083 | None => { | |
1084 | // T was the root table, so we are done. | |
1085 | debug!("no more solutions"); | |
1086 | return Err(RootSearchFail::NoMoreSolutions); | |
1087 | } | |
1088 | }; | |
1089 | ||
1090 | // This subgoal selection for the strand is finished, so take it | |
1091 | let caller_selected_subgoal = caller_strand.selected_subgoal.take().unwrap(); | |
1092 | return match caller_strand.ex_clause.subgoals[caller_selected_subgoal.subgoal_index] { | |
1093 | // T' wanted an answer from T, but none is | |
1094 | // forthcoming. Therefore, the active strand from T' | |
1095 | // has failed and can be discarded. | |
1096 | Literal::Positive(_) => { | |
1097 | debug!("discarding strand because positive literal"); | |
1098 | self.stack.top().active_strand.take(); | |
1099 | self.unwind_stack(); | |
1100 | Err(RootSearchFail::QuantumExceeded) | |
1101 | } | |
1102 | ||
1103 | // T' wanted there to be no answer from T, but none is forthcoming. | |
1104 | Literal::Negative(_) => { | |
1105 | debug!("subgoal was proven because negative literal"); | |
1106 | ||
1107 | // There is no solution for this strand. But, this | |
1108 | // is what we want, so can remove this subgoal and | |
1109 | // keep going. | |
1110 | caller_strand | |
1111 | .ex_clause | |
1112 | .subgoals | |
1113 | .remove(caller_selected_subgoal.subgoal_index); | |
1114 | ||
1115 | // This strand is still active, so continue | |
1116 | Ok(()) | |
1117 | } | |
1118 | }; | |
1119 | } | |
1120 | ||
1b1a35ee XL |
1121 | // We can't consider this table as part of a cycle unless we've handled |
1122 | // all strands, not just non-ambiguous ones. See chalk#571. | |
1123 | if let AnswerMode::Complete = self.forest.tables[table].answer_mode { | |
1124 | debug!("Allowing ambiguous answers."); | |
1125 | self.forest.tables[table].answer_mode = AnswerMode::Ambiguous; | |
1126 | return Err(RootSearchFail::QuantumExceeded); | |
f035d41b XL |
1127 | } |
1128 | ||
f9f354fc XL |
1129 | let clock = self.stack.top().clock; |
1130 | let cyclic_minimums = self.stack.top().cyclic_minimums; | |
1131 | if cyclic_minimums.positive >= clock && cyclic_minimums.negative >= clock { | |
1132 | debug!("cycle with no new answers"); | |
1133 | ||
1134 | if cyclic_minimums.negative < TimeStamp::MAX { | |
1135 | // This is a negative cycle. | |
1136 | self.unwind_stack(); | |
1137 | return Err(RootSearchFail::NegativeCycle); | |
1138 | } | |
1139 | ||
1140 | // If all the things that we recursively depend on have | |
1141 | // positive dependencies on things below us in the stack, | |
1142 | // then no more answers are forthcoming. We can clear all | |
1143 | // the strands for those things recursively. | |
1144 | let table = self.stack.top().table; | |
1b1a35ee | 1145 | let cyclic_strands = self.forest.tables[table].take_strands(); |
f9f354fc XL |
1146 | self.clear_strands_after_cycle(cyclic_strands); |
1147 | ||
1148 | // Now we yield with `QuantumExceeded` | |
1149 | self.unwind_stack(); | |
1150 | return Err(RootSearchFail::QuantumExceeded); | |
1151 | } else { | |
1152 | debug!("table part of a cycle"); | |
1153 | ||
1154 | // This table resulted in a positive cycle, so we have | |
1155 | // to check what this means for the subgoal containing | |
1156 | // this strand | |
1157 | let caller_strand = match self.stack.pop_and_borrow_caller_strand() { | |
1158 | Some(s) => s, | |
1159 | None => { | |
1160 | panic!("nothing on the stack but cyclic result"); | |
1161 | } | |
1162 | }; | |
1163 | ||
1164 | // We can't take this because we might need it later to clear the cycle | |
1165 | let caller_selected_subgoal = caller_strand.selected_subgoal.as_ref().unwrap(); | |
1166 | match caller_strand.ex_clause.subgoals[caller_selected_subgoal.subgoal_index] { | |
1167 | Literal::Positive(_) => { | |
1168 | self.stack | |
1169 | .top() | |
1170 | .cyclic_minimums | |
1171 | .take_minimums(&cyclic_minimums); | |
1172 | } | |
1173 | Literal::Negative(_) => { | |
1174 | // We depend on `not(subgoal)`. For us to continue, | |
1175 | // `subgoal` must be completely evaluated. Therefore, | |
1176 | // we depend (negatively) on the minimum link of | |
1177 | // `subgoal` as a whole -- it doesn't matter whether | |
1178 | // it's pos or neg. | |
1179 | let mins = Minimums { | |
1180 | positive: self.stack.top().clock, | |
1181 | negative: cyclic_minimums.minimum_of_pos_and_neg(), | |
1182 | }; | |
1183 | self.stack.top().cyclic_minimums.take_minimums(&mins); | |
1184 | } | |
1185 | } | |
1186 | ||
1187 | // We can't pursue this strand anymore, so push it back onto the table | |
1188 | let active_strand = self.stack.top().active_strand.take().unwrap(); | |
1189 | let table = self.stack.top().table; | |
1190 | let canonical_active_strand = Forest::canonicalize_strand(self.context, active_strand); | |
1191 | self.forest.tables[table].enqueue_strand(canonical_active_strand); | |
1192 | ||
1193 | // The strand isn't active, but the table is, so just continue | |
1194 | return Ok(()); | |
1195 | } | |
1196 | } | |
1197 | ||
1198 | /// Unwinds the entire stack, returning all active strands back to | |
1199 | /// their tables (this time at the end of the queue). | |
1200 | fn unwind_stack(&mut self) { | |
1201 | loop { | |
1202 | match self.stack.pop_and_take_caller_strand() { | |
1203 | Some(active_strand) => { | |
1204 | let table = self.stack.top().table; | |
1205 | let canonical_active_strand = | |
1206 | Forest::canonicalize_strand(self.context, active_strand); | |
1207 | self.forest.tables[table].enqueue_strand(canonical_active_strand); | |
1208 | } | |
1209 | ||
1210 | None => return, | |
1211 | } | |
1212 | } | |
1213 | } | |
1214 | ||
1215 | /// Invoked after we have determined that every strand in `table` | |
1216 | /// encounters a cycle; `strands` is the set of strands (which | |
1217 | /// have been moved out of the table). This method then | |
1218 | /// recursively clears the active strands from the tables | |
1219 | /// referenced in `strands`, since all of them must encounter | |
1220 | /// cycles too. | |
f035d41b | 1221 | fn clear_strands_after_cycle(&mut self, strands: impl IntoIterator<Item = CanonicalStrand<I>>) { |
f9f354fc XL |
1222 | for strand in strands { |
1223 | let CanonicalStrand { | |
1224 | canonical_ex_clause, | |
1225 | selected_subgoal, | |
1226 | last_pursued_time: _, | |
1227 | } = strand; | |
1228 | let selected_subgoal = selected_subgoal.unwrap_or_else(|| { | |
1229 | panic!( | |
1230 | "clear_strands_after_cycle invoked on strand in table \ | |
1231 | without a selected subgoal: {:?}", | |
1232 | canonical_ex_clause, | |
1233 | ) | |
1234 | }); | |
1235 | ||
1236 | let strand_table = selected_subgoal.subgoal_table; | |
1237 | let strands = self.forest.tables[strand_table].take_strands(); | |
1238 | self.clear_strands_after_cycle(strands); | |
1239 | } | |
1240 | } | |
1241 | ||
f035d41b | 1242 | fn select_subgoal(&mut self, mut strand: &mut Strand<I, C>) -> SubGoalSelection { |
f9f354fc XL |
1243 | loop { |
1244 | while strand.selected_subgoal.is_none() { | |
f035d41b | 1245 | if strand.ex_clause.subgoals.is_empty() { |
f9f354fc | 1246 | if strand.ex_clause.floundered_subgoals.is_empty() { |
f035d41b | 1247 | return SubGoalSelection::NotSelected; |
f9f354fc XL |
1248 | } |
1249 | ||
1250 | self.reconsider_floundered_subgoals(&mut strand.ex_clause); | |
1251 | ||
1252 | if strand.ex_clause.subgoals.is_empty() { | |
f035d41b XL |
1253 | // All the subgoals of this strand floundered. We may be able |
1254 | // to get helpful information from this strand still, but it | |
1255 | // will *always* be ambiguous, so mark it as so. | |
f9f354fc | 1256 | assert!(!strand.ex_clause.floundered_subgoals.is_empty()); |
f035d41b XL |
1257 | strand.ex_clause.ambiguous = true; |
1258 | return SubGoalSelection::NotSelected; | |
f9f354fc XL |
1259 | } |
1260 | ||
1261 | continue; | |
1262 | } | |
1263 | ||
1264 | let subgoal_index = C::next_subgoal_index(&strand.ex_clause); | |
1265 | ||
1266 | // Get or create table for this subgoal. | |
1267 | match self.forest.get_or_create_table_for_subgoal( | |
1268 | self.context, | |
1269 | &mut strand.infer, | |
1270 | &strand.ex_clause.subgoals[subgoal_index], | |
1271 | ) { | |
1272 | Some((subgoal_table, universe_map)) => { | |
1273 | strand.selected_subgoal = Some(SelectedSubgoal { | |
1274 | subgoal_index, | |
1275 | subgoal_table, | |
1276 | universe_map, | |
1277 | answer_index: AnswerIndex::ZERO, | |
1278 | }); | |
1279 | } | |
1280 | ||
1281 | None => { | |
1282 | // If we failed to create a table for the subgoal, | |
1283 | // that is because we have a floundered negative | |
1284 | // literal. | |
1285 | self.flounder_subgoal(&mut strand.ex_clause, subgoal_index); | |
1286 | } | |
1287 | } | |
1288 | } | |
1289 | ||
1290 | let selected_subgoal_table = strand.selected_subgoal.as_ref().unwrap().subgoal_table; | |
1291 | if self.forest.tables[selected_subgoal_table].is_floundered() { | |
1292 | if self.propagate_floundered_subgoal(strand) { | |
1293 | // This strand will never lead anywhere of interest. | |
f035d41b | 1294 | return SubGoalSelection::NotSelected; |
f9f354fc XL |
1295 | } else { |
1296 | // This subgoal has floundered and has been marked. | |
1297 | // We previously would immediately mark the table as | |
1298 | // floundered too, and maybe come back to it. Now, we | |
1299 | // try to see if any other subgoals can be pursued first. | |
1300 | continue; | |
1301 | } | |
1302 | } else { | |
1303 | return SubGoalSelection::Selected; | |
1304 | } | |
1305 | } | |
1306 | } | |
1307 | ||
1308 | /// Invoked when a strand represents an **answer**. This means | |
1309 | /// that the strand has no subgoals left. There are two possibilities: | |
1310 | /// | |
1311 | /// - the strand may represent an answer we have already found; in | |
1312 | /// that case, we can return `None`, as this | |
1313 | /// strand led nowhere of interest. | |
1314 | /// - the strand may represent a new answer, in which case it is | |
1315 | /// added to the table and `Some(())` is returned. | |
f035d41b | 1316 | fn pursue_answer(&mut self, strand: Strand<I, C>) -> Option<AnswerIndex> { |
f9f354fc XL |
1317 | let table = self.stack.top().table; |
1318 | let Strand { | |
1319 | mut infer, | |
1320 | ex_clause: | |
1321 | ExClause { | |
1322 | subst, | |
1323 | constraints, | |
1324 | ambiguous, | |
1325 | subgoals, | |
1326 | delayed_subgoals, | |
1327 | answer_time: _, | |
1328 | floundered_subgoals, | |
1329 | }, | |
1330 | selected_subgoal: _, | |
1331 | last_pursued_time: _, | |
1332 | } = strand; | |
f035d41b | 1333 | // If there are subgoals left, they should be followed |
f9f354fc | 1334 | assert!(subgoals.is_empty()); |
f035d41b XL |
1335 | // We can still try to get an ambiguous answer if there are floundered subgoals |
1336 | let floundered = !floundered_subgoals.is_empty(); | |
1337 | // So let's make sure that it *really* is an ambiguous answer (this should be set previously) | |
1338 | assert!(!floundered || ambiguous); | |
1339 | ||
1340 | // FIXME: If there are floundered subgoals, we *could* potentially | |
1341 | // actually check if the partial answers to any of these subgoals | |
1342 | // conflict. But this requires that we think about whether they are | |
1343 | // positive or negative subgoals. This duplicates some of the logic | |
1344 | // in `merge_answer_into_strand`, so a bit of refactoring is needed. | |
f9f354fc XL |
1345 | |
1346 | // If the answer gets too large, mark the table as floundered. | |
1347 | // This is the *most conservative* course. There are a few alternatives: | |
1348 | // 1) Replace the answer with a truncated version of it. (This was done | |
1349 | // previously, but turned out to be more complicated than we wanted and | |
1350 | // and a source of multiple bugs.) | |
1351 | // 2) Mark this *strand* as floundered. We don't currently have a mechanism | |
1352 | // for this (only floundered subgoals), so implementing this is more | |
1353 | // difficult because we don't want to just *remove* this strand from the | |
1354 | // table, because that might make the table give `NoMoreSolutions`, which | |
1355 | // is *wrong*. | |
1356 | // 3) Do something fancy with delayed subgoals, effectively delayed the | |
1357 | // truncated bits to a different strand (and a more "refined" answer). | |
1358 | // (This one probably needs more thought, but is here for "completeness") | |
1359 | // | |
1360 | // Ultimately, the current decision to flounder the entire table mostly boils | |
1361 | // down to "it works as we expect for the current tests". And, we likely don't | |
1362 | // even *need* the added complexity just for potentially more answers. | |
1363 | if infer.answer_needs_truncation(self.context.interner(), &subst) { | |
1364 | self.forest.tables[table].mark_floundered(); | |
1365 | return None; | |
1366 | } | |
1367 | ||
f035d41b XL |
1368 | let table_goal = &self.forest.tables[table].table_goal; |
1369 | ||
1370 | // FIXME: Avoid double canonicalization | |
1371 | let filtered_delayed_subgoals = delayed_subgoals | |
1372 | .into_iter() | |
1373 | .filter(|delayed_subgoal| { | |
1374 | let (canonicalized, _) = | |
1375 | infer.fully_canonicalize_goal(self.context.interner(), delayed_subgoal); | |
1376 | *table_goal != canonicalized | |
1377 | }) | |
1378 | .collect(); | |
1379 | ||
f9f354fc XL |
1380 | let subst = infer.canonicalize_answer_subst( |
1381 | self.context.interner(), | |
1382 | subst, | |
1383 | constraints, | |
f035d41b XL |
1384 | filtered_delayed_subgoals, |
1385 | ); | |
1b1a35ee | 1386 | debug!(?table, ?subst, ?floundered, "found answer"); |
f9f354fc XL |
1387 | |
1388 | let answer = Answer { subst, ambiguous }; | |
1389 | ||
1390 | // A "trivial" answer is one that is 'just true for all cases' | |
1391 | // -- in other words, it gives no information back to the | |
1392 | // caller. For example, `Vec<u32>: Sized` is "just true". | |
1393 | // Such answers are important because they are the most | |
1394 | // general case, and after we provide a trivial answer, no | |
1395 | // further answers are useful -- therefore we can clear any | |
1396 | // further pending strands (this is a "green cut", in | |
1397 | // Prolog parlance). | |
1398 | // | |
1399 | // This optimization is *crucial* for performance: for | |
1400 | // example, `projection_from_env_slow` fails miserably without | |
1401 | // it. The reason is that we wind up (thanks to implied bounds) | |
1402 | // with a clause like this: | |
1403 | // | |
1404 | // ```ignore | |
1405 | // forall<T> { (<T as SliceExt>::Item: Clone) :- WF(T: SliceExt) } | |
1406 | // ``` | |
1407 | // | |
1408 | // we then apply that clause to `!1: Clone`, resulting in the | |
1409 | // table goal `!1: Clone :- <?0 as SliceExt>::Item = !1, | |
1410 | // WF(?0: SliceExt)`. This causes us to **enumerate all types | |
1411 | // `?0` that where `Slice<?0>` normalizes to `!1` -- this is | |
1412 | // an infinite set of types, effectively. Interestingly, | |
1413 | // though, we only need one and we are done, because (if you | |
1414 | // look) our goal (`!1: Clone`) doesn't have any output | |
1415 | // parameters. | |
1416 | // | |
1417 | // This is actually a kind of general case. Due to Rust's rule | |
1418 | // about constrained impl type parameters, generally speaking | |
1419 | // when we have some free inference variable (like `?0`) | |
1420 | // within our clause, it must appear in the head of the | |
1421 | // clause. This means that the values we create for it will | |
1422 | // propagate up to the caller, and they will quickly surmise | |
1423 | // that there is ambiguity and stop requesting more answers. | |
1424 | // Indeed, the only exception to this rule about constrained | |
1425 | // type parameters if with associated type projections, as in | |
1426 | // the case above! | |
1427 | // | |
1428 | // (Actually, because of the trivial answer cut off rule, we | |
1429 | // never even get to the point of asking the query above in | |
1430 | // `projection_from_env_slow`.) | |
1431 | // | |
1432 | // However, there is one fly in the ointment: answers include | |
1433 | // region constraints, and you might imagine that we could | |
1434 | // find future answers that are also trivial but with distinct | |
1435 | // sets of region constraints. **For this reason, we only | |
1436 | // apply this green cut rule if the set of generated | |
1437 | // constraints is empty.** | |
1438 | // | |
1439 | // The limitation on region constraints is quite a drag! We | |
1440 | // can probably do better, though: for example, coherence | |
1441 | // guarantees that, for any given set of types, only a single | |
1442 | // impl ought to be applicable, and that impl can only impose | |
1443 | // one set of region constraints. However, it's not quite that | |
1444 | // simple, thanks to specialization as well as the possibility | |
1445 | // of proving things from the environment (though the latter | |
1446 | // is a *bit* suspect; e.g., those things in the environment | |
1447 | // must be backed by an impl *eventually*). | |
1448 | let is_trivial_answer = { | |
f035d41b XL |
1449 | self.context |
1450 | .is_trivial_substitution(&self.forest.tables[table].table_goal, &answer.subst) | |
1b1a35ee XL |
1451 | && answer |
1452 | .subst | |
1453 | .value | |
1454 | .constraints | |
1455 | .is_empty(self.context.interner()) | |
f9f354fc XL |
1456 | }; |
1457 | ||
1458 | if let Some(answer_index) = self.forest.tables[table].push_answer(answer) { | |
f035d41b XL |
1459 | // See above, if we have a *complete* and trivial answer, we don't |
1460 | // want to follow any more strands | |
1461 | if !ambiguous && is_trivial_answer { | |
f9f354fc XL |
1462 | self.forest.tables[table].take_strands(); |
1463 | } | |
1464 | ||
1465 | Some(answer_index) | |
1466 | } else { | |
1467 | info!("answer: not a new answer, returning None"); | |
1468 | None | |
1469 | } | |
1470 | } | |
1471 | ||
f035d41b | 1472 | fn reconsider_floundered_subgoals(&mut self, ex_clause: &mut ExClause<I>) { |
f9f354fc XL |
1473 | info!("reconsider_floundered_subgoals(ex_clause={:#?})", ex_clause,); |
1474 | let ExClause { | |
1475 | answer_time, | |
1476 | subgoals, | |
1477 | floundered_subgoals, | |
1478 | .. | |
1479 | } = ex_clause; | |
1480 | for i in (0..floundered_subgoals.len()).rev() { | |
1481 | if floundered_subgoals[i].floundered_time < *answer_time { | |
1482 | let floundered_subgoal = floundered_subgoals.swap_remove(i); | |
1483 | subgoals.push(floundered_subgoal.floundered_literal); | |
1484 | } | |
1485 | } | |
1486 | } | |
1487 | ||
1488 | /// Removes the subgoal at `subgoal_index` from the strand's | |
1489 | /// subgoal list and adds it to the strand's floundered subgoal | |
1490 | /// list. | |
f035d41b XL |
1491 | fn flounder_subgoal(&self, ex_clause: &mut ExClause<I>, subgoal_index: usize) { |
1492 | let _s = debug_span!( | |
1493 | "flounder_subgoal", | |
1494 | answer_time = ?ex_clause.answer_time, | |
1495 | subgoal = ?ex_clause.subgoals[subgoal_index], | |
f9f354fc | 1496 | ); |
f035d41b XL |
1497 | let _s = _s.enter(); |
1498 | ||
f9f354fc XL |
1499 | let floundered_time = ex_clause.answer_time; |
1500 | let floundered_literal = ex_clause.subgoals.remove(subgoal_index); | |
1501 | ex_clause.floundered_subgoals.push(FlounderedSubgoal { | |
1502 | floundered_literal, | |
1503 | floundered_time, | |
1504 | }); | |
1b1a35ee | 1505 | debug!(?ex_clause); |
f9f354fc XL |
1506 | } |
1507 | ||
1508 | /// True if all the tables on the stack starting from `depth` and | |
1509 | /// continuing until the top of the stack are coinductive. | |
1510 | /// | |
1511 | /// Example: Given a program like: | |
1512 | /// | |
1513 | /// ```notrust | |
1514 | /// struct Foo { a: Option<Box<Bar>> } | |
1515 | /// struct Bar { a: Option<Box<Foo>> } | |
1516 | /// trait XXX { } | |
1517 | /// impl<T: Send> XXX for T { } | |
1518 | /// ``` | |
1519 | /// | |
1520 | /// and then a goal of `Foo: XXX`, we would eventually wind up | |
1521 | /// with a stack like this: | |
1522 | /// | |
1523 | /// | StackIndex | Table Goal | | |
1524 | /// | ---------- | ----------- | | |
1525 | /// | 0 | `Foo: XXX` | | |
1526 | /// | 1 | `Foo: Send` | | |
1527 | /// | 2 | `Bar: Send` | | |
1528 | /// | |
1529 | /// Here, the top of the stack is `Bar: Send`. And now we are | |
1530 | /// asking `top_of_stack_is_coinductive_from(1)` -- the answer | |
1531 | /// would be true, since `Send` is an auto trait, which yields a | |
1532 | /// coinductive goal. But `top_of_stack_is_coinductive_from(0)` is | |
1533 | /// false, since `XXX` is not an auto trait. | |
1534 | pub(super) fn top_of_stack_is_coinductive_from(&self, depth: StackIndex) -> bool { | |
1535 | StackIndex::iterate_range(self.stack.top_of_stack_from(depth)).all(|d| { | |
1536 | let table = self.stack[d].table; | |
1537 | self.forest.tables[table].coinductive_goal | |
1538 | }) | |
1539 | } | |
1540 | } |