Skip to content

Commit 54c8544

Browse files
committed
remove trailing newlines from Display etc
These trailing newlines mess with `expect_test` which has some bugs in this area. It also just seems better.
1 parent d12672a commit 54c8544

22 files changed

+22
-50
lines changed

crates/formality-core/src/judgment/proven_set.rs

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -426,8 +426,8 @@ impl std::fmt::Display for FailedJudgment {
426426
if failed_rules.is_empty() {
427427
write!(f, "judgment had no applicable rules: `{judgment}` ",)
428428
} else {
429-
let rules: String = failed_rules.iter().map(|r| r.to_string()).collect();
430-
let rules = indent(rules);
429+
let rules: Vec<String> = failed_rules.iter().map(|r| r.to_string()).collect();
430+
let rules = indent(rules.join("\n"));
431431
write!(
432432
f,
433433
"judgment `{judgment}` failed at the following rule(s):\n{rules}"
@@ -492,7 +492,7 @@ impl<T: Debug> std::fmt::Display for ProvenSet<T> {
492492
Data::Success(set) => {
493493
write!(f, "{{\n")?;
494494
for item in set {
495-
write!(f, "{}", indent(format!("{item:?},\n")))?;
495+
write!(f, "{},\n", indent(format!("{item:?}")))?;
496496
}
497497
write!(f, "}}\n")?;
498498
Ok(())
@@ -503,14 +503,12 @@ impl<T: Debug> std::fmt::Display for ProvenSet<T> {
503503

504504
fn indent(s: impl std::fmt::Display) -> String {
505505
let s = s.to_string();
506-
s.lines()
506+
let lines: Vec<String> = s
507+
.lines()
507508
.map(|l| format!(" {l}"))
508509
.map(|l| l.trim_end().to_string())
509-
.map(|mut l| {
510-
l.push_str("\n");
511-
l
512-
})
513-
.collect()
510+
.collect();
511+
lines.join("\n")
514512
}
515513

516514
/// This trait is used for the `(foo => bar)` patterns.

crates/formality-core/src/judgment/test_filtered.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -51,8 +51,7 @@ fn judgment() {
5151
transitive_reachable(&graph, 0).assert_err(expect_test::expect![[r#"
5252
judgment `transitive_reachable { node: 0, g: Graph { edges: [(0, 1), (1, 2), (2, 4), (2, 3), (3, 6), (4, 8), (8, 10)] } }` failed at the following rule(s):
5353
the rule "base" failed at step #1 (src/file.rs:LL:CC) because
54-
condition evaluted to false: `b % 2 == 0`
55-
"#]]);
54+
condition evaluted to false: `b % 2 == 0`"#]]);
5655

5756
transitive_reachable(&graph, 2).assert_ok(expect_test::expect![[r#"
5857
{

crates/formality-prove/src/test/adt_wf.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,5 @@ fn not_well_formed_adt() {
6363
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
6464
judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
6565
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
66-
expression evaluated to an empty collection: `decls.trait_invariants()`
67-
"#]]);
66+
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]);
6867
}

crates/formality-prove/src/test/eq_assumptions.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -192,8 +192,7 @@ fn test_normalize_assoc_ty_existential0() {
192192
the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because
193193
condition evaluted to false: `env.universe(p) < env.universe(v)`
194194
the rule "normalize-via-impl" failed at step #0 (src/file.rs:LL:CC) because
195-
expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`
196-
"#]]);
195+
expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`"#]]);
197196
}
198197

199198
#[test]

crates/formality-prove/src/test/eq_partial_eq.rs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -54,8 +54,7 @@ fn not_partial_eq_implies_eq() {
5454
the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
5555
judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
5656
the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because
57-
judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
58-
"#]]);
57+
judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`"#]]);
5958
}
6059

6160
#[test]
@@ -102,6 +101,5 @@ fn universals_not_eq() {
102101
the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because
103102
cyclic proof attempt: `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
104103
the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because
105-
judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
106-
"#]]);
104+
judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`"#]]);
107105
}

crates/formality-prove/src/test/is_local.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,7 @@ fn test_forall_not_local() {
2121
the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because
2222
judgment `is_local_trait_ref { goal: Debug(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], coherence_mode: true }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
2323
the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because
24-
condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)`
25-
"#]]);
24+
condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)`"#]]);
2625
}
2726

2827
#[test]

crates/formality-prove/src/test/magic_copy.rs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -69,8 +69,7 @@ fn all_t_not_magic() {
6969
the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because
7070
judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], coherence_mode: false }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`
7171
the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because
72-
judgment had no applicable rules: `prove_via { goal: Magic(!ty_1), via: Copy(?ty_2), assumptions: {}, env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`
73-
"#]]);
72+
judgment had no applicable rules: `prove_via { goal: Magic(!ty_1), via: Copy(?ty_2), assumptions: {}, env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`"#]]);
7473
}
7574

7675
#[test]
@@ -139,6 +138,5 @@ fn all_t_not_copy() {
139138
the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
140139
cyclic proof attempt: `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], coherence_mode: false }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`
141140
the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because
142-
judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], coherence_mode: false }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`
143-
"#]]);
141+
judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], coherence_mode: false }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`"#]]);
144142
}

crates/formality-prove/src/test/occurs_check.rs

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,7 @@ fn direct_cycle() {
3030
the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because
3131
judgment `equate_variable` failed at the following rule(s):
3232
failed at (src/file.rs:LL:CC) because
33-
`?ty_0` occurs in `Vec<?ty_0>`
34-
"#]]);
33+
`?ty_0` occurs in `Vec<?ty_0>`"#]]);
3534
}
3635

3736
/// Test that `X = Vec<Y>` can be solved
@@ -76,8 +75,7 @@ fn indirect_cycle_1() {
7675
the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because
7776
judgment `equate_variable` failed at the following rule(s):
7877
failed at (src/file.rs:LL:CC) because
79-
`?ty_0` occurs in `Vec<?ty_0>`
80-
"#]]);
78+
`?ty_0` occurs in `Vec<?ty_0>`"#]]);
8179
}
8280

8381
/// Test that `X = Vec<X>` cannot be solved (when constructed over several steps)
@@ -102,6 +100,5 @@ fn indirect_cycle_2() {
102100
the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because
103101
judgment `equate_variable` failed at the following rule(s):
104102
failed at (src/file.rs:LL:CC) because
105-
`?ty_0` occurs in `Vec<?ty_0>`
106-
"#]]);
103+
`?ty_0` occurs in `Vec<?ty_0>`"#]]);
107104
}

crates/formality-prove/src/test/universes.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,8 +26,7 @@ fn exists_u_for_t() {
2626
the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because
2727
pattern `None` did not match value `Some(!ty_1)`
2828
the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because
29-
condition evaluted to false: `env.universe(p) < env.universe(v)`
30-
"#]]);
29+
condition evaluted to false: `env.universe(p) < env.universe(v)`"#]]);
3130
}
3231

3332
/// There is U that is equal to some T.

tests/judgment-error-reporting/cyclic_judgment.rs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -74,8 +74,7 @@ fn test() {
7474
expect_test::expect![[r#"
7575
judgment `sub { a: class(Foo), b: class(Bar) }` failed at the following rule(s):
7676
the rule "same class" failed at step #0 (src/file.rs:LL:CC) because
77-
condition evaluted to false: `name_a == name_b`
78-
"#]]
77+
condition evaluted to false: `name_a == name_b`"#]]
7978
);
8079
}
8180

@@ -125,7 +124,6 @@ fn test1() {
125124
the rule "equivalent" failed at step #3 (src/file.rs:LL:CC) because
126125
judgment `sub { a: class(Foo), b: class(Bar) }` failed at the following rule(s):
127126
the rule "same class" failed at step #0 (src/file.rs:LL:CC) because
128-
condition evaluted to false: `name_a == name_b`
129-
"#]]
127+
condition evaluted to false: `name_a == name_b`"#]]
130128
);
131129
}

0 commit comments

Comments
 (0)