diff options
Diffstat (limited to 'vendor/chalk-engine/src/logic.rs')
| -rw-r--r-- | vendor/chalk-engine/src/logic.rs | 1648 |
1 files changed, 1648 insertions, 0 deletions
diff --git a/vendor/chalk-engine/src/logic.rs b/vendor/chalk-engine/src/logic.rs new file mode 100644 index 000000000..681f6e7ed --- /dev/null +++ b/vendor/chalk-engine/src/logic.rs @@ -0,0 +1,1648 @@ +use crate::forest::Forest; +use crate::normalize_deep::DeepNormalizer; +use crate::slg::{ResolventOps, SlgContext, SlgContextOps}; +use crate::stack::{Stack, StackIndex}; +use crate::strand::{CanonicalStrand, SelectedSubgoal, Strand}; +use crate::table::{AnswerIndex, Table}; +use crate::{ + Answer, AnswerMode, CompleteAnswer, ExClause, FlounderedSubgoal, Literal, Minimums, TableIndex, + TimeStamp, +}; + +use chalk_ir::could_match::CouldMatch; +use chalk_ir::interner::Interner; +use chalk_ir::{ + AnswerSubst, Canonical, ConstrainedSubst, Constraints, FallibleOrFloundered, Floundered, Goal, + GoalData, InEnvironment, NoSolution, ProgramClause, Substitution, UCanonical, UniverseMap, +}; +use chalk_solve::clauses::program_clauses_that_could_match; +use chalk_solve::coinductive_goal::IsCoinductive; +use chalk_solve::infer::ucanonicalize::UCanonicalized; +use chalk_solve::infer::InferenceTable; +use chalk_solve::solve::truncate; +use tracing::{debug, debug_span, info, instrument}; + +type RootSearchResult<T> = Result<T, RootSearchFail>; + +/// The different ways that a *root* search (which potentially pursues +/// many strands) can fail. A root search is one that begins with an +/// empty stack. +#[derive(Debug)] +pub(super) enum RootSearchFail { + /// The table we were trying to solve cannot succeed. + NoMoreSolutions, + + /// The table cannot be solved without more type information. + Floundered, + + /// We did not find a solution, but we still have things to try. + /// Repeat the request, and we'll give one of those a spin. + /// + /// (In a purely depth-first-based solver, like Prolog, this + /// doesn't appear.) + QuantumExceeded, + + /// A negative cycle was found. This is fail-fast, so even if there was + /// possibly a solution (ambiguous or not), it may not have been found. + NegativeCycle, + + /// The current answer index is not useful. Currently, this is returned + /// because the current answer needs refining. + InvalidAnswer, +} + +/// This is returned when we try to select a subgoal for a strand. +#[derive(PartialEq)] +enum SubGoalSelection { + /// A subgoal was successfully selected. It has already been checked + /// to not be floundering. However, it may have an answer already, be + /// coinductive, or create a cycle. + Selected, + + /// This strand has no remaining subgoals, but there may still be + /// floundered subgoals. + NotSelected, +} + +/// This is returned `on_no_remaining_subgoals` +enum NoRemainingSubgoalsResult { + /// There is an answer available for the root table + RootAnswerAvailable, + + /// There was a `RootSearchFail` + RootSearchFail(RootSearchFail), + + // This was a success + Success, +} + +impl<I: Interner> Forest<I> { + /// Returns an answer with a given index for the given table. This + /// may require activating a strand and following it. It returns + /// `Ok(answer)` if they answer is available and otherwise a + /// `RootSearchFail` result. + pub(super) fn root_answer( + &mut self, + context: &SlgContextOps<I>, + table: TableIndex, + answer_index: AnswerIndex, + ) -> RootSearchResult<CompleteAnswer<I>> { + let stack = Stack::default(); + + let mut state = SolveState { + forest: self, + context, + stack, + }; + + match state.ensure_root_answer(table, answer_index) { + Ok(()) => { + assert!(state.stack.is_empty()); + let answer = state.forest.answer(table, answer_index); + if !answer.subst.value.delayed_subgoals.is_empty() { + return Err(RootSearchFail::InvalidAnswer); + } + Ok(CompleteAnswer { + subst: Canonical { + binders: answer.subst.binders.clone(), + value: ConstrainedSubst { + subst: answer.subst.value.subst.clone(), + constraints: answer.subst.value.constraints.clone(), + }, + }, + ambiguous: answer.ambiguous, + }) + } + Err(err) => Err(err), + } + } + + pub(super) fn any_future_answer( + &self, + table: TableIndex, + mut answer_index: AnswerIndex, + mut test: impl FnMut(&Substitution<I>) -> bool, + ) -> bool { + // Check any cached answers, starting at `answer_index`. + while let Some(answer) = self.tables[table].answer(answer_index) { + info!("answer cached = {:?}", answer); + if test(&answer.subst.value.subst) { + return true; + } + answer_index.increment(); + } + + // Check any unsolved strands, which may give further answers. + self.tables[table] + .strands() + .any(|strand| test(&strand.value.ex_clause.subst)) + } + + pub(crate) fn answer(&self, table: TableIndex, answer: AnswerIndex) -> &Answer<I> { + self.tables[table].answer(answer).unwrap() + } + + fn canonicalize_strand_from( + context: &SlgContextOps<I>, + infer: &mut InferenceTable<I>, + strand: &Strand<I>, + ) -> CanonicalStrand<I> { + infer + .canonicalize(context.program().interner(), strand.clone()) + .quantified + } + + /// Given a subgoal, converts the literal into u-canonical form + /// and searches for an existing table. If one is found, it is + /// returned, but otherwise a new table is created (and populated + /// with its initial set of strands). + /// + /// Returns `None` if the literal cannot be converted into a table + /// -- for example, this can occur when we have selected a + /// negative literal with free existential variables, in which + /// case the execution is said to "flounder". + /// + /// In terms of the NFTD paper, creating a new table corresponds + /// to the *New Subgoal* step as well as the *Program Clause + /// Resolution* steps. + #[instrument(level = "debug", skip(self, context, infer))] + fn get_or_create_table_for_subgoal( + &mut self, + context: &SlgContextOps<I>, + infer: &mut InferenceTable<I>, + subgoal: &Literal<I>, + ) -> Option<(TableIndex, UniverseMap)> { + // Subgoal abstraction: + let (ucanonical_subgoal, universe_map) = match subgoal { + Literal::Positive(subgoal) => { + Forest::abstract_positive_literal(context, infer, subgoal.clone())? + } + Literal::Negative(subgoal) => { + Forest::abstract_negative_literal(context, infer, subgoal.clone())? + } + }; + + debug!(?ucanonical_subgoal, ?universe_map); + + let table = self.get_or_create_table_for_ucanonical_goal(context, ucanonical_subgoal); + + Some((table, universe_map)) + } + + /// Given a u-canonical goal, searches for an existing table. If + /// one is found, it is returned, but otherwise a new table is + /// created (and populated with its initial set of strands). + /// + /// In terms of the NFTD paper, creating a new table corresponds + /// to the *New Subgoal* step as well as the *Program Clause + /// Resolution* steps. + #[instrument(level = "debug", skip(self, context))] + pub(crate) fn get_or_create_table_for_ucanonical_goal( + &mut self, + context: &SlgContextOps<I>, + goal: UCanonical<InEnvironment<Goal<I>>>, + ) -> TableIndex { + if let Some(table) = self.tables.index_of(&goal) { + debug!(?table, "found existing table"); + return table; + } + + info!( + table = ?self.tables.next_index(), + "creating new table with goal = {:#?}", + goal, + ); + let table = Self::build_table(context, self.tables.next_index(), goal); + self.tables.insert(table) + } + + /// When a table is first created, this function is invoked to + /// create the initial set of strands. If the table represents a + /// domain goal, these strands are created from the program + /// clauses as well as the clauses found in the environment. If + /// the table represents a non-domain goal, such as `for<T> G` + /// etc, then `simplify_goal` is invoked to create a strand + /// that breaks the goal down. + /// + /// In terms of the NFTD paper, this corresponds to the *Program + /// Clause Resolution* step being applied eagerly, as many times + /// as possible. + fn build_table( + context: &SlgContextOps<I>, + table_idx: TableIndex, + goal: UCanonical<InEnvironment<Goal<I>>>, + ) -> Table<I> { + let coinductive = goal.is_coinductive(context.program()); + let mut table = Table::new(goal.clone(), coinductive); + + let goal_data = goal.canonical.value.goal.data(context.program().interner()); + match goal_data { + GoalData::DomainGoal(domain_goal) => { + let canon_domain_goal = UCanonical { + canonical: Canonical { + binders: goal.canonical.binders, + value: InEnvironment::new( + &goal.canonical.value.environment, + domain_goal.clone(), + ), + }, + universes: goal.universes, + }; + + let db = context.program(); + let canon_goal = canon_domain_goal.canonical.value.goal.clone(); + let could_match = |c: &ProgramClause<I>| { + c.could_match(db.interner(), db.unification_database(), &canon_goal) + }; + + match program_clauses_that_could_match(db, &canon_domain_goal) { + Ok(mut clauses) => { + clauses.retain(could_match); + clauses.extend(db.custom_clauses().into_iter().filter(could_match)); + + let (infer, subst, goal) = + chalk_solve::infer::InferenceTable::from_canonical( + context.program().interner(), + canon_domain_goal.universes, + canon_domain_goal.canonical, + ); + + clauses.extend( + db.program_clauses_for_env(&goal.environment) + .iter(db.interner()) + .cloned() + .filter(could_match), + ); + + let InEnvironment { environment, goal } = goal; + + for clause in clauses { + info!("program clause = {:#?}", clause); + let mut infer = infer.clone(); + if let Ok(resolvent) = infer.resolvent_clause( + context.unification_database(), + context.program().interner(), + &environment, + &goal, + &subst, + &clause, + ) { + info!("pushing initial strand with ex-clause: {:#?}", &resolvent,); + let strand = Strand { + ex_clause: resolvent, + selected_subgoal: None, + last_pursued_time: TimeStamp::default(), + }; + let canonical_strand = + Self::canonicalize_strand_from(context, &mut infer, &strand); + table.enqueue_strand(canonical_strand); + } + } + } + Err(Floundered) => { + debug!( + table = ?table_idx, + "Marking table {:?} as floundered! (failed to create program clauses)", + table_idx + ); + table.mark_floundered(); + } + } + } + + _ => { + let (mut infer, subst, InEnvironment { environment, goal }) = + chalk_solve::infer::InferenceTable::from_canonical( + context.program().interner(), + goal.universes, + goal.canonical, + ); + // The goal for this table is not a domain goal, so we instead + // simplify it into a series of *literals*, all of which must be + // true. Thus, in EWFS terms, we are effectively creating a + // single child of the `A :- A` goal that is like `A :- B, C, D` + // where B, C, and D are the simplified subgoals. You can think + // of this as applying built-in "meta program clauses" that + // reduce goals into Domain goals. + match Self::simplify_goal(context, &mut infer, subst, environment, goal) { + FallibleOrFloundered::Ok(ex_clause) => { + info!( + ex_clause = ?DeepNormalizer::normalize_deep( + &mut infer, + context.program().interner(), + ex_clause.clone(), + ), + "pushing initial strand" + ); + let strand = Strand { + ex_clause, + selected_subgoal: None, + last_pursued_time: TimeStamp::default(), + }; + let canonical_strand = + Self::canonicalize_strand_from(context, &mut infer, &strand); + table.enqueue_strand(canonical_strand); + } + FallibleOrFloundered::NoSolution => {} + FallibleOrFloundered::Floundered => table.mark_floundered(), + } + } + } + + table + } + + /// Given a selected positive subgoal, applies the subgoal + /// abstraction function to yield the canonical form that will be + /// used to pick a table. Typically, this abstraction has no + /// effect, and hence we are simply returning the canonical form + /// of `subgoal`; but if the subgoal is getting too big, we return + /// `None`, which causes the subgoal to flounder. + fn abstract_positive_literal( + context: &SlgContextOps<I>, + infer: &mut InferenceTable<I>, + subgoal: InEnvironment<Goal<I>>, + ) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)> { + if truncate::needs_truncation( + context.program().interner(), + infer, + context.max_size(), + &subgoal, + ) { + None + } else { + let canonicalized_goal = infer + .canonicalize(context.program().interner(), subgoal) + .quantified; + let UCanonicalized { + quantified, + universes, + } = InferenceTable::u_canonicalize(context.program().interner(), &canonicalized_goal); + Some((quantified, universes)) + } + } + + /// Given a selected negative subgoal, the subgoal is "inverted" + /// (see `InferenceTable<I, C>::invert`) and then potentially truncated + /// (see `abstract_positive_literal`). The result subgoal is + /// canonicalized. In some cases, this may return `None` and hence + /// fail to yield a useful result, for example if free existential + /// variables appear in `subgoal` (in which case the execution is + /// said to "flounder"). + fn abstract_negative_literal( + context: &SlgContextOps<I>, + infer: &mut InferenceTable<I>, + subgoal: InEnvironment<Goal<I>>, + ) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)> { + // First, we have to check that the selected negative literal + // is ground, and invert any universally quantified variables. + // + // DIVERGENCE -- In the RR paper, to ensure completeness, they + // permit non-ground negative literals, but only consider + // them to succeed when the target table has no answers at + // all. This is equivalent inverting those free existentials + // into universals, as discussed in the comments of + // `invert`. This is clearly *sound*, but the completeness is + // a subtle point. In particular, it can cause **us** to reach + // false conclusions, because e.g. given a program like + // (selected left-to-right): + // + // not { ?T: Copy }, ?T = Vec<u32> + // + // we would select `not { ?T: Copy }` first. For this goal to + // succeed we would require that -- effectively -- `forall<T> + // { not { T: Copy } }`, which clearly doesn't hold. (In the + // terms of RR, we would require that the table for `?T: Copy` + // has failed before we can continue.) + // + // In the RR paper, this is acceptable because they assume all + // of their input programs are both **normal** (negative + // literals are selected after positive ones) and **safe** + // (all free variables in negative literals occur in positive + // literals). It is plausible for us to guarantee "normal" + // form, we can reorder clauses as we need. I suspect we can + // guarantee safety too, but I have to think about it. + // + // For now, we opt for the safer route of terming such + // executions as floundering, because I think our use of + // negative goals is sufficiently limited we can get away with + // it. The practical effect is that we will judge more + // executions as floundering than we ought to (i.e., where we + // could instead generate an (imprecise) result). As you can + // see a bit later, we also diverge in some other aspects that + // affect completeness when it comes to subgoal abstraction. + let inverted_subgoal = infer.invert(context.program().interner(), subgoal)?; + + if truncate::needs_truncation( + context.program().interner(), + infer, + context.max_size(), + &inverted_subgoal, + ) { + None + } else { + let canonicalized_goal = infer + .canonicalize(context.program().interner(), inverted_subgoal) + .quantified; + let UCanonicalized { + quantified, + universes, + } = InferenceTable::u_canonicalize(context.program().interner(), &canonicalized_goal); + Some((quantified, universes)) + } + } +} + +pub(crate) struct SolveState<'forest, I: Interner> { + forest: &'forest mut Forest<I>, + context: &'forest SlgContextOps<'forest, I>, + stack: Stack<I>, +} + +impl<'forest, I: Interner> Drop for SolveState<'forest, I> { + fn drop(&mut self) { + if !self.stack.is_empty() { + if let Some(active_strand) = self.stack.top().active_strand.take() { + let table = self.stack.top().table; + self.forest.tables[table].enqueue_strand(active_strand); + } + self.unwind_stack(); + } + } +} + +impl<'forest, I: Interner> SolveState<'forest, I> { + /// Ensures that answer with the given index is available from the + /// given table. Returns `Ok` if there is an answer. + /// + /// This function first attempts to fetch answer that is cached in + /// the table. If none is found, then it will recursively search + /// to find an answer. + #[instrument(level = "info", skip(self))] + fn ensure_root_answer( + &mut self, + initial_table: TableIndex, + initial_answer: AnswerIndex, + ) -> RootSearchResult<()> { + info!( + "table goal = {:#?}", + self.forest.tables[initial_table].table_goal + ); + // Check if this table has floundered. + if self.forest.tables[initial_table].is_floundered() { + return Err(RootSearchFail::Floundered); + } + // Check for a tabled answer. + if let Some(answer) = self.forest.tables[initial_table].answer(initial_answer) { + info!("answer cached = {:?}", answer); + return Ok(()); + } + + // If no tabled answer is present, we ought to be requesting + // the next available index. + assert_eq!( + self.forest.tables[initial_table].next_answer_index(), + initial_answer + ); + + self.stack + .push(initial_table, Minimums::MAX, self.forest.increment_clock()); + loop { + let clock = self.stack.top().clock; + // If we had an active strand, continue to pursue it + let table = self.stack.top().table; + let table_answer_mode = self.forest.tables[table].answer_mode; + + // We track when we last pursued each strand. If all the strands have been + // pursued at this depth, then that means they all encountered a cycle. + // We also know that if the first strand has been pursued at this depth, + // then all have. Otherwise, an answer to any strand would have provided an + // answer for the table. + let forest = &mut self.forest; + let next_strand = self.stack.top().active_strand.take().or_else(|| { + forest.tables[table].dequeue_next_strand_that(|strand| { + let time_eligble = strand.value.last_pursued_time < clock; + let mode_eligble = match (table_answer_mode, strand.value.ex_clause.ambiguous) { + (AnswerMode::Complete, false) => true, + (AnswerMode::Complete, true) => false, + (AnswerMode::Ambiguous, _) => true, + }; + time_eligble && mode_eligble + }) + }); + match next_strand { + Some(mut canonical_strand) => { + debug!("starting next strand = {:#?}", canonical_strand); + + canonical_strand.value.last_pursued_time = clock; + match self.select_subgoal(&mut canonical_strand) { + SubGoalSelection::Selected => { + // A subgoal has been selected. We now check this subgoal + // table for an existing answer or if it's in a cycle. + // If neither of those are the case, a strand is selected + // and the next loop iteration happens. + self.on_subgoal_selected(canonical_strand)?; + continue; + } + SubGoalSelection::NotSelected => { + match self.on_no_remaining_subgoals(canonical_strand) { + NoRemainingSubgoalsResult::RootAnswerAvailable => return Ok(()), + NoRemainingSubgoalsResult::RootSearchFail(e) => return Err(e), + NoRemainingSubgoalsResult::Success => continue, + }; + } + } + } + None => { + self.on_no_strands_left()?; + continue; + } + } + } + } + + /// This is called when an answer is available for the selected subgoal + /// of the strand. First, if the selected subgoal is a `Positive` subgoal, + /// it first clones the strand pursuing the next answer. Then, it merges the + /// answer into the provided `Strand`. + /// On success, `Ok` is returned and the `Strand` can be continued to process + /// On failure, `Err` is returned and the `Strand` should be discarded + fn merge_answer_into_strand( + &mut self, + infer: &mut InferenceTable<I>, + strand: &mut Strand<I>, + ) -> RootSearchResult<()> { + // At this point, we know we have an answer for + // the selected subgoal of the strand. + // Now, we have to unify that answer onto the strand. + + // If this answer is ambiguous and we don't want ambiguous answers + // yet, then we act like this is a floundered subgoal. + let ambiguous = { + let selected_subgoal = strand.selected_subgoal.as_ref().unwrap(); + let answer = self.forest.answer( + selected_subgoal.subgoal_table, + selected_subgoal.answer_index, + ); + answer.ambiguous + }; + if let AnswerMode::Complete = self.forest.tables[self.stack.top().table].answer_mode { + if ambiguous { + // FIXME: we could try to be a little bit smarter here. This can + // really be split into cases: + // 1) Cases where no amount of solving will cause this ambiguity to change. + // (e.g. `CannnotProve`) + // 2) Cases where we may be able to get a better answer if we + // solve other subgoals first. + // (e.g. the `non_enumerable_traits_reorder` test) + // We really only need to delay merging an ambiguous answer for + // case 2. Do note, though, that even if we *do* merge the answer + // case 1, we should stop solving this strand when in + // `AnswerMode::Complete` since we wouldn't use this answer yet + // *anyways*. + + // The selected subgoal returned an ambiguous answer, but we don't want that. + // So, we treat this subgoal as floundered. + let selected_subgoal = strand.selected_subgoal.take().unwrap(); + self.flounder_subgoal(&mut strand.ex_clause, selected_subgoal.subgoal_index); + return Ok(()); + } + } + + // If this subgoal was a `Positive` one, whichever way this + // particular answer turns out, there may yet be *more* answers, + // if this isn't a trivial substitution. + // Enqueue that alternative for later. + // NOTE: this is separate from the match below because we `take` the selected_subgoal + // below, but here we keep it for the new `Strand`. + let selected_subgoal = strand.selected_subgoal.as_ref().unwrap(); + if let Literal::Positive(_) = strand.ex_clause.subgoals[selected_subgoal.subgoal_index] { + let answer = self.forest.answer( + selected_subgoal.subgoal_table, + selected_subgoal.answer_index, + ); + if !self.forest.tables[selected_subgoal.subgoal_table] + .table_goal + .is_trivial_substitution(self.context.program().interner(), &answer.subst) + { + let mut next_subgoal = selected_subgoal.clone(); + next_subgoal.answer_index.increment(); + let next_strand = Strand { + ex_clause: strand.ex_clause.clone(), + selected_subgoal: Some(next_subgoal), + last_pursued_time: strand.last_pursued_time, + }; + let table = self.stack.top().table; + let canonical_next_strand = + Forest::canonicalize_strand_from(self.context, infer, &next_strand); + self.forest.tables[table].enqueue_strand(canonical_next_strand); + } + } + + // Deselect and remove the selected subgoal, now that we have an answer for it. + let selected_subgoal = strand.selected_subgoal.take().unwrap(); + let subgoal = strand + .ex_clause + .subgoals + .remove(selected_subgoal.subgoal_index); + match subgoal { + Literal::Positive(subgoal) => { + let SelectedSubgoal { + subgoal_index: _, + subgoal_table, + answer_index, + ref universe_map, + } = selected_subgoal; + use chalk_solve::infer::ucanonicalize::UniverseMapExt; + let table_goal = universe_map.map_from_canonical( + self.context.program().interner(), + &self.forest.tables[subgoal_table].table_goal.canonical, + ); + let answer_subst = universe_map.map_from_canonical( + self.context.program().interner(), + &self.forest.answer(subgoal_table, answer_index).subst, + ); + match infer.apply_answer_subst( + self.context.program().interner(), + self.context.unification_database(), + &mut strand.ex_clause, + &subgoal, + &table_goal, + answer_subst, + ) { + Ok(()) => { + let ex_clause = &mut strand.ex_clause; + + // If the answer had was ambiguous, we have to + // ensure that `ex_clause` is also ambiguous. This is + // the SLG FACTOR operation, though NFTD just makes it + // part of computing the SLG resolvent. + if self.forest.answer(subgoal_table, answer_index).ambiguous { + debug!("Marking Strand as ambiguous because answer to (positive) subgoal was ambiguous"); + ex_clause.ambiguous = true; + } + + // Increment the answer time for the `ex_clause`. Floundered + // subgoals may be eligble to be pursued again. + ex_clause.answer_time.increment(); + + // Ok, we've applied the answer to this Strand. + Ok(()) + } + + // This answer led nowhere. Give up for now, but of course + // there may still be other strands to pursue, so return + // `QuantumExceeded`. + Err(NoSolution) => { + info!("answer not unifiable -> NoSolution"); + // This strand as no solution. It is no longer active, + // so it dropped at the end of this scope. + + // Now we want to propogate back to the up with `QuantumExceeded` + self.unwind_stack(); + Err(RootSearchFail::QuantumExceeded) + } + } + } + Literal::Negative(_) => { + let SelectedSubgoal { + subgoal_index: _, + subgoal_table, + answer_index, + universe_map: _, + } = selected_subgoal; + // We got back an answer. This is bad, because we want + // to disprove the subgoal, but it may be + // "conditional" (maybe true, maybe not). + let answer = self.forest.answer(subgoal_table, answer_index); + + // By construction, we do not expect negative subgoals + // to have delayed subgoals. This is because we do not + // need to permit `not { L }` where `L` is a + // coinductive goal. We could improve this if needed, + // but it keeps things simple. + if !answer.subst.value.delayed_subgoals.is_empty() { + panic!("Negative subgoal had delayed_subgoals"); + } + + if !answer.ambiguous { + // We want to disproval the subgoal, but we + // have an unconditional answer for the subgoal, + // therefore we have failed to disprove it. + info!("found unconditional answer to neg literal -> NoSolution"); + + // This strand as no solution. By returning an Err, + // the caller should discard this `Strand`. + + // Now we want to propogate back to the up with `QuantumExceeded` + self.unwind_stack(); + return Err(RootSearchFail::QuantumExceeded); + } + + // Otherwise, the answer is ambiguous. We can keep going, + // but we have to mark our strand, too, as ambiguous. + // + // We want to disproval the subgoal, but we + // have an unconditional answer for the subgoal, + // therefore we have failed to disprove it. + debug!(?strand, "Marking Strand as ambiguous because answer to (negative) subgoal was ambiguous"); + strand.ex_clause.ambiguous = true; + + // Strand is ambigious. + Ok(()) + } + } + } + + /// This is called when the selected subgoal for a strand has floundered. + /// We have to decide what this means for the strand. + /// - If the strand was positively dependent on the subgoal, we flounder, + /// the subgoal, then return `false`. This strand may be able to be + /// retried later. + /// - If the strand was negatively dependent on the subgoal, then strand + /// has led nowhere of interest and we return `true`. This strand should + /// be discarded. + /// + /// In other words, we return whether this strand flounders. + fn propagate_floundered_subgoal(&mut self, strand: &mut CanonicalStrand<I>) -> bool { + // This subgoal selection for the strand is finished, so take it + let selected_subgoal = strand.value.selected_subgoal.take().unwrap(); + match strand.value.ex_clause.subgoals[selected_subgoal.subgoal_index] { + Literal::Positive(_) => { + // If this strand depends on this positively, then we can + // come back to it later. So, we mark that subgoal as + // floundered and yield `QuantumExceeded` up the stack + + // If this subgoal floundered, push it onto the + // floundered list, along with the time that it + // floundered. We'll try to solve some other subgoals + // and maybe come back to it. + self.flounder_subgoal(&mut strand.value.ex_clause, selected_subgoal.subgoal_index); + + false + } + Literal::Negative(_) => { + // Floundering on a negative literal isn't like a + // positive search: we only pursue negative literals + // when we already know precisely the type we are + // looking for. So there's no point waiting for other + // subgoals, we'll never recover more information. + // + // In fact, floundering on negative searches shouldn't + // normally happen, since there are no uninferred + // variables in the goal, but it can with forall + // goals: + // + // forall<T> { not { T: Debug } } + // + // Here, the table we will be searching for answers is + // `?T: Debug`, so it could well flounder. + + // This strand has no solution. It is no longer active, + // so it dropped at the end of this scope. + + true + } + } + } + + /// This is called if the selected subgoal for a `Strand` is + /// a coinductive cycle. + fn on_coinductive_subgoal( + &mut self, + mut canonical_strand: CanonicalStrand<I>, + ) -> Result<(), RootSearchFail> { + // This is a co-inductive cycle. That is, this table + // appears somewhere higher on the stack, and has now + // recursively requested an answer for itself. This + // means that we have to delay this subgoal until we + // reach a trivial self-cycle. + + // This subgoal selection for the strand is finished, so take it + let selected_subgoal = canonical_strand.value.selected_subgoal.take().unwrap(); + match canonical_strand + .value + .ex_clause + .subgoals + .remove(selected_subgoal.subgoal_index) + { + Literal::Positive(subgoal) => { + // We delay this subgoal + let table = self.stack.top().table; + assert!( + self.forest.tables[table].coinductive_goal + && self.forest.tables[selected_subgoal.subgoal_table].coinductive_goal + ); + + canonical_strand + .value + .ex_clause + .delayed_subgoals + .push(subgoal); + + self.stack.top().active_strand = Some(canonical_strand); + Ok(()) + } + Literal::Negative(_) => { + // We don't allow coinduction for negative literals + info!("found coinductive answer to negative literal"); + panic!("Coinductive cycle with negative literal"); + } + } + } + + /// This is called if the selected subgoal for `strand` is + /// a positive, non-coinductive cycle. + /// + /// # Parameters + /// + /// * `strand` the strand from the top of the stack we are pursuing + /// * `minimums` is the collected minimum clock times + fn on_positive_cycle( + &mut self, + canonical_strand: CanonicalStrand<I>, + minimums: Minimums, + ) -> Result<(), RootSearchFail> { + // We can't take this because we might need it later to clear the cycle + let selected_subgoal = canonical_strand.value.selected_subgoal.as_ref().unwrap(); + + match canonical_strand.value.ex_clause.subgoals[selected_subgoal.subgoal_index] { + Literal::Positive(_) => { + self.stack.top().cyclic_minimums.take_minimums(&minimums); + } + Literal::Negative(_) => { + // We depend on `not(subgoal)`. For us to continue, + // `subgoal` must be completely evaluated. Therefore, + // we depend (negatively) on the minimum link of + // `subgoal` as a whole -- it doesn't matter whether + // it's pos or neg. + let mins = Minimums { + positive: self.stack.top().clock, + negative: minimums.minimum_of_pos_and_neg(), + }; + self.stack.top().cyclic_minimums.take_minimums(&mins); + } + } + + // Ok, we've taken the minimums from this cycle above. Now, + // we just return the strand to the table. The table only + // pulls strands if they have not been checked at this + // depth. + // + // We also can't mark these and return early from this + // because the stack above us might change. + let table = self.stack.top().table; + self.forest.tables[table].enqueue_strand(canonical_strand); + + // The strand isn't active, but the table is, so just continue + Ok(()) + } + + /// Invoked after we've selected a (new) subgoal for the top-most + /// strand. Attempts to pursue this selected subgoal. + /// + /// Returns: + /// + /// * `Ok` if we should keep searching. + /// * `Err` if the subgoal failed in some way such that the strand can be abandoned. + fn on_subgoal_selected( + &mut self, + mut canonical_strand: CanonicalStrand<I>, + ) -> Result<(), RootSearchFail> { + // This may be a newly selected subgoal or an existing selected subgoal. + + let SelectedSubgoal { + subgoal_index: _, + subgoal_table, + answer_index, + universe_map: _, + } = *canonical_strand.value.selected_subgoal.as_ref().unwrap(); + + debug!( + ?subgoal_table, + goal = ?self.forest.tables[subgoal_table].table_goal, + "table selection {:?} with goal: {:?}", + subgoal_table, self.forest.tables[subgoal_table].table_goal + ); + + // This is checked inside select_subgoal + assert!(!self.forest.tables[subgoal_table].is_floundered()); + + // Check for a tabled answer. + if let Some(answer) = self.forest.tables[subgoal_table].answer(answer_index) { + info!("answer cached = {:?}", answer); + + // There was a previous answer available for this table + // We need to check if we can merge it into the current `Strand`. + let num_universes = self.forest.tables[self.stack.top().table] + .table_goal + .universes; + let (mut infer, _, mut strand) = chalk_solve::infer::InferenceTable::from_canonical( + self.context.program().interner(), + num_universes, + canonical_strand.clone(), + ); + match self.merge_answer_into_strand(&mut infer, &mut strand) { + Err(e) => { + debug!(?strand, "could not merge into current strand"); + drop(strand); + return Err(e); + } + Ok(_) => { + debug!(?strand, "merged answer into current strand"); + canonical_strand = + Forest::canonicalize_strand_from(self.context, &mut infer, &strand); + self.stack.top().active_strand = Some(canonical_strand); + return Ok(()); + } + } + } + + // If no tabled answer is present, we ought to be requesting + // the next available index. + assert_eq!( + self.forest.tables[subgoal_table].next_answer_index(), + answer_index + ); + + // Next, check if the table is already active. If so, then we + // have a recursive attempt. + if let Some(cyclic_depth) = self.stack.is_active(subgoal_table) { + info!("cycle detected at depth {:?}", cyclic_depth); + let minimums = Minimums { + positive: self.stack[cyclic_depth].clock, + negative: TimeStamp::MAX, + }; + + if self.top_of_stack_is_coinductive_from(cyclic_depth) { + debug!("table is coinductive"); + return self.on_coinductive_subgoal(canonical_strand); + } + + debug!("table encountered a positive cycle"); + return self.on_positive_cycle(canonical_strand, minimums); + } + + // We don't know anything about the selected subgoal table. + // Set this strand as active and push it onto the stack. + self.stack.top().active_strand = Some(canonical_strand); + + let cyclic_minimums = Minimums::MAX; + self.stack.push( + subgoal_table, + cyclic_minimums, + self.forest.increment_clock(), + ); + Ok(()) + } + + /// This is called when there are no remaining subgoals for a strand, so + /// it represents an answer. If the strand is ambiguous and we don't want + /// it yet, we just enqueue it again to pick it up later. Otherwise, we + /// add the answer from the strand onto the table. + fn on_no_remaining_subgoals( + &mut self, + canonical_strand: CanonicalStrand<I>, + ) -> NoRemainingSubgoalsResult { + let ambiguous = canonical_strand.value.ex_clause.ambiguous; + if let AnswerMode::Complete = self.forest.tables[self.stack.top().table].answer_mode { + if ambiguous { + // The strand can only return an ambiguous answer, but we don't + // want that right now, so requeue and we'll deal with it later. + self.forest.tables[self.stack.top().table].enqueue_strand(canonical_strand); + return NoRemainingSubgoalsResult::RootSearchFail(RootSearchFail::QuantumExceeded); + } + } + let floundered = !canonical_strand + .value + .ex_clause + .floundered_subgoals + .is_empty(); + if floundered { + debug!("all remaining subgoals floundered for the table"); + } else { + debug!("no remaining subgoals for the table"); + }; + match self.pursue_answer(canonical_strand) { + Some(answer_index) => { + debug!("answer is available"); + + // We found an answer for this strand, and therefore an + // answer for this table. Now, this table was either a + // subgoal for another strand, or was the root table. + let table = self.stack.top().table; + match self.stack.pop_and_take_caller_strand() { + Some(caller_strand) => { + self.stack.top().active_strand = Some(caller_strand); + NoRemainingSubgoalsResult::Success + } + None => { + // That was the root table, so we are done -- + // *well*, unless there were delayed + // subgoals. In that case, we want to evaluate + // those delayed subgoals to completion, so we + // have to create a fresh strand that will + // take them as goals. Note that we *still + // need the original answer in place*, because + // we might have to build on it (see the + // Delayed Trivial Self Cycle, Variant 3 + // example). + + let answer = self.forest.answer(table, answer_index); + if let Some(strand) = self.create_refinement_strand(table, answer) { + self.forest.tables[table].enqueue_strand(strand); + } + + NoRemainingSubgoalsResult::RootAnswerAvailable + } + } + } + None => { + debug!("answer is not available (or not new)"); + + // This strand led nowhere of interest. There might be *other* + // answers on this table, but we don't care right now, we'll + // try again at another time. + + // Now we yield with `QuantumExceeded` + self.unwind_stack(); + NoRemainingSubgoalsResult::RootSearchFail(RootSearchFail::QuantumExceeded) + } + } + } + + /// A "refinement" strand is used in coinduction. When the root + /// table on the stack publishes an answer has delayed subgoals, + /// we create a new strand that will attempt to prove out those + /// delayed subgoals (the root answer here is not *special* except + /// in so far as that there is nothing above it, and hence we know + /// that the delayed subgoals (which resulted in some cycle) must + /// be referring to a table that now has completed). + /// + /// Note that it is important for this to be a *refinement* strand + /// -- meaning that the answer with delayed subgoals has been + /// published. This is necessary because sometimes the strand must + /// build on that very answer that it is refining. See Delayed + /// Trivial Self Cycle, Variant 3. + fn create_refinement_strand( + &self, + table: TableIndex, + answer: &Answer<I>, + ) -> Option<CanonicalStrand<I>> { + // If there are no delayed subgoals, then there is no need for + // a refinement strand. + if answer.subst.value.delayed_subgoals.is_empty() { + return None; + } + + let num_universes = self.forest.tables[table].table_goal.universes; + let ( + mut infer, + _, + AnswerSubst { + subst, + constraints, + delayed_subgoals, + }, + ) = chalk_solve::infer::InferenceTable::from_canonical( + self.context.program().interner(), + num_universes, + answer.subst.clone(), + ); + + let delayed_subgoals = delayed_subgoals + .into_iter() + .map(Literal::Positive) + .collect(); + + let strand = Strand { + ex_clause: ExClause { + subst, + ambiguous: answer.ambiguous, + constraints: constraints + .as_slice(self.context.program().interner()) + .to_vec(), + subgoals: delayed_subgoals, + delayed_subgoals: Vec::new(), + answer_time: TimeStamp::default(), + floundered_subgoals: Vec::new(), + }, + selected_subgoal: None, + last_pursued_time: TimeStamp::default(), + }; + + Some(Forest::canonicalize_strand_from( + self.context, + &mut infer, + &strand, + )) + } + + fn on_no_strands_left(&mut self) -> Result<(), RootSearchFail> { + let table = self.stack.top().table; + debug!("no more strands available (or all cycles) for {:?}", table); + + // No more strands left to try! This is either because all + // strands have failed, because all strands encountered a + // cycle, or all strands have would give ambiguous answers. + + if self.forest.tables[table].strands_mut().count() == 0 { + // All strands for the table T on the top of the stack + // have **failed**. Hence we can pop it off the stack and + // check what this means for the table T' that was just + // below T on the stack (if any). + debug!("no more strands available"); + let caller_strand = match self.stack.pop_and_borrow_caller_strand() { + Some(s) => s, + None => { + // T was the root table, so we are done. + debug!("no more solutions"); + return Err(RootSearchFail::NoMoreSolutions); + } + }; + + // This subgoal selection for the strand is finished, so take it + let caller_selected_subgoal = caller_strand.value.selected_subgoal.take().unwrap(); + return match caller_strand.value.ex_clause.subgoals + [caller_selected_subgoal.subgoal_index] + { + // T' wanted an answer from T, but none is + // forthcoming. Therefore, the active strand from T' + // has failed and can be discarded. + Literal::Positive(_) => { + debug!("discarding strand because positive literal"); + self.stack.top().active_strand.take(); + self.unwind_stack(); + Err(RootSearchFail::QuantumExceeded) + } + + // T' wanted there to be no answer from T, but none is forthcoming. + Literal::Negative(_) => { + debug!("subgoal was proven because negative literal"); + + // There is no solution for this strand. But, this + // is what we want, so can remove this subgoal and + // keep going. + caller_strand + .value + .ex_clause + .subgoals + .remove(caller_selected_subgoal.subgoal_index); + + // This strand is still active, so continue + Ok(()) + } + }; + } + + // We can't consider this table as part of a cycle unless we've handled + // all strands, not just non-ambiguous ones. See chalk#571. + if let AnswerMode::Complete = self.forest.tables[table].answer_mode { + debug!("Allowing ambiguous answers."); + self.forest.tables[table].answer_mode = AnswerMode::Ambiguous; + return Err(RootSearchFail::QuantumExceeded); + } + + let clock = self.stack.top().clock; + let cyclic_minimums = self.stack.top().cyclic_minimums; + if cyclic_minimums.positive >= clock && cyclic_minimums.negative >= clock { + debug!("cycle with no new answers"); + + if cyclic_minimums.negative < TimeStamp::MAX { + // This is a negative cycle. + self.unwind_stack(); + return Err(RootSearchFail::NegativeCycle); + } + + // If all the things that we recursively depend on have + // positive dependencies on things below us in the stack, + // then no more answers are forthcoming. We can clear all + // the strands for those things recursively. + let table = self.stack.top().table; + let cyclic_strands = self.forest.tables[table].take_strands(); + self.clear_strands_after_cycle(cyclic_strands); + + // Now we yield with `QuantumExceeded` + self.unwind_stack(); + Err(RootSearchFail::QuantumExceeded) + } else { + debug!("table part of a cycle"); + + // This table resulted in a positive cycle, so we have + // to check what this means for the subgoal containing + // this strand + let caller_strand = match self.stack.pop_and_borrow_caller_strand() { + Some(s) => s, + None => { + panic!("nothing on the stack but cyclic result"); + } + }; + + // We can't take this because we might need it later to clear the cycle + let caller_selected_subgoal = caller_strand.value.selected_subgoal.as_ref().unwrap(); + match caller_strand.value.ex_clause.subgoals[caller_selected_subgoal.subgoal_index] { + Literal::Positive(_) => { + self.stack + .top() + .cyclic_minimums + .take_minimums(&cyclic_minimums); + } + Literal::Negative(_) => { + // We depend on `not(subgoal)`. For us to continue, + // `subgoal` must be completely evaluated. Therefore, + // we depend (negatively) on the minimum link of + // `subgoal` as a whole -- it doesn't matter whether + // it's pos or neg. + let mins = Minimums { + positive: self.stack.top().clock, + negative: cyclic_minimums.minimum_of_pos_and_neg(), + }; + self.stack.top().cyclic_minimums.take_minimums(&mins); + } + } + + // We can't pursue this strand anymore, so push it back onto the table + let active_strand = self.stack.top().active_strand.take().unwrap(); + let table = self.stack.top().table; + self.forest.tables[table].enqueue_strand(active_strand); + + // The strand isn't active, but the table is, so just continue + Ok(()) + } + } + + /// Unwinds the entire stack, returning all active strands back to + /// their tables (this time at the end of the queue). + fn unwind_stack(&mut self) { + loop { + match self.stack.pop_and_take_caller_strand() { + Some(active_strand) => { + let table = self.stack.top().table; + self.forest.tables[table].enqueue_strand(active_strand); + } + + None => return, + } + } + } + + /// Invoked after we have determined that every strand in `table` + /// encounters a cycle; `strands` is the set of strands (which + /// have been moved out of the table). This method then + /// recursively clears the active strands from the tables + /// referenced in `strands`, since all of them must encounter + /// cycles too. + fn clear_strands_after_cycle(&mut self, strands: impl IntoIterator<Item = CanonicalStrand<I>>) { + for strand in strands { + let selected_subgoal = strand.value.selected_subgoal; + let ex_clause = strand.value.ex_clause; + let selected_subgoal = selected_subgoal.unwrap_or_else(|| { + panic!( + "clear_strands_after_cycle invoked on strand in table \ + without a selected subgoal: {:?}", + ex_clause, + ) + }); + + let strand_table = selected_subgoal.subgoal_table; + let strands = self.forest.tables[strand_table].take_strands(); + self.clear_strands_after_cycle(strands); + } + } + + fn select_subgoal( + &mut self, + mut canonical_strand: &mut CanonicalStrand<I>, + ) -> SubGoalSelection { + loop { + while canonical_strand.value.selected_subgoal.is_none() { + if canonical_strand.value.ex_clause.subgoals.is_empty() { + if canonical_strand + .value + .ex_clause + .floundered_subgoals + .is_empty() + { + return SubGoalSelection::NotSelected; + } + + self.reconsider_floundered_subgoals(&mut canonical_strand.value.ex_clause); + + if canonical_strand.value.ex_clause.subgoals.is_empty() { + // All the subgoals of this strand floundered. We may be able + // to get helpful information from this strand still, but it + // will *always* be ambiguous, so mark it as so. + assert!(!canonical_strand + .value + .ex_clause + .floundered_subgoals + .is_empty()); + canonical_strand.value.ex_clause.ambiguous = true; + return SubGoalSelection::NotSelected; + } + + continue; + } + + let subgoal_index = + SlgContext::next_subgoal_index(&canonical_strand.value.ex_clause); + + // Get or create table for this subgoal. + let num_universes = self.forest.tables[self.stack.top().table] + .table_goal + .universes; + let (mut infer, _, strand) = chalk_solve::infer::InferenceTable::from_canonical( + self.context.program().interner(), + num_universes, + canonical_strand.clone(), + ); + match self.forest.get_or_create_table_for_subgoal( + self.context, + &mut infer, + &strand.ex_clause.subgoals[subgoal_index], + ) { + Some((subgoal_table, universe_map)) => { + canonical_strand.value.selected_subgoal = Some(SelectedSubgoal { + subgoal_index, + subgoal_table, + universe_map, + answer_index: AnswerIndex::ZERO, + }); + } + + None => { + // If we failed to create a table for the subgoal, + // that is because we have a floundered negative + // literal. + self.flounder_subgoal(&mut canonical_strand.value.ex_clause, subgoal_index); + } + } + } + + let selected_subgoal_table = canonical_strand + .value + .selected_subgoal + .as_ref() + .unwrap() + .subgoal_table; + if self.forest.tables[selected_subgoal_table].is_floundered() { + if self.propagate_floundered_subgoal(canonical_strand) { + // This strand will never lead anywhere of interest. + return SubGoalSelection::NotSelected; + } else { + // This subgoal has floundered and has been marked. + // We previously would immediately mark the table as + // floundered too, and maybe come back to it. Now, we + // try to see if any other subgoals can be pursued first. + continue; + } + } else { + return SubGoalSelection::Selected; + } + } + } + + /// Invoked when a strand represents an **answer**. This means + /// that the strand has no subgoals left. There are two possibilities: + /// + /// - the strand may represent an answer we have already found; in + /// that case, we can return `None`, as this + /// strand led nowhere of interest. + /// - the strand may represent a new answer, in which case it is + /// added to the table and `Some(())` is returned. + fn pursue_answer(&mut self, canonical_strand: CanonicalStrand<I>) -> Option<AnswerIndex> { + let table = self.stack.top().table; + let Canonical { + binders, + value: strand, + } = canonical_strand; + let ExClause { + subst, + constraints, + ambiguous, + subgoals, + delayed_subgoals, + answer_time: _, + floundered_subgoals, + } = strand.ex_clause; + // If there are subgoals left, they should be followed + assert!(subgoals.is_empty()); + // We can still try to get an ambiguous answer if there are floundered subgoals + let floundered = !floundered_subgoals.is_empty(); + // So let's make sure that it *really* is an ambiguous answer (this should be set previously) + assert!(!floundered || ambiguous); + + // FIXME: If there are floundered subgoals, we *could* potentially + // actually check if the partial answers to any of these subgoals + // conflict. But this requires that we think about whether they are + // positive or negative subgoals. This duplicates some of the logic + // in `merge_answer_into_strand`, so a bit of refactoring is needed. + + // If the answer gets too large, mark the table as floundered. + // This is the *most conservative* course. There are a few alternatives: + // 1) Replace the answer with a truncated version of it. (This was done + // previously, but turned out to be more complicated than we wanted and + // and a source of multiple bugs.) + // 2) Mark this *strand* as floundered. We don't currently have a mechanism + // for this (only floundered subgoals), so implementing this is more + // difficult because we don't want to just *remove* this strand from the + // table, because that might make the table give `NoMoreSolutions`, which + // is *wrong*. + // 3) Do something fancy with delayed subgoals, effectively delayed the + // truncated bits to a different strand (and a more "refined" answer). + // (This one probably needs more thought, but is here for "completeness") + // + // Ultimately, the current decision to flounder the entire table mostly boils + // down to "it works as we expect for the current tests". And, we likely don't + // even *need* the added complexity just for potentially more answers. + if truncate::needs_truncation( + self.context.program().interner(), + &mut InferenceTable::new(), + self.context.max_size(), + &subst, + ) { + self.forest.tables[table].mark_floundered(); + return None; + } + + let table_goal = &self.forest.tables[table].table_goal; + + let filtered_delayed_subgoals = delayed_subgoals + .into_iter() + .filter(|delayed_subgoal| { + let canonicalized = InferenceTable::u_canonicalize( + self.context.program().interner(), + &chalk_ir::Canonical { + binders: binders.clone(), + value: delayed_subgoal.clone(), + }, + ) + .quantified; + *table_goal != canonicalized + }) + .collect(); + + let subst = Canonical { + binders, + value: AnswerSubst { + subst, + constraints: Constraints::from_iter(self.context.program().interner(), constraints), + delayed_subgoals: filtered_delayed_subgoals, + }, + }; + debug!(?table, ?subst, ?floundered, "found answer"); + + let answer = Answer { subst, ambiguous }; + + // A "trivial" answer is one that is 'just true for all cases' + // -- in other words, it gives no information back to the + // caller. For example, `Vec<u32>: Sized` is "just true". + // Such answers are important because they are the most + // general case, and after we provide a trivial answer, no + // further answers are useful -- therefore we can clear any + // further pending strands (this is a "green cut", in + // Prolog parlance). + // + // This optimization is *crucial* for performance: for + // example, `projection_from_env_slow` fails miserably without + // it. The reason is that we wind up (thanks to implied bounds) + // with a clause like this: + // + // ```ignore + // forall<T> { (<T as SliceExt>::Item: Clone) :- WF(T: SliceExt) } + // ``` + // + // we then apply that clause to `!1: Clone`, resulting in the + // table goal `!1: Clone :- <?0 as SliceExt>::Item = !1, + // WF(?0: SliceExt)`. This causes us to **enumerate all types + // `?0` that where `Slice<?0>` normalizes to `!1` -- this is + // an infinite set of types, effectively. Interestingly, + // though, we only need one and we are done, because (if you + // look) our goal (`!1: Clone`) doesn't have any output + // parameters. + // + // This is actually a kind of general case. Due to Rust's rule + // about constrained impl type parameters, generally speaking + // when we have some free inference variable (like `?0`) + // within our clause, it must appear in the head of the + // clause. This means that the values we create for it will + // propagate up to the caller, and they will quickly surmise + // that there is ambiguity and stop requesting more answers. + // Indeed, the only exception to this rule about constrained + // type parameters if with associated type projections, as in + // the case above! + // + // (Actually, because of the trivial answer cut off rule, we + // never even get to the point of asking the query above in + // `projection_from_env_slow`.) + // + // However, there is one fly in the ointment: answers include + // region constraints, and you might imagine that we could + // find future answers that are also trivial but with distinct + // sets of region constraints. **For this reason, we only + // apply this green cut rule if the set of generated + // constraints is empty.** + // + // The limitation on region constraints is quite a drag! We + // can probably do better, though: for example, coherence + // guarantees that, for any given set of types, only a single + // impl ought to be applicable, and that impl can only impose + // one set of region constraints. However, it's not quite that + // simple, thanks to specialization as well as the possibility + // of proving things from the environment (though the latter + // is a *bit* suspect; e.g., those things in the environment + // must be backed by an impl *eventually*). + let is_trivial_answer = { + self.forest.tables[table] + .table_goal + .is_trivial_substitution(self.context.program().interner(), &answer.subst) + && answer + .subst + .value + .constraints + .is_empty(self.context.program().interner()) + }; + + if let Some(answer_index) = self.forest.tables[table].push_answer(answer) { + // See above, if we have a *complete* and trivial answer, we don't + // want to follow any more strands + if !ambiguous && is_trivial_answer { + self.forest.tables[table].take_strands(); + } + + Some(answer_index) + } else { + info!("answer: not a new answer, returning None"); + None + } + } + + fn reconsider_floundered_subgoals(&mut self, ex_clause: &mut ExClause<I>) { + info!("reconsider_floundered_subgoals(ex_clause={:#?})", ex_clause,); + let ExClause { + answer_time, + subgoals, + floundered_subgoals, + .. + } = ex_clause; + for i in (0..floundered_subgoals.len()).rev() { + if floundered_subgoals[i].floundered_time < *answer_time { + let floundered_subgoal = floundered_subgoals.swap_remove(i); + subgoals.push(floundered_subgoal.floundered_literal); + } + } + } + + /// Removes the subgoal at `subgoal_index` from the strand's + /// subgoal list and adds it to the strand's floundered subgoal + /// list. + fn flounder_subgoal(&self, ex_clause: &mut ExClause<I>, subgoal_index: usize) { + let _s = debug_span!( + "flounder_subgoal", + answer_time = ?ex_clause.answer_time, + subgoal = ?ex_clause.subgoals[subgoal_index], + ); + let _s = _s.enter(); + + let floundered_time = ex_clause.answer_time; + let floundered_literal = ex_clause.subgoals.remove(subgoal_index); + ex_clause.floundered_subgoals.push(FlounderedSubgoal { + floundered_literal, + floundered_time, + }); + debug!(?ex_clause); + } + + /// True if all the tables on the stack starting from `depth` and + /// continuing until the top of the stack are coinductive. + /// + /// Example: Given a program like: + /// + /// ```notrust + /// struct Foo { a: Option<Box<Bar>> } + /// struct Bar { a: Option<Box<Foo>> } + /// trait XXX { } + /// impl<T: Send> XXX for T { } + /// ``` + /// + /// and then a goal of `Foo: XXX`, we would eventually wind up + /// with a stack like this: + /// + /// | StackIndex | Table Goal | + /// | ---------- | ----------- | + /// | 0 | `Foo: XXX` | + /// | 1 | `Foo: Send` | + /// | 2 | `Bar: Send` | + /// + /// Here, the top of the stack is `Bar: Send`. And now we are + /// asking `top_of_stack_is_coinductive_from(1)` -- the answer + /// would be true, since `Send` is an auto trait, which yields a + /// coinductive goal. But `top_of_stack_is_coinductive_from(0)` is + /// false, since `XXX` is not an auto trait. + pub(super) fn top_of_stack_is_coinductive_from(&self, depth: StackIndex) -> bool { + StackIndex::iterate_range(self.stack.top_of_stack_from(depth)).all(|d| { + let table = self.stack[d].table; + self.forest.tables[table].coinductive_goal + }) + } +} |