|
1 | 1 | use super::{CanonicalInput, Certainty, Goal, NoSolution, QueryInput, QueryResult}; |
2 | 2 | use crate::{traits::IsNormalizesToHack, ty}; |
| 3 | +use format::ProofTreeFormatter; |
3 | 4 | use std::fmt::{Debug, Write}; |
4 | 5 |
|
| 6 | +mod format; |
| 7 | + |
5 | 8 | #[derive(Eq, PartialEq, Debug, Hash, HashStable)] |
6 | 9 | pub enum CacheHit { |
7 | 10 | Provisional, |
@@ -74,133 +77,3 @@ impl Debug for GoalCandidate<'_> { |
74 | 77 | ProofTreeFormatter { f, on_newline: true }.format_candidate(self) |
75 | 78 | } |
76 | 79 | } |
77 | | - |
78 | | -struct ProofTreeFormatter<'a, 'b> { |
79 | | - f: &'a mut (dyn Write + 'b), |
80 | | - on_newline: bool, |
81 | | -} |
82 | | - |
83 | | -impl Write for ProofTreeFormatter<'_, '_> { |
84 | | - fn write_str(&mut self, s: &str) -> std::fmt::Result { |
85 | | - for line in s.split_inclusive("\n") { |
86 | | - if self.on_newline { |
87 | | - self.f.write_str(" ")?; |
88 | | - } |
89 | | - self.on_newline = line.ends_with("\n"); |
90 | | - self.f.write_str(line)?; |
91 | | - } |
92 | | - |
93 | | - Ok(()) |
94 | | - } |
95 | | -} |
96 | | - |
97 | | -impl ProofTreeFormatter<'_, '_> { |
98 | | - fn nested(&mut self) -> ProofTreeFormatter<'_, '_> { |
99 | | - ProofTreeFormatter { f: self, on_newline: true } |
100 | | - } |
101 | | - |
102 | | - fn format_goal_evaluation(&mut self, goal: &GoalEvaluation<'_>) -> std::fmt::Result { |
103 | | - let f = &mut *self.f; |
104 | | - |
105 | | - let goal_text = match goal.is_normalizes_to_hack { |
106 | | - IsNormalizesToHack::Yes => "NORMALIZES-TO HACK GOAL", |
107 | | - IsNormalizesToHack::No => "GOAL", |
108 | | - }; |
109 | | - |
110 | | - writeln!(f, "{}: {:?}", goal_text, goal.uncanonicalized_goal,)?; |
111 | | - writeln!(f, "CANONICALIZED: {:?}", goal.canonicalized_goal)?; |
112 | | - |
113 | | - match &goal.kind { |
114 | | - GoalEvaluationKind::CacheHit(CacheHit::Global) => { |
115 | | - writeln!(f, "GLOBAL CACHE HIT: {:?}", goal.result) |
116 | | - } |
117 | | - GoalEvaluationKind::CacheHit(CacheHit::Provisional) => { |
118 | | - writeln!(f, "PROVISIONAL CACHE HIT: {:?}", goal.result) |
119 | | - } |
120 | | - GoalEvaluationKind::Uncached { revisions } => { |
121 | | - for (n, step) in revisions.iter().enumerate() { |
122 | | - let f = &mut *self.f; |
123 | | - writeln!(f, "REVISION {n}: {:?}", step.result)?; |
124 | | - let mut f = self.nested(); |
125 | | - f.format_evaluation_step(step)?; |
126 | | - } |
127 | | - |
128 | | - let f = &mut *self.f; |
129 | | - writeln!(f, "RESULT: {:?}", goal.result) |
130 | | - } |
131 | | - }?; |
132 | | - |
133 | | - if goal.returned_goals.len() > 0 { |
134 | | - let f = &mut *self.f; |
135 | | - writeln!(f, "NESTED GOALS ADDED TO CALLER: [")?; |
136 | | - let mut f = self.nested(); |
137 | | - for goal in goal.returned_goals.iter() { |
138 | | - writeln!(f, "ADDED GOAL: {:?},", goal)?; |
139 | | - } |
140 | | - writeln!(self.f, "]")?; |
141 | | - } |
142 | | - |
143 | | - Ok(()) |
144 | | - } |
145 | | - |
146 | | - fn format_evaluation_step( |
147 | | - &mut self, |
148 | | - evaluation_step: &GoalEvaluationStep<'_>, |
149 | | - ) -> std::fmt::Result { |
150 | | - let f = &mut *self.f; |
151 | | - writeln!(f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?; |
152 | | - |
153 | | - for candidate in &evaluation_step.candidates { |
154 | | - let mut f = self.nested(); |
155 | | - f.format_candidate(candidate)?; |
156 | | - } |
157 | | - for nested_goal_evaluation in &evaluation_step.nested_goal_evaluations { |
158 | | - let mut f = self.nested(); |
159 | | - f.format_nested_goal_evaluation(nested_goal_evaluation)?; |
160 | | - } |
161 | | - |
162 | | - Ok(()) |
163 | | - } |
164 | | - |
165 | | - fn format_candidate(&mut self, candidate: &GoalCandidate<'_>) -> std::fmt::Result { |
166 | | - let f = &mut *self.f; |
167 | | - |
168 | | - match &candidate.kind { |
169 | | - CandidateKind::NormalizedSelfTyAssembly => { |
170 | | - writeln!(f, "NORMALIZING SELF TY FOR ASSEMBLY:") |
171 | | - } |
172 | | - CandidateKind::Candidate { name, result } => { |
173 | | - writeln!(f, "CANDIDATE {}: {:?}", name, result) |
174 | | - } |
175 | | - }?; |
176 | | - |
177 | | - let mut f = self.nested(); |
178 | | - for candidate in &candidate.candidates { |
179 | | - f.format_candidate(candidate)?; |
180 | | - } |
181 | | - for nested_evaluations in &candidate.nested_goal_evaluations { |
182 | | - f.format_nested_goal_evaluation(nested_evaluations)?; |
183 | | - } |
184 | | - |
185 | | - Ok(()) |
186 | | - } |
187 | | - |
188 | | - fn format_nested_goal_evaluation( |
189 | | - &mut self, |
190 | | - nested_goal_evaluation: &AddedGoalsEvaluation<'_>, |
191 | | - ) -> std::fmt::Result { |
192 | | - let f = &mut *self.f; |
193 | | - writeln!(f, "TRY_EVALUATE_ADDED_GOALS: {:?}", nested_goal_evaluation.result)?; |
194 | | - |
195 | | - for (n, revision) in nested_goal_evaluation.evaluations.iter().enumerate() { |
196 | | - let f = &mut *self.f; |
197 | | - writeln!(f, "REVISION {n}")?; |
198 | | - let mut f = self.nested(); |
199 | | - for goal_evaluation in revision { |
200 | | - f.format_goal_evaluation(goal_evaluation)?; |
201 | | - } |
202 | | - } |
203 | | - |
204 | | - Ok(()) |
205 | | - } |
206 | | -} |
0 commit comments