Skip to content

Commit

Permalink
PR: debug 'fn', add some not well-formed tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@shua
shua committed Jul 11, 2024
1 parent 68b412a commit d081f2f
Show file tree
Hide file tree
Showing 2 changed files with 69 additions and 7 deletions.
12 changes: 6 additions & 6 deletions crates/formality-types/src/grammar/ty/debug_impls.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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("(", ")", &parameters[..len - 1])
)?;
"fn{:?} -> {:?}",
PrettyParameters::new("(", ")", &parameters[..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))
Expand Down
64 changes: 63 additions & 1 deletion src/test/functions.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ fn lifetime() {
}

#[test]
fn wf() {
fn well_formed_function_ptrs() {
crate::assert_ok!(
[
crate Foo {
Expand All @@ -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<ty T>() -> T where T: Foo { trusted }
fn bar(fn foo<u32>) -> () { trusted }
}
]

[ /* TODO */ ]

expect_test::expect![[r#"
judgment `prove_wc_list { goal: {@ wf(fn foo<u32>)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [], [], [], [], [], [fn foo <ty> ([]) -> ^ty0_0 where {Foo(^ty0_0)}, fn bar ([fn foo<u32>]) -> ()], {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<u32>), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [], [], [], [], [], [fn foo <ty> ([]) -> ^ty0_0 where {Foo(^ty0_0)}, fn bar ([fn foo<u32>]) -> ()], {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<u32>, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [], [], [], [], [], [fn foo <ty> ([]) -> ^ty0_0 where {Foo(^ty0_0)}, fn bar ([fn foo<u32>]) -> ()], {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 <ty> ], [], [], [], [], [], [fn foo <ty> ([]) -> ^ty0_0 where {Foo(^ty0_0)}, fn bar ([fn foo<u32>]) -> ()], {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 <ty> ], [], [], [], [], [], [fn foo <ty> ([]) -> ^ty0_0 where {Foo(^ty0_0)}, fn bar ([fn foo<u32>]) -> ()], {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 <ty> ], [], [], [], [], [], [fn foo <ty> ([]) -> ^ty0_0 where {Foo(^ty0_0)}, fn bar ([fn foo<u32>]) -> ()], {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<ty T> where T: Foo {}
fn foo<ty T>(fn(baz<T>)) -> () { trusted }
}
]

[ r#"the rule "fn-ptr" failed"#, ]

expect_test::expect![[r#"
judgment `prove_wc_list { goal: {@ wf(fn(baz<!ty_0>) -> ())}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [], [], [], [], [adt baz <ty> where {Foo(^ty0_0)}], [fn foo <ty> ([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<!ty_0>) -> ()), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [], [], [], [], [adt baz <ty> where {Foo(^ty0_0)}], [fn foo <ty> ([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<!ty_0>) -> (), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [], [], [], [], [adt baz <ty> where {Foo(^ty0_0)}], [fn foo <ty> ([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<!ty_0>, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [], [], [], [], [adt baz <ty> where {Foo(^ty0_0)}], [fn foo <ty> ([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 <ty> ], [], [], [], [], [adt baz <ty> where {Foo(^ty0_0)}], [fn foo <ty> ([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 <ty> ], [], [], [], [], [adt baz <ty> where {Foo(^ty0_0)}], [fn foo <ty> ([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 <ty> ], [], [], [], [], [adt baz <ty> where {Foo(^ty0_0)}], [fn foo <ty> ([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()`"#]]
)
}

0 comments on commit d081f2f

Please sign in to comment.