From d081f2f152f99ecc81d05d8a375ce2d090404866 Mon Sep 17 00:00:00 2001 From: shua Date: Thu, 11 Jul 2024 16:40:23 +0200 Subject: [PATCH] PR: debug 'fn', add some not well-formed tests --- .../src/grammar/ty/debug_impls.rs | 12 ++-- src/test/functions.rs | 64 ++++++++++++++++++- 2 files changed, 69 insertions(+), 7 deletions(-) diff --git a/crates/formality-types/src/grammar/ty/debug_impls.rs b/crates/formality-types/src/grammar/ty/debug_impls.rs index dd4c535e..79846855 100644 --- a/crates/formality-types/src/grammar/ty/debug_impls.rs +++ b/crates/formality-types/src/grammar/ty/debug_impls.rs @@ -34,22 +34,22 @@ impl Debug for RigidTy { } RigidName::FnDef(name) => { let parameters = PrettyParameters::new("<", ">", parameters); - write!(f, "{name:?}{parameters:?}",) + write!(f, "fn {name:?}{parameters:?}",) } RigidName::FnPtr(arity) if parameters.len() == *arity + 1 => { let len = parameters.len(); if *arity != 0 { write!( f, - "{:?}", - PrettyParameters::new("(", ")", ¶meters[..len - 1]) - )?; + "fn{:?} -> {:?}", + PrettyParameters::new("(", ")", ¶meters[..len - 1]), + parameters[len - 1] + ) } else { // PrettyParameters would skip the separators // for 0 arity - write!(f, "()")?; + write!(f, "fn() -> {:?}", parameters[len - 1]) } - write!(f, "-> {:?}", parameters[len - 1]) } _ => { write!(f, "{:?}{:?}", name, PrettyParameters::angle(parameters)) diff --git a/src/test/functions.rs b/src/test/functions.rs index 2ccb156d..edf06b9a 100644 --- a/src/test/functions.rs +++ b/src/test/functions.rs @@ -44,7 +44,7 @@ fn lifetime() { } #[test] -fn wf() { +fn well_formed_function_ptrs() { crate::assert_ok!( [ crate Foo { @@ -56,3 +56,65 @@ fn wf() { expect_test::expect!["()"] ) } + +#[test] +fn not_well_formed_fn_def() { + crate::assert_err!( + [ + crate Foo { + trait Foo {} + fn foo() -> T where T: Foo { trusted } + fn bar(fn foo) -> () { trusted } + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + judgment `prove_wc_list { goal: {@ wf(fn foo)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [], [fn foo ([]) -> ^ty0_0 where {Foo(^ty0_0)}, fn bar ([fn foo]) -> ()], {Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ wf(fn foo), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [], [fn foo ([]) -> ^ty0_0 where {Foo(^ty0_0)}, fn bar ([fn foo]) -> ()], {Foo}, {}) }` 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: fn foo, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [], [fn foo ([]) -> ^ty0_0 where {Foo(^ty0_0)}, fn bar ([fn foo]) -> ()], {Foo}, {}) }` failed at the following rule(s): + the rule "fn-defs" 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(u32)}, assumptions: {}, decls: decls(222, [trait Foo ], [], [], [], [], [], [fn foo ([]) -> ^ty0_0 where {Foo(^ty0_0)}, fn bar ([fn foo]) -> ()], {Foo}, {}) }` 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(u32)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [], [fn foo ([]) -> ^ty0_0 where {Foo(^ty0_0)}, fn bar ([fn foo]) -> ()], {Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Foo(u32), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [], [fn foo ([]) -> ^ty0_0 where {Foo(^ty0_0)}, fn bar ([fn foo]) -> ()], {Foo}, {}) }` 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()`"#]] + ) +} + +#[test] +fn not_well_formed_function_ptr() { + crate::assert_err!( + [ + crate Foo { + trait Foo {} + struct baz where T: Foo {} + fn foo(fn(baz)) -> () { trusted } + } + ] + + [ r#"the rule "fn-ptr" failed"#, ] + + expect_test::expect![[r#" + judgment `prove_wc_list { goal: {@ wf(fn(baz) -> ())}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [adt baz where {Foo(^ty0_0)}], [fn foo ([fn(baz<^ty0_0>) -> ()]) -> ()], {Foo}, {baz}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ wf(fn(baz) -> ()), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [adt baz where {Foo(^ty0_0)}], [fn foo ([fn(baz<^ty0_0>) -> ()]) -> ()], {Foo}, {baz}) }` 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: fn(baz) -> (), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [adt baz where {Foo(^ty0_0)}], [fn foo ([fn(baz<^ty0_0>) -> ()]) -> ()], {Foo}, {baz}) }` failed at the following rule(s): + the rule "fn-ptr" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wf { goal: baz, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [adt baz where {Foo(^ty0_0)}], [fn foo ([fn(baz<^ty0_0>) -> ()]) -> ()], {Foo}, {baz}) }` 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: [!ty_0], bias: Soundness }, known_true: true, substitution: {} }, goal: {Foo(!ty_0)}, assumptions: {}, decls: decls(222, [trait Foo ], [], [], [], [], [adt baz where {Foo(^ty0_0)}], [fn foo ([fn(baz<^ty0_0>) -> ()]) -> ()], {Foo}, {baz}) }` 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(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [adt baz where {Foo(^ty0_0)}], [fn foo ([fn(baz<^ty0_0>) -> ()]) -> ()], {Foo}, {baz}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Foo(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [adt baz where {Foo(^ty0_0)}], [fn foo ([fn(baz<^ty0_0>) -> ()]) -> ()], {Foo}, {baz}) }` 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()`"#]] + ) +}