diff --git a/crates/formality-check/src/where_clauses.rs b/crates/formality-check/src/where_clauses.rs index 6844f6e6..9547e450 100644 --- a/crates/formality-check/src/where_clauses.rs +++ b/crates/formality-check/src/where_clauses.rs @@ -1,85 +1,20 @@ use fn_error_context::context; -use formality_core::Upcast; use formality_prove::Env; -use formality_rust::{ - grammar::{WhereClause, WhereClauseData}, - prove::ToWcs, -}; -use formality_types::grammar::{ConstData, Fallible, Parameter, Relation, TraitRef}; +use formality_rust::{grammar::WhereClause, prove::ToWcs}; +use formality_types::grammar::{Fallible, Wcs}; impl super::Check<'_> { + #[context("prove_where_clauses_well_formed({where_clauses:?})")] pub(crate) fn prove_where_clauses_well_formed( &self, env: &Env, assumptions: impl ToWcs, where_clauses: &[WhereClause], ) -> Fallible<()> { - for where_clause in where_clauses { - self.prove_where_clause_well_formed(env, &assumptions, where_clause)?; - } - Ok(()) - } - - #[context("prove_where_clause_well_formed({where_clause:?})")] - // FIXME(oli-obk): figure out why is this a function and not a `judgment_fn`. - fn prove_where_clause_well_formed( - &self, - in_env: &Env, - assumptions: impl ToWcs, - where_clause: &WhereClause, - ) -> Fallible<()> { - match where_clause.data() { - WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => self - .prove_trait_ref_well_formed( - in_env, - assumptions, - trait_id.with(self_ty, parameters), - ), - WhereClauseData::AliasEq(alias_ty, ty) => { - self.prove_parameter_well_formed(in_env, &assumptions, alias_ty)?; - self.prove_parameter_well_formed(in_env, &assumptions, ty) - } - WhereClauseData::Outlives(a, b) => { - self.prove_parameter_well_formed(in_env, &assumptions, a)?; - self.prove_parameter_well_formed(in_env, assumptions, b) - } - WhereClauseData::ForAll(binder) => { - let mut e = in_env.clone(); - let wc = e.instantiate_universally(binder); - self.prove_where_clause_well_formed(&e, assumptions, &wc) - } - WhereClauseData::TypeOfConst(ct, ty) => { - match ct.data() { - ConstData::Value(_, t) => { - self.prove_goal(in_env, &assumptions, Relation::equals(ty, t))? - } - ConstData::Variable(_) => {} - } - // FIXME(oli-obk): prove that there is no `TypeOfConst` bound for a different type. - self.prove_parameter_well_formed(in_env, &assumptions, ct.clone())?; - self.prove_parameter_well_formed(in_env, assumptions, ty.clone()) - } - } - } - - fn prove_parameter_well_formed( - &self, - env: &Env, - assumptions: impl ToWcs, - parameter: impl Upcast, - ) -> Fallible<()> { - let parameter: Parameter = parameter.upcast(); - self.prove_goal(env, assumptions, parameter.well_formed()) - } - - fn prove_trait_ref_well_formed( - &self, - env: &Env, - assumptions: impl ToWcs, - trait_ref: impl Upcast, - ) -> Fallible<()> { - let trait_ref: TraitRef = trait_ref.upcast(); - self.prove_goal(env, assumptions, trait_ref.well_formed())?; - Ok(()) + let wcs: Wcs = where_clauses + .into_iter() + .flat_map(|wc| wc.well_formed().into_iter()) + .collect(); + self.prove_goal(env, assumptions, wcs) } } diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 56928abf..6309b9c2 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -4,8 +4,8 @@ use formality_core::{term, Upcast}; use formality_prove::Safety; use formality_types::{ grammar::{ - AdtId, AliasTy, AssociatedItemId, Binder, Const, CrateId, Fallible, FieldId, FnId, Lt, - Parameter, TraitId, TraitRef, Ty, Wc, + AdtId, AliasTy, AssociatedItemId, Binder, Const, ConstData, CrateId, Fallible, FieldId, + FnId, Lt, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, Wcs, }, rust::Term, }; @@ -351,6 +351,56 @@ impl WhereClause { WhereClauseData::TypeOfConst(_, _) => None, } } + + pub fn well_formed(&self) -> Wcs { + match self.data() { + WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => { + trait_id.with(self_ty, parameters).well_formed().upcast() + } + WhereClauseData::AliasEq(alias_ty, ty) => { + let alias_param: Parameter = alias_ty.upcast(); + let ty_param: Parameter = ty.upcast(); + [ + alias_param.well_formed().upcast(), + ty_param.well_formed().upcast(), + ] + .into_iter() + .collect() + } + WhereClauseData::Outlives(a, b) => { + let a_param: Parameter = a.upcast(); + let b_param: Parameter = b.upcast(); + [ + a_param.well_formed().upcast(), + b_param.well_formed().upcast(), + ] + .into_iter() + .collect() + } + WhereClauseData::ForAll(binder) => { + let (vars, body) = binder.open(); + body.well_formed() + .into_iter() + .map(|wc| Wc::for_all(&vars, wc)) + .collect() + } + WhereClauseData::TypeOfConst(ct, ty) => { + let mut wcs = vec![]; + match ct.data() { + ConstData::Value(_, t) => { + wcs.push(Relation::equals(ty, t)); + } + ConstData::Variable(_) => {} + } + // FIXME(oli-obk): prove that there is no `TypeOfConst` bound for a different type. + let ct_param: Parameter = ct.upcast(); + let ty_param: Parameter = ty.upcast(); + wcs.push(ct_param.well_formed()); + wcs.push(ty_param.well_formed()); + wcs.into_iter().map(|r| r.upcast()).collect() + } + } + } } #[term] diff --git a/src/test/consts.rs b/src/test/consts.rs index f988af36..09703dd1 100644 --- a/src/test/consts.rs +++ b/src/test/consts.rs @@ -17,8 +17,8 @@ fn nonsense_rigid_const_bound() { check_trait(Foo) Caused by: - 0: prove_where_clause_well_formed(type_of_const value(0, bool) is u32) - 1: judgment `prove_wc_list { goal: {u32 = bool}, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + 0: prove_where_clauses_well_formed([type_of_const value(0, bool) is u32]) + 1: judgment `prove_wc_list { goal: {u32 = bool, @ wf(u32), @ wf(const value(0, bool))}, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , 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: u32 = bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because diff --git a/src/test/mod.rs b/src/test/mod.rs index b525f96e..950a8b90 100644 --- a/src/test/mod.rs +++ b/src/test/mod.rs @@ -45,7 +45,7 @@ fn hello_world_fail() { check_trait(Foo) Caused by: - 0: prove_where_clause_well_formed(!ty_2 : Bar ) + 0: prove_where_clauses_well_formed([!ty_2 : Bar ]) 1: judgment `prove_wc_list { goal: {@ WellFormedTraitRef(Bar(!ty_0, !ty_1))}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because judgment `prove_wc { goal: @ WellFormedTraitRef(Bar(!ty_0, !ty_1)), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): @@ -120,16 +120,17 @@ fn basic_where_clauses_fail() { check_trait(WellFormed) Caused by: - 0: prove_where_clause_well_formed(for u32 : A <^ty0_0>) - 1: prove_where_clause_well_formed(u32 : A ) - 2: judgment `prove_wc_list { goal: {@ WellFormedTraitRef(A(u32, !ty_0))}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + 0: prove_where_clauses_well_formed([for u32 : A <^ty0_0>]) + 1: judgment `prove_wc_list { goal: {for @ WellFormedTraitRef(A(u32, ^ty0_0))}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ WellFormedTraitRef(A(u32, !ty_0)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): - the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {B(!ty_0)}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: B(!ty_0), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` 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_wc { goal: for @ WellFormedTraitRef(A(u32, ^ty0_0)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + the rule "forall" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ WellFormedTraitRef(A(u32, !ty_1)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {B(!ty_0)}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: B(!ty_0), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` 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()`"#]] ) }