2 Context
, ContextOps
, InferenceTable
, ResolventOps
, TruncateOps
, UnificationOps
,
4 use crate::forest
::Forest
;
5 use crate::stack
::{Stack, StackIndex}
;
6 use crate::strand
::{CanonicalStrand, SelectedSubgoal, Strand}
;
7 use crate::table
::{AnswerIndex, Table}
;
9 Answer
, AnswerMode
, CompleteAnswer
, ExClause
, FlounderedSubgoal
, Literal
, Minimums
, TableIndex
,
13 use chalk_ir
::interner
::Interner
;
15 Canonical
, ConstrainedSubst
, DomainGoal
, Floundered
, Goal
, GoalData
, InEnvironment
, NoSolution
,
16 Substitution
, UCanonical
, UniverseMap
, WhereClause
,
18 use tracing
::{debug, debug_span, info, instrument}
;
20 type RootSearchResult
<T
> = Result
<T
, RootSearchFail
>;
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
26 pub(super) enum RootSearchFail
{
27 /// The table we were trying to solve cannot succeed.
30 /// The table cannot be solved without more type information.
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.
36 /// (In a purely depth-first-based solver, like Prolog, this
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.
44 /// The current answer index is not useful. Currently, this is returned
45 /// because the current answer needs refining.
49 /// This is returned when we try to select a subgoal for a strand.
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.
57 /// This strand has no remaining subgoals, but there may still be
58 /// floundered subgoals.
62 /// This is returned `on_no_remaining_subgoals`
63 enum NoRemainingSubgoalsResult
{
64 /// There is an answer available for the root table
67 /// There was a `RootSearchFail`
68 RootSearchFail(RootSearchFail
),
74 impl<I
: Interner
, C
: Context
<I
>> Forest
<I
, C
> {
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(
81 context
: &impl ContextOps
<I
, C
>,
83 answer_index
: AnswerIndex
,
84 ) -> RootSearchResult
<CompleteAnswer
<I
>> {
85 let stack
= Stack
::default();
87 let mut state
= SolveState
{
93 match state
.ensure_root_answer(table
, answer_index
) {
95 assert
!(state
.stack
.is_empty());
96 let answer
= state
.forest
.answer(table
, answer_index
);
97 if !answer
.subst
.value
.delayed_subgoals
.is_empty() {
98 return Err(RootSearchFail
::InvalidAnswer
);
102 binders
: answer
.subst
.binders
.clone(),
103 value
: ConstrainedSubst
{
104 subst
: answer
.subst
.value
.subst
.clone(),
105 constraints
: answer
.subst
.value
.constraints
.clone(),
108 ambiguous
: answer
.ambiguous
,
111 Err(err
) => Err(err
),
115 pub(super) fn any_future_answer(
119 mut test
: impl FnMut(&Substitution
<I
>) -> bool
,
121 if let Some(answer
) = self.tables
[table
].answer(answer
) {
122 info
!("answer cached = {:?}", answer
);
123 return test(&answer
.subst
.value
.subst
);
128 .any(|strand
| test(&strand
.canonical_ex_clause
.value
.subst
))
131 pub(crate) fn answer(&self, table
: TableIndex
, answer
: AnswerIndex
) -> &Answer
<I
> {
132 self.tables
[table
].answer(answer
).unwrap()
135 fn canonicalize_strand(
136 context
: &impl ContextOps
<I
, C
>,
137 strand
: Strand
<I
, C
>,
138 ) -> CanonicalStrand
<I
> {
145 Forest
::canonicalize_strand_from(
154 fn canonicalize_strand_from(
155 context
: &impl ContextOps
<I
, C
>,
156 infer
: &mut dyn InferenceTable
<I
, C
>,
157 ex_clause
: &ExClause
<I
>,
158 selected_subgoal
: Option
<SelectedSubgoal
>,
159 last_pursued_time
: TimeStamp
,
160 ) -> CanonicalStrand
<I
> {
161 let canonical_ex_clause
= infer
.canonicalize_ex_clause(context
.interner(), &ex_clause
);
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).
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".
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.
182 #[instrument(level = "debug", skip(self, context, infer))]
183 fn get_or_create_table_for_subgoal(
185 context
: &impl ContextOps
<I
, C
>,
186 infer
: &mut dyn InferenceTable
<I
, C
>,
187 subgoal
: &Literal
<I
>,
188 ) -> Option
<(TableIndex
, UniverseMap
)> {
189 // Subgoal abstraction:
190 let (ucanonical_subgoal
, universe_map
) = match subgoal
{
191 Literal
::Positive(subgoal
) => {
192 Forest
::abstract_positive_literal(context
, infer
, subgoal
)?
194 Literal
::Negative(subgoal
) => {
195 Forest
::abstract_negative_literal(context
, infer
, subgoal
)?
199 debug
!("ucanonical_subgoal={:?}", ucanonical_subgoal
);
200 debug
!("universe_map={:?}", universe_map
);
202 let table
= self.get_or_create_table_for_ucanonical_goal(context
, ucanonical_subgoal
);
204 Some((table
, universe_map
))
207 /// Given a u-canonical goal, searches for an existing table. If
208 /// one is found, it is returned, but otherwise a new table is
209 /// created (and populated with its initial set of strands).
211 /// In terms of the NFTD paper, creating a new table corresponds
212 /// to the *New Subgoal* step as well as the *Program Clause
213 /// Resolution* steps.
214 #[instrument(level = "debug", skip(self, context))]
215 pub(crate) fn get_or_create_table_for_ucanonical_goal(
217 context
: &impl ContextOps
<I
, C
>,
218 goal
: UCanonical
<InEnvironment
<Goal
<I
>>>,
220 if let Some(table
) = self.tables
.index_of(&goal
) {
221 debug
!("found existing table {:?}", table
);
226 "creating new table {:?} and goal {:#?}",
227 self.tables
.next_index(),
230 let table
= Self::build_table(context
, self.tables
.next_index(), goal
);
231 self.tables
.insert(table
)
234 /// When a table is first created, this function is invoked to
235 /// create the initial set of strands. If the table represents a
236 /// domain goal, these strands are created from the program
237 /// clauses as well as the clauses found in the environment. If
238 /// the table represents a non-domain goal, such as `for<T> G`
239 /// etc, then `simplify_goal` is invoked to create a strand
240 /// that breaks the goal down.
242 /// In terms of the NFTD paper, this corresponds to the *Program
243 /// Clause Resolution* step being applied eagerly, as many times
246 context
: &impl ContextOps
<I
, C
>,
247 table_idx
: TableIndex
,
248 goal
: UCanonical
<InEnvironment
<Goal
<I
>>>,
250 let mut table
= Table
::new(goal
.clone(), context
.is_coinductive(&goal
));
251 let (mut infer
, subst
, environment
, goal
) = context
.instantiate_ucanonical_goal(&goal
);
252 let goal_data
= goal
.data(context
.interner());
254 let is_outlives_goal
= |dg
: &DomainGoal
<I
>| {
255 if let DomainGoal
::Holds(WhereClause
::LifetimeOutlives(_
)) = dg
{
263 GoalData
::DomainGoal(domain_goal
) if !is_outlives_goal(domain_goal
) => {
264 match context
.program_clauses(&environment
, &domain_goal
, &mut infer
) {
266 for clause
in clauses
{
267 info
!("program clause = {:#?}", clause
);
268 let mut infer
= infer
.clone();
269 if let Ok(resolvent
) = infer
.resolvent_clause(
276 info
!("pushing initial strand with ex-clause: {:#?}", &resolvent
,);
277 let strand
= Strand
{
279 ex_clause
: resolvent
,
280 selected_subgoal
: None
,
281 last_pursued_time
: TimeStamp
::default(),
283 let canonical_strand
= Self::canonicalize_strand(context
, strand
);
284 table
.enqueue_strand(canonical_strand
);
290 "Marking table {:?} as floundered! (failed to create program clauses)",
293 table
.mark_floundered();
299 // `canonical_goal` is a goal. We can simplify it
300 // into a series of *literals*, all of which must be
301 // true. Thus, in EWFS terms, we are effectively
302 // creating a single child of the `A :- A` goal that
303 // is like `A :- B, C, D` where B, C, and D are the
304 // simplified subgoals. You can think of this as
305 // applying built-in "meta program clauses" that
306 // reduce goals into Domain goals.
307 if let Ok(ex_clause
) =
308 Self::simplify_goal(context
, &mut infer
, subst
, environment
, goal
)
311 "pushing initial strand with ex-clause: {:#?}",
312 infer
.debug_ex_clause(context
.interner(), &ex_clause
),
314 let strand
= Strand
{
317 selected_subgoal
: None
,
318 last_pursued_time
: TimeStamp
::default(),
320 let canonical_strand
= Self::canonicalize_strand(context
, strand
);
321 table
.enqueue_strand(canonical_strand
);
329 /// Given a selected positive subgoal, applies the subgoal
330 /// abstraction function to yield the canonical form that will be
331 /// used to pick a table. Typically, this abstraction has no
332 /// effect, and hence we are simply returning the canonical form
333 /// of `subgoal`; but if the subgoal is getting too big, we return
334 /// `None`, which causes the subgoal to flounder.
335 fn abstract_positive_literal(
336 context
: &impl ContextOps
<I
, C
>,
337 infer
: &mut dyn InferenceTable
<I
, C
>,
338 subgoal
: &InEnvironment
<Goal
<I
>>,
339 ) -> Option
<(UCanonical
<InEnvironment
<Goal
<I
>>>, UniverseMap
)> {
340 if infer
.goal_needs_truncation(context
.interner(), subgoal
) {
343 Some(infer
.fully_canonicalize_goal(context
.interner(), subgoal
))
347 /// Given a selected negative subgoal, the subgoal is "inverted"
348 /// (see `InferenceTable<I, C>::invert`) and then potentially truncated
349 /// (see `abstract_positive_literal`). The result subgoal is
350 /// canonicalized. In some cases, this may return `None` and hence
351 /// fail to yield a useful result, for example if free existential
352 /// variables appear in `subgoal` (in which case the execution is
353 /// said to "flounder").
354 fn abstract_negative_literal(
355 context
: &impl ContextOps
<I
, C
>,
356 infer
: &mut dyn InferenceTable
<I
, C
>,
357 subgoal
: &InEnvironment
<Goal
<I
>>,
358 ) -> Option
<(UCanonical
<InEnvironment
<Goal
<I
>>>, UniverseMap
)> {
359 // First, we have to check that the selected negative literal
360 // is ground, and invert any universally quantified variables.
362 // DIVERGENCE -- In the RR paper, to ensure completeness, they
363 // permit non-ground negative literals, but only consider
364 // them to succeed when the target table has no answers at
365 // all. This is equivalent inverting those free existentials
366 // into universals, as discussed in the comments of
367 // `invert`. This is clearly *sound*, but the completeness is
368 // a subtle point. In particular, it can cause **us** to reach
369 // false conclusions, because e.g. given a program like
370 // (selected left-to-right):
372 // not { ?T: Copy }, ?T = Vec<u32>
374 // we would select `not { ?T: Copy }` first. For this goal to
375 // succeed we would require that -- effectively -- `forall<T>
376 // { not { T: Copy } }`, which clearly doesn't hold. (In the
377 // terms of RR, we would require that the table for `?T: Copy`
378 // has failed before we can continue.)
380 // In the RR paper, this is acceptable because they assume all
381 // of their input programs are both **normal** (negative
382 // literals are selected after positive ones) and **safe**
383 // (all free variables in negative literals occur in positive
384 // literals). It is plausible for us to guarantee "normal"
385 // form, we can reorder clauses as we need. I suspect we can
386 // guarantee safety too, but I have to think about it.
388 // For now, we opt for the safer route of terming such
389 // executions as floundering, because I think our use of
390 // negative goals is sufficiently limited we can get away with
391 // it. The practical effect is that we will judge more
392 // executions as floundering than we ought to (i.e., where we
393 // could instead generate an (imprecise) result). As you can
394 // see a bit later, we also diverge in some other aspects that
395 // affect completeness when it comes to subgoal abstraction.
396 let inverted_subgoal
= infer
.invert_goal(context
.interner(), subgoal
)?
;
398 if infer
.goal_needs_truncation(context
.interner(), &inverted_subgoal
) {
401 Some(infer
.fully_canonicalize_goal(context
.interner(), &inverted_subgoal
))
406 pub(crate) struct SolveState
<'forest
, I
: Interner
, C
: Context
<I
>, CO
: ContextOps
<I
, C
>> {
407 forest
: &'forest
mut Forest
<I
, C
>,
408 context
: &'forest CO
,
412 impl<'forest
, I
: Interner
, C
: Context
<I
> + 'forest
, CO
: ContextOps
<I
, C
> + 'forest
> Drop
413 for SolveState
<'forest
, I
, C
, CO
>
416 if !self.stack
.is_empty() {
417 if let Some(active_strand
) = self.stack
.top().active_strand
.take() {
418 let table
= self.stack
.top().table
;
419 let canonical_active_strand
=
420 Forest
::canonicalize_strand(self.context
, active_strand
);
421 self.forest
.tables
[table
].enqueue_strand(canonical_active_strand
);
428 impl<'forest
, I
: Interner
, C
: Context
<I
> + 'forest
, CO
: ContextOps
<I
, C
> + 'forest
>
429 SolveState
<'forest
, I
, C
, CO
>
431 /// Ensures that answer with the given index is available from the
432 /// given table. Returns `Ok` if there is an answer.
434 /// This function first attempts to fetch answer that is cached in
435 /// the table. If none is found, then it will recursively search
436 /// to find an answer.
437 #[instrument(level = "info", skip(self))]
438 fn ensure_root_answer(
440 initial_table
: TableIndex
,
441 initial_answer
: AnswerIndex
,
442 ) -> RootSearchResult
<()> {
444 "table goal = {:#?}",
445 self.forest
.tables
[initial_table
].table_goal
447 // Check if this table has floundered.
448 if self.forest
.tables
[initial_table
].is_floundered() {
449 return Err(RootSearchFail
::Floundered
);
451 // Check for a tabled answer.
452 if let Some(answer
) = self.forest
.tables
[initial_table
].answer(initial_answer
) {
453 info
!("answer cached = {:?}", answer
);
457 // If no tabled answer is present, we ought to be requesting
458 // the next available index.
460 self.forest
.tables
[initial_table
].next_answer_index(),
465 .push(initial_table
, Minimums
::MAX
, self.forest
.increment_clock());
467 // FIXME: use depth for debug/info printing
469 let clock
= self.stack
.top().clock
;
470 // If we had an active strand, continue to pursue it
471 let table
= self.stack
.top().table
;
472 let table_answer_mode
= self.forest
.tables
[table
].answer_mode
;
474 // We track when we last pursued each strand. If all the strands have been
475 // pursued at this depth, then that means they all encountered a cycle.
476 // We also know that if the first strand has been pursued at this depth,
477 // then all have. Otherwise, an answer to any strand would have provided an
478 // answer for the table.
479 let num_universes
= self.forest
.tables
[table
].table_goal
.universes
;
480 let forest
= &mut self.forest
;
481 let context
= &self.context
;
482 let next_strand
= self.stack
.top().active_strand
.take().or_else(|| {
484 .dequeue_next_strand_that(|strand
| {
485 let (_
, ex_clause
) = context
486 .instantiate_ex_clause(num_universes
, &strand
.canonical_ex_clause
);
487 let time_eligble
= strand
.last_pursued_time
< clock
;
488 let mode_eligble
= match (table_answer_mode
, ex_clause
.ambiguous
) {
489 (AnswerMode
::Complete
, false) => true,
490 (AnswerMode
::Complete
, true) => false,
491 (AnswerMode
::Ambiguous
, _
) => true,
493 time_eligble
&& mode_eligble
495 .map(|canonical_strand
| {
496 let CanonicalStrand
{
500 } = canonical_strand
;
501 let (infer
, ex_clause
) =
502 context
.instantiate_ex_clause(num_universes
, &canonical_ex_clause
);
503 let strand
= Strand
{
506 selected_subgoal
: selected_subgoal
.clone(),
513 Some(mut strand
) => {
514 debug
!("next strand: {:#?}", strand
);
516 strand
.last_pursued_time
= clock
;
517 match self.select_subgoal(&mut strand
) {
518 SubGoalSelection
::Selected
=> {
519 // A subgoal has been selected. We now check this subgoal
520 // table for an existing answer or if it's in a cycle.
521 // If neither of those are the case, a strand is selected
522 // and the next loop iteration happens.
523 self.on_subgoal_selected(strand
)?
;
526 SubGoalSelection
::NotSelected
=> {
527 match self.on_no_remaining_subgoals(strand
) {
528 NoRemainingSubgoalsResult
::RootAnswerAvailable
=> return Ok(()),
529 NoRemainingSubgoalsResult
::RootSearchFail(e
) => return Err(e
),
530 NoRemainingSubgoalsResult
::Success
=> continue,
536 self.on_no_strands_left()?
;
543 /// This is called when an answer is available for the selected subgoal
544 /// of the strand. First, if the selected subgoal is a `Positive` subgoal,
545 /// it first clones the strand pursuing the next answer. Then, it merges the
546 /// answer into the provided `Strand`.
547 /// On success, `Ok` is returned and the `Strand` can be continued to process
548 /// On failure, `Err` is returned and the `Strand` should be discarded
549 fn merge_answer_into_strand(&mut self, strand
: &mut Strand
<I
, C
>) -> RootSearchResult
<()> {
550 // At this point, we know we have an answer for
551 // the selected subgoal of the strand.
552 // Now, we have to unify that answer onto the strand.
554 // If this answer is ambiguous and we don't want ambiguous answers
555 // yet, then we act like this is a floundered subgoal.
557 let selected_subgoal
= strand
.selected_subgoal
.as_ref().unwrap();
558 let answer
= self.forest
.answer(
559 selected_subgoal
.subgoal_table
,
560 selected_subgoal
.answer_index
,
564 if let AnswerMode
::Complete
= self.forest
.tables
[self.stack
.top().table
].answer_mode
{
566 // FIXME: we could try to be a little bit smarter here. This can
567 // really be split into cases:
568 // 1) Cases where no amount of solving will cause this ambiguity to change.
569 // (e.g. `CannnotProve`)
570 // 2) Cases where we may be able to get a better answer if we
571 // solve other subgoals first.
572 // (e.g. the `non_enumerable_traits_reorder` test)
573 // We really only need to delay merging an ambiguous answer for
574 // case 2. Do note, though, that even if we *do* merge the answer
575 // case 1, we should stop solving this strand when in
576 // `AnswerMode::Complete` since we wouldn't use this answer yet
579 // The selected subgoal returned an ambiguous answer, but we don't want that.
580 // So, we treat this subgoal as floundered.
581 let selected_subgoal
= strand
.selected_subgoal
.take().unwrap();
582 self.flounder_subgoal(&mut strand
.ex_clause
, selected_subgoal
.subgoal_index
);
587 // If this subgoal was a `Positive` one, whichever way this
588 // particular answer turns out, there may yet be *more* answers,
589 // if this isn't a trivial substitution.
590 // Enqueue that alternative for later.
591 // NOTE: this is separate from the match below because we `take` the selected_subgoal
592 // below, but here we keep it for the new `Strand`.
593 let selected_subgoal
= strand
.selected_subgoal
.as_ref().unwrap();
594 if let Literal
::Positive(_
) = strand
.ex_clause
.subgoals
[selected_subgoal
.subgoal_index
] {
595 let answer
= self.forest
.answer(
596 selected_subgoal
.subgoal_table
,
597 selected_subgoal
.answer_index
,
599 if !self.context
.is_trivial_substitution(
600 &self.forest
.tables
[selected_subgoal
.subgoal_table
].table_goal
,
603 let mut next_subgoal
= selected_subgoal
.clone();
604 next_subgoal
.answer_index
.increment();
605 let next_strand
= Strand
{
606 infer
: strand
.infer
.clone(),
607 ex_clause
: strand
.ex_clause
.clone(),
608 selected_subgoal
: Some(next_subgoal
),
609 last_pursued_time
: strand
.last_pursued_time
.clone(),
611 let table
= self.stack
.top().table
;
612 let canonical_next_strand
= Forest
::canonicalize_strand(self.context
, next_strand
);
613 self.forest
.tables
[table
].enqueue_strand(canonical_next_strand
);
617 // Deselect and remove the selected subgoal, now that we have an answer for it.
618 let selected_subgoal
= strand
.selected_subgoal
.take().unwrap();
622 .remove(selected_subgoal
.subgoal_index
);
624 Literal
::Positive(subgoal
) => {
625 let SelectedSubgoal
{
630 } = selected_subgoal
;
631 let table_goal
= &self.context
.map_goal_from_canonical(
633 &self.forest
.tables
[subgoal_table
].table_goal
.canonical
,
635 let answer_subst
= &self.context
.map_subst_from_canonical(
637 &self.forest
.answer(subgoal_table
, answer_index
).subst
,
639 match strand
.infer
.apply_answer_subst(
640 self.context
.interner(),
641 &mut strand
.ex_clause
,
651 last_pursued_time
: _
,
654 // If the answer had was ambiguous, we have to
655 // ensure that `ex_clause` is also ambiguous. This is
656 // the SLG FACTOR operation, though NFTD just makes it
657 // part of computing the SLG resolvent.
658 if self.forest
.answer(subgoal_table
, answer_index
).ambiguous
{
659 debug
!("Marking Strand as ambiguous because answer to (positive) subgoal was ambiguous");
660 ex_clause
.ambiguous
= true;
663 // Increment the answer time for the `ex_clause`. Floundered
664 // subgoals may be eligble to be pursued again.
665 ex_clause
.answer_time
.increment();
667 // Ok, we've applied the answer to this Strand.
671 // This answer led nowhere. Give up for now, but of course
672 // there may still be other strands to pursue, so return
673 // `QuantumExceeded`.
675 info
!("answer not unifiable -> NoSolution");
676 // This strand as no solution. It is no longer active,
677 // so it dropped at the end of this scope.
679 // Now we want to propogate back to the up with `QuantumExceeded`
681 return Err(RootSearchFail
::QuantumExceeded
);
685 Literal
::Negative(_
) => {
686 let SelectedSubgoal
{
691 } = selected_subgoal
;
692 // We got back an answer. This is bad, because we want
693 // to disprove the subgoal, but it may be
694 // "conditional" (maybe true, maybe not).
695 let answer
= self.forest
.answer(subgoal_table
, answer_index
);
697 // By construction, we do not expect negative subgoals
698 // to have delayed subgoals. This is because we do not
699 // need to permit `not { L }` where `L` is a
700 // coinductive goal. We could improve this if needed,
701 // but it keeps things simple.
702 if !answer
.subst
.value
.delayed_subgoals
.is_empty() {
703 panic
!("Negative subgoal had delayed_subgoals");
706 if !answer
.ambiguous
{
707 // We want to disproval the subgoal, but we
708 // have an unconditional answer for the subgoal,
709 // therefore we have failed to disprove it.
710 info
!("found unconditional answer to neg literal -> NoSolution");
712 // This strand as no solution. By returning an Err,
713 // the caller should discard this `Strand`.
715 // Now we want to propogate back to the up with `QuantumExceeded`
717 return Err(RootSearchFail
::QuantumExceeded
);
720 // Otherwise, the answer is ambiguous. We can keep going,
721 // but we have to mark our strand, too, as ambiguous.
723 // We want to disproval the subgoal, but we
724 // have an unconditional answer for the subgoal,
725 // therefore we have failed to disprove it.
726 debug
!("Marking Strand as ambiguous because answer to (negative) subgoal was ambiguous");
727 strand
.ex_clause
.ambiguous
= true;
729 // Strand is ambigious.
735 /// This is called when the selected subgoal for a strand has floundered.
736 /// We have to decide what this means for the strand.
737 /// - If the strand was positively dependent on the subgoal, we flounder,
738 /// the subgoal, then return `false`. This strand may be able to be
740 /// - If the strand was negatively dependent on the subgoal, then strand
741 /// has led nowhere of interest and we return `true`. This strand should
744 /// In other words, we return whether this strand flounders.
745 fn propagate_floundered_subgoal(&mut self, strand
: &mut Strand
<I
, C
>) -> bool
{
746 // This subgoal selection for the strand is finished, so take it
747 let selected_subgoal
= strand
.selected_subgoal
.take().unwrap();
748 match strand
.ex_clause
.subgoals
[selected_subgoal
.subgoal_index
] {
749 Literal
::Positive(_
) => {
750 // If this strand depends on this positively, then we can
751 // come back to it later. So, we mark that subgoal as
752 // floundered and yield `QuantumExceeded` up the stack
754 // If this subgoal floundered, push it onto the
755 // floundered list, along with the time that it
756 // floundered. We'll try to solve some other subgoals
757 // and maybe come back to it.
758 self.flounder_subgoal(&mut strand
.ex_clause
, selected_subgoal
.subgoal_index
);
762 Literal
::Negative(_
) => {
763 // Floundering on a negative literal isn't like a
764 // positive search: we only pursue negative literals
765 // when we already know precisely the type we are
766 // looking for. So there's no point waiting for other
767 // subgoals, we'll never recover more information.
769 // In fact, floundering on negative searches shouldn't
770 // normally happen, since there are no uninferred
771 // variables in the goal, but it can with forall
774 // forall<T> { not { T: Debug } }
776 // Here, the table we will be searching for answers is
777 // `?T: Debug`, so it could well flounder.
779 // This strand has no solution. It is no longer active,
780 // so it dropped at the end of this scope.
787 /// This is called if the selected subgoal for a `Strand` is
788 /// a coinductive cycle.
789 fn on_coinductive_subgoal(&mut self, mut strand
: Strand
<I
, C
>) -> Result
<(), RootSearchFail
> {
790 // This is a co-inductive cycle. That is, this table
791 // appears somewhere higher on the stack, and has now
792 // recursively requested an answer for itself. This
793 // means that we have to delay this subgoal until we
794 // reach a trivial self-cycle.
796 // This subgoal selection for the strand is finished, so take it
797 let selected_subgoal
= strand
.selected_subgoal
.take().unwrap();
801 .remove(selected_subgoal
.subgoal_index
)
803 Literal
::Positive(subgoal
) => {
804 // We delay this subgoal
805 let table
= self.stack
.top().table
;
807 self.forest
.tables
[table
].coinductive_goal
808 && self.forest
.tables
[selected_subgoal
.subgoal_table
].coinductive_goal
811 strand
.ex_clause
.delayed_subgoals
.push(subgoal
);
813 self.stack
.top().active_strand
= Some(strand
);
816 Literal
::Negative(_
) => {
817 // We don't allow coinduction for negative literals
818 info
!("found coinductive answer to negative literal");
819 panic
!("Coinductive cycle with negative literal");
824 /// This is called if the selected subgoal for `strand` is
825 /// a positive, non-coinductive cycle.
829 /// * `strand` the strand from the top of the stack we are pursuing
830 /// * `minimums` is the collected minimum clock times
831 fn on_positive_cycle(
833 strand
: Strand
<I
, C
>,
835 ) -> Result
<(), RootSearchFail
> {
836 // We can't take this because we might need it later to clear the cycle
837 let selected_subgoal
= strand
.selected_subgoal
.as_ref().unwrap();
839 match strand
.ex_clause
.subgoals
[selected_subgoal
.subgoal_index
] {
840 Literal
::Positive(_
) => {
841 self.stack
.top().cyclic_minimums
.take_minimums(&minimums
);
843 Literal
::Negative(_
) => {
844 // We depend on `not(subgoal)`. For us to continue,
845 // `subgoal` must be completely evaluated. Therefore,
846 // we depend (negatively) on the minimum link of
847 // `subgoal` as a whole -- it doesn't matter whether
849 let mins
= Minimums
{
850 positive
: self.stack
.top().clock
,
851 negative
: minimums
.minimum_of_pos_and_neg(),
853 self.stack
.top().cyclic_minimums
.take_minimums(&mins
);
857 // Ok, we've taken the minimums from this cycle above. Now,
858 // we just return the strand to the table. The table only
859 // pulls strands if they have not been checked at this
862 // We also can't mark these and return early from this
863 // because the stack above us might change.
864 let table
= self.stack
.top().table
;
865 let canonical_strand
= Forest
::canonicalize_strand(self.context
, strand
);
866 self.forest
.tables
[table
].enqueue_strand(canonical_strand
);
868 // The strand isn't active, but the table is, so just continue
872 /// Invoked after we've selected a (new) subgoal for the top-most
873 /// strand. Attempts to pursue this selected subgoal.
877 /// * `Ok` if we should keep searching.
878 /// * `Err` if the subgoal failed in some way such that the strand can be abandoned.
879 fn on_subgoal_selected(&mut self, mut strand
: Strand
<I
, C
>) -> Result
<(), RootSearchFail
> {
880 // This may be a newly selected subgoal or an existing selected subgoal.
882 let SelectedSubgoal
{
887 } = *strand
.selected_subgoal
.as_ref().unwrap();
890 "table selection {:?} with goal: {:#?}",
891 subgoal_table
, self.forest
.tables
[subgoal_table
].table_goal
894 // This is checked inside select_subgoal
895 assert
!(!self.forest
.tables
[subgoal_table
].is_floundered());
897 // Check for a tabled answer.
898 if let Some(answer
) = self.forest
.tables
[subgoal_table
].answer(answer_index
) {
899 info
!("answer cached = {:?}", answer
);
901 // There was a previous answer available for this table
902 // We need to check if we can merge it into the current `Strand`.
903 match self.merge_answer_into_strand(&mut strand
) {
905 debug
!("could not merge into current strand");
910 debug
!("merged answer into current strand");
911 self.stack
.top().active_strand
= Some(strand
);
917 // If no tabled answer is present, we ought to be requesting
918 // the next available index.
920 self.forest
.tables
[subgoal_table
].next_answer_index(),
924 // Next, check if the table is already active. If so, then we
925 // have a recursive attempt.
926 if let Some(cyclic_depth
) = self.stack
.is_active(subgoal_table
) {
927 info
!("cycle detected at depth {:?}", cyclic_depth
);
928 let minimums
= Minimums
{
929 positive
: self.stack
[cyclic_depth
].clock
,
930 negative
: TimeStamp
::MAX
,
933 if self.top_of_stack_is_coinductive_from(cyclic_depth
) {
934 debug
!("table is coinductive");
935 return self.on_coinductive_subgoal(strand
);
938 debug
!("table encountered a positive cycle");
939 return self.on_positive_cycle(strand
, minimums
);
942 // We don't know anything about the selected subgoal table.
943 // Set this strand as active and push it onto the stack.
944 self.stack
.top().active_strand
= Some(strand
);
946 let cyclic_minimums
= Minimums
::MAX
;
950 self.forest
.increment_clock(),
955 /// This is called when there are no remaining subgoals for a strand, so
956 /// it represents an answer. If the strand is ambiguous and we don't want
957 /// it yet, we just enqueue it again to pick it up later. Otherwise, we
958 /// add the answer from the strand onto the table.
959 fn on_no_remaining_subgoals(&mut self, strand
: Strand
<I
, C
>) -> NoRemainingSubgoalsResult
{
960 let ambiguous
= strand
.ex_clause
.ambiguous
;
961 if let AnswerMode
::Complete
= self.forest
.tables
[self.stack
.top().table
].answer_mode
{
963 // The strand can only return an ambiguous answer, but we don't
964 // want that right now, so requeue and we'll deal with it later.
965 let canonical_strand
= Forest
::canonicalize_strand(self.context
, strand
);
966 self.forest
.tables
[self.stack
.top().table
].enqueue_strand(canonical_strand
);
967 return NoRemainingSubgoalsResult
::RootSearchFail(RootSearchFail
::QuantumExceeded
);
970 let floundered
= strand
.ex_clause
.floundered_subgoals
.len() > 0;
972 debug
!("all remaining subgoals floundered for the table");
974 debug
!("no remaining subgoals for the table");
976 match self.pursue_answer(strand
) {
977 Some(answer_index
) => {
978 debug
!("answer is available");
980 // We found an answer for this strand, and therefore an
981 // answer for this table. Now, this table was either a
982 // subgoal for another strand, or was the root table.
983 let table
= self.stack
.top().table
;
984 match self.stack
.pop_and_take_caller_strand() {
985 Some(caller_strand
) => {
986 self.stack
.top().active_strand
= Some(caller_strand
);
987 return NoRemainingSubgoalsResult
::Success
;
990 // That was the root table, so we are done --
991 // *well*, unless there were delayed
992 // subgoals. In that case, we want to evaluate
993 // those delayed subgoals to completion, so we
994 // have to create a fresh strand that will
995 // take them as goals. Note that we *still
996 // need the original answer in place*, because
997 // we might have to build on it (see the
998 // Delayed Trivial Self Cycle, Variant 3
1001 let answer
= self.forest
.answer(table
, answer_index
);
1002 if let Some(strand
) = self.create_refinement_strand(table
, answer
) {
1003 self.forest
.tables
[table
].enqueue_strand(strand
);
1006 return NoRemainingSubgoalsResult
::RootAnswerAvailable
;
1011 debug
!("answer is not available (or not new)");
1013 // This strand led nowhere of interest. There might be *other*
1014 // answers on this table, but we don't care right now, we'll
1015 // try again at another time.
1017 // Now we yield with `QuantumExceeded`
1018 self.unwind_stack();
1019 return NoRemainingSubgoalsResult
::RootSearchFail(RootSearchFail
::QuantumExceeded
);
1024 /// A "refinement" strand is used in coinduction. When the root
1025 /// table on the stack publishes an answer has delayed subgoals,
1026 /// we create a new strand that will attempt to prove out those
1027 /// delayed subgoals (the root answer here is not *special* except
1028 /// in so far as that there is nothing above it, and hence we know
1029 /// that the delayed subgoals (which resulted in some cycle) must
1030 /// be referring to a table that now has completed).
1032 /// Note that it is important for this to be a *refinement* strand
1033 /// -- meaning that the answer with delayed subgoals has been
1034 /// published. This is necessary because sometimes the strand must
1035 /// build on that very answer that it is refining. See Delayed
1036 /// Trivial Self Cycle, Variant 3.
1037 fn create_refinement_strand(
1041 ) -> Option
<CanonicalStrand
<I
>> {
1042 // If there are no delayed subgoals, then there is no need for
1043 // a refinement strand.
1044 if answer
.subst
.value
.delayed_subgoals
.is_empty() {
1048 let num_universes
= self.forest
.tables
[table
].table_goal
.universes
;
1049 let (table
, subst
, constraints
, delayed_subgoals
) = self
1051 .instantiate_answer_subst(num_universes
, &answer
.subst
);
1053 let delayed_subgoals
= delayed_subgoals
1055 .map(Literal
::Positive
)
1058 let strand
= Strand
{
1060 ex_clause
: ExClause
{
1062 ambiguous
: answer
.ambiguous
,
1064 subgoals
: delayed_subgoals
,
1065 delayed_subgoals
: Vec
::new(),
1066 answer_time
: TimeStamp
::default(),
1067 floundered_subgoals
: Vec
::new(),
1069 selected_subgoal
: None
,
1070 last_pursued_time
: TimeStamp
::default(),
1073 Some(Forest
::canonicalize_strand(self.context
, strand
))
1076 fn on_no_strands_left(&mut self) -> Result
<(), RootSearchFail
> {
1077 debug
!("no more strands available (or all cycles)");
1079 // No more strands left to try! This is either because all
1080 // strands have failed, because all strands encountered a
1081 // cycle, or all strands have would give ambiguous answers.
1083 let table
= self.stack
.top().table
;
1084 if self.forest
.tables
[table
].strands_mut().count() == 0 {
1085 // All strands for the table T on the top of the stack
1086 // have **failed**. Hence we can pop it off the stack and
1087 // check what this means for the table T' that was just
1088 // below T on the stack (if any).
1089 debug
!("no more strands available");
1090 let caller_strand
= match self.stack
.pop_and_borrow_caller_strand() {
1093 // T was the root table, so we are done.
1094 debug
!("no more solutions");
1095 return Err(RootSearchFail
::NoMoreSolutions
);
1099 // This subgoal selection for the strand is finished, so take it
1100 let caller_selected_subgoal
= caller_strand
.selected_subgoal
.take().unwrap();
1101 return match caller_strand
.ex_clause
.subgoals
[caller_selected_subgoal
.subgoal_index
] {
1102 // T' wanted an answer from T, but none is
1103 // forthcoming. Therefore, the active strand from T'
1104 // has failed and can be discarded.
1105 Literal
::Positive(_
) => {
1106 debug
!("discarding strand because positive literal");
1107 self.stack
.top().active_strand
.take();
1108 self.unwind_stack();
1109 Err(RootSearchFail
::QuantumExceeded
)
1112 // T' wanted there to be no answer from T, but none is forthcoming.
1113 Literal
::Negative(_
) => {
1114 debug
!("subgoal was proven because negative literal");
1116 // There is no solution for this strand. But, this
1117 // is what we want, so can remove this subgoal and
1122 .remove(caller_selected_subgoal
.subgoal_index
);
1124 // This strand is still active, so continue
1130 let num_universes
= self.forest
.tables
[table
].table_goal
.universes
;
1131 let table_answer_mode
= self.forest
.tables
[table
].answer_mode
;
1132 let forest
= &mut self.forest
;
1133 let context
= &self.context
;
1134 let strand_is_participating
= |strand
: &CanonicalStrand
<I
>| {
1135 let (_
, ex_clause
) =
1136 context
.instantiate_ex_clause(num_universes
, &strand
.canonical_ex_clause
);
1137 match (table_answer_mode
, ex_clause
.ambiguous
) {
1138 (AnswerMode
::Complete
, true) => false,
1139 (AnswerMode
::Complete
, false) => true,
1140 (AnswerMode
::Ambiguous
, _
) => true,
1143 if forest
.tables
[table
]
1145 .all(|s
| !strand_is_participating(s
))
1147 // If no strands are participating, then that means they are all
1148 // ambiguous and we are in complete mode.
1149 debug
!("All strands would return ambiguous answers.");
1150 match self.forest
.tables
[table
].answer_mode
{
1151 AnswerMode
::Complete
=> {
1152 debug
!("Allowing ambiguous answers.");
1153 self.forest
.tables
[table
].answer_mode
= AnswerMode
::Ambiguous
;
1154 return Err(RootSearchFail
::QuantumExceeded
);
1156 AnswerMode
::Ambiguous
=> {
1162 let clock
= self.stack
.top().clock
;
1163 let cyclic_minimums
= self.stack
.top().cyclic_minimums
;
1164 if cyclic_minimums
.positive
>= clock
&& cyclic_minimums
.negative
>= clock
{
1165 debug
!("cycle with no new answers");
1167 if cyclic_minimums
.negative
< TimeStamp
::MAX
{
1168 // This is a negative cycle.
1169 self.unwind_stack();
1170 return Err(RootSearchFail
::NegativeCycle
);
1173 // If all the things that we recursively depend on have
1174 // positive dependencies on things below us in the stack,
1175 // then no more answers are forthcoming. We can clear all
1176 // the strands for those things recursively.
1177 let table
= self.stack
.top().table
;
1178 // N.B. If we try to pursue a strand and it's found to be ambiguous,
1179 // we know that isn't part of a cycle.
1180 let cyclic_strands
= self.forest
.tables
[table
].drain_strands(strand_is_participating
);
1181 self.clear_strands_after_cycle(cyclic_strands
);
1183 // Now we yield with `QuantumExceeded`
1184 self.unwind_stack();
1185 return Err(RootSearchFail
::QuantumExceeded
);
1187 debug
!("table part of a cycle");
1189 // This table resulted in a positive cycle, so we have
1190 // to check what this means for the subgoal containing
1192 let caller_strand
= match self.stack
.pop_and_borrow_caller_strand() {
1195 panic
!("nothing on the stack but cyclic result");
1199 // We can't take this because we might need it later to clear the cycle
1200 let caller_selected_subgoal
= caller_strand
.selected_subgoal
.as_ref().unwrap();
1201 match caller_strand
.ex_clause
.subgoals
[caller_selected_subgoal
.subgoal_index
] {
1202 Literal
::Positive(_
) => {
1206 .take_minimums(&cyclic_minimums
);
1208 Literal
::Negative(_
) => {
1209 // We depend on `not(subgoal)`. For us to continue,
1210 // `subgoal` must be completely evaluated. Therefore,
1211 // we depend (negatively) on the minimum link of
1212 // `subgoal` as a whole -- it doesn't matter whether
1214 let mins
= Minimums
{
1215 positive
: self.stack
.top().clock
,
1216 negative
: cyclic_minimums
.minimum_of_pos_and_neg(),
1218 self.stack
.top().cyclic_minimums
.take_minimums(&mins
);
1222 // We can't pursue this strand anymore, so push it back onto the table
1223 let active_strand
= self.stack
.top().active_strand
.take().unwrap();
1224 let table
= self.stack
.top().table
;
1225 let canonical_active_strand
= Forest
::canonicalize_strand(self.context
, active_strand
);
1226 self.forest
.tables
[table
].enqueue_strand(canonical_active_strand
);
1228 // The strand isn't active, but the table is, so just continue
1233 /// Unwinds the entire stack, returning all active strands back to
1234 /// their tables (this time at the end of the queue).
1235 fn unwind_stack(&mut self) {
1237 match self.stack
.pop_and_take_caller_strand() {
1238 Some(active_strand
) => {
1239 let table
= self.stack
.top().table
;
1240 let canonical_active_strand
=
1241 Forest
::canonicalize_strand(self.context
, active_strand
);
1242 self.forest
.tables
[table
].enqueue_strand(canonical_active_strand
);
1250 /// Invoked after we have determined that every strand in `table`
1251 /// encounters a cycle; `strands` is the set of strands (which
1252 /// have been moved out of the table). This method then
1253 /// recursively clears the active strands from the tables
1254 /// referenced in `strands`, since all of them must encounter
1256 fn clear_strands_after_cycle(&mut self, strands
: impl IntoIterator
<Item
= CanonicalStrand
<I
>>) {
1257 for strand
in strands
{
1258 let CanonicalStrand
{
1259 canonical_ex_clause
,
1261 last_pursued_time
: _
,
1263 let selected_subgoal
= selected_subgoal
.unwrap_or_else(|| {
1265 "clear_strands_after_cycle invoked on strand in table \
1266 without a selected subgoal: {:?}",
1267 canonical_ex_clause
,
1271 let strand_table
= selected_subgoal
.subgoal_table
;
1272 let strands
= self.forest
.tables
[strand_table
].take_strands();
1273 self.clear_strands_after_cycle(strands
);
1277 fn select_subgoal(&mut self, mut strand
: &mut Strand
<I
, C
>) -> SubGoalSelection
{
1279 while strand
.selected_subgoal
.is_none() {
1280 if strand
.ex_clause
.subgoals
.is_empty() {
1281 if strand
.ex_clause
.floundered_subgoals
.is_empty() {
1282 return SubGoalSelection
::NotSelected
;
1285 self.reconsider_floundered_subgoals(&mut strand
.ex_clause
);
1287 if strand
.ex_clause
.subgoals
.is_empty() {
1288 // All the subgoals of this strand floundered. We may be able
1289 // to get helpful information from this strand still, but it
1290 // will *always* be ambiguous, so mark it as so.
1291 assert
!(!strand
.ex_clause
.floundered_subgoals
.is_empty());
1292 strand
.ex_clause
.ambiguous
= true;
1293 return SubGoalSelection
::NotSelected
;
1299 let subgoal_index
= C
::next_subgoal_index(&strand
.ex_clause
);
1301 // Get or create table for this subgoal.
1302 match self.forest
.get_or_create_table_for_subgoal(
1305 &strand
.ex_clause
.subgoals
[subgoal_index
],
1307 Some((subgoal_table
, universe_map
)) => {
1308 strand
.selected_subgoal
= Some(SelectedSubgoal
{
1312 answer_index
: AnswerIndex
::ZERO
,
1317 // If we failed to create a table for the subgoal,
1318 // that is because we have a floundered negative
1320 self.flounder_subgoal(&mut strand
.ex_clause
, subgoal_index
);
1325 let selected_subgoal_table
= strand
.selected_subgoal
.as_ref().unwrap().subgoal_table
;
1326 if self.forest
.tables
[selected_subgoal_table
].is_floundered() {
1327 if self.propagate_floundered_subgoal(strand
) {
1328 // This strand will never lead anywhere of interest.
1329 return SubGoalSelection
::NotSelected
;
1331 // This subgoal has floundered and has been marked.
1332 // We previously would immediately mark the table as
1333 // floundered too, and maybe come back to it. Now, we
1334 // try to see if any other subgoals can be pursued first.
1338 return SubGoalSelection
::Selected
;
1343 /// Invoked when a strand represents an **answer**. This means
1344 /// that the strand has no subgoals left. There are two possibilities:
1346 /// - the strand may represent an answer we have already found; in
1347 /// that case, we can return `None`, as this
1348 /// strand led nowhere of interest.
1349 /// - the strand may represent a new answer, in which case it is
1350 /// added to the table and `Some(())` is returned.
1351 fn pursue_answer(&mut self, strand
: Strand
<I
, C
>) -> Option
<AnswerIndex
> {
1352 let table
= self.stack
.top().table
;
1363 floundered_subgoals
,
1365 selected_subgoal
: _
,
1366 last_pursued_time
: _
,
1368 // If there are subgoals left, they should be followed
1369 assert
!(subgoals
.is_empty());
1370 // We can still try to get an ambiguous answer if there are floundered subgoals
1371 let floundered
= !floundered_subgoals
.is_empty();
1372 // So let's make sure that it *really* is an ambiguous answer (this should be set previously)
1373 assert
!(!floundered
|| ambiguous
);
1375 // FIXME: If there are floundered subgoals, we *could* potentially
1376 // actually check if the partial answers to any of these subgoals
1377 // conflict. But this requires that we think about whether they are
1378 // positive or negative subgoals. This duplicates some of the logic
1379 // in `merge_answer_into_strand`, so a bit of refactoring is needed.
1381 // If the answer gets too large, mark the table as floundered.
1382 // This is the *most conservative* course. There are a few alternatives:
1383 // 1) Replace the answer with a truncated version of it. (This was done
1384 // previously, but turned out to be more complicated than we wanted and
1385 // and a source of multiple bugs.)
1386 // 2) Mark this *strand* as floundered. We don't currently have a mechanism
1387 // for this (only floundered subgoals), so implementing this is more
1388 // difficult because we don't want to just *remove* this strand from the
1389 // table, because that might make the table give `NoMoreSolutions`, which
1391 // 3) Do something fancy with delayed subgoals, effectively delayed the
1392 // truncated bits to a different strand (and a more "refined" answer).
1393 // (This one probably needs more thought, but is here for "completeness")
1395 // Ultimately, the current decision to flounder the entire table mostly boils
1396 // down to "it works as we expect for the current tests". And, we likely don't
1397 // even *need* the added complexity just for potentially more answers.
1398 if infer
.answer_needs_truncation(self.context
.interner(), &subst
) {
1399 self.forest
.tables
[table
].mark_floundered();
1403 let table_goal
= &self.forest
.tables
[table
].table_goal
;
1405 // FIXME: Avoid double canonicalization
1406 let filtered_delayed_subgoals
= delayed_subgoals
1408 .filter(|delayed_subgoal
| {
1409 let (canonicalized
, _
) =
1410 infer
.fully_canonicalize_goal(self.context
.interner(), delayed_subgoal
);
1411 *table_goal
!= canonicalized
1415 let subst
= infer
.canonicalize_answer_subst(
1416 self.context
.interner(),
1419 filtered_delayed_subgoals
,
1422 "answer: table={:?}, subst={:?}, floundered={:?}",
1423 table
, subst
, floundered
1426 let answer
= Answer { subst, ambiguous }
;
1428 // A "trivial" answer is one that is 'just true for all cases'
1429 // -- in other words, it gives no information back to the
1430 // caller. For example, `Vec<u32>: Sized` is "just true".
1431 // Such answers are important because they are the most
1432 // general case, and after we provide a trivial answer, no
1433 // further answers are useful -- therefore we can clear any
1434 // further pending strands (this is a "green cut", in
1435 // Prolog parlance).
1437 // This optimization is *crucial* for performance: for
1438 // example, `projection_from_env_slow` fails miserably without
1439 // it. The reason is that we wind up (thanks to implied bounds)
1440 // with a clause like this:
1443 // forall<T> { (<T as SliceExt>::Item: Clone) :- WF(T: SliceExt) }
1446 // we then apply that clause to `!1: Clone`, resulting in the
1447 // table goal `!1: Clone :- <?0 as SliceExt>::Item = !1,
1448 // WF(?0: SliceExt)`. This causes us to **enumerate all types
1449 // `?0` that where `Slice<?0>` normalizes to `!1` -- this is
1450 // an infinite set of types, effectively. Interestingly,
1451 // though, we only need one and we are done, because (if you
1452 // look) our goal (`!1: Clone`) doesn't have any output
1455 // This is actually a kind of general case. Due to Rust's rule
1456 // about constrained impl type parameters, generally speaking
1457 // when we have some free inference variable (like `?0`)
1458 // within our clause, it must appear in the head of the
1459 // clause. This means that the values we create for it will
1460 // propagate up to the caller, and they will quickly surmise
1461 // that there is ambiguity and stop requesting more answers.
1462 // Indeed, the only exception to this rule about constrained
1463 // type parameters if with associated type projections, as in
1466 // (Actually, because of the trivial answer cut off rule, we
1467 // never even get to the point of asking the query above in
1468 // `projection_from_env_slow`.)
1470 // However, there is one fly in the ointment: answers include
1471 // region constraints, and you might imagine that we could
1472 // find future answers that are also trivial but with distinct
1473 // sets of region constraints. **For this reason, we only
1474 // apply this green cut rule if the set of generated
1475 // constraints is empty.**
1477 // The limitation on region constraints is quite a drag! We
1478 // can probably do better, though: for example, coherence
1479 // guarantees that, for any given set of types, only a single
1480 // impl ought to be applicable, and that impl can only impose
1481 // one set of region constraints. However, it's not quite that
1482 // simple, thanks to specialization as well as the possibility
1483 // of proving things from the environment (though the latter
1484 // is a *bit* suspect; e.g., those things in the environment
1485 // must be backed by an impl *eventually*).
1486 let is_trivial_answer
= {
1488 .is_trivial_substitution(&self.forest
.tables
[table
].table_goal
, &answer
.subst
)
1489 && answer
.subst
.value
.constraints
.is_empty()
1492 if let Some(answer_index
) = self.forest
.tables
[table
].push_answer(answer
) {
1493 // See above, if we have a *complete* and trivial answer, we don't
1494 // want to follow any more strands
1495 if !ambiguous
&& is_trivial_answer
{
1496 self.forest
.tables
[table
].take_strands();
1501 info
!("answer: not a new answer, returning None");
1506 fn reconsider_floundered_subgoals(&mut self, ex_clause
: &mut ExClause
<I
>) {
1507 info
!("reconsider_floundered_subgoals(ex_clause={:#?})", ex_clause
,);
1511 floundered_subgoals
,
1514 for i
in (0..floundered_subgoals
.len()).rev() {
1515 if floundered_subgoals
[i
].floundered_time
< *answer_time
{
1516 let floundered_subgoal
= floundered_subgoals
.swap_remove(i
);
1517 subgoals
.push(floundered_subgoal
.floundered_literal
);
1522 /// Removes the subgoal at `subgoal_index` from the strand's
1523 /// subgoal list and adds it to the strand's floundered subgoal
1525 fn flounder_subgoal(&self, ex_clause
: &mut ExClause
<I
>, subgoal_index
: usize) {
1526 let _s
= debug_span
!(
1528 answer_time
= ?ex_clause
.answer_time
,
1529 subgoal
= ?ex_clause
.subgoals
[subgoal_index
],
1531 let _s
= _s
.enter();
1533 let floundered_time
= ex_clause
.answer_time
;
1534 let floundered_literal
= ex_clause
.subgoals
.remove(subgoal_index
);
1535 ex_clause
.floundered_subgoals
.push(FlounderedSubgoal
{
1539 debug
!("flounder_subgoal: ex_clause={:#?}", ex_clause
);
1542 /// True if all the tables on the stack starting from `depth` and
1543 /// continuing until the top of the stack are coinductive.
1545 /// Example: Given a program like:
1548 /// struct Foo { a: Option<Box<Bar>> }
1549 /// struct Bar { a: Option<Box<Foo>> }
1551 /// impl<T: Send> XXX for T { }
1554 /// and then a goal of `Foo: XXX`, we would eventually wind up
1555 /// with a stack like this:
1557 /// | StackIndex | Table Goal |
1558 /// | ---------- | ----------- |
1559 /// | 0 | `Foo: XXX` |
1560 /// | 1 | `Foo: Send` |
1561 /// | 2 | `Bar: Send` |
1563 /// Here, the top of the stack is `Bar: Send`. And now we are
1564 /// asking `top_of_stack_is_coinductive_from(1)` -- the answer
1565 /// would be true, since `Send` is an auto trait, which yields a
1566 /// coinductive goal. But `top_of_stack_is_coinductive_from(0)` is
1567 /// false, since `XXX` is not an auto trait.
1568 pub(super) fn top_of_stack_is_coinductive_from(&self, depth
: StackIndex
) -> bool
{
1569 StackIndex
::iterate_range(self.stack
.top_of_stack_from(depth
)).all(|d
| {
1570 let table
= self.stack
[d
].table
;
1571 self.forest
.tables
[table
].coinductive_goal