From f183c891f4dd3fa566c79634aadef68806a7310b Mon Sep 17 00:00:00 2001 From: shua Date: Sat, 22 Jun 2024 17:14:22 +0200 Subject: [PATCH 1/4] track adt variant and field names do not conflict The intent of this change is to add a check for adts that enum variant names are unique, and that struct and enum field names are unique (within a given enum variant). --- crates/formality-check/src/adts.rs | 18 +++++++++++---- src/test/mod.rs | 36 ++++++++++++++++++++++++++++++ 2 files changed, 50 insertions(+), 4 deletions(-) diff --git a/crates/formality-check/src/adts.rs b/crates/formality-check/src/adts.rs index dde84ab1..de3210eb 100644 --- a/crates/formality-check/src/adts.rs +++ b/crates/formality-check/src/adts.rs @@ -1,3 +1,6 @@ +use std::collections::HashSet; + +use anyhow::bail; use formality_prove::Env; use formality_rust::grammar::{Adt, AdtBoundData, Field, Variant}; use formality_types::grammar::Fallible; @@ -15,10 +18,17 @@ impl super::Check<'_> { self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?; - // FIXME: check names are unique or integers from 0..n - - for Variant { name: _, fields } in &variants { - for Field { name: _, ty } in fields { + // names is used to check that there are no name conflicts + let mut names = HashSet::new(); + for Variant { name, fields } in &variants { + if !names.insert((name, None)) { + bail!("variant \"{name:?}\" defined multiple times"); + } + let vname = name; + for Field { name, ty } in fields { + if !names.insert((vname, Some(name))) { + bail!("field \"{name:?}\" of variant \"{vname:?}\" defined multiple times"); + } self.prove_goal(&env, &where_clauses, ty.well_formed())?; } } diff --git a/src/test/mod.rs b/src/test/mod.rs index d926aae3..e6c48666 100644 --- a/src/test/mod.rs +++ b/src/test/mod.rs @@ -133,3 +133,39 @@ fn basic_where_clauses_fail() { expression evaluated to an empty collection: `decls.trait_invariants()`"#]] ) } + +#[test] +fn basic_adt_variant_dup() { + crate::assert_err!( + [ + crate Foo { + enum Bar { + Baz{}, + Baz{}, + } + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#"variant "Baz" defined multiple times"#]] + ) +} + +#[test] +fn basic_adt_field_dup() { + crate::assert_err!( + [ + crate Foo { + struct Bar { + baz: (), + baz: (), + } + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#"field "baz" of variant "struct" defined multiple times"#]] + ) +} From 87873d957d19f004d020990d3e76df8598fa72b6 Mon Sep 17 00:00:00 2001 From: shua Date: Tue, 25 Jun 2024 16:56:05 +0200 Subject: [PATCH 2/4] check fields before trait solving --- crates/formality-check/src/adts.rs | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/crates/formality-check/src/adts.rs b/crates/formality-check/src/adts.rs index de3210eb..eb99b82b 100644 --- a/crates/formality-check/src/adts.rs +++ b/crates/formality-check/src/adts.rs @@ -9,26 +9,31 @@ impl super::Check<'_> { pub(super) fn check_adt(&self, adt: &Adt) -> Fallible<()> { let Adt { id: _, binder } = adt; - let mut env = Env::default(); - - let AdtBoundData { - where_clauses, - variants, - } = env.instantiate_universally(binder); - - self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?; - // names is used to check that there are no name conflicts let mut names = HashSet::new(); - for Variant { name, fields } in &variants { + for Variant { name, fields } in &adt.binder.open().1.variants { if !names.insert((name, None)) { bail!("variant \"{name:?}\" defined multiple times"); } let vname = name; - for Field { name, ty } in fields { + for Field { name, ty: _ } in fields { if !names.insert((vname, Some(name))) { bail!("field \"{name:?}\" of variant \"{vname:?}\" defined multiple times"); } + } + } + + let mut env = Env::default(); + + let AdtBoundData { + where_clauses, + variants, + } = env.instantiate_universally(binder); + + self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?; + + for Variant { name: _, fields } in &variants { + for Field { name: _, ty } in fields { self.prove_goal(&env, &where_clauses, ty.well_formed())?; } } From 8b5e7a2936231a847afdc1d6b339b4383daeff99 Mon Sep 17 00:00:00 2001 From: shua Date: Mon, 1 Jul 2024 18:01:35 +0200 Subject: [PATCH 3/4] PR: s/open()/peek()/ --- crates/formality-check/src/adts.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/formality-check/src/adts.rs b/crates/formality-check/src/adts.rs index eb99b82b..dcf8df85 100644 --- a/crates/formality-check/src/adts.rs +++ b/crates/formality-check/src/adts.rs @@ -11,7 +11,7 @@ impl super::Check<'_> { // names is used to check that there are no name conflicts let mut names = HashSet::new(); - for Variant { name, fields } in &adt.binder.open().1.variants { + for Variant { name, fields } in &adt.binder.peek().variants { if !names.insert((name, None)) { bail!("variant \"{name:?}\" defined multiple times"); } From 61cf9b5d38b76637cd0dd85ab4bfbb61a9993dda Mon Sep 17 00:00:00 2001 From: shua Date: Mon, 1 Jul 2024 19:29:23 +0200 Subject: [PATCH 4/4] PR: add test description text --- src/test/mod.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/test/mod.rs b/src/test/mod.rs index 20921acd..0e5b3870 100644 --- a/src/test/mod.rs +++ b/src/test/mod.rs @@ -147,7 +147,7 @@ fn basic_adt_variant_dup() { } ] - [ /* TODO */ ] + [ r#"variant "Baz" defined multiple times"#, ] expect_test::expect![[r#"variant "Baz" defined multiple times"#]] ) @@ -165,12 +165,13 @@ fn basic_adt_field_dup() { } ] - [ /* TODO */ ] + [ r#"field "baz" of variant "struct" defined multiple times"#, ] expect_test::expect![[r#"field "baz" of variant "struct" defined multiple times"#]] ) } +#[test] fn trait_items_with_duplicate_fn_names() { crate::assert_err!( [