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