smaller decls output

Decls debug rendering is a bit noisy, especially since decls does not
change, but is printed for every step that failed.  With this change,
decls is only printed in the `prove` judgement, with the expectation that
this is the main entrypoint for proofs.

crates/formality-prove/src/decls.rs

@@ -6,6 +6,7 @@ use formality_types::grammar::{
 };
 
 #[term]
+#[customize(debug)]
 pub struct Decls {
     pub max_size: usize,
 
@@ -20,6 +21,31 @@ pub struct Decls {
     pub local_adt_ids: Set<AdtId>,
 }
 
+impl std::fmt::Debug for Decls {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        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()
+    }
+}
+
 impl Decls {
     /// Max size used in unit tests that are not stress testing maximum size.
     pub const DEFAULT_MAX_SIZE: usize = 222;

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(222, [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(222, [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(222, [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(222, [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(222, [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(222, [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()`"#]]);
 }