From 8a0d32c32ffbd6355d646b79317f5764de02cbc0 Mon Sep 17 00:00:00 2001 From: scalexm Date: Wed, 12 Jul 2017 13:34:53 +0200 Subject: [PATCH 1/2] Add implied bounds on structs --- src/lower/mod.rs | 118 +++++++++++++++++++--------------------------- src/solve/test.rs | 64 +++++++++++++++++++++++++ 2 files changed, 113 insertions(+), 69 deletions(-) diff --git a/src/lower/mod.rs b/src/lower/mod.rs index 5049d705668..ea9b9d6eac9 100644 --- a/src/lower/mod.rs +++ b/src/lower/mod.rs @@ -1018,43 +1018,64 @@ impl Anonymize for [ir::ParameterKind] { } } -impl ir::StructDatum { - fn to_program_clauses(&self, program: &ir::Program) -> Vec { - // Given: - // - // struct Foo { } - // - // we generate the following clause: - // - // for WF(Foo) :- WF(?T), (?T: Eq), WF(?T: Eq). +macro_rules! well_formed { + ($self: ident, $value: expr, $constructor: expr, $program: expr) => {{ + let where_clauses = $self.binders.value.where_clauses + .iter() + .cloned() + .flat_map(|wc| wc.expanded($program)); + + let where_clauses: Vec = where_clauses.collect(); let wf = ir::ProgramClause { - implication: self.binders.map_ref(|bound_datum| { + implication: $self.binders.map_ref(|_| { ir::ProgramClauseImplication { - consequence: ir::WellFormed::Ty(bound_datum.self_ty.clone().cast()).cast(), - + consequence: $constructor($value.clone().cast()).cast(), conditions: { - let tys = bound_datum.self_ty - .parameters - .iter() - .filter_map(|pk| pk.as_ref().ty()) - .cloned() - .map(|ty| ir::WellFormed::Ty(ty)) - .casted(); - - let where_clauses = bound_datum.where_clauses.iter() - .cloned() - .flat_map(|wc| wc.expanded(program)) - .casted(); - - tys.chain(where_clauses).collect() + let tys = $value.parameters + .iter() + .filter_map(|pk| pk.as_ref().ty()) + .cloned() + .map(|ty| ir::WellFormed::Ty(ty)) + .casted(); + + tys.chain(where_clauses.iter().cloned().casted()).collect() } } }), fallback_clause: false, }; - vec![wf] + let mut clauses = vec![wf]; + for cond in where_clauses { + clauses.push(ir::ProgramClause { + implication: $self.binders.map_ref(|_| { + ir::ProgramClauseImplication { + consequence: cond, + conditions: vec![$constructor($value.clone().cast()).cast()] + } + }), + fallback_clause: false, + }); + } + + clauses + }}; +} + +impl ir::StructDatum { + fn to_program_clauses(&self, program: &ir::Program) -> Vec { + // Given: + // + // struct Foo { } + // + // we generate the following clause: + // + // for WF(Foo) :- WF(?T), (?T: Eq), WF(?T: Eq). + // for (?T: Eq) :- WF(Foo). + // for WF(?T: Eq) :- WF(Foo). + + well_formed!(self, self.binders.value.self_ty, ir::WellFormed::Ty, program) } } @@ -1076,48 +1097,7 @@ impl ir::TraitDatum { // for (?Self: Eq) :- WF(?Self: Ord) // for WF(?Self: Ord) :- WF(?Self: Ord) - let where_clauses = self.binders.value.where_clauses - .iter() - .cloned() - .flat_map(|wc| wc.expanded(program)) - .collect::>(); - - let wf = ir::WellFormed::TraitRef(self.binders.value.trait_ref.clone()); - - let clauses = ir::ProgramClause { - implication: self.binders.map_ref(|bound| { - ir::ProgramClauseImplication { - consequence: wf.clone().cast(), - - conditions: { - let tys = bound.trait_ref.parameters - .iter() - .filter_map(|pk| pk.as_ref().ty()) - .cloned() - .map(|ty| ir::WellFormed::Ty(ty)) - .casted(); - - tys.chain(where_clauses.iter().cloned().casted()).collect() - } - } - }), - fallback_clause: false, - }; - - let mut clauses = vec![clauses]; - for wc in where_clauses { - clauses.push(ir::ProgramClause { - implication: self.binders.map_ref(|_| { - ir::ProgramClauseImplication { - consequence: wc, - conditions: vec![wf.clone().cast()] - } - }), - fallback_clause: false, - }); - } - - clauses + well_formed!(self, self.binders.value.trait_ref, ir::WellFormed::TraitRef, program) } } diff --git a/src/solve/test.rs b/src/solve/test.rs index 19132b001db..a3005be3ef3 100644 --- a/src/solve/test.rs +++ b/src/solve/test.rs @@ -1596,3 +1596,67 @@ fn mixed_semantics() { } } } + +#[test] +fn implied_bounds() { + test! { + program { + trait Hash { } + struct Set where K: Hash { } + + struct NotHash { } + + struct i32 { } + impl Hash for i32 { } + + trait Eq { } + trait Ord where Self: Eq { } + + struct Ordered where U: Ord { } + } + + // We know that `Set` is well-formed so `K` must implement `Hash`. + goal { + forall { + if (WellFormed(Set)) { + K: Hash + } + } + } yields { + "Unique" + } + + // The following function: + // ``` + // fn foo(arg: Set>) { + // /* assume that WellFormed(Set>) inside here */ + // } + // ``` + // cannot be called whatever the value of `T` is because + // there is no `Hash` impl for `NotHash` hence `Set>` + // cannot be well-formed. + // + // Since both `Hash` and `NotHash` are local types, a local negative + // reasoning is allowed and the following query fails (it should be run in + // `compat` mode). We can then issue a warning saying that the function cannot be + // called. + goal { + exists { + WellFormed(Set>) + } + } yields { + "No possible solution" + } + + // Transitive implied bounds + goal { + forall { + if (WellFormed(Ordered)) { + U: Eq + } + } + } yields { + "Unique" + } + } +} From 873d0fe79554a2c292bd8f2b7974ea2a5ba75391 Mon Sep 17 00:00:00 2001 From: scalexm Date: Mon, 17 Jul 2017 14:04:35 +0200 Subject: [PATCH 2/2] Remove WF checks for parameters --- src/lower/mod.rs | 71 +++++++++++++++++++++++++++++++---------------- src/solve/test.rs | 47 ++++++++++++++++++------------- 2 files changed, 75 insertions(+), 43 deletions(-) diff --git a/src/lower/mod.rs b/src/lower/mod.rs index ea9b9d6eac9..13254f3c1cc 100644 --- a/src/lower/mod.rs +++ b/src/lower/mod.rs @@ -1018,29 +1018,46 @@ impl Anonymize for [ir::ParameterKind] { } } -macro_rules! well_formed { - ($self: ident, $value: expr, $constructor: expr, $program: expr) => {{ - let where_clauses = $self.binders.value.where_clauses - .iter() - .cloned() - .flat_map(|wc| wc.expanded($program)); +trait ExpandWhereClauses { + fn expanded_where_clauses(&self, program: &ir::Program) -> Vec; +} - let where_clauses: Vec = where_clauses.collect(); +impl ExpandWhereClauses for ir::StructDatumBound { + fn expanded_where_clauses(&self, program: &ir::Program) -> Vec { + self.where_clauses + .iter() + .cloned() + .flat_map(|wc| wc.expanded(program)) + .collect() + } +} + +impl ExpandWhereClauses for ir::TraitDatumBound { + fn expanded_where_clauses(&self, program: &ir::Program) -> Vec { + self.where_clauses + .iter() + .cloned() + .flat_map(|wc| wc.expanded(program)) + .collect() + } +} + +trait WellFormed { + fn wf_clauses(&self, wf_predicate: ir::WellFormed, program: &ir::Program) + -> Vec; +} + +impl WellFormed for ir::Binders { + fn wf_clauses(&self, wf_predicate: ir::WellFormed, program: &ir::Program) + -> Vec + { + let where_clauses = self.value.expanded_where_clauses(program); let wf = ir::ProgramClause { - implication: $self.binders.map_ref(|_| { + implication: self.map_ref(|_| { ir::ProgramClauseImplication { - consequence: $constructor($value.clone().cast()).cast(), - conditions: { - let tys = $value.parameters - .iter() - .filter_map(|pk| pk.as_ref().ty()) - .cloned() - .map(|ty| ir::WellFormed::Ty(ty)) - .casted(); - - tys.chain(where_clauses.iter().cloned().casted()).collect() - } + consequence: wf_predicate.clone().cast(), + conditions: where_clauses.iter().cloned().casted().collect(), } }), fallback_clause: false, @@ -1049,10 +1066,10 @@ macro_rules! well_formed { let mut clauses = vec![wf]; for cond in where_clauses { clauses.push(ir::ProgramClause { - implication: $self.binders.map_ref(|_| { + implication: self.map_ref(|_| { ir::ProgramClauseImplication { consequence: cond, - conditions: vec![$constructor($value.clone().cast()).cast()] + conditions: vec![wf_predicate.clone().cast()] } }), fallback_clause: false, @@ -1060,7 +1077,7 @@ macro_rules! well_formed { } clauses - }}; + } } impl ir::StructDatum { @@ -1075,7 +1092,10 @@ impl ir::StructDatum { // for (?T: Eq) :- WF(Foo). // for WF(?T: Eq) :- WF(Foo). - well_formed!(self, self.binders.value.self_ty, ir::WellFormed::Ty, program) + self.binders.wf_clauses( + ir::WellFormed::Ty(self.binders.value.self_ty.clone().cast()), + program + ) } } @@ -1097,7 +1117,10 @@ impl ir::TraitDatum { // for (?Self: Eq) :- WF(?Self: Ord) // for WF(?Self: Ord) :- WF(?Self: Ord) - well_formed!(self, self.binders.value.trait_ref, ir::WellFormed::TraitRef, program) + self.binders.wf_clauses( + ir::WellFormed::TraitRef(self.binders.value.trait_ref.clone().cast()), + program + ) } } diff --git a/src/solve/test.rs b/src/solve/test.rs index a3005be3ef3..308e7fee429 100644 --- a/src/solve/test.rs +++ b/src/solve/test.rs @@ -131,10 +131,11 @@ fn prove_forall() { trait Marker { } impl Marker for Vec { } - trait Clone { } - impl Clone for Foo { } + trait Eq { } + trait Ord where Self: Eq { } - impl Clone for Vec where T: Clone { } + impl Eq> for Vec where T: Eq { } + impl Ord> for Vec where T: Ord { } } goal { @@ -164,19 +165,19 @@ fn prove_forall() { "Unique; substitution [], lifetime constraints []" } - // Here, we don't know that `T: Clone`, so we can't prove that - // `Vec: Clone`. + // Here, we don't know that `T: Eq`, so we can't prove that + // `Vec: Eq>`. goal { - forall { Vec: Clone } + forall { Vec: Eq> } } yields { - "CannotProve" + "No possible solution" } - // Here, we do know that `T: Clone`, so we can. + // Here, we do know that `T: Eq`, so we can. goal { forall { - if (T: Clone) { - Vec: Clone + if (T: Eq) { + Vec: Eq> } } } yields { @@ -184,16 +185,26 @@ fn prove_forall() { } // This fails because we used `if_raw`, and hence we do not - // know that `WF(T: Clone)` holds. + // know that `WF(T: Ord)` hence `T: Eq` holds. goal { forall { - if_raw (T: Clone) { - Vec: Clone + if_raw (T: Ord) { + Vec: Ord> } } } yields { "CannotProve" } + + goal { + forall { + if (T: Ord) { + Vec: Ord> + } + } + } yields { + "Unique" + } } } @@ -1539,10 +1550,9 @@ fn coinductive_semantics() { "CannotProve" } - // `WellFormed(T)` because of the hand-written impl for `Ptr`. goal { forall { - if (WellFormed(T), T: Send) { + if (T: Send) { List: Send } } @@ -1636,10 +1646,9 @@ fn implied_bounds() { // there is no `Hash` impl for `NotHash` hence `Set>` // cannot be well-formed. // - // Since both `Hash` and `NotHash` are local types, a local negative - // reasoning is allowed and the following query fails (it should be run in - // `compat` mode). We can then issue a warning saying that the function cannot be - // called. + // Since `NotHash` is a local type, a local negative + // reasoning is allowed and the following query fails. We can then issue + // a warning saying that the function cannot be called. goal { exists { WellFormed(Set>)