From 869ff06c724c36c24f9d1d4808880b376672f5d4 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Sun, 6 May 2018 23:41:19 -0500 Subject: [PATCH 1/3] Refactor LowerWhereClause for multiple domain goals --- src/ir/lowering/mod.rs | 55 ++++++++++++++++++++++++++++-------------- src/ir/mod.rs | 23 ++++++++++++++++++ 2 files changed, 60 insertions(+), 18 deletions(-) diff --git a/src/ir/lowering/mod.rs b/src/ir/lowering/mod.rs index 395c8cca4ba..be346d05b8d 100644 --- a/src/ir/lowering/mod.rs +++ b/src/ir/lowering/mod.rs @@ -412,26 +412,36 @@ trait LowerWhereClauseVec { impl LowerWhereClauseVec for [WhereClause] { fn lower(&self, env: &Env) -> Result> { - self.iter().map(|wc| wc.lower(env)).collect() + self.iter() + .flat_map(|wc| match wc.lower(env) { + Ok(v) => v.into_iter().map(Ok).collect(), + Err(e) => vec![Err(e)], + }) + .collect() } } impl LowerWhereClauseVec for [QuantifiedWhereClause] { fn lower(&self, env: &Env) -> Result> { - self.iter().map(|wc| wc.lower(env)).collect() + self.iter() + .flat_map(|wc| match wc.lower(env) { + Ok(v) => v.into_iter().map(Ok).collect(), + Err(e) => vec![Err(e)], + }) + .collect() } } trait LowerWhereClause { - fn lower(&self, env: &Env) -> Result; + fn lower(&self, env: &Env) -> Result>; } /// Lowers a where-clause in the context of a clause (i.e. in "negative" /// position); this is limited to the kinds of where-clauses users can actually /// type in Rust and well-formedness checks. impl LowerWhereClause for WhereClause { - fn lower(&self, env: &Env) -> Result { - Ok(match self { + fn lower(&self, env: &Env) -> Result> { + let goal = match self { WhereClause::Implemented { trait_ref } => { ir::DomainGoal::Holds(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?)) } @@ -478,17 +488,18 @@ impl LowerWhereClause for WhereClause { target: target.lower(env)? }) } - }) + }; + Ok(vec![goal]) } } impl LowerWhereClause for QuantifiedWhereClause { - fn lower(&self, env: &Env) -> Result { + fn lower(&self, env: &Env) -> Result> { let parameter_kinds = self.parameter_kinds.iter().map(|pk| pk.lower()); let binders = env.in_binders(parameter_kinds, |env| { Ok(self.where_clause.lower(env)?) })?; - Ok(binders) + Ok(binders.into_iter().collect()) } } @@ -497,7 +508,7 @@ impl LowerWhereClause for QuantifiedWhereClause { /// can appear, because it includes all the sorts of things that the compiler /// must verify. impl LowerWhereClause for WhereClause { - fn lower(&self, env: &Env) -> Result { + fn lower(&self, env: &Env) -> Result> { Ok(match *self { WhereClause::Implemented { .. } | WhereClause::ProjectionEq { .. } @@ -507,17 +518,17 @@ impl LowerWhereClause for WhereClause { | WhereClause::TyFromEnv { .. } | WhereClause::TraitRefFromEnv { .. } | WhereClause::Derefs { .. } => { - let g: ir::DomainGoal = self.lower(env)?; - g.cast() + let goals: Vec = self.lower(env)?; + goals.into_iter().map(|g| g.cast()).collect() } - WhereClause::UnifyTys { ref a, ref b } => ir::EqGoal { + WhereClause::UnifyTys { ref a, ref b } => vec![ir::EqGoal { a: ir::ParameterKind::Ty(a.lower(env)?), b: ir::ParameterKind::Ty(b.lower(env)?), - }.cast(), - WhereClause::UnifyLifetimes { ref a, ref b } => ir::EqGoal { + }.cast()], + WhereClause::UnifyLifetimes { ref a, ref b } => vec![ir::EqGoal { a: ir::ParameterKind::Lifetime(a.lower(env)?), b: ir::ParameterKind::Lifetime(b.lower(env)?), - }.cast(), + }.cast()], WhereClause::TraitInScope { trait_name } => { let id = match env.lookup(trait_name)? { NameLookup::Type(id) => id, @@ -528,7 +539,7 @@ impl LowerWhereClause for WhereClause { bail!(ErrorKind::NotTrait(trait_name)); } - ir::DomainGoal::InScope(id).cast() + vec![ir::DomainGoal::InScope(id).cast()] } }) } @@ -837,7 +848,10 @@ trait LowerClause { impl LowerClause for Clause { fn lower_clause(&self, env: &Env) -> Result { let implication = env.in_binders(self.all_parameters(), |env| { - let consequence: ir::DomainGoal = self.consequence.lower(env)?; + let consequences: Vec = self.consequence.lower(env)?; + assert_eq!(1, consequences.len()); + let consequence = consequences.into_iter().next().unwrap(); + let mut conditions: Vec = self.conditions .iter() .map(|g| g.lower(env).map(|g| *g)) @@ -976,7 +990,12 @@ impl<'k> LowerGoal> for Goal { Ok(Box::new(ir::Goal::And(g1.lower(env)?, g2.lower(env)?))) } Goal::Not(g) => Ok(Box::new(ir::Goal::Not(g.lower(env)?))), - Goal::Leaf(wc) => Ok(Box::new(ir::Goal::Leaf(wc.lower(env)?))), + Goal::Leaf(wc) => { + let leaf = wc.lower(env)?; + assert_eq!(1, leaf.len()); + let leaf = leaf.into_iter().next().unwrap(); + Ok(Box::new(ir::Goal::Leaf(leaf))) + } } } } diff --git a/src/ir/mod.rs b/src/ir/mod.rs index 66844c61b9f..bd7c8d4da9f 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -687,6 +687,29 @@ impl Binders { } } +/// Allows iterating over a Binders>, for instance. +/// Each element will include the same set of parameter bounds. +impl IntoIterator for Binders { + type Item = Binders<::Item>; + type IntoIter = BindersIntoIterator; + + fn into_iter(self) -> Self::IntoIter { + BindersIntoIterator { iter: self.value.into_iter(), binders: self.binders } + } +} + +pub struct BindersIntoIterator { + iter: ::IntoIter, + binders: Vec>, +} + +impl Iterator for BindersIntoIterator { + type Item = Binders<::Item>; + fn next(&mut self) -> Option { + self.iter.next().map(|v| Binders { binders: self.binders.clone(), value: v }) + } +} + /// Represents one clause of the form `consequence :- conditions` where /// `conditions = cond_1 && cond_2 && ...` is the conjunction of the individual /// conditions. From a5325197e25477e350a293b4b5944f7a8e846a68 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Mon, 7 May 2018 22:10:47 -0500 Subject: [PATCH 2/3] Refactor LowerClause to permit multiple clauses --- src/ir/lowering/mod.rs | 68 +++++++++++++++++++++++++++--------------- 1 file changed, 44 insertions(+), 24 deletions(-) diff --git a/src/ir/lowering/mod.rs b/src/ir/lowering/mod.rs index be346d05b8d..f48d4a00403 100644 --- a/src/ir/lowering/mod.rs +++ b/src/ir/lowering/mod.rs @@ -3,7 +3,7 @@ use std::collections::BTreeMap; use chalk_parse::ast::*; use lalrpop_intern::intern; -use cast::Cast; +use cast::{Cast, Caster}; use errors::*; use ir::{self, Anonymize, ToParameter}; use solve::SolverChoice; @@ -205,7 +205,7 @@ impl LowerProgram for Program { impl_data.insert(item_id, d.lower_impl(&empty_env)?); } Item::Clause(ref clause) => { - custom_clauses.push(clause.lower_clause(&empty_env)?); + custom_clauses.extend(clause.lower_clause(&empty_env)?); } } } @@ -412,12 +412,7 @@ trait LowerWhereClauseVec { impl LowerWhereClauseVec for [WhereClause] { fn lower(&self, env: &Env) -> Result> { - self.iter() - .flat_map(|wc| match wc.lower(env) { - Ok(v) => v.into_iter().map(Ok).collect(), - Err(e) => vec![Err(e)], - }) - .collect() + self.iter().flat_map(|wc| wc.lower(env).apply_result()).collect() } } @@ -519,7 +514,7 @@ impl LowerWhereClause for WhereClause { | WhereClause::TraitRefFromEnv { .. } | WhereClause::Derefs { .. } => { let goals: Vec = self.lower(env)?; - goals.into_iter().map(|g| g.cast()).collect() + goals.into_iter().casted().collect() } WhereClause::UnifyTys { ref a, ref b } => vec![ir::EqGoal { a: ir::ParameterKind::Ty(a.lower(env)?), @@ -842,15 +837,13 @@ impl LowerImpl for Impl { } trait LowerClause { - fn lower_clause(&self, env: &Env) -> Result; + fn lower_clause(&self, env: &Env) -> Result>; } impl LowerClause for Clause { - fn lower_clause(&self, env: &Env) -> Result { - let implication = env.in_binders(self.all_parameters(), |env| { + fn lower_clause(&self, env: &Env) -> Result> { + let implications = env.in_binders(self.all_parameters(), |env| { let consequences: Vec = self.consequence.lower(env)?; - assert_eq!(1, consequences.len()); - let consequence = consequences.into_iter().next().unwrap(); let mut conditions: Vec = self.conditions .iter() @@ -862,17 +855,27 @@ impl LowerClause for Clause { // therefore reverse. conditions.reverse(); - Ok(ir::ProgramClauseImplication { - consequence, - conditions, - }) + let implications = consequences + .into_iter() + .map(|consequence| ir::ProgramClauseImplication { + consequence, + conditions: conditions.clone(), + }) + .collect::>(); + Ok(implications) })?; - if implication.binders.is_empty() { - Ok(ir::ProgramClause::Implies(implication.value)) - } else { - Ok(ir::ProgramClause::ForAll(implication)) - } + let clauses = implications + .into_iter() + .map(|implication: ir::Binders| { + if implication.binders.is_empty() { + ir::ProgramClause::Implies(implication.value) + } else { + ir::ProgramClause::ForAll(implication) + } + }) + .collect(); + Ok(clauses) } } @@ -982,7 +985,8 @@ impl<'k> LowerGoal> for Goal { // `if (FromEnv(T: Trait)) { ... /* this part is untouched */ ... }`. let where_clauses: Result> = wc.into_iter() - .map(|wc| Ok(wc.lower_clause(env)?.into_from_env_clause())) + .flat_map(|wc| wc.lower_clause(env).apply_result()) + .map(|result| result.map(|wc| wc.into_from_env_clause())) .collect(); Ok(Box::new(ir::Goal::Implies(where_clauses?, g.lower(env)?))) } @@ -1025,3 +1029,19 @@ impl LowerQuantifiedGoal for Goal { Ok(Box::new(ir::Goal::Quantified(quantifier_kind, subgoal))) } } + +/// Lowers Result> -> Vec>. +trait ApplyResult { + type Output; + fn apply_result(self) -> Self::Output; +} + +impl ApplyResult for Result> { + type Output = Vec>; + fn apply_result(self) -> Self::Output { + match self { + Ok(v) => v.into_iter().map(Ok).collect(), + Err(e) => vec![Err(e)], + } + } +} From f7099016cb5a660caa500b2177a6482c63aa1de1 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Mon, 7 May 2018 22:45:30 -0500 Subject: [PATCH 3/3] Handle multiple leaf goals in LowerGoal --- src/ir/lowering/mod.rs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/ir/lowering/mod.rs b/src/ir/lowering/mod.rs index f48d4a00403..5cb2463b00f 100644 --- a/src/ir/lowering/mod.rs +++ b/src/ir/lowering/mod.rs @@ -6,6 +6,7 @@ use lalrpop_intern::intern; use cast::{Cast, Caster}; use errors::*; use ir::{self, Anonymize, ToParameter}; +use itertools::Itertools; use solve::SolverChoice; mod test; @@ -995,10 +996,11 @@ impl<'k> LowerGoal> for Goal { } Goal::Not(g) => Ok(Box::new(ir::Goal::Not(g.lower(env)?))), Goal::Leaf(wc) => { - let leaf = wc.lower(env)?; - assert_eq!(1, leaf.len()); - let leaf = leaf.into_iter().next().unwrap(); - Ok(Box::new(ir::Goal::Leaf(leaf))) + // A where clause can lower to multiple leaf goals; wrap these in Goal::And. + let leaves = wc.lower(env)?.into_iter().map(ir::Goal::Leaf); + let goal = leaves.fold1(|goal, leaf| ir::Goal::And(Box::new(goal), Box::new(leaf))) + .expect("at least one goal"); + Ok(Box::new(goal)) } } }