From 3691f7cfb8c149eed2013f5c5deffa7cd70216ae Mon Sep 17 00:00:00 2001 From: Leander Tentrup Date: Wed, 1 Nov 2023 10:45:50 +0100 Subject: [PATCH] Extend well-formedness check of ADTs to include where-clauses (#148) * Extend well-formedness check of ADTs to include where-clauses * Update adt_wf.rs --------- Co-authored-by: Niko Matsakis --- crates/formality-prove/src/decls.rs | 29 ++++++++++++ crates/formality-prove/src/prove/prove_wf.rs | 10 +++- crates/formality-prove/src/test.rs | 1 + crates/formality-prove/src/test/adt_wf.rs | 48 ++++++++++++++++++++ crates/formality-rust/src/prove.rs | 42 +++++++++++++++-- 5 files changed, 124 insertions(+), 6 deletions(-) create mode 100644 crates/formality-prove/src/test/adt_wf.rs diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index a64ba6c8..814e9fa9 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -15,6 +15,7 @@ pub struct Decls { pub neg_impl_decls: Vec, pub alias_eq_decls: Vec, pub alias_bound_decls: Vec, + pub adt_decls: Vec, pub local_trait_ids: Set, pub local_adt_ids: Set, } @@ -70,6 +71,13 @@ impl Decls { &self.alias_bound_decls } + pub fn adt_decl(&self, adt_id: &AdtId) -> &AdtDecl { + let mut v: Vec<_> = self.adt_decls.iter().filter(|t| t.id == *adt_id).collect(); + assert!(!v.is_empty(), "no ADT named `{adt_id:?}`"); + assert!(v.len() <= 1, "multiple ADTs named `{adt_id:?}`"); + v.pop().unwrap() + } + /// Return the set of "trait invariants" for all traits. /// See [`TraitDecl::trait_invariants`]. pub fn trait_invariants(&self) -> Set { @@ -87,6 +95,7 @@ impl Decls { neg_impl_decls: vec![], alias_eq_decls: vec![], alias_bound_decls: vec![], + adt_decls: vec![], local_trait_ids: set![], local_adt_ids: set![], } @@ -257,3 +266,23 @@ pub struct AliasBoundDeclBoundData { pub ensures: Binder, pub where_clause: Wcs, } + +/// An "ADT declaration" declares an ADT name, its generics, and its where-clauses. +/// It doesn't capture the ADT fields, yet. +/// +/// In Rust syntax, it covers the `struct Foo where X: Bar` part of the declaration, but not what appears in the `{...}`. +#[term(adt $id $binder)] +pub struct AdtDecl { + /// The name of the ADT. + pub id: AdtId, + + /// The binder here captures the generics of the ADT. + pub binder: Binder, +} + +/// The "bound data" for a [`AdtDecl`][]. +#[term(where $where_clause)] +pub struct AdtDeclBoundData { + /// The where-clauses declared on the ADT, + pub where_clause: Wcs, +} diff --git a/crates/formality-prove/src/prove/prove_wf.rs b/crates/formality-prove/src/prove/prove_wf.rs index 4b700be7..0ec8c7dd 100644 --- a/crates/formality-prove/src/prove/prove_wf.rs +++ b/crates/formality-prove/src/prove/prove_wf.rs @@ -3,7 +3,10 @@ use formality_types::grammar::{ AliasName, AliasTy, ConstData, Parameter, Parameters, RigidName, RigidTy, UniversalVar, Wcs, }; -use crate::{decls::Decls, prove::combinators::for_all}; +use crate::{ + decls::Decls, + prove::{combinators::for_all, prove_after::prove_after}, +}; use super::{constraints::Constraints, env::Env}; @@ -41,8 +44,11 @@ judgment_fn! { ( (for_all(&decls, &env, &assumptions, ¶meters, &prove_wf) => c) + (let t = decls.adt_decl(&adt_id)) + (let t = t.binder.instantiate_with(¶meters).unwrap()) + (prove_after(&decls, c, &assumptions, t.where_clause) => c) --- ("ADT") - (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::AdtId(_), parameters }) => c) + (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::AdtId(adt_id), parameters }) => c) ) ( diff --git a/crates/formality-prove/src/test.rs b/crates/formality-prove/src/test.rs index 8780005d..f04b7e12 100644 --- a/crates/formality-prove/src/test.rs +++ b/crates/formality-prove/src/test.rs @@ -1,3 +1,4 @@ +mod adt_wf; mod eq_assumptions; mod eq_partial_eq; mod exists_constraints; diff --git a/crates/formality-prove/src/test/adt_wf.rs b/crates/formality-prove/src/test/adt_wf.rs new file mode 100644 index 00000000..d3bf00d9 --- /dev/null +++ b/crates/formality-prove/src/test/adt_wf.rs @@ -0,0 +1,48 @@ +use expect_test::expect; +use formality_core::test; +use formality_types::{ + grammar::{Parameter, Relation, Wcs}, + rust::term, +}; + +use crate::{decls::Decls, prove::prove}; + +fn decls() -> Decls { + Decls { + trait_decls: vec![term("trait Foo where {}")], + impl_decls: vec![term("impl<> Foo(u32) where {}")], + adt_decls: vec![term("adt X where {Foo(T)}")], + ..Decls::empty() + } +} + +#[test] +fn well_formed_adt() { + let assumptions: Wcs = Wcs::t(); + let goal: Parameter = term("X"); + let constraints = prove(decls(), (), assumptions, Relation::WellFormed(goal)); + expect![[r#" + { + Constraints { + env: Env { + variables: [], + coherence_mode: false, + }, + known_true: true, + substitution: {}, + }, + } + "#]] + .assert_debug_eq(&constraints); +} + +#[test] +fn not_well_formed_adt() { + let assumptions: Wcs = Wcs::t(); + let goal: Parameter = term("X"); + let constraints = prove(decls(), (), assumptions, Relation::WellFormed(goal)); + expect![[r#" + {} + "#]] + .assert_debug_eq(&constraints); +} diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index 89a548e7..67e25b48 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -1,8 +1,8 @@ use crate::grammar::{ - AssociatedTy, AssociatedTyBoundData, AssociatedTyValue, AssociatedTyValueBoundData, Crate, - CrateItem, ImplItem, NegTraitImpl, NegTraitImplBoundData, Program, Trait, TraitBoundData, - TraitImpl, TraitImplBoundData, TraitItem, WhereBound, WhereBoundData, WhereClause, - WhereClauseData, + Adt, AdtBoundData, AssociatedTy, AssociatedTyBoundData, AssociatedTyValue, + AssociatedTyValueBoundData, Crate, CrateItem, ImplItem, NegTraitImpl, NegTraitImplBoundData, + Program, Trait, TraitBoundData, TraitImpl, TraitImplBoundData, TraitItem, WhereBound, + WhereBoundData, WhereClause, WhereClauseData, }; use formality_core::{seq, Set, To, Upcast, Upcasted}; use formality_prove as prove; @@ -22,6 +22,7 @@ impl Program { neg_impl_decls: self.neg_impl_decls(), alias_eq_decls: self.alias_eq_decls(), alias_bound_decls: self.alias_bound_decls(), + adt_decls: self.adt_decls(), local_trait_ids: self.local_trait_ids(), local_adt_ids: self.local_adt_ids(), } @@ -56,6 +57,10 @@ impl Program { .collect() } + fn adt_decls(&self) -> Vec { + self.crates.iter().flat_map(|c| c.adt_decls()).collect() + } + fn local_trait_ids(&self) -> Set { self.crates .last() @@ -279,6 +284,35 @@ impl Crate { .collect() } + fn adt_decls(&self) -> Vec { + self.items + .iter() + .flat_map(|item| match item { + CrateItem::Struct(s) => Some(s.to_adt()), + CrateItem::Enum(e) => Some(e.to_adt()), + _ => None, + }) + .map(|Adt { id, binder }| { + let ( + vars, + AdtBoundData { + where_clauses, + variants: _, + }, + ) = binder.open(); + prove::AdtDecl { + id: id.clone(), + binder: Binder::new( + vars, + prove::AdtDeclBoundData { + where_clause: where_clauses.iter().flat_map(|wc| wc.to_wcs()).collect(), + }, + ), + } + }) + .collect() + } + fn adt_ids(&self) -> Set { self.items .iter()