Skip to content

Commit

Permalink
deduplicate where-clause well formed checks
Browse files Browse the repository at this point in the history
The intent of this change is to deduplicate some logic around where clause
well-formed checks. To that end, the existing check was removed and replaced
with a well_formed method on WhereClause, which returns a set of predicates
to be checked with a standard 'prove' call.
  • Loading branch information
shua committed Jun 30, 2024
1 parent 915661b commit 0d1cdff
Show file tree
Hide file tree
Showing 4 changed files with 74 additions and 88 deletions.
81 changes: 8 additions & 73 deletions crates/formality-check/src/where_clauses.rs
Original file line number Diff line number Diff line change
@@ -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<Parameter>,
) -> 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<TraitRef>,
) -> 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)
}
}
54 changes: 52 additions & 2 deletions crates/formality-rust/src/grammar.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,

Check warning on line 8 in crates/formality-rust/src/grammar.rs

View workflow job for this annotation

GitHub Actions / rust-test (macos-latest)

unused import: `Predicate`

Check warning on line 8 in crates/formality-rust/src/grammar.rs

View workflow job for this annotation

GitHub Actions / rust-test (ubuntu-latest)

unused import: `Predicate`

Check warning on line 8 in crates/formality-rust/src/grammar.rs

View workflow job for this annotation

GitHub Actions / rust-test (windows-latest)

unused import: `Predicate`
},
rust::Term,
};
Expand Down Expand Up @@ -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]
Expand Down
4 changes: 2 additions & 2 deletions src/test/consts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 <ty> 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 <ty> 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 <ty> 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
Expand Down
23 changes: 12 additions & 11 deletions src/test/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ fn hello_world_fail() {
check_trait(Foo)
Caused by:
0: prove_where_clause_well_formed(!ty_2 : Bar <!ty_1>)
0: prove_where_clauses_well_formed([!ty_2 : Bar <!ty_1>])
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 <ty, ty> where {Bar(^ty0_1, ^ty0_0)}, trait Bar <ty, ty> where {Baz(^ty0_1)}, trait Baz <ty> ], [], [], [], [], [], {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 <ty, ty> where {Bar(^ty0_1, ^ty0_0)}, trait Bar <ty, ty> where {Baz(^ty0_1)}, trait Baz <ty> ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s):
Expand Down Expand Up @@ -120,16 +120,17 @@ fn basic_where_clauses_fail() {
check_trait(WellFormed)
Caused by:
0: prove_where_clause_well_formed(for <ty> u32 : A <^ty0_0>)
1: prove_where_clause_well_formed(u32 : A <!ty_2>)
2: judgment `prove_wc_list { goal: {@ WellFormedTraitRef(A(u32, !ty_0))}, assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s):
0: prove_where_clauses_well_formed([for <ty> u32 : A <^ty0_0>])
1: judgment `prove_wc_list { goal: {for <ty> @ WellFormedTraitRef(A(u32, ^ty0_0))}, assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> 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 <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> 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 <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> 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 <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> 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 <ty> @ WellFormedTraitRef(A(u32, ^ty0_0)), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> 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 <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> 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 <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> 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 <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> 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()`"#]]
)
}

0 comments on commit 0d1cdff

Please sign in to comment.