rustc_next_trait_solver/solve/inspect/
build.rs1use std::marker::PhantomData;
8
9use derive_where::derive_where;
10use rustc_type_ir::inherent::*;
11use rustc_type_ir::{self as ty, Interner};
12
13use crate::delegate::SolverDelegate;
14use crate::solve::eval_ctxt::canonical;
15use crate::solve::{
16 Certainty, GenerateProofTree, Goal, GoalEvaluationKind, GoalSource, QueryResult, inspect,
17};
18
19pub(crate) struct ProofTreeBuilder<D, I = <D as SolverDelegate>::Interner>
40where
41 D: SolverDelegate<Interner = I>,
42 I: Interner,
43{
44 _infcx: PhantomData<D>,
45 state: Option<Box<DebugSolver<I>>>,
46}
47
48#[derive_where(Debug; I: Interner)]
53enum DebugSolver<I: Interner> {
54 Root,
55 GoalEvaluation(WipGoalEvaluation<I>),
56 CanonicalGoalEvaluationStep(WipCanonicalGoalEvaluationStep<I>),
57}
58
59impl<I: Interner> From<WipGoalEvaluation<I>> for DebugSolver<I> {
60 fn from(g: WipGoalEvaluation<I>) -> DebugSolver<I> {
61 DebugSolver::GoalEvaluation(g)
62 }
63}
64
65impl<I: Interner> From<WipCanonicalGoalEvaluationStep<I>> for DebugSolver<I> {
66 fn from(g: WipCanonicalGoalEvaluationStep<I>) -> DebugSolver<I> {
67 DebugSolver::CanonicalGoalEvaluationStep(g)
68 }
69}
70
71#[derive_where(PartialEq, Eq, Debug; I: Interner)]
72struct WipGoalEvaluation<I: Interner> {
73 pub uncanonicalized_goal: Goal<I, I::Predicate>,
74 pub orig_values: Vec<I::GenericArg>,
75 pub encountered_overflow: bool,
76 pub final_revision: Option<WipCanonicalGoalEvaluationStep<I>>,
78 pub result: Option<QueryResult<I>>,
79}
80
81impl<I: Interner> WipGoalEvaluation<I> {
82 fn finalize(self) -> inspect::GoalEvaluation<I> {
83 inspect::GoalEvaluation {
84 uncanonicalized_goal: self.uncanonicalized_goal,
85 orig_values: self.orig_values,
86 kind: if self.encountered_overflow {
87 assert!(self.final_revision.is_none());
88 inspect::GoalEvaluationKind::Overflow
89 } else {
90 let final_revision = self.final_revision.unwrap().finalize();
91 inspect::GoalEvaluationKind::Evaluation { final_revision }
92 },
93 result: self.result.unwrap(),
94 }
95 }
96}
97
98#[derive_where(PartialEq, Eq, Debug; I: Interner)]
102struct WipCanonicalGoalEvaluationStep<I: Interner> {
103 var_values: Vec<I::GenericArg>,
110 probe_depth: usize,
111 evaluation: WipProbe<I>,
112}
113
114impl<I: Interner> WipCanonicalGoalEvaluationStep<I> {
115 fn current_evaluation_scope(&mut self) -> &mut WipProbe<I> {
116 let mut current = &mut self.evaluation;
117 for _ in 0..self.probe_depth {
118 match current.steps.last_mut() {
119 Some(WipProbeStep::NestedProbe(p)) => current = p,
120 _ => panic!(),
121 }
122 }
123 current
124 }
125
126 fn finalize(self) -> inspect::Probe<I> {
127 let evaluation = self.evaluation.finalize();
128 match evaluation.kind {
129 inspect::ProbeKind::Root { .. } => evaluation,
130 _ => unreachable!("unexpected root evaluation: {evaluation:?}"),
131 }
132 }
133}
134
135#[derive_where(PartialEq, Eq, Debug; I: Interner)]
136struct WipProbe<I: Interner> {
137 initial_num_var_values: usize,
138 steps: Vec<WipProbeStep<I>>,
139 kind: Option<inspect::ProbeKind<I>>,
140 final_state: Option<inspect::CanonicalState<I, ()>>,
141}
142
143impl<I: Interner> WipProbe<I> {
144 fn finalize(self) -> inspect::Probe<I> {
145 inspect::Probe {
146 steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
147 kind: self.kind.unwrap(),
148 final_state: self.final_state.unwrap(),
149 }
150 }
151}
152
153#[derive_where(PartialEq, Eq, Debug; I: Interner)]
154enum WipProbeStep<I: Interner> {
155 AddGoal(GoalSource, inspect::CanonicalState<I, Goal<I, I::Predicate>>),
156 NestedProbe(WipProbe<I>),
157 MakeCanonicalResponse { shallow_certainty: Certainty },
158 RecordImplArgs { impl_args: inspect::CanonicalState<I, I::GenericArgs> },
159}
160
161impl<I: Interner> WipProbeStep<I> {
162 fn finalize(self) -> inspect::ProbeStep<I> {
163 match self {
164 WipProbeStep::AddGoal(source, goal) => inspect::ProbeStep::AddGoal(source, goal),
165 WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
166 WipProbeStep::RecordImplArgs { impl_args } => {
167 inspect::ProbeStep::RecordImplArgs { impl_args }
168 }
169 WipProbeStep::MakeCanonicalResponse { shallow_certainty } => {
170 inspect::ProbeStep::MakeCanonicalResponse { shallow_certainty }
171 }
172 }
173 }
174}
175
176impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
177 fn new(state: impl Into<DebugSolver<I>>) -> ProofTreeBuilder<D> {
178 ProofTreeBuilder { state: Some(Box::new(state.into())), _infcx: PhantomData }
179 }
180
181 fn opt_nested<T: Into<DebugSolver<I>>>(&self, state: impl FnOnce() -> Option<T>) -> Self {
182 ProofTreeBuilder {
183 state: self.state.as_ref().and_then(|_| Some(state()?.into())).map(Box::new),
184 _infcx: PhantomData,
185 }
186 }
187
188 fn nested<T: Into<DebugSolver<I>>>(&self, state: impl FnOnce() -> T) -> Self {
189 ProofTreeBuilder {
190 state: self.state.as_ref().map(|_| Box::new(state().into())),
191 _infcx: PhantomData,
192 }
193 }
194
195 fn as_mut(&mut self) -> Option<&mut DebugSolver<I>> {
196 self.state.as_deref_mut()
197 }
198
199 pub(crate) fn take_and_enter_probe(&mut self) -> ProofTreeBuilder<D> {
200 let mut nested = ProofTreeBuilder { state: self.state.take(), _infcx: PhantomData };
201 nested.enter_probe();
202 nested
203 }
204
205 pub(crate) fn finalize(self) -> Option<inspect::GoalEvaluation<I>> {
206 match *self.state? {
207 DebugSolver::GoalEvaluation(wip_goal_evaluation) => {
208 Some(wip_goal_evaluation.finalize())
209 }
210 root => unreachable!("unexpected proof tree builder root node: {:?}", root),
211 }
212 }
213
214 pub(crate) fn new_maybe_root(generate_proof_tree: GenerateProofTree) -> ProofTreeBuilder<D> {
215 match generate_proof_tree {
216 GenerateProofTree::No => ProofTreeBuilder::new_noop(),
217 GenerateProofTree::Yes => ProofTreeBuilder::new_root(),
218 }
219 }
220
221 fn new_root() -> ProofTreeBuilder<D> {
222 ProofTreeBuilder::new(DebugSolver::Root)
223 }
224
225 fn new_noop() -> ProofTreeBuilder<D> {
226 ProofTreeBuilder { state: None, _infcx: PhantomData }
227 }
228
229 pub(crate) fn is_noop(&self) -> bool {
230 self.state.is_none()
231 }
232
233 pub(in crate::solve) fn new_goal_evaluation(
234 &mut self,
235 uncanonicalized_goal: Goal<I, I::Predicate>,
236 orig_values: &[I::GenericArg],
237 kind: GoalEvaluationKind,
238 ) -> ProofTreeBuilder<D> {
239 self.opt_nested(|| match kind {
240 GoalEvaluationKind::Root => Some(WipGoalEvaluation {
241 uncanonicalized_goal,
242 orig_values: orig_values.to_vec(),
243 encountered_overflow: false,
244 final_revision: None,
245 result: None,
246 }),
247 GoalEvaluationKind::Nested => None,
248 })
249 }
250
251 pub(crate) fn canonical_goal_evaluation_overflow(&mut self) {
252 if let Some(this) = self.as_mut() {
253 match this {
254 DebugSolver::GoalEvaluation(goal_evaluation) => {
255 goal_evaluation.encountered_overflow = true;
256 }
257 _ => unreachable!(),
258 };
259 }
260 }
261
262 pub(crate) fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<D>) {
263 if let Some(this) = self.as_mut() {
264 match this {
265 DebugSolver::Root => *this = *goal_evaluation.state.unwrap(),
266 DebugSolver::CanonicalGoalEvaluationStep(_) => {
267 assert!(goal_evaluation.state.is_none())
268 }
269 _ => unreachable!(),
270 }
271 }
272 }
273
274 pub(crate) fn new_goal_evaluation_step(
275 &mut self,
276 var_values: ty::CanonicalVarValues<I>,
277 ) -> ProofTreeBuilder<D> {
278 self.nested(|| WipCanonicalGoalEvaluationStep {
279 var_values: var_values.var_values.to_vec(),
280 evaluation: WipProbe {
281 initial_num_var_values: var_values.len(),
282 steps: vec![],
283 kind: None,
284 final_state: None,
285 },
286 probe_depth: 0,
287 })
288 }
289
290 pub(crate) fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<D>) {
291 if let Some(this) = self.as_mut() {
292 match (this, *goal_evaluation_step.state.unwrap()) {
293 (
294 DebugSolver::GoalEvaluation(goal_evaluation),
295 DebugSolver::CanonicalGoalEvaluationStep(goal_evaluation_step),
296 ) => {
297 goal_evaluation.final_revision = Some(goal_evaluation_step);
298 }
299 _ => unreachable!(),
300 }
301 }
302 }
303
304 pub(crate) fn add_var_value<T: Into<I::GenericArg>>(&mut self, arg: T) {
305 match self.as_mut() {
306 None => {}
307 Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
308 state.var_values.push(arg.into());
309 }
310 Some(s) => panic!("tried to add var values to {s:?}"),
311 }
312 }
313
314 fn enter_probe(&mut self) {
315 match self.as_mut() {
316 None => {}
317 Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
318 let initial_num_var_values = state.var_values.len();
319 state.current_evaluation_scope().steps.push(WipProbeStep::NestedProbe(WipProbe {
320 initial_num_var_values,
321 steps: vec![],
322 kind: None,
323 final_state: None,
324 }));
325 state.probe_depth += 1;
326 }
327 Some(s) => panic!("tried to start probe to {s:?}"),
328 }
329 }
330
331 pub(crate) fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<I>) {
332 match self.as_mut() {
333 None => {}
334 Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
335 let prev = state.current_evaluation_scope().kind.replace(probe_kind);
336 assert_eq!(prev, None);
337 }
338 _ => panic!(),
339 }
340 }
341
342 pub(crate) fn probe_final_state(
343 &mut self,
344 delegate: &D,
345 max_input_universe: ty::UniverseIndex,
346 ) {
347 match self.as_mut() {
348 None => {}
349 Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
350 let final_state = canonical::make_canonical_state(
351 delegate,
352 &state.var_values,
353 max_input_universe,
354 (),
355 );
356 let prev = state.current_evaluation_scope().final_state.replace(final_state);
357 assert_eq!(prev, None);
358 }
359 _ => panic!(),
360 }
361 }
362
363 pub(crate) fn add_goal(
364 &mut self,
365 delegate: &D,
366 max_input_universe: ty::UniverseIndex,
367 source: GoalSource,
368 goal: Goal<I, I::Predicate>,
369 ) {
370 match self.as_mut() {
371 None => {}
372 Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
373 let goal = canonical::make_canonical_state(
374 delegate,
375 &state.var_values,
376 max_input_universe,
377 goal,
378 );
379 state.current_evaluation_scope().steps.push(WipProbeStep::AddGoal(source, goal))
380 }
381 _ => panic!(),
382 }
383 }
384
385 pub(crate) fn record_impl_args(
386 &mut self,
387 delegate: &D,
388 max_input_universe: ty::UniverseIndex,
389 impl_args: I::GenericArgs,
390 ) {
391 match self.as_mut() {
392 Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
393 let impl_args = canonical::make_canonical_state(
394 delegate,
395 &state.var_values,
396 max_input_universe,
397 impl_args,
398 );
399 state
400 .current_evaluation_scope()
401 .steps
402 .push(WipProbeStep::RecordImplArgs { impl_args });
403 }
404 None => {}
405 _ => panic!(),
406 }
407 }
408
409 pub(crate) fn make_canonical_response(&mut self, shallow_certainty: Certainty) {
410 match self.as_mut() {
411 Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
412 state
413 .current_evaluation_scope()
414 .steps
415 .push(WipProbeStep::MakeCanonicalResponse { shallow_certainty });
416 }
417 None => {}
418 _ => panic!(),
419 }
420 }
421
422 pub(crate) fn finish_probe(mut self) -> ProofTreeBuilder<D> {
423 match self.as_mut() {
424 None => {}
425 Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
426 assert_ne!(state.probe_depth, 0);
427 let num_var_values = state.current_evaluation_scope().initial_num_var_values;
428 state.var_values.truncate(num_var_values);
429 state.probe_depth -= 1;
430 }
431 _ => panic!(),
432 }
433
434 self
435 }
436
437 pub(crate) fn query_result(&mut self, result: QueryResult<I>) {
438 if let Some(this) = self.as_mut() {
439 match this {
440 DebugSolver::GoalEvaluation(goal_evaluation) => {
441 assert_eq!(goal_evaluation.result.replace(result), None);
442 }
443 DebugSolver::CanonicalGoalEvaluationStep(evaluation_step) => {
444 assert_eq!(
445 evaluation_step
446 .evaluation
447 .kind
448 .replace(inspect::ProbeKind::Root { result }),
449 None
450 );
451 }
452 _ => unreachable!(),
453 }
454 }
455 }
456}