Skip to content

Commit 0e53834

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #187 from shua/decl
reduce decls Debug noise
2 parents 8cc6aba + 3315fed commit 0e53834

20 files changed

+650
-550
lines changed

‎crates/formality-prove/src/prove.rs

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,9 @@ mod prove_wc_list;
1313
mod prove_wf;
1414

1515
pub use constraints::Constraints;
16+
use formality_core::judgment::{FailedRule, TryIntoIter};
1617
use formality_core::visit::CoreVisit;
17-
use formality_core::{ProvenSet, Upcast};
18+
use formality_core::{set, ProvenSet, Upcast};
1819
use formality_types::grammar::Wcs;
1920
use tracing::Level;
2021

@@ -53,7 +54,20 @@ pub fn prove(
5354

5455
assert!(env.encloses(term_in));
5556

56-
let result_set = prove_wc_list(decls, &env, assumptions, goal);
57+
struct ProveFailureLabel(String);
58+
let label = ProveFailureLabel(format!(
59+
"prove {{ goal: {goal:?}, assumptions: {assumptions:?}, env: {env:?}, decls: {decls:?} }}"
60+
));
61+
impl std::fmt::Debug for ProveFailureLabel {
62+
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
63+
f.write_str(&self.0)
64+
}
65+
}
66+
let result_set =
67+
match prove_wc_list(decls, &env, assumptions, goal).try_into_iter(|| "".to_string()) {
68+
Ok(s) => ProvenSet::from_iter(s),
69+
Err(e) => ProvenSet::failed_rules(label, set![FailedRule::new(e)]),
70+
};
5771

5872
tracing::debug!(?result_set);
5973

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

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -48,12 +48,12 @@ judgment_fn! {
4848
/// Note that per RFC #2451, upstream crates are not permitted to add blanket impls
4949
/// and so new upstream impls for local types cannot be added.
5050
pub fn may_be_remote(
51-
decls: Decls,
51+
_decls: Decls,
5252
env: Env,
5353
assumptions: Wcs,
5454
goal: TraitRef,
5555
) => Constraints {
56-
debug(assumptions, goal, decls, env)
56+
debug(assumptions, goal, env)
5757
assert(env.bias() == Bias::Completeness)
5858

5959
(
@@ -75,12 +75,12 @@ judgment_fn! {
7575
judgment_fn! {
7676
/// True if an impl defining this trait-reference could appear in a downstream crate.
7777
fn may_be_downstream_trait_ref(
78-
decls: Decls,
78+
_decls: Decls,
7979
env: Env,
8080
assumptions: Wcs,
8181
goal: TraitRef,
8282
) => Constraints {
83-
debug(goal, assumptions, env, decls)
83+
debug(goal, assumptions, env)
8484
assert(env.bias() == Bias::Completeness)
8585
(
8686
// There may be a downstream parameter at position i...
@@ -94,12 +94,12 @@ judgment_fn! {
9494

9595
judgment_fn! {
9696
fn may_be_downstream_parameter(
97-
decls: Decls,
97+
_decls: Decls,
9898
env: Env,
9999
assumptions: Wcs,
100100
parameter: Parameter,
101101
) => Constraints {
102-
debug(parameter, assumptions, env, decls)
102+
debug(parameter, assumptions, env)
103103
assert(env.bias() == Bias::Completeness)
104104
(
105105
// existential variables *could* be inferred to downstream types; depends on the substitution
@@ -179,12 +179,12 @@ fn may_contain_downstream_type(
179179

180180
judgment_fn! {
181181
fn normalizes_to_not_downstream(
182-
decls: Decls,
182+
_decls: Decls,
183183
env: Env,
184184
assumptions: Wcs,
185185
parameter: Parameter,
186186
) => Constraints {
187-
debug(parameter, assumptions, env, decls)
187+
debug(parameter, assumptions, env)
188188

189189
(
190190
(prove_normalize(&decls, &env, &assumptions, parameter) => (c1, parameter))
@@ -198,12 +198,12 @@ judgment_fn! {
198198

199199
judgment_fn! {
200200
pub fn is_local_trait_ref(
201-
decls: Decls,
201+
_decls: Decls,
202202
env: Env,
203203
assumptions: Wcs,
204204
goal: TraitRef,
205205
) => Constraints {
206-
debug(goal, assumptions, env, decls)
206+
debug(goal, assumptions, env)
207207
assert(env.bias() == Bias::Soundness)
208208
(
209209
(if decls.is_local_trait_id(&goal.trait_id))
@@ -235,12 +235,12 @@ judgment_fn! {
235235
/// with something like `Vec<DownstreamType>`, but that is not considered downstream
236236
/// as the outermost type (`Vec`) is upstream.
237237
fn is_not_downstream(
238-
decls: Decls,
238+
_decls: Decls,
239239
env: Env,
240240
assumptions: Wcs,
241241
parameter: Parameter,
242242
) => Constraints {
243-
debug(parameter, assumptions, env, decls)
243+
debug(parameter, assumptions, env)
244244
assert(env.bias() == Bias::Soundness)
245245

246246
(
@@ -276,12 +276,12 @@ judgment_fn! {
276276

277277
judgment_fn! {
278278
fn is_local_parameter(
279-
decls: Decls,
279+
_decls: Decls,
280280
env: Env,
281281
assumptions: Wcs,
282282
goal: Parameter,
283283
) => Constraints {
284-
debug(goal, assumptions, env, decls)
284+
debug(goal, assumptions, env)
285285
assert(env.bias() == Bias::Soundness)
286286

287287
// If we can normalize `goal` to something else, check if that normalized form is local.

‎crates/formality-prove/src/prove/prove_after.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,12 +7,12 @@ use super::constraints::Constraints;
77

88
judgment_fn! {
99
pub fn prove_after(
10-
decls: Decls,
10+
_decls: Decls,
1111
constraints: Constraints,
1212
assumptions: Wcs,
1313
goal: Wcs,
1414
) => Constraints {
15-
debug(constraints, goal, assumptions, decls)
15+
debug(constraints, goal, assumptions)
1616

1717
(
1818
(let (assumptions, goal) = c1.substitution().apply(&(assumptions, goal)))

‎crates/formality-prove/src/prove/prove_eq.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -22,13 +22,13 @@ pub fn eq(a: impl Upcast<Parameter>, b: impl Upcast<Parameter>) -> Relation {
2222

2323
judgment_fn! {
2424
pub fn prove_eq(
25-
decls: Decls,
25+
_decls: Decls,
2626
env: Env,
2727
assumptions: Wcs,
2828
a: Parameter,
2929
b: Parameter,
3030
) => Constraints {
31-
debug(a, b, assumptions, env, decls)
31+
debug(a, b, assumptions, env)
3232

3333
assert(a.kind() == b.kind())
3434

@@ -75,13 +75,13 @@ judgment_fn! {
7575

7676
judgment_fn! {
7777
pub fn prove_existential_var_eq(
78-
decls: Decls,
78+
_decls: Decls,
7979
env: Env,
8080
assumptions: Wcs,
8181
v: ExistentialVar,
8282
b: Parameter,
8383
) => Constraints {
84-
debug(v, b, assumptions, env, decls)
84+
debug(v, b, assumptions, env)
8585

8686
(
8787
(if let None = t.downcast::<Variable>())

‎crates/formality-prove/src/prove/prove_normalize.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -15,12 +15,12 @@ use super::constraints::Constraints;
1515

1616
judgment_fn! {
1717
pub fn prove_normalize(
18-
decls: Decls,
18+
_decls: Decls,
1919
env: Env,
2020
assumptions: Wcs,
2121
p: Parameter,
2222
) => (Constraints, Parameter) {
23-
debug(p, assumptions, env, decls)
23+
debug(p, assumptions, env)
2424

2525
(
2626
(&assumptions => a)!
@@ -48,13 +48,13 @@ judgment_fn! {
4848

4949
judgment_fn! {
5050
fn prove_normalize_via(
51-
decls: Decls,
51+
_decls: Decls,
5252
env: Env,
5353
assumptions: Wcs,
5454
via: Wc,
5555
goal: Parameter,
5656
) => (Constraints, Parameter) {
57-
debug(goal, via, assumptions, env, decls)
57+
debug(goal, via, assumptions, env)
5858

5959
// The following 2 rules handle normalization of existential variables. We look specifically for
6060
// the case of a assumption `?X = Y`, which lets us normalize `?X` to `Y`, and ignore
@@ -126,13 +126,13 @@ judgment_fn! {
126126

127127
judgment_fn! {
128128
fn prove_syntactically_eq(
129-
decls: Decls,
129+
_decls: Decls,
130130
env: Env,
131131
assumptions: Wcs,
132132
a: Parameter,
133133
b: Parameter,
134134
) => Constraints {
135-
debug(a, b, assumptions, env, decls)
135+
debug(a, b, assumptions, env)
136136

137137
trivial(a == b => Constraints::none(env))
138138

‎crates/formality-prove/src/prove/prove_via.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,13 @@ use crate::{
88

99
judgment_fn! {
1010
pub fn prove_via(
11-
decls: Decls,
11+
_decls: Decls,
1212
env: Env,
1313
assumptions: Wcs,
1414
via: WcData,
1515
goal: WcData,
1616
) => Constraints {
17-
debug(goal, via, assumptions, env, decls)
17+
debug(goal, via, assumptions, env)
1818

1919
(
2020
(let (skel_c, parameters_c) = pred_1.debone())

‎crates/formality-prove/src/prove/prove_wc.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,12 +18,12 @@ use super::constraints::Constraints;
1818

1919
judgment_fn! {
2020
pub fn prove_wc(
21-
decls: Decls,
21+
_decls: Decls,
2222
env: Env,
2323
assumptions: Wcs,
2424
goal: Wc,
2525
) => Constraints {
26-
debug(goal, assumptions, env, decls)
26+
debug(goal, assumptions, env)
2727

2828
(
2929
(let (env, subst) = env.universal_substitution(&binder))

‎crates/formality-prove/src/prove/prove_wc_list.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,12 +10,12 @@ use super::{env::Env, prove_wc::prove_wc};
1010

1111
judgment_fn! {
1212
pub fn prove_wc_list(
13-
decls: Decls,
13+
_decls: Decls,
1414
env: Env,
1515
assumptions: Wcs,
1616
goal: Wcs,
1717
) => Constraints {
18-
debug(goal, assumptions, env, decls)
18+
debug(goal, assumptions, env)
1919

2020
assert(env.encloses((&assumptions, &goal)))
2121

‎crates/formality-prove/src/prove/prove_wf.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,12 +12,12 @@ use super::{constraints::Constraints, env::Env};
1212

1313
judgment_fn! {
1414
pub fn prove_wf(
15-
decls: Decls,
15+
_decls: Decls,
1616
env: Env,
1717
assumptions: Wcs,
1818
goal: Parameter,
1919
) => Constraints {
20-
debug(goal, assumptions, env, decls)
20+
debug(goal, assumptions, env)
2121

2222
assert(env.encloses((&assumptions, &goal)))
2323

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

Lines changed: 17 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -51,17 +51,21 @@ fn not_well_formed_adt() {
5151
assumptions,
5252
Relation::WellFormed(goal),
5353
).assert_err(expect![[r#"
54-
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):
55-
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
56-
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):
57-
the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because
58-
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):
59-
the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because
60-
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):
61-
the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
62-
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):
63-
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
64-
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):
65-
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()`"#]]);
54+
judgment `prove { 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):
55+
failed at (src/file.rs:LL:CC) because
56+
judgment `prove_wc_list { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
57+
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
58+
judgment `prove_wc { goal: @ wf(X<u64>), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
59+
the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because
60+
judgment `prove_wf { goal: X<u64>, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
61+
the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because
62+
judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {} }` failed at the following rule(s):
63+
the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
64+
judgment `prove { 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):
65+
failed at (src/file.rs:LL:CC) because
66+
judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
67+
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
68+
judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
69+
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
70+
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]);
6771
}

0 commit comments

Comments
 (0)