Skip to content

Commit 3d95004

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #177 from shua/wcwf
replace custom wf check with well_formed constructor
2 parents 3523b85 + 675a22f commit 3d95004

File tree

4 files changed

+74
-88
lines changed

4 files changed

+74
-88
lines changed

‎crates/formality-check/src/where_clauses.rs

Lines changed: 8 additions & 73 deletions
Original file line numberDiff line numberDiff line change
@@ -1,85 +1,20 @@
11
use fn_error_context::context;
2-
use formality_core::Upcast;
32
use formality_prove::Env;
4-
use formality_rust::{
5-
grammar::{WhereClause, WhereClauseData},
6-
prove::ToWcs,
7-
};
8-
use formality_types::grammar::{ConstData, Fallible, Parameter, Relation, TraitRef};
3+
use formality_rust::{grammar::WhereClause, prove::ToWcs};
4+
use formality_types::grammar::{Fallible, Wcs};
95

106
impl super::Check<'_> {
7+
#[context("prove_where_clauses_well_formed({where_clauses:?})")]
118
pub(crate) fn prove_where_clauses_well_formed(
129
&self,
1310
env: &Env,
1411
assumptions: impl ToWcs,
1512
where_clauses: &[WhereClause],
1613
) -> Fallible<()> {
17-
for where_clause in where_clauses {
18-
self.prove_where_clause_well_formed(env, &assumptions, where_clause)?;
19-
}
20-
Ok(())
21-
}
22-
23-
#[context("prove_where_clause_well_formed({where_clause:?})")]
24-
// FIXME(oli-obk): figure out why is this a function and not a `judgment_fn`.
25-
fn prove_where_clause_well_formed(
26-
&self,
27-
in_env: &Env,
28-
assumptions: impl ToWcs,
29-
where_clause: &WhereClause,
30-
) -> Fallible<()> {
31-
match where_clause.data() {
32-
WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => self
33-
.prove_trait_ref_well_formed(
34-
in_env,
35-
assumptions,
36-
trait_id.with(self_ty, parameters),
37-
),
38-
WhereClauseData::AliasEq(alias_ty, ty) => {
39-
self.prove_parameter_well_formed(in_env, &assumptions, alias_ty)?;
40-
self.prove_parameter_well_formed(in_env, &assumptions, ty)
41-
}
42-
WhereClauseData::Outlives(a, b) => {
43-
self.prove_parameter_well_formed(in_env, &assumptions, a)?;
44-
self.prove_parameter_well_formed(in_env, assumptions, b)
45-
}
46-
WhereClauseData::ForAll(binder) => {
47-
let mut e = in_env.clone();
48-
let wc = e.instantiate_universally(binder);
49-
self.prove_where_clause_well_formed(&e, assumptions, &wc)
50-
}
51-
WhereClauseData::TypeOfConst(ct, ty) => {
52-
match ct.data() {
53-
ConstData::Value(_, t) => {
54-
self.prove_goal(in_env, &assumptions, Relation::equals(ty, t))?
55-
}
56-
ConstData::Variable(_) => {}
57-
}
58-
// FIXME(oli-obk): prove that there is no `TypeOfConst` bound for a different type.
59-
self.prove_parameter_well_formed(in_env, &assumptions, ct.clone())?;
60-
self.prove_parameter_well_formed(in_env, assumptions, ty.clone())
61-
}
62-
}
63-
}
64-
65-
fn prove_parameter_well_formed(
66-
&self,
67-
env: &Env,
68-
assumptions: impl ToWcs,
69-
parameter: impl Upcast<Parameter>,
70-
) -> Fallible<()> {
71-
let parameter: Parameter = parameter.upcast();
72-
self.prove_goal(env, assumptions, parameter.well_formed())
73-
}
74-
75-
fn prove_trait_ref_well_formed(
76-
&self,
77-
env: &Env,
78-
assumptions: impl ToWcs,
79-
trait_ref: impl Upcast<TraitRef>,
80-
) -> Fallible<()> {
81-
let trait_ref: TraitRef = trait_ref.upcast();
82-
self.prove_goal(env, assumptions, trait_ref.well_formed())?;
83-
Ok(())
14+
let wcs: Wcs = where_clauses
15+
.into_iter()
16+
.flat_map(|wc| wc.well_formed().into_iter())
17+
.collect();
18+
self.prove_goal(env, assumptions, wcs)
8419
}
8520
}

‎crates/formality-rust/src/grammar.rs

Lines changed: 52 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ use formality_core::{term, Upcast};
44
use formality_prove::Safety;
55
use formality_types::{
66
grammar::{
7-
AdtId, AliasTy, AssociatedItemId, Binder, Const, CrateId, Fallible, FieldId, FnId, Lt,
8-
Parameter, TraitId, TraitRef, Ty, Wc,
7+
AdtId, AliasTy, AssociatedItemId, Binder, Const, ConstData, CrateId, Fallible, FieldId,
8+
FnId, Lt, Parameter, Relation, TraitId, TraitRef, Ty, Wc, Wcs,
99
},
1010
rust::Term,
1111
};
@@ -351,6 +351,56 @@ impl WhereClause {
351351
WhereClauseData::TypeOfConst(_, _) => None,
352352
}
353353
}
354+
355+
pub fn well_formed(&self) -> Wcs {
356+
match self.data() {
357+
WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => {
358+
trait_id.with(self_ty, parameters).well_formed().upcast()
359+
}
360+
WhereClauseData::AliasEq(alias_ty, ty) => {
361+
let alias_param: Parameter = alias_ty.upcast();
362+
let ty_param: Parameter = ty.upcast();
363+
[
364+
alias_param.well_formed().upcast(),
365+
ty_param.well_formed().upcast(),
366+
]
367+
.into_iter()
368+
.collect()
369+
}
370+
WhereClauseData::Outlives(a, b) => {
371+
let a_param: Parameter = a.upcast();
372+
let b_param: Parameter = b.upcast();
373+
[
374+
a_param.well_formed().upcast(),
375+
b_param.well_formed().upcast(),
376+
]
377+
.into_iter()
378+
.collect()
379+
}
380+
WhereClauseData::ForAll(binder) => {
381+
let (vars, body) = binder.open();
382+
body.well_formed()
383+
.into_iter()
384+
.map(|wc| Wc::for_all(&vars, wc))
385+
.collect()
386+
}
387+
WhereClauseData::TypeOfConst(ct, ty) => {
388+
let mut wcs = vec![];
389+
match ct.data() {
390+
ConstData::Value(_, t) => {
391+
wcs.push(Relation::equals(ty, t));
392+
}
393+
ConstData::Variable(_) => {}
394+
}
395+
// FIXME(oli-obk): prove that there is no `TypeOfConst` bound for a different type.
396+
let ct_param: Parameter = ct.upcast();
397+
let ty_param: Parameter = ty.upcast();
398+
wcs.push(ct_param.well_formed());
399+
wcs.push(ty_param.well_formed());
400+
wcs.into_iter().map(|r| r.upcast()).collect()
401+
}
402+
}
403+
}
354404
}
355405

356406
#[term]

‎src/test/consts.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ fn nonsense_rigid_const_bound() {
1717
check_trait(Foo)
1818
1919
Caused by:
20-
0: prove_where_clause_well_formed(type_of_const value(0, bool) is u32)
21-
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):
20+
0: prove_where_clauses_well_formed([type_of_const value(0, bool) is u32])
21+
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):
2222
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
2323
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):
2424
the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because

‎src/test/mod.rs

Lines changed: 12 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ fn hello_world_fail() {
4545
check_trait(Foo)
4646
4747
Caused by:
48-
0: prove_where_clause_well_formed(!ty_2 : Bar <!ty_1>)
48+
0: prove_where_clauses_well_formed([!ty_2 : Bar <!ty_1>])
4949
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):
5050
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
5151
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):
@@ -120,16 +120,17 @@ fn basic_where_clauses_fail() {
120120
check_trait(WellFormed)
121121
122122
Caused by:
123-
0: prove_where_clause_well_formed(for <ty> u32 : A <^ty0_0>)
124-
1: prove_where_clause_well_formed(u32 : A <!ty_2>)
125-
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):
123+
0: prove_where_clauses_well_formed([for <ty> u32 : A <^ty0_0>])
124+
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):
126125
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
127-
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):
128-
the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because
129-
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):
130-
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
131-
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):
132-
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
133-
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]
126+
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):
127+
the rule "forall" failed at step #2 (src/file.rs:LL:CC) because
128+
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):
129+
the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because
130+
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):
131+
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
132+
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):
133+
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
134+
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]
134135
)
135136
}

0 commit comments

Comments
 (0)