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::{Certainty, Goal, GoalSource, QueryResult, inspect};
16
17/// We need to know whether to build a prove tree while evaluating. We
18/// pass a `ProofTreeBuilder` with `state: Some(None)` into the search
19/// graph which then causes the initial `EvalCtxt::compute_goal` to actually
20/// build a proof tree which then gets written into the `state`.
21///
22/// Building the proof tree for a single evaluation step happens via the
23/// [EvaluationStepBuilder] which is updated by the `EvalCtxt` when
24/// appropriate.
25pub(crate) struct ProofTreeBuilder<D, I = <D as SolverDelegate>::Interner>
26where
27    D: SolverDelegate<Interner = I>,
28    I: Interner,
29{
30    state: Option<Box<Option<inspect::Probe<I>>>>,
31    _infcx: PhantomData<D>,
32}
33
34impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
35    pub(crate) fn new() -> ProofTreeBuilder<D> {
36        ProofTreeBuilder { state: Some(Box::new(None)), _infcx: PhantomData }
37    }
38
39    pub(crate) fn new_noop() -> ProofTreeBuilder<D> {
40        ProofTreeBuilder { state: None, _infcx: PhantomData }
41    }
42
43    pub(crate) fn is_noop(&self) -> bool {
44        self.state.is_none()
45    }
46
47    pub(crate) fn new_evaluation_step(
48        &mut self,
49        var_values: ty::CanonicalVarValues<I>,
50    ) -> EvaluationStepBuilder<D> {
51        if self.is_noop() {
52            EvaluationStepBuilder { state: None, _infcx: PhantomData }
53        } else {
54            EvaluationStepBuilder {
55                state: Some(Box::new(WipEvaluationStep {
56                    var_values: var_values.var_values.to_vec(),
57                    evaluation: WipProbe {
58                        initial_num_var_values: var_values.len(),
59                        steps: vec![],
60                        kind: None,
61                        final_state: None,
62                    },
63                    probe_depth: 0,
64                })),
65                _infcx: PhantomData,
66            }
67        }
68    }
69
70    pub(crate) fn finish_evaluation_step(
71        &mut self,
72        goal_evaluation_step: EvaluationStepBuilder<D>,
73    ) {
74        if let Some(this) = self.state.as_deref_mut() {
75            *this = Some(goal_evaluation_step.state.unwrap().finalize());
76        }
77    }
78
79    pub(crate) fn unwrap(self) -> inspect::Probe<I> {
80        self.state.unwrap().unwrap()
81    }
82}
83
84pub(crate) struct EvaluationStepBuilder<D, I = <D as SolverDelegate>::Interner>
85where
86    D: SolverDelegate<Interner = I>,
87    I: Interner,
88{
89    state: Option<Box<WipEvaluationStep<I>>>,
90    _infcx: PhantomData<D>,
91}
92
93#[derive_where(PartialEq, Eq, Debug; I: Interner)]
94struct WipEvaluationStep<I: Interner> {
95    /// Unlike `EvalCtxt::var_values`, we append a new
96    /// generic arg here whenever we create a new inference
97    /// variable.
98    ///
99    /// This is necessary as we otherwise don't unify these
100    /// vars when instantiating multiple `CanonicalState`.
101    var_values: Vec<I::GenericArg>,
102    probe_depth: usize,
103    evaluation: WipProbe<I>,
104}
105
106impl<I: Interner> WipEvaluationStep<I> {
107    fn current_evaluation_scope(&mut self) -> &mut WipProbe<I> {
108        let mut current = &mut self.evaluation;
109        for _ in 0..self.probe_depth {
110            match current.steps.last_mut() {
111                Some(WipProbeStep::NestedProbe(p)) => current = p,
112                _ => panic!(),
113            }
114        }
115        current
116    }
117
118    fn finalize(self) -> inspect::Probe<I> {
119        let evaluation = self.evaluation.finalize();
120        match evaluation.kind {
121            inspect::ProbeKind::Root { .. } => evaluation,
122            _ => unreachable!("unexpected root evaluation: {evaluation:?}"),
123        }
124    }
125}
126
127#[derive_where(PartialEq, Debug; I: Interner)]
128struct WipProbe<I: Interner> {
129    initial_num_var_values: usize,
130    steps: Vec<WipProbeStep<I>>,
131    kind: Option<inspect::ProbeKind<I>>,
132    final_state: Option<inspect::CanonicalState<I, ()>>,
133}
134
135impl<I: Interner> Eq for WipProbe<I> {}
136
137impl<I: Interner> WipProbe<I> {
138    fn finalize(self) -> inspect::Probe<I> {
139        inspect::Probe {
140            steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
141            kind: self.kind.unwrap(),
142            final_state: self.final_state.unwrap(),
143        }
144    }
145}
146
147#[derive_where(PartialEq, Debug; I: Interner)]
148enum WipProbeStep<I: Interner> {
149    AddGoal(GoalSource, inspect::CanonicalState<I, Goal<I, I::Predicate>>),
150    NestedProbe(WipProbe<I>),
151    MakeCanonicalResponse { shallow_certainty: Certainty },
152    RecordImplArgs { impl_args: inspect::CanonicalState<I, I::GenericArgs> },
153}
154
155impl<I: Interner> Eq for WipProbeStep<I> {}
156
157impl<I: Interner> WipProbeStep<I> {
158    fn finalize(self) -> inspect::ProbeStep<I> {
159        match self {
160            WipProbeStep::AddGoal(source, goal) => inspect::ProbeStep::AddGoal(source, goal),
161            WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
162            WipProbeStep::RecordImplArgs { impl_args } => {
163                inspect::ProbeStep::RecordImplArgs { impl_args }
164            }
165            WipProbeStep::MakeCanonicalResponse { shallow_certainty } => {
166                inspect::ProbeStep::MakeCanonicalResponse { shallow_certainty }
167            }
168        }
169    }
170}
171
172impl<D: SolverDelegate<Interner = I>, I: Interner> EvaluationStepBuilder<D> {
173    pub(crate) fn new_noop() -> EvaluationStepBuilder<D> {
174        EvaluationStepBuilder { state: None, _infcx: PhantomData }
175    }
176
177    pub(crate) fn is_noop(&self) -> bool {
178        self.state.is_none()
179    }
180
181    fn as_mut(&mut self) -> Option<&mut WipEvaluationStep<I>> {
182        self.state.as_deref_mut()
183    }
184
185    pub(crate) fn take_and_enter_probe(&mut self) -> EvaluationStepBuilder<D> {
186        let mut nested = EvaluationStepBuilder { state: self.state.take(), _infcx: PhantomData };
187        nested.enter_probe();
188        nested
189    }
190
191    pub(crate) fn add_var_value<T: Into<I::GenericArg>>(&mut self, arg: T) {
192        if let Some(this) = self.as_mut() {
193            this.var_values.push(arg.into());
194        }
195    }
196
197    fn enter_probe(&mut self) {
198        if let Some(this) = self.as_mut() {
199            let initial_num_var_values = this.var_values.len();
200            this.current_evaluation_scope().steps.push(WipProbeStep::NestedProbe(WipProbe {
201                initial_num_var_values,
202                steps: vec![],
203                kind: None,
204                final_state: None,
205            }));
206            this.probe_depth += 1;
207        }
208    }
209
210    pub(crate) fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<I>) {
211        if let Some(this) = self.as_mut() {
212            let prev = this.current_evaluation_scope().kind.replace(probe_kind);
213            assert_eq!(prev, None);
214        }
215    }
216
217    pub(crate) fn probe_final_state(
218        &mut self,
219        delegate: &D,
220        max_input_universe: ty::UniverseIndex,
221    ) {
222        if let Some(this) = self.as_mut() {
223            let final_state =
224                canonical::make_canonical_state(delegate, &this.var_values, max_input_universe, ());
225            let prev = this.current_evaluation_scope().final_state.replace(final_state);
226            assert_eq!(prev, None);
227        }
228    }
229
230    pub(crate) fn add_goal(
231        &mut self,
232        delegate: &D,
233        max_input_universe: ty::UniverseIndex,
234        source: GoalSource,
235        goal: Goal<I, I::Predicate>,
236    ) {
237        if let Some(this) = self.as_mut() {
238            let goal = canonical::make_canonical_state(
239                delegate,
240                &this.var_values,
241                max_input_universe,
242                goal,
243            );
244            this.current_evaluation_scope().steps.push(WipProbeStep::AddGoal(source, goal))
245        }
246    }
247
248    pub(crate) fn record_impl_args(
249        &mut self,
250        delegate: &D,
251        max_input_universe: ty::UniverseIndex,
252        impl_args: I::GenericArgs,
253    ) {
254        if let Some(this) = self.as_mut() {
255            let impl_args = canonical::make_canonical_state(
256                delegate,
257                &this.var_values,
258                max_input_universe,
259                impl_args,
260            );
261            this.current_evaluation_scope().steps.push(WipProbeStep::RecordImplArgs { impl_args });
262        }
263    }
264
265    pub(crate) fn make_canonical_response(&mut self, shallow_certainty: Certainty) {
266        if let Some(this) = self.as_mut() {
267            this.current_evaluation_scope()
268                .steps
269                .push(WipProbeStep::MakeCanonicalResponse { shallow_certainty });
270        }
271    }
272
273    pub(crate) fn finish_probe(mut self) -> EvaluationStepBuilder<D> {
274        if let Some(this) = self.as_mut() {
275            assert_ne!(this.probe_depth, 0);
276            let num_var_values = this.current_evaluation_scope().initial_num_var_values;
277            this.var_values.truncate(num_var_values);
278            this.probe_depth -= 1;
279        }
280
281        self
282    }
283
284    pub(crate) fn query_result(&mut self, result: QueryResult<I>) {
285        if let Some(this) = self.as_mut() {
286            assert_eq!(this.evaluation.kind.replace(inspect::ProbeKind::Root { result }), None);
287        }
288    }
289}
rustc_next_trait_solver/solve/inspect/build.rs

rustc_next_trait_solver/solve/inspect/
build.rs
