Skip to content

Commit edd1d86

Browse files
jackh726jackh726
committed
Add lifetime outlives
1 parent ffa2e51 commit edd1d86

File tree

13 files changed

+110
-14
lines changed

13 files changed

+110
-14
lines changed

‎chalk-engine/src/simplify.rs

Lines changed: 17 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,8 @@ use crate::{ExClause, Literal, TimeStamp};
55
use chalk_ir::debug;
66
use chalk_ir::interner::Interner;
77
use chalk_ir::{
8-
Environment, Fallible, Goal, GoalData, InEnvironment, QuantifierKind, Substitution,
8+
Constraint, DomainGoal, Environment, Fallible, Goal, GoalData, InEnvironment, QuantifierKind,
9+
Substitution, WhereClause,
910
};
1011

1112
impl<I: Interner, C: Context<I>> Forest<I, C> {
@@ -68,14 +69,22 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
6869
&goal.b,
6970
&mut ex_clause,
7071
)?,
71-
GoalData::DomainGoal(domain_goal) => {
72-
ex_clause
73-
.subgoals
74-
.push(Literal::Positive(InEnvironment::new(
72+
GoalData::DomainGoal(domain_goal) => match domain_goal {
73+
DomainGoal::Holds(WhereClause::LifetimeOutlives(a, b)) => {
74+
ex_clause.constraints.push(InEnvironment::new(
7575
&environment,
76-
context.into_goal(domain_goal.clone()),
77-
)));
78-
}
76+
Constraint::Outlives(a.clone(), b.clone()),
77+
));
78+
}
79+
_ => {
80+
ex_clause
81+
.subgoals
82+
.push(Literal::Positive(InEnvironment::new(
83+
&environment,
84+
context.into_goal(domain_goal.clone()),
85+
)));
86+
}
87+
},
7988
GoalData::CannotProve(()) => {
8089
debug!("Marking Strand as ambiguous because of a `CannotProve` subgoal");
8190
ex_clause.ambiguous = true;

‎chalk-integration/src/lowering.rs

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -874,6 +874,12 @@ impl LowerWhereClause<chalk_ir::WhereClause<ChalkIr>> for WhereClause {
874874
}),
875875
chalk_ir::WhereClause::Implemented(projection.trait_ref.lower(env)?),
876876
],
877+
WhereClause::LifetimeOutlives { a, b } => {
878+
vec![chalk_ir::WhereClause::LifetimeOutlives(
879+
a.lower(env)?,
880+
b.lower(env)?,
881+
)]
882+
}
877883
};
878884
Ok(where_clauses)
879885
}

‎chalk-ir/src/debug.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -630,6 +630,7 @@ impl<I: Interner> Debug for WhereClause<I> {
630630
match self {
631631
WhereClause::Implemented(tr) => write!(fmt, "Implemented({:?})", tr.with_colon()),
632632
WhereClause::AliasEq(a) => write!(fmt, "{:?}", a),
633+
WhereClause::LifetimeOutlives(a, b) => write!(fmt, "{:?}: {:?}", a, b),
633634
}
634635
}
635636
}

‎chalk-ir/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1189,6 +1189,7 @@ impl<I: Interner> TraitRef<I> {
11891189
pub enum WhereClause<I: Interner> {
11901190
Implemented(TraitRef<I>),
11911191
AliasEq(AliasEq<I>),
1192+
LifetimeOutlives(Lifetime<I>, Lifetime<I>),
11921193
}
11931194

11941195
#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)]

‎chalk-parse/src/ast.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -331,6 +331,7 @@ impl fmt::Display for Identifier {
331331
pub enum WhereClause {
332332
Implemented { trait_ref: TraitRef },
333333
ProjectionEq { projection: ProjectionTy, ty: Ty },
334+
LifetimeOutlives { a: Lifetime, b: Lifetime },
334335
}
335336

336337
#[derive(Clone, PartialEq, Eq, Debug)]

‎chalk-parse/src/parser.lalrpop

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -367,6 +367,11 @@ WhereClause: WhereClause = {
367367
let projection = ProjectionTy { trait_ref, name, args: a2 };
368368
WhereClause::ProjectionEq { projection, ty }
369369
},
370+
371+
// 'a: 'b
372+
<a:Lifetime> ":" <b:Lifetime> => {
373+
WhereClause::LifetimeOutlives { a, b }
374+
}
370375
};
371376

372377
QuantifiedWhereClause: QuantifiedWhereClause = {

‎chalk-solve/src/clauses.rs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -322,6 +322,15 @@ fn program_clauses_that_could_match<I: Interner>(
322322
.opaque_ty_data(opaque_ty.opaque_ty_id)
323323
.to_program_clauses(builder),
324324
},
325+
DomainGoal::Holds(WhereClause::LifetimeOutlives(a, b)) => {
326+
builder.push_clause(
327+
DomainGoal::Holds(WhereClause::LifetimeOutlives(a.clone(), b.clone())),
328+
Some(DomainGoal::Holds(WhereClause::LifetimeOutlives(
329+
a.clone(),
330+
b.clone(),
331+
))),
332+
);
333+
}
325334
DomainGoal::WellFormed(WellFormed::Trait(trait_ref))
326335
| DomainGoal::LocalImplAllowed(trait_ref) => {
327336
db.trait_datum(trait_ref.trait_id)

‎chalk-solve/src/clauses/dyn_ty.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,7 @@ pub(super) fn build_dyn_self_ty_clauses<I: Interner>(
7272
}
7373
// Associated item bindings are just taken as facts (?)
7474
WhereClause::AliasEq(_) => builder.push_fact(wc),
75+
WhereClause::LifetimeOutlives(..) => {}
7576
});
7677
}
7778
});
@@ -160,6 +161,7 @@ pub fn super_traits<I: Interner>(
160161
Some(tr.clone())
161162
}
162163
WhereClause::AliasEq(_) => None,
164+
WhereClause::LifetimeOutlives(..) => None,
163165
})
164166
})
165167
.collect::<Vec<_>>()

‎chalk-solve/src/coinductive_goal.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ impl<I: Interner> IsCoinductive<I> for Goal<I> {
2424
|| db.trait_datum(tr.trait_id).is_coinductive_trait()
2525
}
2626
WhereClause::AliasEq(..) => false,
27+
WhereClause::LifetimeOutlives(..) => false,
2728
},
2829
GoalData::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => true,
2930
GoalData::Quantified(QuantifierKind::ForAll, goal) => {

‎chalk-solve/src/solve/slg/resolvent.rs

Lines changed: 37 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,26 @@ impl<I: Interner> context::ResolventOps<I, SlgContext<I>> for TruncatingInferenc
9292
debug!("consequence = {:?}", consequence);
9393
debug!("conditions = {:?}", conditions);
9494

95+
let constraints = conditions
96+
.iter(interner)
97+
.filter_map(|c| match c.data(interner) {
98+
GoalData::DomainGoal(DomainGoal::Holds(WhereClause::LifetimeOutlives(a, b))) => {
99+
Some(InEnvironment::new(
100+
environment,
101+
Constraint::Outlives(a.clone(), b.clone()),
102+
))
103+
}
104+
GoalData::Not(c1) => match c1.data(interner) {
105+
GoalData::DomainGoal(DomainGoal::Holds(WhereClause::LifetimeOutlives(
106+
_a,
107+
_b,
108+
))) => panic!("Not allowed."),
109+
_ => None,
110+
},
111+
_ => None,
112+
})
113+
.collect();
114+
95115
// Unify the selected literal Li with C'.
96116
let unification_result = self
97117
.infer
@@ -101,7 +121,7 @@ impl<I: Interner> context::ResolventOps<I, SlgContext<I>> for TruncatingInferenc
101121
let mut ex_clause = ExClause {
102122
subst: subst.clone(),
103123
ambiguous: false,
104-
constraints: vec![],
124+
constraints,
105125
subgoals: vec![],
106126
delayed_subgoals: vec![],
107127
answer_time: TimeStamp::default(),
@@ -111,15 +131,26 @@ impl<I: Interner> context::ResolventOps<I, SlgContext<I>> for TruncatingInferenc
111131
// Add the subgoals/region-constraints that unification gave us.
112132
slg::into_ex_clause(interner, unification_result, &mut ex_clause);
113133

114-
// Add the `conditions` from the program clause into the result too.
115-
ex_clause
116-
.subgoals
117-
.extend(conditions.iter(interner).map(|c| match c.data(interner) {
134+
let conditions_iter = conditions
135+
.iter(interner)
136+
.filter(|c| match c.data(interner) {
137+
GoalData::DomainGoal(DomainGoal::Holds(WhereClause::LifetimeOutlives(..))) => false,
138+
GoalData::Not(c1) => match c1.data(interner) {
139+
GoalData::DomainGoal(DomainGoal::Holds(WhereClause::LifetimeOutlives(..))) => {
140+
false
141+
}
142+
_ => true,
143+
},
144+
_ => true,
145+
})
146+
.map(|c| match c.data(interner) {
118147
GoalData::Not(c1) => {
119148
Literal::Negative(InEnvironment::new(environment, Goal::clone(c1)))
120149
}
121150
_ => Literal::Positive(InEnvironment::new(environment, Goal::clone(c))),
122-
}));
151+
});
152+
// Add the `conditions` from the program clause into the result too.
153+
ex_clause.subgoals.extend(conditions_iter);
123154

124155
Ok(ex_clause)
125156
}

0 commit comments

Comments
 (0)