hir_ty/next_solver/
format_proof_tree.rs

1use rustc_type_ir::{solve::GoalSource, solve::inspect::GoalEvaluation};
2use serde_derive::{Deserialize, Serialize};
3
4use crate::next_solver::inspect::{InspectCandidate, InspectGoal};
5use crate::next_solver::{AnyImplId, infer::InferCtxt};
6use crate::{Span, next_solver::DbInterner};
7
8#[derive(Debug, Clone, Serialize, Deserialize)]
9pub struct ProofTreeData {
10    pub goal: String,
11    pub result: String,
12    pub depth: usize,
13    pub candidates: Vec<CandidateData>,
14}
15
16#[derive(Debug, Clone, Serialize, Deserialize)]
17pub struct CandidateData {
18    pub kind: String,
19    pub result: String,
20    pub impl_header: Option<String>,
21    pub nested_goals: Vec<ProofTreeData>,
22}
23
24pub fn dump_proof_tree_structured<'db>(
25    proof_tree: GoalEvaluation<DbInterner<'db>>,
26    _span: Span,
27    infcx: &InferCtxt<'db>,
28) -> ProofTreeData {
29    let goal_eval = InspectGoal::new(infcx, 0, proof_tree, None, GoalSource::Misc);
30    let mut serializer = ProofTreeSerializer::new(infcx);
31    serializer.serialize_goal(&goal_eval)
32}
33
34struct ProofTreeSerializer<'a, 'db> {
35    infcx: &'a InferCtxt<'db>,
36}
37
38impl<'a, 'db> ProofTreeSerializer<'a, 'db> {
39    fn new(infcx: &'a InferCtxt<'db>) -> Self {
40        Self { infcx }
41    }
42
43    fn serialize_goal(&mut self, goal: &InspectGoal<'_, 'db>) -> ProofTreeData {
44        let candidates = goal.candidates();
45        let candidates_data: Vec<CandidateData> =
46            candidates.iter().map(|c| self.serialize_candidate(c)).collect();
47
48        ProofTreeData {
49            goal: format!("{:?}", goal.goal()),
50            result: format!("{:?}", goal.result()),
51            depth: goal.depth(),
52            candidates: candidates_data,
53        }
54    }
55
56    fn serialize_candidate(&mut self, candidate: &InspectCandidate<'_, 'db>) -> CandidateData {
57        let kind = candidate.kind();
58        let impl_header = self.get_impl_header(candidate);
59
60        let mut nested = Vec::new();
61        self.infcx.probe(|_| {
62            for nested_goal in candidate.instantiate_nested_goals(Span::Dummy) {
63                nested.push(self.serialize_goal(&nested_goal));
64            }
65        });
66
67        CandidateData {
68            kind: format!("{:?}", kind),
69            result: format!("{:?}", candidate.result()),
70            impl_header,
71            nested_goals: nested,
72        }
73    }
74
75    fn get_impl_header(&self, candidate: &InspectCandidate<'_, 'db>) -> Option<String> {
76        use rustc_type_ir::solve::inspect::ProbeKind;
77        match candidate.kind() {
78            ProbeKind::TraitCandidate { source, .. } => {
79                use hir_def::{Lookup, src::HasSource};
80                use rustc_type_ir::solve::CandidateSource;
81                let db = self.infcx.interner.db;
82                match source {
83                    CandidateSource::Impl(impl_def_id) => match impl_def_id {
84                        AnyImplId::ImplId(impl_def_id) => {
85                            let impl_src = impl_def_id.lookup(db).source(db);
86                            Some(impl_src.value.to_string())
87                        }
88                        AnyImplId::BuiltinDeriveImplId(impl_id) => {
89                            let impl_loc = impl_id.loc(db);
90                            let adt_src = match impl_loc.adt {
91                                hir_def::AdtId::StructId(adt) => {
92                                    adt.loc(db).source(db).value.to_string()
93                                }
94                                hir_def::AdtId::UnionId(adt) => {
95                                    adt.loc(db).source(db).value.to_string()
96                                }
97                                hir_def::AdtId::EnumId(adt) => {
98                                    adt.loc(db).source(db).value.to_string()
99                                }
100                            };
101                            Some(format!("#[derive(${})]\n{}", impl_loc.trait_.name(), adt_src))
102                        }
103                    },
104                    _ => None,
105                }
106            }
107            _ => None,
108        }
109    }
110}
hir_ty/next_solver/format_proof_tree.rs

hir_ty/next_solver/
format_proof_tree.rs
