Skip to content

Commit a94a018

Browse files
authored
Merge pull request #345 from yaahc/jane/intern-param
Add &self arg to intern_param
2 parents 981a3cc + 2e7f4f9 commit a94a018

34 files changed

+749
-411
lines changed

chalk-derive/src/lib.rs

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,9 @@ pub fn derive_fold(item: TokenStream) -> TokenStream {
3030
impl #impl_generics Fold < #arg, #arg > for #type_name #ty_generics #where_clause_ref {
3131
type Result = Self;
3232

33-
fn fold_with(
33+
fn fold_with<'i>(
3434
&self,
35-
folder: &mut dyn Folder < #arg, #arg >,
35+
folder: &mut dyn Folder < 'i, #arg, #arg >,
3636
binders: usize,
3737
) -> ::chalk_engine::fallible::Fallible<Self::Result> {
3838
#body
@@ -94,11 +94,15 @@ pub fn derive_fold(item: TokenStream) -> TokenStream {
9494
{
9595
type Result = #type_name < _U >;
9696

97-
fn fold_with(
97+
fn fold_with<'i>(
9898
&self,
99-
folder: &mut dyn Folder < _I, _TI >,
99+
folder: &mut dyn Folder < 'i, _I, _TI >,
100100
binders: usize,
101-
) -> ::chalk_engine::fallible::Fallible<Self::Result> {
101+
) -> ::chalk_engine::fallible::Fallible<Self::Result>
102+
where
103+
_I: 'i,
104+
_TI: 'i,
105+
{
102106
#body
103107
}
104108
}
@@ -129,11 +133,15 @@ pub fn derive_fold(item: TokenStream) -> TokenStream {
129133
{
130134
type Result = #type_name < _TI >;
131135

132-
fn fold_with(
136+
fn fold_with<'i>(
133137
&self,
134-
folder: &mut dyn Folder < #i, _TI >,
138+
folder: &mut dyn Folder < 'i, #i, _TI >,
135139
binders: usize,
136-
) -> ::chalk_engine::fallible::Fallible<Self::Result> {
140+
) -> ::chalk_engine::fallible::Fallible<Self::Result>
141+
where
142+
#i: 'i,
143+
_TI: 'i,
144+
{
137145
#body
138146
}
139147
}

chalk-engine/src/context.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -172,9 +172,6 @@ pub trait Context: Clone + Debug {
172172
// Used by: simplify
173173
fn add_clauses(env: &Self::Environment, clauses: Self::ProgramClauses) -> Self::Environment;
174174

175-
/// Upcast this domain goal into a more general goal.
176-
fn into_goal(domain_goal: Self::DomainGoal) -> Self::Goal;
177-
178175
/// Selects the next appropriate subgoal index for evaluation.
179176
/// Used by: logic
180177
fn next_subgoal_index(ex_clause: &ExClause<Self>) -> usize;
@@ -265,6 +262,9 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
265262
) -> C::CanonicalAnswerSubst;
266263

267264
fn interner(&self) -> &C::Interner;
265+
266+
/// Upcast this domain goal into a more general goal.
267+
fn into_goal(&self, domain_goal: C::DomainGoal) -> C::Goal;
268268
}
269269

270270
/// Methods for combining solutions to yield an aggregate solution.

chalk-engine/src/logic.rs

Lines changed: 3 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -297,13 +297,9 @@ impl<C: Context> Forest<C> {
297297
// simplified subgoals. You can think of this as
298298
// applying built-in "meta program clauses" that
299299
// reduce HH goals into Domain goals.
300-
if let Ok(ex_clause) = Self::simplify_hh_goal(
301-
context.interner(),
302-
&mut infer,
303-
subst,
304-
environment,
305-
hh_goal,
306-
) {
300+
if let Ok(ex_clause) =
301+
Self::simplify_hh_goal(context, &mut infer, subst, environment, hh_goal)
302+
{
307303
info!(
308304
"pushing initial strand with ex-clause: {:#?}",
309305
infer.debug_ex_clause(context.interner(), &ex_clause),

chalk-engine/src/simplify.rs

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
use crate::context::{Context, InferenceTable};
1+
use crate::context::{Context, ContextOps, InferenceTable};
22
use crate::fallible::Fallible;
33
use crate::forest::Forest;
44
use crate::hh::HhGoal;
@@ -9,7 +9,7 @@ impl<C: Context> Forest<C> {
99
/// and negative HH goals. This operation may fail if the HH goal
1010
/// includes unifications that cannot be completed.
1111
pub(super) fn simplify_hh_goal(
12-
interner: &C::Interner,
12+
context: &impl ContextOps<C>,
1313
infer: &mut dyn InferenceTable<C>,
1414
subst: C::Substitution,
1515
initial_environment: C::Environment,
@@ -31,11 +31,13 @@ impl<C: Context> Forest<C> {
3131
while let Some((environment, hh_goal)) = pending_goals.pop() {
3232
match hh_goal {
3333
HhGoal::ForAll(subgoal) => {
34-
let subgoal = infer.instantiate_binders_universally(interner, &subgoal);
34+
let subgoal =
35+
infer.instantiate_binders_universally(context.interner(), &subgoal);
3536
pending_goals.push((environment, C::into_hh_goal(subgoal)));
3637
}
3738
HhGoal::Exists(subgoal) => {
38-
let subgoal = infer.instantiate_binders_existentially(interner, &subgoal);
39+
let subgoal =
40+
infer.instantiate_binders_existentially(context.interner(), &subgoal);
3941
pending_goals.push((environment, C::into_hh_goal(subgoal)))
4042
}
4143
HhGoal::Implies(wc, subgoal) => {
@@ -56,7 +58,7 @@ impl<C: Context> Forest<C> {
5658
)));
5759
}
5860
HhGoal::Unify(variance, a, b) => infer.unify_parameters_into_ex_clause(
59-
interner,
61+
context.interner(),
6062
&environment,
6163
variance,
6264
&a,
@@ -68,7 +70,7 @@ impl<C: Context> Forest<C> {
6870
.subgoals
6971
.push(Literal::Positive(C::goal_in_environment(
7072
&environment,
71-
C::into_goal(domain_goal),
73+
context.into_goal(domain_goal),
7274
)));
7375
}
7476
HhGoal::CannotProve => {

chalk-integration/src/lowering.rs

Lines changed: 46 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -608,10 +608,13 @@ trait LowerDomainGoal {
608608

609609
impl LowerDomainGoal for DomainGoal {
610610
fn lower(&self, env: &Env) -> LowerResult<Vec<chalk_ir::DomainGoal<ChalkIr>>> {
611+
let interner = env.interner();
611612
let goals = match self {
612-
DomainGoal::Holds { where_clause } => {
613-
where_clause.lower(env)?.into_iter().casted().collect()
614-
}
613+
DomainGoal::Holds { where_clause } => where_clause
614+
.lower(env)?
615+
.into_iter()
616+
.casted(interner)
617+
.collect(),
615618
DomainGoal::Normalize { alias, ty } => {
616619
vec![chalk_ir::DomainGoal::Normalize(chalk_ir::Normalize {
617620
alias: alias.lower(env)?,
@@ -655,18 +658,21 @@ trait LowerLeafGoal {
655658

656659
impl LowerLeafGoal for LeafGoal {
657660
fn lower(&self, env: &Env) -> LowerResult<chalk_ir::Goal<ChalkIr>> {
661+
let interner = env.interner();
658662
Ok(match self {
659-
LeafGoal::DomainGoal { goal } => goal.lower(env)?.into_iter().casted().collect(),
663+
LeafGoal::DomainGoal { goal } => {
664+
chalk_ir::Goal::all(interner, goal.lower(env)?.into_iter().casted(interner))
665+
}
660666
LeafGoal::UnifyTys { a, b } => chalk_ir::EqGoal {
661-
a: a.lower(env)?.cast(),
662-
b: b.lower(env)?.cast(),
667+
a: a.lower(env)?.cast(interner),
668+
b: b.lower(env)?.cast(interner),
663669
}
664-
.cast::<chalk_ir::Goal<ChalkIr>>(),
670+
.cast::<chalk_ir::Goal<ChalkIr>>(interner),
665671
LeafGoal::UnifyLifetimes { ref a, ref b } => chalk_ir::EqGoal {
666-
a: a.lower(env)?.cast(),
667-
b: b.lower(env)?.cast(),
672+
a: a.lower(env)?.cast(interner),
673+
b: b.lower(env)?.cast(interner),
668674
}
669-
.cast::<chalk_ir::Goal<ChalkIr>>(),
675+
.cast::<chalk_ir::Goal<ChalkIr>>(interner),
670676
})
671677
}
672678
}
@@ -718,14 +724,15 @@ trait LowerTraitRef {
718724

719725
impl LowerTraitRef for TraitRef {
720726
fn lower(&self, env: &Env) -> LowerResult<chalk_ir::TraitRef<ChalkIr>> {
727+
let interner = env.interner();
721728
let without_self = TraitBound {
722729
trait_name: self.trait_name,
723730
args_no_self: self.args.iter().cloned().skip(1).collect(),
724731
}
725732
.lower(env)?;
726733

727734
let self_parameter = self.args[0].lower(env)?;
728-
Ok(without_self.as_trait_ref(self_parameter.assert_ty_ref().clone()))
735+
Ok(without_self.as_trait_ref(interner, self_parameter.assert_ty_ref().clone()))
729736
}
730737
}
731738

@@ -910,6 +917,7 @@ impl LowerAliasTy for AliasTy {
910917
ref name,
911918
ref args,
912919
} = *self;
920+
let interner = env.interner();
913921
let chalk_ir::TraitRef {
914922
trait_id,
915923
substitution: trait_substitution,
@@ -945,7 +953,7 @@ impl LowerAliasTy for AliasTy {
945953

946954
Ok(chalk_ir::AliasTy {
947955
associated_ty_id: lookup.id,
948-
substitution: chalk_ir::Substitution::from(args),
956+
substitution: chalk_ir::Substitution::from(interner, args),
949957
})
950958
}
951959
}
@@ -956,6 +964,7 @@ trait LowerTy {
956964

957965
impl LowerTy for Ty {
958966
fn lower(&self, env: &Env) -> LowerResult<chalk_ir::Ty<ChalkIr>> {
967+
let interner = env.interner();
959968
match *self {
960969
Ty::Id { name } => match env.lookup_type(name)? {
961970
TypeLookup::Struct(id) => {
@@ -969,14 +978,12 @@ impl LowerTy for Ty {
969978
} else {
970979
Ok(chalk_ir::TyData::Apply(chalk_ir::ApplicationTy {
971980
name: chalk_ir::TypeName::Struct(id),
972-
substitution: chalk_ir::Substitution::empty(),
981+
substitution: chalk_ir::Substitution::empty(interner),
973982
})
974-
.intern(env.interner()))
983+
.intern(interner))
975984
}
976985
}
977-
TypeLookup::Parameter(d) => {
978-
Ok(chalk_ir::TyData::BoundVar(d).intern(env.interner()))
979-
}
986+
TypeLookup::Parameter(d) => Ok(chalk_ir::TyData::BoundVar(d).intern(interner)),
980987
},
981988

982989
Ty::Dyn { ref bounds } => Ok(chalk_ir::TyData::Dyn(chalk_ir::DynTy {
@@ -989,15 +996,15 @@ impl LowerTy for Ty {
989996
.iter()
990997
.flat_map(|qil| {
991998
qil.into_where_clauses(
992-
env.interner(),
993-
chalk_ir::TyData::BoundVar(0).intern(env.interner()),
999+
interner,
1000+
chalk_ir::TyData::BoundVar(0).intern(interner),
9941001
)
9951002
})
9961003
.collect())
9971004
},
9981005
)?,
9991006
})
1000-
.intern(env.interner())),
1007+
.intern(interner)),
10011008

10021009
Ty::Apply { name, ref args } => {
10031010
let id = match env.lookup_type(name)? {
@@ -1014,8 +1021,10 @@ impl LowerTy for Ty {
10141021
})?;
10151022
}
10161023

1017-
let substitution =
1018-
chalk_ir::Substitution::from_fallible(args.iter().map(|t| Ok(t.lower(env)?)))?;
1024+
let substitution = chalk_ir::Substitution::from_fallible(
1025+
interner,
1026+
args.iter().map(|t| Ok(t.lower(env)?)),
1027+
)?;
10191028

10201029
for (param, arg) in k.binders.binders.iter().zip(args.iter()) {
10211030
if param.kind() != arg.kind() {
@@ -1031,11 +1040,11 @@ impl LowerTy for Ty {
10311040
name: chalk_ir::TypeName::Struct(id),
10321041
substitution: substitution,
10331042
})
1034-
.intern(env.interner()))
1043+
.intern(interner))
10351044
}
10361045

10371046
Ty::Alias { ref alias } => {
1038-
Ok(chalk_ir::TyData::Alias(alias.lower(env)?).intern(env.interner()))
1047+
Ok(chalk_ir::TyData::Alias(alias.lower(env)?).intern(interner))
10391048
}
10401049

10411050
Ty::ForAll {
@@ -1050,9 +1059,9 @@ impl LowerTy for Ty {
10501059

10511060
let function = chalk_ir::Fn {
10521061
num_binders: lifetime_names.len(),
1053-
parameters: vec![ty.lower(&quantified_env)?.cast()],
1062+
parameters: vec![ty.lower(&quantified_env)?.cast(interner)],
10541063
};
1055-
Ok(chalk_ir::TyData::Function(function).intern(env.interner()))
1064+
Ok(chalk_ir::TyData::Function(function).intern(interner))
10561065
}
10571066
}
10581067
}
@@ -1064,9 +1073,10 @@ trait LowerParameter {
10641073

10651074
impl LowerParameter for Parameter {
10661075
fn lower(&self, env: &Env) -> LowerResult<chalk_ir::Parameter<ChalkIr>> {
1076+
let interner = env.interner();
10671077
match *self {
1068-
Parameter::Ty(ref t) => Ok(t.lower(env)?.cast()),
1069-
Parameter::Lifetime(ref l) => Ok(l.lower(env)?.cast()),
1078+
Parameter::Ty(ref t) => Ok(t.lower(env)?.cast(interner)),
1079+
Parameter::Lifetime(ref l) => Ok(l.lower(env)?.cast(interner)),
10701080
}
10711081
}
10721082
}
@@ -1077,10 +1087,11 @@ trait LowerLifetime {
10771087

10781088
impl LowerLifetime for Lifetime {
10791089
fn lower(&self, env: &Env) -> LowerResult<chalk_ir::Lifetime<ChalkIr>> {
1090+
let interner = env.interner();
10801091
match *self {
10811092
Lifetime::Id { name } => match env.lookup_lifetime(name)? {
10821093
LifetimeLookup::Parameter(d) => {
1083-
Ok(chalk_ir::LifetimeData::BoundVar(d).intern(env.interner()))
1094+
Ok(chalk_ir::LifetimeData::BoundVar(d).intern(interner))
10841095
}
10851096
},
10861097
}
@@ -1150,10 +1161,12 @@ trait LowerClause {
11501161

11511162
impl LowerClause for Clause {
11521163
fn lower_clause(&self, env: &Env) -> LowerResult<Vec<chalk_ir::ProgramClause<ChalkIr>>> {
1164+
let interner = env.interner();
11531165
let implications = env.in_binders(self.all_parameters(), |env| {
11541166
let consequences: Vec<chalk_ir::DomainGoal<ChalkIr>> = self.consequence.lower(env)?;
11551167

11561168
let conditions = chalk_ir::Goals::from_fallible(
1169+
interner,
11571170
// Subtle: in the SLG solver, we pop conditions from R to
11581171
// L. To preserve the expected order (L to R), we must
11591172
// therefore reverse.
@@ -1269,6 +1282,7 @@ impl LowerGoal<LoweredProgram> for Goal {
12691282

12701283
impl<'k> LowerGoal<Env<'k>> for Goal {
12711284
fn lower(&self, env: &Env<'k>) -> LowerResult<chalk_ir::Goal<ChalkIr>> {
1285+
let interner = env.interner();
12721286
match self {
12731287
Goal::ForAll(ids, g) => g.lower_quantified(env, chalk_ir::QuantifierKind::ForAll, ids),
12741288
Goal::Exists(ids, g) => g.lower_quantified(env, chalk_ir::QuantifierKind::Exists, ids),
@@ -1280,18 +1294,19 @@ impl<'k> LowerGoal<Env<'k>> for Goal {
12801294
let where_clauses: LowerResult<Vec<_>> = hyp
12811295
.into_iter()
12821296
.flat_map(|h| h.lower_clause(env).apply_result())
1283-
.map(|result| result.map(|h| h.into_from_env_clause()))
1297+
.map(|result| result.map(|h| h.into_from_env_clause(interner)))
12841298
.collect();
12851299
Ok(chalk_ir::GoalData::Implies(where_clauses?, g.lower(env)?).intern())
12861300
}
12871301
Goal::And(g1, g2s) => {
12881302
let goals = chalk_ir::Goals::from_fallible(
1303+
interner,
12891304
Some(g1).into_iter().chain(g2s).map(|g| g.lower(env)),
12901305
)?;
12911306
Ok(chalk_ir::GoalData::All(goals).intern())
12921307
}
12931308
Goal::Not(g) => Ok(chalk_ir::GoalData::Not(g.lower(env)?).intern()),
1294-
Goal::Compatible(g) => Ok(g.lower(env)?.compatible(env.interner())),
1309+
Goal::Compatible(g) => Ok(g.lower(env)?.compatible(interner)),
12951310
Goal::Leaf(leaf) => {
12961311
// A where clause can lower to multiple leaf goals; wrap these in Goal::And.
12971312
Ok(leaf.lower(env)?)

0 commit comments

Comments
 (0)