Skip to content

Commit d383af7

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #355 from crlf0710/master
Extract Debug for GoalData implementation.
2 parents c7bd2bf + 2106b3d commit d383af7

File tree

3 files changed

+217
-84
lines changed

3 files changed

+217
-84
lines changed

‎chalk-integration/src/program.rs

Lines changed: 11 additions & 83 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,9 @@ use chalk_ir::debug::Angle;
44
use chalk_ir::interner::ChalkIr;
55
use chalk_ir::tls;
66
use chalk_ir::{
7-
debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, GoalData, Goals, ImplId,
8-
Lifetime, Parameter, ParameterKind, ProgramClause, ProgramClauseImplication, StructId,
9-
Substitution, TraitId, Ty, TyData, TypeName,
7+
debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplId, Lifetime,
8+
Parameter, ProgramClause, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
9+
TyData, TypeName,
1010
};
1111
use chalk_rust_ir::{
1212
AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum,
@@ -143,10 +143,7 @@ impl tls::DebugContext for Program {
143143
fmt: &mut fmt::Formatter<'_>,
144144
) -> Result<(), fmt::Error> {
145145
let interner = self.interner();
146-
match parameter.data(interner) {
147-
ParameterKind::Ty(n) => write!(fmt, "{:?}", n),
148-
ParameterKind::Lifetime(n) => write!(fmt, "{:?}", n),
149-
}
146+
write!(fmt, "{:?}", parameter.data(interner).inner_debug())
150147
}
151148

152149
fn debug_goal(
@@ -155,27 +152,7 @@ impl tls::DebugContext for Program {
155152
fmt: &mut fmt::Formatter<'_>,
156153
) -> Result<(), fmt::Error> {
157154
let interner = self.interner();
158-
match goal.data(interner) {
159-
GoalData::Quantified(qkind, ref subgoal) => {
160-
write!(fmt, "{:?}<", qkind)?;
161-
for (index, binder) in subgoal.binders.iter().enumerate() {
162-
if index > 0 {
163-
write!(fmt, ", ")?;
164-
}
165-
match *binder {
166-
ParameterKind::Ty(()) => write!(fmt, "type")?,
167-
ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
168-
}
169-
}
170-
write!(fmt, "> {{ {:?} }}", subgoal.value)
171-
}
172-
GoalData::Implies(ref wc, ref g) => write!(fmt, "if ({:?}) {{ {:?} }}", wc, g),
173-
GoalData::All(ref goals) => write!(fmt, "all{:?}", goals),
174-
GoalData::Not(ref g) => write!(fmt, "not {{ {:?} }}", g),
175-
GoalData::EqGoal(ref wc) => write!(fmt, "{:?}", wc),
176-
GoalData::DomainGoal(ref wc) => write!(fmt, "{:?}", wc),
177-
GoalData::CannotProve(()) => write!(fmt, r"¯\_(ツ)_/¯"),
178-
}
155+
write!(fmt, "{:?}", goal.data(interner))
179156
}
180157

181158
fn debug_goals(
@@ -184,15 +161,7 @@ impl tls::DebugContext for Program {
184161
fmt: &mut fmt::Formatter<'_>,
185162
) -> Result<(), fmt::Error> {
186163
let interner = self.interner();
187-
write!(fmt, "(")?;
188-
for (goal, index) in goals.iter(interner).zip(0..) {
189-
if index > 0 {
190-
write!(fmt, ", ")?;
191-
}
192-
write!(fmt, "{:?}", goal)?;
193-
}
194-
write!(fmt, ")")?;
195-
Ok(())
164+
write!(fmt, "{:?}", goals.debug(interner))
196165
}
197166

198167
fn debug_program_clause_implication(
@@ -201,20 +170,7 @@ impl tls::DebugContext for Program {
201170
fmt: &mut fmt::Formatter<'_>,
202171
) -> Result<(), fmt::Error> {
203172
let interner = self.interner();
204-
write!(fmt, "{:?}", pci.consequence)?;
205-
206-
let conditions = pci.conditions.as_slice(interner);
207-
208-
let conds = conditions.len();
209-
if conds == 0 {
210-
return Ok(());
211-
}
212-
213-
write!(fmt, " :- ")?;
214-
for cond in &conditions[..conds - 1] {
215-
write!(fmt, "{:?}, ", cond)?;
216-
}
217-
write!(fmt, "{:?}", conditions[conds - 1])
173+
write!(fmt, "{:?}", pci.debug(interner))
218174
}
219175

220176
fn debug_application_ty(
@@ -223,8 +179,7 @@ impl tls::DebugContext for Program {
223179
fmt: &mut fmt::Formatter<'_>,
224180
) -> Result<(), fmt::Error> {
225181
let interner = self.interner();
226-
let ApplicationTy { name, substitution } = application_ty;
227-
write!(fmt, "{:?}{:?}", name, substitution.with_angle(interner))
182+
write!(fmt, "{:?}", application_ty.debug(interner))
228183
}
229184

230185
fn debug_substitution(
@@ -233,43 +188,16 @@ impl tls::DebugContext for Program {
233188
fmt: &mut fmt::Formatter<'_>,
234189
) -> Result<(), fmt::Error> {
235190
let interner = self.interner();
236-
let mut first = true;
237-
238-
write!(fmt, "[")?;
239-
240-
for (index, value) in substitution.iter(interner).enumerate() {
241-
if first {
242-
first = false;
243-
} else {
244-
write!(fmt, ", ")?;
245-
}
246-
247-
write!(fmt, "?{} := {:?}", index, value)?;
248-
}
249-
250-
write!(fmt, "]")?;
251-
252-
Ok(())
191+
write!(fmt, "{:?}", substitution.debug(interner))
253192
}
254193

255194
fn debug_separator_trait_ref(
256195
&self,
257-
separator_trait_ref: &SeparatorTraitRef<ChalkIr>,
196+
separator_trait_ref: &SeparatorTraitRef<'_, ChalkIr>,
258197
fmt: &mut fmt::Formatter<'_>,
259198
) -> Result<(), fmt::Error> {
260199
let interner = self.interner();
261-
let parameters = separator_trait_ref
262-
.trait_ref
263-
.substitution
264-
.parameters(interner);
265-
write!(
266-
fmt,
267-
"{:?}{}{:?}{:?}",
268-
parameters[0],
269-
separator_trait_ref.separator,
270-
separator_trait_ref.trait_ref.trait_id,
271-
Angle(&parameters[1..])
272-
)
200+
write!(fmt, "{:?}", separator_trait_ref.debug(interner))
273201
}
274202
}
275203

‎chalk-ir/src/debug.rs

Lines changed: 205 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -169,6 +169,176 @@ impl<I: Interner> Debug for LifetimeData<I> {
169169
}
170170
}
171171

172+
impl<I: Interner> Debug for GoalData<I> {
173+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
174+
match self {
175+
GoalData::Quantified(qkind, ref subgoal) => {
176+
write!(fmt, "{:?}<", qkind)?;
177+
for (index, binder) in subgoal.binders.iter().enumerate() {
178+
if index > 0 {
179+
write!(fmt, ", ")?;
180+
}
181+
match *binder {
182+
ParameterKind::Ty(()) => write!(fmt, "type")?,
183+
ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
184+
}
185+
}
186+
write!(fmt, "> {{ {:?} }}", subgoal.value)
187+
}
188+
GoalData::Implies(ref wc, ref g) => write!(fmt, "if ({:?}) {{ {:?} }}", wc, g),
189+
GoalData::All(ref goals) => write!(fmt, "all{:?}", goals),
190+
GoalData::Not(ref g) => write!(fmt, "not {{ {:?} }}", g),
191+
GoalData::EqGoal(ref wc) => write!(fmt, "{:?}", wc),
192+
GoalData::DomainGoal(ref wc) => write!(fmt, "{:?}", wc),
193+
GoalData::CannotProve(()) => write!(fmt, r"¯\_(ツ)_/¯"),
194+
}
195+
}
196+
}
197+
198+
pub struct GoalsDebug<'a, I: Interner> {
199+
goals: &'a Goals<I>,
200+
interner: &'a I,
201+
}
202+
203+
impl<'a, I: Interner> Debug for GoalsDebug<'a, I> {
204+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
205+
write!(fmt, "(")?;
206+
for (goal, index) in self.goals.iter(self.interner).zip(0..) {
207+
if index > 0 {
208+
write!(fmt, ", ")?;
209+
}
210+
write!(fmt, "{:?}", goal)?;
211+
}
212+
write!(fmt, ")")?;
213+
Ok(())
214+
}
215+
}
216+
217+
impl<I: Interner> Goals<I> {
218+
pub fn debug<'a>(&'a self, interner: &'a I) -> GoalsDebug<'a, I> {
219+
GoalsDebug {
220+
goals: self,
221+
interner,
222+
}
223+
}
224+
}
225+
226+
pub struct ParameterDataInnerDebug<'a, I: Interner>(&'a ParameterData<I>);
227+
228+
impl<'a, I: Interner> Debug for ParameterDataInnerDebug<'a, I> {
229+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
230+
match self.0 {
231+
ParameterKind::Ty(n) => write!(fmt, "{:?}", n),
232+
ParameterKind::Lifetime(n) => write!(fmt, "{:?}", n),
233+
}
234+
}
235+
}
236+
237+
impl<I: Interner> ParameterData<I> {
238+
pub fn inner_debug(&self) -> ParameterDataInnerDebug<'_, I> {
239+
ParameterDataInnerDebug(self)
240+
}
241+
}
242+
243+
pub struct ProgramClauseImplicationDebug<'a, I: Interner> {
244+
pci: &'a ProgramClauseImplication<I>,
245+
interner: &'a I,
246+
}
247+
248+
impl<'a, I: Interner> Debug for ProgramClauseImplicationDebug<'a, I> {
249+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
250+
let ProgramClauseImplicationDebug { pci, interner } = self;
251+
write!(fmt, "{:?}", pci.consequence)?;
252+
253+
let conditions = pci.conditions.as_slice(interner);
254+
255+
let conds = conditions.len();
256+
if conds == 0 {
257+
return Ok(());
258+
}
259+
260+
write!(fmt, " :- ")?;
261+
for cond in &conditions[..conds - 1] {
262+
write!(fmt, "{:?}, ", cond)?;
263+
}
264+
write!(fmt, "{:?}", conditions[conds - 1])
265+
}
266+
}
267+
268+
impl<I: Interner> ProgramClauseImplication<I> {
269+
pub fn debug<'a>(&'a self, interner: &'a I) -> ProgramClauseImplicationDebug<'a, I> {
270+
ProgramClauseImplicationDebug {
271+
pci: self,
272+
interner,
273+
}
274+
}
275+
}
276+
277+
pub struct ApplicationTyDebug<'a, I: Interner> {
278+
application_ty: &'a ApplicationTy<I>,
279+
interner: &'a I,
280+
}
281+
282+
impl<'a, I: Interner> Debug for ApplicationTyDebug<'a, I> {
283+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
284+
let ApplicationTyDebug {
285+
application_ty,
286+
interner,
287+
} = self;
288+
let ApplicationTy { name, substitution } = application_ty;
289+
write!(fmt, "{:?}{:?}", name, substitution.with_angle(interner))
290+
}
291+
}
292+
293+
impl<I: Interner> ApplicationTy<I> {
294+
pub fn debug<'a>(&'a self, interner: &'a I) -> ApplicationTyDebug<'a, I> {
295+
ApplicationTyDebug {
296+
application_ty: self,
297+
interner,
298+
}
299+
}
300+
}
301+
302+
pub struct SubstitutionDebug<'a, I: Interner> {
303+
substitution: &'a Substitution<I>,
304+
interner: &'a I,
305+
}
306+
307+
impl<'a, I: Interner> Debug for SubstitutionDebug<'a, I> {
308+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
309+
let SubstitutionDebug {
310+
substitution,
311+
interner,
312+
} = self;
313+
let mut first = true;
314+
315+
write!(fmt, "[")?;
316+
317+
for (index, value) in substitution.iter(interner).enumerate() {
318+
if first {
319+
first = false;
320+
} else {
321+
write!(fmt, ", ")?;
322+
}
323+
324+
write!(fmt, "?{} := {:?}", index, value)?;
325+
}
326+
327+
write!(fmt, "]")?;
328+
329+
Ok(())
330+
}
331+
}
332+
333+
impl<I: Interner> Substitution<I> {
334+
pub fn debug<'a>(&'a self, interner: &'a I) -> SubstitutionDebug<'a, I> {
335+
SubstitutionDebug {
336+
substitution: self,
337+
interner,
338+
}
339+
}
340+
}
341+
172342
impl Debug for PlaceholderIndex {
173343
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
174344
let PlaceholderIndex { ui, idx } = self;
@@ -205,6 +375,41 @@ pub struct SeparatorTraitRef<'me, I: Interner> {
205375
pub separator: &'me str,
206376
}
207377

378+
pub struct SeparatorTraitRefDebug<'a, 'me, I: Interner> {
379+
separator_trait_ref: &'a SeparatorTraitRef<'me, I>,
380+
interner: &'a I,
381+
}
382+
383+
impl<'a, 'me, I: Interner> Debug for SeparatorTraitRefDebug<'a, 'me, I> {
384+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
385+
let SeparatorTraitRefDebug {
386+
separator_trait_ref,
387+
interner,
388+
} = self;
389+
let parameters = separator_trait_ref
390+
.trait_ref
391+
.substitution
392+
.parameters(interner);
393+
write!(
394+
fmt,
395+
"{:?}{}{:?}{:?}",
396+
parameters[0],
397+
separator_trait_ref.separator,
398+
separator_trait_ref.trait_ref.trait_id,
399+
Angle(&parameters[1..])
400+
)
401+
}
402+
}
403+
404+
impl<'me, I: Interner> SeparatorTraitRef<'me, I> {
405+
pub fn debug<'a>(&'a self, interner: &'a I) -> SeparatorTraitRefDebug<'a, 'me, I> {
406+
SeparatorTraitRefDebug {
407+
separator_trait_ref: self,
408+
interner,
409+
}
410+
}
411+
}
412+
208413
pub struct Angle<'a, T>(pub &'a [T]);
209414

210415
impl<'a, T: Debug> Debug for Angle<'a, T> {

‎chalk-ir/src/lib.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1179,7 +1179,7 @@ where
11791179
}
11801180
}
11811181

1182-
#[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, HasInterner)]
1182+
#[derive(Clone, PartialEq, Eq, Hash, Fold, HasInterner)]
11831183
/// A general goal; this is the full range of questions you can pose to Chalk.
11841184
pub enum GoalData<I: Interner> {
11851185
/// Introduces a binding at depth 0, shifting other bindings up

0 commit comments

Comments
 (0)