11use super :: * ;
22
33pub ( 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 ) ,
65}
76
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 < ' _ , ' _ > {
917 fn write_str ( & mut self , s : & str ) -> std:: fmt:: Result {
1018 for line in s. split_inclusive ( "\n " ) {
1119 if self . on_newline {
@@ -19,49 +27,52 @@ impl Write for ProofTreeFormatter<'_, '_> {
1927 }
2028}
2129
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 }
2533 }
2634
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+ }
2941
42+ pub ( super ) fn format_goal_evaluation ( & mut self , goal : & GoalEvaluation < ' _ > ) -> std:: fmt:: Result {
3043 let goal_text = match goal. is_normalizes_to_hack {
3144 IsNormalizesToHack :: Yes => "NORMALIZES-TO HACK GOAL" ,
3245 IsNormalizesToHack :: No => "GOAL" ,
3346 } ;
3447
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) ?;
3750
3851 match & goal. kind {
3952 GoalEvaluationKind :: CacheHit ( CacheHit :: Global ) => {
40- writeln ! ( f, "GLOBAL CACHE HIT: {:?}" , goal. result)
53+ writeln ! ( self . f, "GLOBAL CACHE HIT: {:?}" , goal. result)
4154 }
4255 GoalEvaluationKind :: CacheHit ( CacheHit :: Provisional ) => {
43- writeln ! ( f, "PROVISIONAL CACHE HIT: {:?}" , goal. result)
56+ writeln ! ( self . f, "PROVISIONAL CACHE HIT: {:?}" , goal. result)
4457 }
4558 GoalEvaluationKind :: Uncached { revisions } => {
4659 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) ) ?;
5162 }
52-
53- let f = & mut * self . f ;
54- writeln ! ( f, "RESULT: {:?}" , goal. result)
63+ writeln ! ( self . f, "RESULT: {:?}" , goal. result)
5564 }
5665 } ?;
5766
5867 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+
6576 writeln ! ( self . f, "]" ) ?;
6677 }
6778
@@ -72,58 +83,53 @@ impl ProofTreeFormatter<'_, '_> {
7283 & mut self ,
7384 evaluation_step : & GoalEvaluationStep < ' _ > ,
7485 ) -> 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) ?;
7787
7888 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) ) ?;
8190 }
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) ) ?;
8593 }
8694
8795 Ok ( ( ) )
8896 }
8997
9098 pub ( super ) fn format_candidate ( & mut self , candidate : & GoalCandidate < ' _ > ) -> std:: fmt:: Result {
91- let f = & mut * self . f ;
92-
9399 match & candidate. kind {
94100 CandidateKind :: NormalizedSelfTyAssembly => {
95- writeln ! ( f, "NORMALIZING SELF TY FOR ASSEMBLY:" )
101+ writeln ! ( self . f, "NORMALIZING SELF TY FOR ASSEMBLY:" )
96102 }
97103 CandidateKind :: Candidate { name, result } => {
98- writeln ! ( f, "CANDIDATE {}: {:?}" , name, result)
104+ writeln ! ( self . f, "CANDIDATE {}: {:?}" , name, result)
99105 }
100106 } ?;
101107
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+ } )
111117 }
112118
113119 pub ( super ) fn format_nested_goal_evaluation (
114120 & mut self ,
115121 nested_goal_evaluation : & AddedGoalsEvaluation < ' _ > ,
116122 ) -> 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) ?;
119124
120125 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+ } ) ?;
127133 }
128134
129135 Ok ( ( ) )
0 commit comments