| use crate::solve::inspect::{self, ProofTreeBuilder}; |
| use crate::solve::{ |
| CacheData, CanonicalInput, Certainty, QueryResult, SolverMode, FIXPOINT_STEP_LIMIT, |
| }; |
|
| #[derive(Copy, Clone, PartialEq, Eq, Debug)] |
| pub struct SolverLimit(usize); |
|
| rustc_index::newtype_index! { |
| #[orderable] |
| #[gate_rustc_only] |
| pub struct StackDepth {} |
| } |
|
| bitflags::bitflags! { |
| /// Whether and how this goal has been used as the root of a |
| /// cycle. We track the kind of cycle as we're otherwise forced |
| /// to always rerun at least once. |
| #[derive(Debug, Clone, Copy, PartialEq, Eq)] |
| struct HasBeenUsed: u8 { |
| const INDUCTIVE_CYCLE = 1 << 0; |
| const COINDUCTIVE_CYCLE = 1 << 1; |
| } |
| } |
|
| #[derive(derivative::Derivative)] |
| #[derivative(Debug(bound = ""))] |
| struct StackEntry<I: Interner> { |
| input: CanonicalInput<I>, |
|
| available_depth: SolverLimit, |
|
| /// The maximum depth reached by this stack entry, only up-to date |
| /// for the top of the stack and lazily updated for the rest. |
| reached_depth: StackDepth, |
|
| /// Whether this entry is a non-root cycle participant. |
| /// |
| /// We must not move the result of non-root cycle participants to the |
| /// global cache. We store the highest stack depth of a head of a cycle |
| /// this goal is involved in. This necessary to soundly cache its |
| /// provisional result. |
| non_root_cycle_participant: Option<StackDepth>, |
|
| encountered_overflow: bool, |
|
| has_been_used: HasBeenUsed, |
|
| /// We put only the root goal of a coinductive cycle into the global cache. |
| /// |
| /// If we were to use that result when later trying to prove another cycle |
| /// participant, we can end up with unstable query results. |
| /// |
| /// See tests/ui/next-solver/coinduction/incompleteness-unstable-result.rs for |
| /// an example of where this is needed. |
| /// |
| /// There can be multiple roots on the same stack, so we need to track |
| /// cycle participants per root: |
| /// ```plain |
| /// A :- B |
| /// B :- A, C |
| /// C :- D |
| /// D :- C |
| /// ``` |
| nested_goals: HashSet<CanonicalInput<I>>, |
| /// Starts out as `None` and gets set when rerunning this |
| /// goal in case we encounter a cycle. |
| provisional_result: Option<QueryResult<I>>, |
| } |
|
| /// The provisional result for a goal which is not on the stack. |
| #[derive(Debug)] |
| struct DetachedEntry<I: Interner> { |
| /// The head of the smallest non-trivial cycle involving this entry. |
| /// |
| /// Given the following rules, when proving `A` the head for |
| /// the provisional entry of `C` would be `B`. |
| /// ```plain |
| /// A :- B |
| /// B :- C |
| /// C :- A + B + C |
| /// ``` |
| head: StackDepth, |
| result: QueryResult<I>, |
| } |
| use rustc_type_ir::inherent::Predicate; |
| use rustc_type_ir::search_graph::{self, CycleKind, UsageKind}; |
| use rustc_type_ir::solve::{CanonicalInput, Certainty, QueryResult}; |
| use rustc_type_ir::Interner; |
| use std:📑:PhantomData; |