Merge pull request #451 from jackh726/lifetime_outlives

Add lifetime outlives goal

Author: nikomatsakis

chalk-engine/src/simplify.rs

@@ -5,7 +5,8 @@ use crate::{ExClause, Literal, TimeStamp};
 use chalk_ir::debug;
 use chalk_ir::interner::Interner;
 use chalk_ir::{
-    Environment, Fallible, Goal, GoalData, InEnvironment, QuantifierKind, Substitution,
+    Constraint, DomainGoal, Environment, Fallible, Goal, GoalData, InEnvironment, LifetimeOutlives,
+    QuantifierKind, Substitution, WhereClause,
 };
 
 impl<I: Interner, C: Context<I>> Forest<I, C> {
@@ -68,14 +69,22 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
                     &goal.b,
                     &mut ex_clause,
                 )?,
-                GoalData::DomainGoal(domain_goal) => {
-                    ex_clause
-                        .subgoals
-                        .push(Literal::Positive(InEnvironment::new(
+                GoalData::DomainGoal(domain_goal) => match domain_goal {
+                    DomainGoal::Holds(WhereClause::LifetimeOutlives(LifetimeOutlives { a, b })) => {
+                        ex_clause.constraints.push(InEnvironment::new(
                             &environment,
-                            context.into_goal(domain_goal.clone()),
-                        )));
-                }
+                            Constraint::Outlives(a.clone(), b.clone()),
+                        ));
+                    }
+                    _ => {
+                        ex_clause
+                            .subgoals
+                            .push(Literal::Positive(InEnvironment::new(
+                                &environment,
+                                context.into_goal(domain_goal.clone()),
+                            )));
+                    }
+                },
                 GoalData::CannotProve(()) => {
                     debug!("Marking Strand as ambiguous because of a `CannotProve` subgoal");
                     ex_clause.ambiguous = true;

chalk-integration/src/lowering.rs

@@ -874,6 +874,14 @@ impl LowerWhereClause<chalk_ir::WhereClause<ChalkIr>> for WhereClause {
                 }),
                 chalk_ir::WhereClause::Implemented(projection.trait_ref.lower(env)?),
             ],
+            WhereClause::LifetimeOutlives { a, b } => {
+                vec![chalk_ir::WhereClause::LifetimeOutlives(
+                    chalk_ir::LifetimeOutlives {
+                        a: a.lower(env)?,
+                        b: b.lower(env)?,
+                    },
+                )]
+            }
         };
         Ok(where_clauses)
     }

chalk-ir/src/cast.rs

@@ -98,6 +98,12 @@ impl<I: Interner> CastTo<WhereClause<I>> for AliasEq<I> {
     }
 }
 
+impl<I: Interner> CastTo<WhereClause<I>> for LifetimeOutlives<I> {
+    fn cast_to(self, _interner: &I) -> WhereClause<I> {
+        WhereClause::LifetimeOutlives(self)
+    }
+}
+
 impl<T, I> CastTo<DomainGoal<I>> for T
 where
     T: CastTo<WhereClause<I>>,

chalk-ir/src/debug.rs

@@ -536,6 +536,12 @@ impl<'me, I: Interner> SeparatorTraitRef<'me, I> {
     }
 }
 
+impl<I: Interner> Debug for LifetimeOutlives<I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
+        write!(fmt, "{:?}: {:?}", self.a, self.b)
+    }
+}
+
 pub struct ProjectionTyDebug<'a, I: Interner> {
     projection_ty: &'a ProjectionTy<I>,
     interner: &'a I,
@@ -630,6 +636,7 @@ impl<I: Interner> Debug for WhereClause<I> {
         match self {
             WhereClause::Implemented(tr) => write!(fmt, "Implemented({:?})", tr.with_colon()),
             WhereClause::AliasEq(a) => write!(fmt, "{:?}", a),
+            WhereClause::LifetimeOutlives(l_o) => write!(fmt, "{:?}", l_o),
         }
     }
 }

chalk-ir/src/lib.rs

@@ -1184,11 +1184,17 @@ impl<I: Interner> TraitRef<I> {
     }
 }
 
+#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)]
+pub struct LifetimeOutlives<I: Interner> {
+    pub a: Lifetime<I>,
+    pub b: Lifetime<I>,
+}
 /// Where clauses that can be written by a Rust programmer.
 #[derive(Clone, PartialEq, Eq, Hash, Fold, SuperVisit, HasInterner, Zip)]
 pub enum WhereClause<I: Interner> {
     Implemented(TraitRef<I>),
     AliasEq(AliasEq<I>),
+    LifetimeOutlives(LifetimeOutlives<I>),
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)]

chalk-parse/src/ast.rs

@@ -331,6 +331,7 @@ impl fmt::Display for Identifier {
 pub enum WhereClause {
     Implemented { trait_ref: TraitRef },
     ProjectionEq { projection: ProjectionTy, ty: Ty },
+    LifetimeOutlives { a: Lifetime, b: Lifetime },
 }
 
 #[derive(Clone, PartialEq, Eq, Debug)]

chalk-parse/src/parser.lalrpop

@@ -367,6 +367,11 @@ WhereClause: WhereClause = {
         let projection = ProjectionTy { trait_ref, name, args: a2 };
         WhereClause::ProjectionEq { projection, ty }
     },
+
+    // 'a: 'b
+    <a:Lifetime> ":" <b:Lifetime> => {
+        WhereClause::LifetimeOutlives { a, b }
+    }
 };
 
 QuantifiedWhereClause: QuantifiedWhereClause = {

chalk-solve/src/clauses.rs

@@ -322,6 +322,7 @@ fn program_clauses_that_could_match<I: Interner>(
                 .opaque_ty_data(opaque_ty.opaque_ty_id)
                 .to_program_clauses(builder),
         },
+        DomainGoal::Holds(WhereClause::LifetimeOutlives(_)) => {}
         DomainGoal::WellFormed(WellFormed::Trait(trait_ref))
         | DomainGoal::LocalImplAllowed(trait_ref) => {
             db.trait_datum(trait_ref.trait_id)

chalk-solve/src/clauses/dyn_ty.rs

@@ -72,6 +72,7 @@ pub(super) fn build_dyn_self_ty_clauses<I: Interner>(
                 }
                 // Associated item bindings are just taken as facts (?)
                 WhereClause::AliasEq(_) => builder.push_fact(wc),
+                WhereClause::LifetimeOutlives(..) => {}
             });
         }
     });
@@ -160,6 +161,7 @@ pub fn super_traits<I: Interner>(
                                 Some(tr.clone())
                             }
                             WhereClause::AliasEq(_) => None,
+                            WhereClause::LifetimeOutlives(..) => None,
                         })
                     })
                     .collect::<Vec<_>>()

chalk-solve/src/coinductive_goal.rs

@@ -24,6 +24,7 @@ impl<I: Interner> IsCoinductive<I> for Goal<I> {
                         || db.trait_datum(tr.trait_id).is_coinductive_trait()
                 }
                 WhereClause::AliasEq(..) => false,
+                WhereClause::LifetimeOutlives(..) => false,
             },
             GoalData::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => true,
             GoalData::Quantified(QuantifierKind::ForAll, goal) => {