1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
use super::*;
pub(super) struct ProofTreeFormatter<'a, 'b> {
f: &'a mut (dyn Write + 'b),
}
/// A formatter which adds 4 spaces of indentation to its input before
/// passing it on to its nested formatter.
///
/// We can use this for arbitrary levels of indentation by nesting it.
struct Indentor<'a, 'b> {
f: &'a mut (dyn Write + 'b),
on_newline: bool,
}
impl Write for Indentor<'_, '_> {
fn write_str(&mut self, s: &str) -> std::fmt::Result {
for line in s.split_inclusive('\n') {
if self.on_newline {
self.f.write_str(" ")?;
}
self.on_newline = line.ends_with('\n');
self.f.write_str(line)?;
}
Ok(())
}
}
impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
pub(super) fn new(f: &'a mut (dyn Write + 'b)) -> Self {
ProofTreeFormatter { f }
}
fn nested<F, R>(&mut self, func: F) -> R
where
F: FnOnce(&mut ProofTreeFormatter<'_, '_>) -> R,
{
func(&mut ProofTreeFormatter { f: &mut Indentor { f: self.f, on_newline: true } })
}
pub(super) fn format_goal_evaluation(&mut self, goal: &GoalEvaluation<'_>) -> std::fmt::Result {
let goal_text = match goal.is_normalizes_to_hack {
IsNormalizesToHack::Yes => "NORMALIZES-TO HACK GOAL",
IsNormalizesToHack::No => "GOAL",
};
writeln!(self.f, "{}: {:?}", goal_text, goal.uncanonicalized_goal)?;
writeln!(self.f, "CANONICALIZED: {:?}", goal.canonicalized_goal)?;
match &goal.kind {
GoalEvaluationKind::CacheHit(CacheHit::Global) => {
writeln!(self.f, "GLOBAL CACHE HIT: {:?}", goal.result)
}
GoalEvaluationKind::CacheHit(CacheHit::Provisional) => {
writeln!(self.f, "PROVISIONAL CACHE HIT: {:?}", goal.result)
}
GoalEvaluationKind::Uncached { revisions } => {
for (n, step) in revisions.iter().enumerate() {
writeln!(self.f, "REVISION {n}: {:?}", step.result)?;
self.nested(|this| this.format_evaluation_step(step))?;
}
writeln!(self.f, "RESULT: {:?}", goal.result)
}
}?;
if goal.returned_goals.len() > 0 {
writeln!(self.f, "NESTED GOALS ADDED TO CALLER: [")?;
self.nested(|this| {
for goal in goal.returned_goals.iter() {
writeln!(this.f, "ADDED GOAL: {goal:?},")?;
}
Ok(())
})?;
writeln!(self.f, "]")?;
}
Ok(())
}
pub(super) fn format_evaluation_step(
&mut self,
evaluation_step: &GoalEvaluationStep<'_>,
) -> std::fmt::Result {
writeln!(self.f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?;
for candidate in &evaluation_step.candidates {
self.nested(|this| this.format_candidate(candidate))?;
}
for nested in &evaluation_step.nested_goal_evaluations {
self.nested(|this| this.format_nested_goal_evaluation(nested))?;
}
Ok(())
}
pub(super) fn format_candidate(&mut self, candidate: &GoalCandidate<'_>) -> std::fmt::Result {
match &candidate.kind {
CandidateKind::NormalizedSelfTyAssembly => {
writeln!(self.f, "NORMALIZING SELF TY FOR ASSEMBLY:")
}
CandidateKind::UnsizeAssembly => {
writeln!(self.f, "ASSEMBLING CANDIDATES FOR UNSIZING:")
}
CandidateKind::UpcastProbe => {
writeln!(self.f, "PROBING FOR PROJECTION COMPATIBILITY FOR UPCASTING:")
}
CandidateKind::Candidate { name, result } => {
writeln!(self.f, "CANDIDATE {name}: {result:?}")
}
}?;
self.nested(|this| {
for candidate in &candidate.candidates {
this.format_candidate(candidate)?;
}
for nested in &candidate.nested_goal_evaluations {
this.format_nested_goal_evaluation(nested)?;
}
Ok(())
})
}
pub(super) fn format_nested_goal_evaluation(
&mut self,
nested_goal_evaluation: &AddedGoalsEvaluation<'_>,
) -> std::fmt::Result {
writeln!(self.f, "TRY_EVALUATE_ADDED_GOALS: {:?}", nested_goal_evaluation.result)?;
for (n, revision) in nested_goal_evaluation.evaluations.iter().enumerate() {
writeln!(self.f, "REVISION {n}")?;
self.nested(|this| {
for goal_evaluation in revision {
this.format_goal_evaluation(goal_evaluation)?;
}
Ok(())
})?;
}
Ok(())
}
}
|
