Skip to content

Commit 46658a6

Browse files
jackh726jackh726
committed
Add a LifetimeOutlives struct
1 parent cf0ce2d commit 46658a6

File tree

8 files changed

+82
-32
lines changed

8 files changed

+82
-32
lines changed

‎chalk-engine/src/simplify.rs‎

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

1212
impl<I: Interner, C: Context<I>> Forest<I, C> {
@@ -70,7 +70,7 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
7070
&mut ex_clause,
7171
)?,
7272
GoalData::DomainGoal(domain_goal) => match domain_goal {
73-
DomainGoal::Holds(WhereClause::LifetimeOutlives(a, b)) => {
73+
DomainGoal::Holds(WhereClause::LifetimeOutlives(LifetimeOutlives { a, b })) => {
7474
ex_clause.constraints.push(InEnvironment::new(
7575
&environment,
7676
Constraint::Outlives(a.clone(), b.clone()),

‎chalk-integration/src/lowering.rs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -876,8 +876,10 @@ impl LowerWhereClause<chalk_ir::WhereClause<ChalkIr>> for WhereClause {
876876
],
877877
WhereClause::LifetimeOutlives { a, b } => {
878878
vec![chalk_ir::WhereClause::LifetimeOutlives(
879-
a.lower(env)?,
880-
b.lower(env)?,
879+
chalk_ir::LifetimeOutlives {
880+
a: a.lower(env)?,
881+
b: b.lower(env)?,
882+
},
881883
)]
882884
}
883885
};

‎chalk-ir/src/cast.rs‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,12 @@ impl<I: Interner> CastTo<WhereClause<I>> for AliasEq<I> {
9898
}
9999
}
100100

101+
impl<I: Interner> CastTo<WhereClause<I>> for LifetimeOutlives<I> {
102+
fn cast_to(self, _interner: &I) -> WhereClause<I> {
103+
WhereClause::LifetimeOutlives(self)
104+
}
105+
}
106+
101107
impl<T, I> CastTo<DomainGoal<I>> for T
102108
where
103109
T: CastTo<WhereClause<I>>,

‎chalk-ir/src/debug.rs‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -536,6 +536,12 @@ impl<'me, I: Interner> SeparatorTraitRef<'me, I> {
536536
}
537537
}
538538

539+
impl<I: Interner> Debug for LifetimeOutlives<I> {
540+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
541+
write!(fmt, "{:?}: {:?}", self.a, self.b)
542+
}
543+
}
544+
539545
pub struct ProjectionTyDebug<'a, I: Interner> {
540546
projection_ty: &'a ProjectionTy<I>,
541547
interner: &'a I,
@@ -630,7 +636,7 @@ impl<I: Interner> Debug for WhereClause<I> {
630636
match self {
631637
WhereClause::Implemented(tr) => write!(fmt, "Implemented({:?})", tr.with_colon()),
632638
WhereClause::AliasEq(a) => write!(fmt, "{:?}", a),
633-
WhereClause::LifetimeOutlives(a, b) => write!(fmt, "{:?}: {:?}", a, b),
639+
WhereClause::LifetimeOutlives(l_o) => write!(fmt, "{:?}", l_o),
634640
}
635641
}
636642
}

‎chalk-ir/src/lib.rs‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1184,12 +1184,17 @@ impl<I: Interner> TraitRef<I> {
11841184
}
11851185
}
11861186

1187+
#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)]
1188+
pub struct LifetimeOutlives<I: Interner> {
1189+
pub a: Lifetime<I>,
1190+
pub b: Lifetime<I>,
1191+
}
11871192
/// Where clauses that can be written by a Rust programmer.
11881193
#[derive(Clone, PartialEq, Eq, Hash, Fold, SuperVisit, HasInterner, Zip)]
11891194
pub enum WhereClause<I: Interner> {
11901195
Implemented(TraitRef<I>),
11911196
AliasEq(AliasEq<I>),
1192-
LifetimeOutlives(Lifetime<I>, Lifetime<I>),
1197+
LifetimeOutlives(LifetimeOutlives<I>),
11931198
}
11941199

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

‎chalk-solve/src/clauses.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -322,7 +322,7 @@ 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(_, _)) => {}
325+
DomainGoal::Holds(WhereClause::LifetimeOutlives(_)) => {}
326326
DomainGoal::WellFormed(WellFormed::Trait(trait_ref))
327327
| DomainGoal::LocalImplAllowed(trait_ref) => {
328328
db.trait_datum(trait_ref.trait_id)

‎chalk-solve/src/infer/unify.rs‎

Lines changed: 45 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -81,9 +81,8 @@ impl<'t, I: Interner> Unifier<'t, I> {
8181
})
8282
}
8383

84-
fn unify_ty_ty<'a>(&mut self, a: &'a Ty<I>, b: &'a Ty<I>) -> Fallible<()> {
84+
fn unify_ty_ty(&mut self, a: &Ty<I>, b: &Ty<I>) -> Fallible<()> {
8585
let interner = self.interner;
86-
// ^^ ^^ ^^ FIXME rustc bug
8786

8887
let n_a = self.table.normalize_ty_shallow(interner, a);
8988
let n_b = self.table.normalize_ty_shallow(interner, b);
@@ -343,28 +342,12 @@ impl<'t, I: Interner> Unifier<'t, I> {
343342
Ok(())
344343
}
345344

346-
(&LifetimeData::InferenceVar(var), &LifetimeData::Placeholder(idx))
347-
| (&LifetimeData::Placeholder(idx), &LifetimeData::InferenceVar(var)) => {
348-
let var = EnaVariable::from(var);
349-
let var_ui = self.table.universe_of_unbound_var(var);
350-
if var_ui.can_see(idx.ui) {
351-
debug!(
352-
"unify_lifetime_lifetime: {:?} in {:?} can see {:?}; unifying",
353-
var, var_ui, idx.ui
354-
);
355-
let v = LifetimeData::Placeholder(idx).intern(interner);
356-
self.table
357-
.unify
358-
.unify_var_value(var, InferenceValue::from_lifetime(interner, v))
359-
.unwrap();
360-
Ok(())
361-
} else {
362-
debug!(
363-
"unify_lifetime_lifetime: {:?} in {:?} cannot see {:?}; pushing constraint",
364-
var, var_ui, idx.ui
365-
);
366-
Ok(self.push_lifetime_eq_constraint(a.clone(), b.clone()))
367-
}
345+
(&LifetimeData::InferenceVar(a_var), &LifetimeData::Placeholder(b_idx)) => {
346+
self.unify_lifetime_var(a, b, a_var, b, b_idx.ui)
347+
}
348+
349+
(&LifetimeData::Placeholder(a_idx), &LifetimeData::InferenceVar(b_var)) => {
350+
self.unify_lifetime_var(a, b, b_var, a, a_idx.ui)
368351
}
369352

370353
(&LifetimeData::Placeholder(_), &LifetimeData::Placeholder(_)) => {
@@ -384,6 +367,44 @@ impl<'t, I: Interner> Unifier<'t, I> {
384367
}
385368
}
386369

370+
fn unify_lifetime_var(
371+
&mut self,
372+
a: &Lifetime<I>,
373+
b: &Lifetime<I>,
374+
var: InferenceVar,
375+
value: &Lifetime<I>,
376+
value_ui: UniverseIndex,
377+
) -> Fallible<()> {
378+
debug_heading!(
379+
"unify_lifetime_var(var={:?}, value={:?}, value_ui={:?})",
380+
var,
381+
value,
382+
value_ui
383+
);
384+
let var = EnaVariable::from(var);
385+
let var_ui = self.table.universe_of_unbound_var(var);
386+
if var_ui.can_see(value_ui) {
387+
debug!(
388+
"unify_lifetime_var: {:?} in {:?} can see {:?}; unifying",
389+
var, var_ui, value_ui
390+
);
391+
self.table
392+
.unify
393+
.unify_var_value(
394+
var,
395+
InferenceValue::from_lifetime(&self.interner, value.clone()),
396+
)
397+
.unwrap();
398+
Ok(())
399+
} else {
400+
debug!(
401+
"unify_lifetime_var: {:?} in {:?} cannot see {:?}; pushing constraint",
402+
var, var_ui, value_ui
403+
);
404+
Ok(self.push_lifetime_eq_constraint(a.clone(), b.clone()))
405+
}
406+
}
407+
387408
fn unify_const_const<'a>(&mut self, a: &'a Const<I>, b: &'a Const<I>) -> Fallible<()> {
388409
let interner = self.interner;
389410

‎tests/test/misc.rs‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -630,5 +630,15 @@ fn lifetime_outlives_constraints() {
630630
} yields[SolverChoice::slg(10, None)] {
631631
"Unique; for<?U0,?U0> { substitution [?0 := '^0.0, ?1 := '^0.1], lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0: '^0.1 }] }"
632632
}
633+
634+
goal {
635+
forall<'a> {
636+
exists<'b> {
637+
Bar: Foo<'a, 'b>
638+
}
639+
}
640+
} yields[SolverChoice::slg(10, None)] {
641+
"Unique; for<?U1> { substitution [?0 := '^0.0], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '^0.0 }] }"
642+
}
633643
}
634644
}

0 commit comments

Comments
 (0)