rustc_next_trait_solver/solve/inspect/
build.rs

1//! Building proof trees incrementally during trait solving.
2//!
3//! This code is *a bit* of a mess and can hopefully be
4//! mostly ignored. For a general overview of how it works,
5//! see the comment on [ProofTreeBuilder].
6
7use 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
19/// The core data structure when building proof trees.
20///
21/// In case the current evaluation does not generate a proof
22/// tree, `state` is simply `None` and we avoid any work.
23///
24/// The possible states of the solver are represented via
25/// variants of [DebugSolver]. For any nested computation we call
26/// `ProofTreeBuilder::new_nested_computation_kind` which
27/// creates a new `ProofTreeBuilder` to temporarily replace the
28/// current one. Once that nested computation is done,
29/// `ProofTreeBuilder::nested_computation_kind` is called
30/// to add the finished nested evaluation to the parent.
31///
32/// We provide additional information to the current state
33/// by calling methods such as `ProofTreeBuilder::probe_kind`.
34///
35/// The actual structure closely mirrors the finished proof
36/// trees. At the end of trait solving `ProofTreeBuilder::finalize`
37/// is called to recursively convert the whole structure to a
38/// finished proof tree.
39pub(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/// The current state of the proof tree builder, at most places
49/// in the code, only one or two variants are actually possible.
50///
51/// We simply ICE in case that assumption is broken.
52#[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    /// After we finished evaluating this is moved into `kind`.
77    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/// This only exists during proof tree building and does not have
99/// a corresponding struct in `inspect`. We need this to track a
100/// bunch of metadata about the current evaluation.
101#[derive_where(PartialEq, Eq, Debug; I: Interner)]
102struct WipCanonicalGoalEvaluationStep<I: Interner> {
103    /// Unlike `EvalCtxt::var_values`, we append a new
104    /// generic arg here whenever we create a new inference
105    /// variable.
106    ///
107    /// This is necessary as we otherwise don't unify these
108    /// vars when instantiating multiple `CanonicalState`.
109    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}