PR: separate decls by field

rust-lang · Jul 12, 2024 · d698205 · d698205
1 parent f909754
commit d698205
Show file tree

Hide file tree

Showing 12 changed files with 248 additions and 237 deletions.
diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs
@@ -23,15 +23,26 @@ pub struct Decls {
 
 impl std::fmt::Debug for Decls {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        f.write_str("decls")?;
-        f.debug_list()
-            .entries(&self.trait_decls)
-            .entries(&self.impl_decls)
-            .entries(&self.neg_impl_decls)
-            .entries(&self.alias_eq_decls)
-            .entries(&self.alias_bound_decls)
-            .entries(&self.adt_decls)
-            .finish()
+        let mut f = f.debug_struct("Decls");
+        if !self.trait_decls.is_empty() {
+            f.field("trait_decls", &self.trait_decls);
+        }
+        if !self.impl_decls.is_empty() {
+            f.field("impl_decls", &self.impl_decls);
+        }
+        if !self.neg_impl_decls.is_empty() {
+            f.field("neg_impl_decls", &self.neg_impl_decls);
+        }
+        if !self.alias_eq_decls.is_empty() {
+            f.field("alias_eq_decls", &self.alias_eq_decls);
+        }
+        if !self.alias_bound_decls.is_empty() {
+            f.field("alias_bound_decls", &self.alias_bound_decls);
+        }
+        if !self.adt_decls.is_empty() {
+            f.field("adt_decls", &self.adt_decls);
+        }
+        f.finish_non_exhaustive()
     }
 }
 

diff --git a/crates/formality-prove/src/test/adt_wf.rs b/crates/formality-prove/src/test/adt_wf.rs
@@ -51,17 +51,17 @@ fn not_well_formed_adt() {
         assumptions,
         Relation::WellFormed(goal),
     ).assert_err(expect![[r#"
-        judgment `prove_wc_list { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls[trait Foo <ty> , impl Foo(u32), adt X <ty> where {Foo(^ty0_0)}] }` failed at the following rule(s):
+        judgment `prove_wc_list { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: Decls { trait_decls: [trait Foo <ty> ], impl_decls: [impl Foo(u32)], adt_decls: [adt X <ty> where {Foo(^ty0_0)}], .. } }` failed at the following rule(s):
           the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-            judgment `prove_wc { goal: @ wf(X<u64>), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls[trait Foo <ty> , impl Foo(u32), adt X <ty> where {Foo(^ty0_0)}] }` failed at the following rule(s):
+            judgment `prove_wc { goal: @ wf(X<u64>), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: Decls { trait_decls: [trait Foo <ty> ], impl_decls: [impl Foo(u32)], adt_decls: [adt X <ty> where {Foo(^ty0_0)}], .. } }` failed at the following rule(s):
               the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because
-                judgment `prove_wf { goal: X<u64>, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls[trait Foo <ty> , impl Foo(u32), adt X <ty> where {Foo(^ty0_0)}] }` failed at the following rule(s):
+                judgment `prove_wf { goal: X<u64>, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: Decls { trait_decls: [trait Foo <ty> ], impl_decls: [impl Foo(u32)], adt_decls: [adt X <ty> where {Foo(^ty0_0)}], .. } }` failed at the following rule(s):
                   the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because
-                    judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {}, decls: decls[trait Foo <ty> , impl Foo(u32), adt X <ty> where {Foo(^ty0_0)}] }` failed at the following rule(s):
+                    judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {}, decls: Decls { trait_decls: [trait Foo <ty> ], impl_decls: [impl Foo(u32)], adt_decls: [adt X <ty> where {Foo(^ty0_0)}], .. } }` failed at the following rule(s):
                       the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
-                        judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls[trait Foo <ty> , impl Foo(u32), adt X <ty> where {Foo(^ty0_0)}] }` failed at the following rule(s):
+                        judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: Decls { trait_decls: [trait Foo <ty> ], impl_decls: [impl Foo(u32)], adt_decls: [adt X <ty> where {Foo(^ty0_0)}], .. } }` failed at the following rule(s):
                           the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-                            judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls[trait Foo <ty> , impl Foo(u32), adt X <ty> where {Foo(^ty0_0)}] }` failed at the following rule(s):
+                            judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: Decls { trait_decls: [trait Foo <ty> ], impl_decls: [impl Foo(u32)], adt_decls: [adt X <ty> where {Foo(^ty0_0)}], .. } }` failed at the following rule(s):
                               the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
                                 expression evaluated to an empty collection: `decls.trait_invariants()`"#]]);
 }