Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

reduce decls Debug noise #187

Merged
merged 1 commit into from
Oct 1, 2024
Merged

reduce decls Debug noise #187

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 16 additions & 2 deletions crates/formality-prove/src/prove.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,9 @@ mod prove_wc_list;
mod prove_wf;

pub use constraints::Constraints;
use formality_core::judgment::{FailedRule, TryIntoIter};
use formality_core::visit::CoreVisit;
use formality_core::{ProvenSet, Upcast};
use formality_core::{set, ProvenSet, Upcast};
use formality_types::grammar::Wcs;
use tracing::Level;

Expand Down Expand Up @@ -53,7 +54,20 @@ pub fn prove(

assert!(env.encloses(term_in));

let result_set = prove_wc_list(decls, &env, assumptions, goal);
struct ProveFailureLabel(String);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Question: is it even worth including the "decls" here? I'm inclined to think "not really".

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's nice to see it at least once in proof trace on failure.

let label = ProveFailureLabel(format!(
"prove {{ goal: {goal:?}, assumptions: {assumptions:?}, env: {env:?}, decls: {decls:?} }}"
));
impl std::fmt::Debug for ProveFailureLabel {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
f.write_str(&self.0)
}
}
let result_set =
match prove_wc_list(decls, &env, assumptions, goal).try_into_iter(|| "".to_string()) {
Ok(s) => ProvenSet::from_iter(s),
Err(e) => ProvenSet::failed_rules(label, set![FailedRule::new(e)]),
};

tracing::debug!(?result_set);

Expand Down
28 changes: 14 additions & 14 deletions crates/formality-prove/src/prove/is_local.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,12 +48,12 @@ judgment_fn! {
/// Note that per RFC #2451, upstream crates are not permitted to add blanket impls
/// and so new upstream impls for local types cannot be added.
pub fn may_be_remote(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
goal: TraitRef,
) => Constraints {
debug(assumptions, goal, decls, env)
debug(assumptions, goal, env)
assert(env.bias() == Bias::Completeness)

(
Expand All @@ -75,12 +75,12 @@ judgment_fn! {
judgment_fn! {
/// True if an impl defining this trait-reference could appear in a downstream crate.
fn may_be_downstream_trait_ref(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
goal: TraitRef,
) => Constraints {
debug(goal, assumptions, env, decls)
debug(goal, assumptions, env)
assert(env.bias() == Bias::Completeness)
(
// There may be a downstream parameter at position i...
Expand All @@ -94,12 +94,12 @@ judgment_fn! {

judgment_fn! {
fn may_be_downstream_parameter(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
parameter: Parameter,
) => Constraints {
debug(parameter, assumptions, env, decls)
debug(parameter, assumptions, env)
assert(env.bias() == Bias::Completeness)
(
// existential variables *could* be inferred to downstream types; depends on the substitution
Expand Down Expand Up @@ -179,12 +179,12 @@ fn may_contain_downstream_type(

judgment_fn! {
fn normalizes_to_not_downstream(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
parameter: Parameter,
) => Constraints {
debug(parameter, assumptions, env, decls)
debug(parameter, assumptions, env)

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

judgment_fn! {
pub fn is_local_trait_ref(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
goal: TraitRef,
) => Constraints {
debug(goal, assumptions, env, decls)
debug(goal, assumptions, env)
assert(env.bias() == Bias::Soundness)
(
(if decls.is_local_trait_id(&goal.trait_id))
Expand Down Expand Up @@ -235,12 +235,12 @@ judgment_fn! {
/// with something like `Vec<DownstreamType>`, but that is not considered downstream
/// as the outermost type (`Vec`) is upstream.
fn is_not_downstream(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
parameter: Parameter,
) => Constraints {
debug(parameter, assumptions, env, decls)
debug(parameter, assumptions, env)
assert(env.bias() == Bias::Soundness)

(
Expand Down Expand Up @@ -276,12 +276,12 @@ judgment_fn! {

judgment_fn! {
fn is_local_parameter(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
goal: Parameter,
) => Constraints {
debug(goal, assumptions, env, decls)
debug(goal, assumptions, env)
assert(env.bias() == Bias::Soundness)

// If we can normalize `goal` to something else, check if that normalized form is local.
Expand Down
4 changes: 2 additions & 2 deletions crates/formality-prove/src/prove/prove_after.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,12 @@ use super::constraints::Constraints;

judgment_fn! {
pub fn prove_after(
decls: Decls,
_decls: Decls,
constraints: Constraints,
assumptions: Wcs,
goal: Wcs,
) => Constraints {
debug(constraints, goal, assumptions, decls)
debug(constraints, goal, assumptions)

(
(let (assumptions, goal) = c1.substitution().apply(&(assumptions, goal)))
Expand Down
8 changes: 4 additions & 4 deletions crates/formality-prove/src/prove/prove_eq.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,13 +22,13 @@ pub fn eq(a: impl Upcast<Parameter>, b: impl Upcast<Parameter>) -> Relation {

judgment_fn! {
pub fn prove_eq(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
a: Parameter,
b: Parameter,
) => Constraints {
debug(a, b, assumptions, env, decls)
debug(a, b, assumptions, env)

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

Expand Down Expand Up @@ -75,13 +75,13 @@ judgment_fn! {

judgment_fn! {
pub fn prove_existential_var_eq(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
v: ExistentialVar,
b: Parameter,
) => Constraints {
debug(v, b, assumptions, env, decls)
debug(v, b, assumptions, env)

(
(if let None = t.downcast::<Variable>())
Expand Down
12 changes: 6 additions & 6 deletions crates/formality-prove/src/prove/prove_normalize.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,12 +15,12 @@ use super::constraints::Constraints;

judgment_fn! {
pub fn prove_normalize(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
p: Parameter,
) => (Constraints, Parameter) {
debug(p, assumptions, env, decls)
debug(p, assumptions, env)

(
(&assumptions => a)!
Expand Down Expand Up @@ -48,13 +48,13 @@ judgment_fn! {

judgment_fn! {
fn prove_normalize_via(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
via: Wc,
goal: Parameter,
) => (Constraints, Parameter) {
debug(goal, via, assumptions, env, decls)
debug(goal, via, assumptions, env)

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

judgment_fn! {
fn prove_syntactically_eq(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
a: Parameter,
b: Parameter,
) => Constraints {
debug(a, b, assumptions, env, decls)
debug(a, b, assumptions, env)

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

Expand Down
4 changes: 2 additions & 2 deletions crates/formality-prove/src/prove/prove_via.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,13 @@ use crate::{

judgment_fn! {
pub fn prove_via(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
via: WcData,
goal: WcData,
) => Constraints {
debug(goal, via, assumptions, env, decls)
debug(goal, via, assumptions, env)

(
(let (skel_c, parameters_c) = pred_1.debone())
Expand Down
4 changes: 2 additions & 2 deletions crates/formality-prove/src/prove/prove_wc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,12 +18,12 @@ use super::constraints::Constraints;

judgment_fn! {
pub fn prove_wc(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
goal: Wc,
) => Constraints {
debug(goal, assumptions, env, decls)
debug(goal, assumptions, env)

(
(let (env, subst) = env.universal_substitution(&binder))
Expand Down
4 changes: 2 additions & 2 deletions crates/formality-prove/src/prove/prove_wc_list.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,12 +10,12 @@ use super::{env::Env, prove_wc::prove_wc};

judgment_fn! {
pub fn prove_wc_list(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
goal: Wcs,
) => Constraints {
debug(goal, assumptions, env, decls)
debug(goal, assumptions, env)

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

Expand Down
4 changes: 2 additions & 2 deletions crates/formality-prove/src/prove/prove_wf.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,12 @@ use super::{constraints::Constraints, env::Env};

judgment_fn! {
pub fn prove_wf(
decls: Decls,
_decls: Decls,
env: Env,
assumptions: Wcs,
goal: Parameter,
) => Constraints {
debug(goal, assumptions, env, decls)
debug(goal, assumptions, env)

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

Expand Down
30 changes: 17 additions & 13 deletions crates/formality-prove/src/test/adt_wf.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,17 +51,21 @@ 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):
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):
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):
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):
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):
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):
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]);
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):
failed at (src/file.rs:LL:CC) because
judgment `prove_wc_list { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` 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 } }` 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 } }` 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: {} }` failed at the following rule(s):
the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
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):
failed at (src/file.rs:LL:CC) because
judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` 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 } }` 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()`"#]]);
}
Loading
Loading