@@ -39,44 +39,49 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
39
39
func ( & mut ProofTreeFormatter { f : & mut Indentor { f : self . f , on_newline : true } } )
40
40
}
41
41
42
- pub ( super ) fn format_goal_evaluation ( & mut self , goal : & GoalEvaluation < ' _ > ) -> std:: fmt:: Result {
43
- let goal_text = match goal . is_normalizes_to_hack {
42
+ pub ( super ) fn format_goal_evaluation ( & mut self , eval : & GoalEvaluation < ' _ > ) -> std:: fmt:: Result {
43
+ let goal_text = match eval . is_normalizes_to_hack {
44
44
IsNormalizesToHack :: Yes => "NORMALIZES-TO HACK GOAL" ,
45
45
IsNormalizesToHack :: No => "GOAL" ,
46
46
} ;
47
+ writeln ! ( self . f, "{}: {:?}" , goal_text, eval. uncanonicalized_goal) ?;
48
+ self . nested ( |this| this. format_canonical_goal_evaluation ( & eval. evaluation ) ) ?;
49
+ if eval. returned_goals . len ( ) > 0 {
50
+ writeln ! ( self . f, "NESTED GOALS ADDED TO CALLER: [" ) ?;
51
+ self . nested ( |this| {
52
+ for goal in eval. returned_goals . iter ( ) {
53
+ writeln ! ( this. f, "ADDED GOAL: {goal:?}," ) ?;
54
+ }
55
+ Ok ( ( ) )
56
+ } ) ?;
47
57
48
- writeln ! ( self . f, "{}: {:?}" , goal_text, goal. uncanonicalized_goal) ?;
49
- writeln ! ( self . f, "CANONICALIZED: {:?}" , goal. canonicalized_goal) ?;
58
+ writeln ! ( self . f, "]" )
59
+ } else {
60
+ Ok ( ( ) )
61
+ }
62
+ }
63
+
64
+ pub ( super ) fn format_canonical_goal_evaluation (
65
+ & mut self ,
66
+ eval : & CanonicalGoalEvaluation < ' _ > ,
67
+ ) -> std:: fmt:: Result {
68
+ writeln ! ( self . f, "GOAL: {:?}" , eval. goal) ?;
50
69
51
- match & goal . kind {
70
+ match & eval . kind {
52
71
GoalEvaluationKind :: CacheHit ( CacheHit :: Global ) => {
53
- writeln ! ( self . f, "GLOBAL CACHE HIT: {:?}" , goal . result)
72
+ writeln ! ( self . f, "GLOBAL CACHE HIT: {:?}" , eval . result)
54
73
}
55
74
GoalEvaluationKind :: CacheHit ( CacheHit :: Provisional ) => {
56
- writeln ! ( self . f, "PROVISIONAL CACHE HIT: {:?}" , goal . result)
75
+ writeln ! ( self . f, "PROVISIONAL CACHE HIT: {:?}" , eval . result)
57
76
}
58
77
GoalEvaluationKind :: Uncached { revisions } => {
59
78
for ( n, step) in revisions. iter ( ) . enumerate ( ) {
60
79
writeln ! ( self . f, "REVISION {n}: {:?}" , step. result) ?;
61
80
self . nested ( |this| this. format_evaluation_step ( step) ) ?;
62
81
}
63
- writeln ! ( self . f, "RESULT: {:?}" , goal . result)
82
+ writeln ! ( self . f, "RESULT: {:?}" , eval . result)
64
83
}
65
- } ?;
66
-
67
- if goal. returned_goals . len ( ) > 0 {
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
-
76
- writeln ! ( self . f, "]" ) ?;
77
84
}
78
-
79
- Ok ( ( ) )
80
85
}
81
86
82
87
pub ( super ) fn format_evaluation_step (
@@ -88,8 +93,8 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
88
93
for candidate in & evaluation_step. candidates {
89
94
self . nested ( |this| this. format_candidate ( candidate) ) ?;
90
95
}
91
- for nested in & evaluation_step. nested_goal_evaluations {
92
- self . nested ( |this| this. format_nested_goal_evaluation ( nested) ) ?;
96
+ for nested in & evaluation_step. added_goals_evaluations {
97
+ self . nested ( |this| this. format_added_goals_evaluation ( nested) ) ?;
93
98
}
94
99
95
100
Ok ( ( ) )
@@ -115,20 +120,20 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
115
120
for candidate in & candidate. candidates {
116
121
this. format_candidate ( candidate) ?;
117
122
}
118
- for nested in & candidate. nested_goal_evaluations {
119
- this. format_nested_goal_evaluation ( nested) ?;
123
+ for nested in & candidate. added_goals_evaluations {
124
+ this. format_added_goals_evaluation ( nested) ?;
120
125
}
121
126
Ok ( ( ) )
122
127
} )
123
128
}
124
129
125
- pub ( super ) fn format_nested_goal_evaluation (
130
+ pub ( super ) fn format_added_goals_evaluation (
126
131
& mut self ,
127
- nested_goal_evaluation : & AddedGoalsEvaluation < ' _ > ,
132
+ added_goals_evaluation : & AddedGoalsEvaluation < ' _ > ,
128
133
) -> std:: fmt:: Result {
129
- writeln ! ( self . f, "TRY_EVALUATE_ADDED_GOALS: {:?}" , nested_goal_evaluation . result) ?;
134
+ writeln ! ( self . f, "TRY_EVALUATE_ADDED_GOALS: {:?}" , added_goals_evaluation . result) ?;
130
135
131
- for ( n, revision) in nested_goal_evaluation . evaluations . iter ( ) . enumerate ( ) {
136
+ for ( n, revision) in added_goals_evaluation . evaluations . iter ( ) . enumerate ( ) {
132
137
writeln ! ( self . f, "REVISION {n}" ) ?;
133
138
self . nested ( |this| {
134
139
for goal_evaluation in revision {
0 commit comments