Refactor LowerWhereClause for multiple domain goals

Author: tmandry

src/ir/lowering/mod.rs

@@ -412,26 +412,36 @@ trait LowerWhereClauseVec<T> {
 
 impl LowerWhereClauseVec<ir::DomainGoal> for [WhereClause] {
     fn lower(&self, env: &Env) -> Result<Vec<ir::DomainGoal>> {
-        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<ir::QuantifiedDomainGoal> for [QuantifiedWhereClause] {
     fn lower(&self, env: &Env) -> Result<Vec<ir::QuantifiedDomainGoal>> {
-        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<T> {
-    fn lower(&self, env: &Env) -> Result<T>;
+    fn lower(&self, env: &Env) -> Result<Vec<T>>;
 }
 
 /// 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<ir::DomainGoal> for WhereClause {
-    fn lower(&self, env: &Env) -> Result<ir::DomainGoal> {
-        Ok(match self {
+    fn lower(&self, env: &Env) -> Result<Vec<ir::DomainGoal>> {
+        let goal = match self {
             WhereClause::Implemented { trait_ref } => {
                 ir::DomainGoal::Holds(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?))
             }
@@ -478,17 +488,18 @@ impl LowerWhereClause<ir::DomainGoal> for WhereClause {
                                         target: target.lower(env)?
                                     })
             }
-        })
+        };
+        Ok(vec![goal])
     }
 }
 
 impl LowerWhereClause<ir::QuantifiedDomainGoal> for QuantifiedWhereClause {
-    fn lower(&self, env: &Env) -> Result<ir::QuantifiedDomainGoal> {
+    fn lower(&self, env: &Env) -> Result<Vec<ir::QuantifiedDomainGoal>> {
         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<ir::QuantifiedDomainGoal> for QuantifiedWhereClause {
 /// can appear, because it includes all the sorts of things that the compiler
 /// must verify.
 impl LowerWhereClause<ir::LeafGoal> for WhereClause {
-    fn lower(&self, env: &Env) -> Result<ir::LeafGoal> {
+    fn lower(&self, env: &Env) -> Result<Vec<ir::LeafGoal>> {
         Ok(match *self {
             WhereClause::Implemented { .. }
             | WhereClause::ProjectionEq { .. }
@@ -507,17 +518,17 @@ impl LowerWhereClause<ir::LeafGoal> for WhereClause {
             | WhereClause::TyFromEnv { .. }
             | WhereClause::TraitRefFromEnv { .. }
             | WhereClause::Derefs { .. } => {
-                let g: ir::DomainGoal = self.lower(env)?;
-                g.cast()
+                let goals: Vec<ir::DomainGoal> = 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<ir::LeafGoal> 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<ir::ProgramClause> {
         let implication = env.in_binders(self.all_parameters(), |env| {
-            let consequence: ir::DomainGoal = self.consequence.lower(env)?;
+            let consequences: Vec<ir::DomainGoal> = self.consequence.lower(env)?;
+            assert_eq!(1, consequences.len());
+            let consequence = consequences.into_iter().next().unwrap();
+
             let mut conditions: Vec<ir::Goal> = self.conditions
                 .iter()
                 .map(|g| g.lower(env).map(|g| *g))
@@ -976,7 +990,12 @@ impl<'k> LowerGoal<Env<'k>> 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)))
+            }
         }
     }
 }

src/ir/mod.rs

@@ -687,6 +687,29 @@ impl<T> Binders<T> {
     }
 }
 
+/// Allows iterating over a Binders<Vec<T>>, for instance.
+/// Each element will include the same set of parameter bounds.
+impl<V: IntoIterator> IntoIterator for Binders<V> {
+    type Item = Binders<<V as IntoIterator>::Item>;
+    type IntoIter = BindersIntoIterator<V>;
+
+    fn into_iter(self) -> Self::IntoIter {
+        BindersIntoIterator { iter: self.value.into_iter(), binders: self.binders }
+    }
+}
+
+pub struct BindersIntoIterator<V: IntoIterator> {
+    iter: <V as IntoIterator>::IntoIter,
+    binders: Vec<ParameterKind<()>>,
+}
+
+impl<V: IntoIterator> Iterator for BindersIntoIterator<V> {
+    type Item = Binders<<V as IntoIterator>::Item>;
+    fn next(&mut self) -> Option<Self::Item> {
+        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.