smaller decls output

Decls debug rendering is a bit noisey, especially when most of the fields
are empty. This change updates the debug implementation to only print out
the decls fields and to print it all as one big list.

The motivation is that the Decls object is usually created from a Program
which itself is simply a list of declarations. The local_ids fields are
only there to make lookup faster and contain no more info than the decls
themselves. One can separate the types of decls visually because they
have some prefix (eg `trait`, `fn`) so printing them as on big
heterogenuous list loses no information compared to printing every field
separately.

The end result is going from
```decls(222, {trait Foo}, [],[],[],[],{Foo},{})```
to
```decls[trait Foo]```

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,20 @@ 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 {
+        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()
+    }
+}
+
 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 Foo <ty> , impl Foo(u32), 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 Foo <ty> , impl Foo(u32), 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 Foo <ty> , impl Foo(u32), 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 Foo <ty> , impl Foo(u32), 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 Foo <ty> , impl Foo(u32), 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 Foo <ty> , impl Foo(u32), 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()`"#]]);
 }