rustc_next_trait_solver/solve/
search_graph.rs

Help
1use std::convert::Infallible;
2use std::marker::PhantomData;
3
4use rustc_type_ir::Interner;
5use rustc_type_ir::inherent::*;
6use rustc_type_ir::search_graph::{self, PathKind};
7use rustc_type_ir::solve::{CanonicalInput, Certainty, QueryResult};
8
9use super::inspect::ProofTreeBuilder;
10use super::{FIXPOINT_STEP_LIMIT, has_no_inference_or_external_constraints};
11use crate::delegate::SolverDelegate;
12
13/// This type is never constructed. We only use it to implement `search_graph::Delegate`
14/// for all types which impl `SolverDelegate` and doing it directly fails in coherence.
15pub(super) struct SearchGraphDelegate<D: SolverDelegate> {
16    _marker: PhantomData<D>,
17}
18pub(super) type SearchGraph<D> = search_graph::SearchGraph<SearchGraphDelegate<D>>;
19impl<D, I> search_graph::Delegate for SearchGraphDelegate<D>
20where
21    D: SolverDelegate<Interner = I>,
22    I: Interner,
23{
24    type Cx = D::Interner;
25
26    const ENABLE_PROVISIONAL_CACHE: bool = true;
27    type ValidationScope = Infallible;
28    fn enter_validation_scope(
29        _cx: Self::Cx,
30        _input: CanonicalInput<I>,
31    ) -> Option<Self::ValidationScope> {
32        None
33    }
34
35    const FIXPOINT_STEP_LIMIT: usize = FIXPOINT_STEP_LIMIT;
36
37    type ProofTreeBuilder = ProofTreeBuilder<D>;
38    fn inspect_is_noop(inspect: &mut Self::ProofTreeBuilder) -> bool {
39        inspect.is_noop()
40    }
41
42    const DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW: usize = 4;
43
44    fn initial_provisional_result(
45        cx: I,
46        kind: PathKind,
47        input: CanonicalInput<I>,
48    ) -> QueryResult<I> {
49        match kind {
50            PathKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes),
51            PathKind::Inductive => response_no_constraints(cx, input, Certainty::overflow(false)),
52        }
53    }
54
55    fn is_initial_provisional_result(
56        cx: Self::Cx,
57        kind: PathKind,
58        input: CanonicalInput<I>,
59        result: QueryResult<I>,
60    ) -> bool {
61        match kind {
62            PathKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes) == result,
63            PathKind::Inductive => {
64                response_no_constraints(cx, input, Certainty::overflow(false)) == result
65            }
66        }
67    }
68
69    fn on_stack_overflow(
70        cx: I,
71        inspect: &mut ProofTreeBuilder<D>,
72        input: CanonicalInput<I>,
73    ) -> QueryResult<I> {
74        inspect.canonical_goal_evaluation_overflow();
75        response_no_constraints(cx, input, Certainty::overflow(true))
76    }
77
78    fn on_fixpoint_overflow(cx: I, input: CanonicalInput<I>) -> QueryResult<I> {
79        response_no_constraints(cx, input, Certainty::overflow(false))
80    }
81
82    fn is_ambiguous_result(result: QueryResult<I>) -> bool {
83        result.is_ok_and(|response| {
84            has_no_inference_or_external_constraints(response)
85                && matches!(response.value.certainty, Certainty::Maybe(_))
86        })
87    }
88
89    fn propagate_ambiguity(
90        cx: I,
91        for_input: CanonicalInput<I>,
92        from_result: QueryResult<I>,
93    ) -> QueryResult<I> {
94        let certainty = from_result.unwrap().value.certainty;
95        response_no_constraints(cx, for_input, certainty)
96    }
97
98    fn step_is_coinductive(cx: I, input: CanonicalInput<I>) -> bool {
99        input.canonical.value.goal.predicate.is_coinductive(cx)
100    }
101}
102
103fn response_no_constraints<I: Interner>(
104    cx: I,
105    input: CanonicalInput<I>,
106    certainty: Certainty,
107) -> QueryResult<I> {
108    Ok(super::response_no_constraints_raw(
109        cx,
110        input.canonical.max_universe,
111        input.canonical.variables,
112        certainty,
113    ))
114}
rustc_next_trait_solver/solve/search_graph.rs

rustc_next_trait_solver/solve/
search_graph.rs
