rustc_next_trait_solver/solve/
search_graph.rs1use std::convert::Infallible;
2use std::marker::PhantomData;
3
4use rustc_type_ir::data_structures::ensure_sufficient_stack;
5use rustc_type_ir::search_graph::{self, PathKind};
6use rustc_type_ir::solve::{CanonicalInput, Certainty, NoSolution, QueryResult};
7use rustc_type_ir::{Interner, TypingMode};
8
9use crate::delegate::SolverDelegate;
10use crate::solve::inspect::ProofTreeBuilder;
11use crate::solve::{EvalCtxt, FIXPOINT_STEP_LIMIT, has_no_inference_or_external_constraints};
12
13pub(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::Unknown => response_no_constraints(cx, input, Certainty::overflow(false)),
52 PathKind::Inductive => match input.typing_mode {
62 TypingMode::Coherence => {
63 response_no_constraints(cx, input, Certainty::overflow(false))
64 }
65 TypingMode::Analysis { .. }
66 | TypingMode::Borrowck { .. }
67 | TypingMode::PostBorrowckAnalysis { .. }
68 | TypingMode::PostAnalysis => Err(NoSolution),
69 },
70 }
71 }
72
73 fn is_initial_provisional_result(
74 cx: Self::Cx,
75 kind: PathKind,
76 input: CanonicalInput<I>,
77 result: QueryResult<I>,
78 ) -> bool {
79 Self::initial_provisional_result(cx, kind, input) == result
80 }
81
82 fn on_stack_overflow(
83 cx: I,
84 input: CanonicalInput<I>,
85 inspect: &mut ProofTreeBuilder<D>,
86 ) -> QueryResult<I> {
87 inspect.canonical_goal_evaluation_overflow();
88 response_no_constraints(cx, input, Certainty::overflow(true))
89 }
90
91 fn on_fixpoint_overflow(cx: I, input: CanonicalInput<I>) -> QueryResult<I> {
92 response_no_constraints(cx, input, Certainty::overflow(false))
93 }
94
95 fn is_ambiguous_result(result: QueryResult<I>) -> bool {
96 result.is_ok_and(|response| {
97 has_no_inference_or_external_constraints(response)
98 && matches!(response.value.certainty, Certainty::Maybe(_))
99 })
100 }
101
102 fn propagate_ambiguity(
103 cx: I,
104 for_input: CanonicalInput<I>,
105 from_result: QueryResult<I>,
106 ) -> QueryResult<I> {
107 let certainty = from_result.unwrap().value.certainty;
108 response_no_constraints(cx, for_input, certainty)
109 }
110
111 fn compute_goal(
112 search_graph: &mut SearchGraph<D>,
113 cx: I,
114 input: CanonicalInput<I>,
115 inspect: &mut Self::ProofTreeBuilder,
116 ) -> QueryResult<I> {
117 ensure_sufficient_stack(|| {
118 EvalCtxt::enter_canonical(cx, search_graph, input, inspect, |ecx, goal| {
119 let result = ecx.compute_goal(goal);
120 ecx.inspect.query_result(result);
121 result
122 })
123 })
124 }
125}
126
127fn response_no_constraints<I: Interner>(
128 cx: I,
129 input: CanonicalInput<I>,
130 certainty: Certainty,
131) -> QueryResult<I> {
132 Ok(super::response_no_constraints_raw(
133 cx,
134 input.canonical.max_universe,
135 input.canonical.variables,
136 certainty,
137 ))
138}