Skip to content

Commit 4895b95

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #346 from yaahc/jane/intern-goal
Add self param to intern_goal
2 parents a94a018 + 5acc1fd commit 4895b95

File tree

8 files changed

+63
-40
lines changed

8 files changed

+63
-40
lines changed

‎chalk-integration/src/lowering.rs

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1296,16 +1296,16 @@ impl<'k> LowerGoal<Env<'k>> for Goal {
12961296
.flat_map(|h| h.lower_clause(env).apply_result())
12971297
.map(|result| result.map(|h| h.into_from_env_clause(interner)))
12981298
.collect();
1299-
Ok(chalk_ir::GoalData::Implies(where_clauses?, g.lower(env)?).intern())
1299+
Ok(chalk_ir::GoalData::Implies(where_clauses?, g.lower(env)?).intern(interner))
13001300
}
13011301
Goal::And(g1, g2s) => {
13021302
let goals = chalk_ir::Goals::from_fallible(
13031303
interner,
13041304
Some(g1).into_iter().chain(g2s).map(|g| g.lower(env)),
13051305
)?;
1306-
Ok(chalk_ir::GoalData::All(goals).intern())
1306+
Ok(chalk_ir::GoalData::All(goals).intern(interner))
13071307
}
1308-
Goal::Not(g) => Ok(chalk_ir::GoalData::Not(g.lower(env)?).intern()),
1308+
Goal::Not(g) => Ok(chalk_ir::GoalData::Not(g.lower(env)?).intern(interner)),
13091309
Goal::Compatible(g) => Ok(g.lower(env)?.compatible(interner)),
13101310
Goal::Leaf(leaf) => {
13111311
// A where clause can lower to multiple leaf goals; wrap these in Goal::And.
@@ -1331,13 +1331,14 @@ impl LowerQuantifiedGoal for Goal {
13311331
quantifier_kind: chalk_ir::QuantifierKind,
13321332
parameter_kinds: &[ParameterKind],
13331333
) -> LowerResult<chalk_ir::Goal<ChalkIr>> {
1334+
let interner = env.interner();
13341335
if parameter_kinds.is_empty() {
13351336
return self.lower(env);
13361337
}
13371338

13381339
let parameter_kinds = parameter_kinds.iter().map(|pk| pk.lower());
13391340
let subgoal = env.in_binders(parameter_kinds, |env| self.lower(env))?;
1340-
Ok(chalk_ir::GoalData::Quantified(quantifier_kind, subgoal).intern())
1341+
Ok(chalk_ir::GoalData::Quantified(quantifier_kind, subgoal).intern(interner))
13411342
}
13421343
}
13431344

‎chalk-ir/src/cast.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -108,7 +108,7 @@ where
108108
T: CastTo<DomainGoal<I>>,
109109
{
110110
fn cast_to(self, interner: &I) -> Goal<I> {
111-
GoalData::DomainGoal(self.cast(interner)).intern()
111+
GoalData::DomainGoal(self.cast(interner)).intern(interner)
112112
}
113113
}
114114

@@ -131,8 +131,8 @@ impl<I: Interner> CastTo<DomainGoal<I>> for FromEnv<I> {
131131
}
132132

133133
impl<I: Interner> CastTo<Goal<I>> for EqGoal<I> {
134-
fn cast_to(self, _interner: &I) -> Goal<I> {
135-
GoalData::EqGoal(self).intern()
134+
fn cast_to(self, interner: &I) -> Goal<I> {
135+
GoalData::EqGoal(self).intern(interner)
136136
}
137137
}
138138

@@ -145,7 +145,7 @@ impl<T: CastTo<Goal<I>>, I: Interner> CastTo<Goal<I>> for Binders<T> {
145145
QuantifierKind::ForAll,
146146
self.map(|bound| bound.cast(interner)),
147147
)
148-
.intern()
148+
.intern(interner)
149149
}
150150
}
151151
}

‎chalk-ir/src/fold.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -411,7 +411,8 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for Goal<I> {
411411
I: 'i,
412412
TI: 'i,
413413
{
414-
Ok(Goal::new(self.data().fold_with(folder, binders)?))
414+
let interner = folder.target_interner();
415+
Ok(Goal::new(interner, self.data().fold_with(folder, binders)?))
415416
}
416417
}
417418

‎chalk-ir/src/interner.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -162,7 +162,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
162162
/// normally invoked directly; instead, you invoke
163163
/// `GoalData::intern` (which will ultimately call this
164164
/// method).
165-
fn intern_goal(data: GoalData<Self>) -> Self::InternedGoal;
165+
fn intern_goal(&self, data: GoalData<Self>) -> Self::InternedGoal;
166166

167167
/// Lookup the `GoalData` that was interned to create a `InternedGoal`.
168168
fn goal_data(goal: &Self::InternedGoal) -> &GoalData<Self>;
@@ -295,7 +295,7 @@ mod default {
295295
parameter
296296
}
297297

298-
fn intern_goal(goal: GoalData<ChalkIr>) -> Arc<GoalData<ChalkIr>> {
298+
fn intern_goal(&self, goal: GoalData<ChalkIr>) -> Arc<GoalData<ChalkIr>> {
299299
Arc::new(goal)
300300
}
301301

‎chalk-ir/src/lib.rs

Lines changed: 19 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1071,29 +1071,34 @@ pub struct Goal<I: Interner> {
10711071
}
10721072

10731073
impl<I: Interner> Goal<I> {
1074-
pub fn new(interned: GoalData<I>) -> Self {
1075-
let interned = I::intern_goal(interned);
1074+
pub fn new(interner: &I, interned: GoalData<I>) -> Self {
1075+
let interned = I::intern_goal(interner, interned);
10761076
Self { interned }
10771077
}
10781078

10791079
pub fn data(&self) -> &GoalData<I> {
10801080
I::goal_data(&self.interned)
10811081
}
10821082

1083-
pub fn quantify(self, kind: QuantifierKind, binders: Vec<ParameterKind<()>>) -> Goal<I> {
1083+
pub fn quantify(
1084+
self,
1085+
interner: &I,
1086+
kind: QuantifierKind,
1087+
binders: Vec<ParameterKind<()>>,
1088+
) -> Goal<I> {
10841089
GoalData::Quantified(
10851090
kind,
10861091
Binders {
10871092
value: self,
10881093
binders,
10891094
},
10901095
)
1091-
.intern()
1096+
.intern(interner)
10921097
}
10931098

10941099
/// Takes a goal `G` and turns it into `not { G }`
1095-
pub fn negate(self) -> Self {
1096-
GoalData::Not(self).intern()
1100+
pub fn negate(self, interner: &I) -> Self {
1101+
GoalData::Not(self).intern(interner)
10971102
}
10981103

10991104
/// Takes a goal `G` and turns it into `compatible { G }`
@@ -1114,14 +1119,14 @@ impl<I: Interner> Goal<I> {
11141119
],
11151120
goal,
11161121
)
1117-
.intern()
1122+
.intern(interner)
11181123
}),
11191124
)
1120-
.intern()
1125+
.intern(interner)
11211126
}
11221127

1123-
pub fn implied_by(self, predicates: Vec<ProgramClause<I>>) -> Goal<I> {
1124-
GoalData::Implies(predicates, self).intern()
1128+
pub fn implied_by(self, interner: &I, predicates: Vec<ProgramClause<I>>) -> Goal<I> {
1129+
GoalData::Implies(predicates, self).intern(interner)
11251130
}
11261131

11271132
/// True if this goal is "trivially true" -- i.e., no work is
@@ -1150,14 +1155,14 @@ where
11501155
interner,
11511156
Some(goal0).into_iter().chain(Some(goal1)).chain(iter),
11521157
);
1153-
GoalData::All(goals).intern()
1158+
GoalData::All(goals).intern(interner)
11541159
} else {
11551160
// One goal to prove
11561161
goal0
11571162
}
11581163
} else {
11591164
// No goals to prove, always true
1160-
GoalData::All(Goals::new(interner)).intern()
1165+
GoalData::All(Goals::new(interner)).intern(interner)
11611166
}
11621167
}
11631168
}
@@ -1192,8 +1197,8 @@ pub enum GoalData<I: Interner> {
11921197
}
11931198

11941199
impl<I: Interner> GoalData<I> {
1195-
pub fn intern(self) -> Goal<I> {
1196-
Goal::new(self)
1200+
pub fn intern(self, interner: &I) -> Goal<I> {
1201+
Goal::new(interner, self)
11971202
}
11981203
}
11991204

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -430,7 +430,7 @@ impl<I: Interner> ToProgramClauses<I> for TraitDatum<I> {
430430
.chain(iter::once(
431431
DomainGoal::DownstreamType(type_parameters[i].clone()).cast(interner),
432432
))
433-
.chain(iter::once(GoalData::CannotProve(()).intern())),
433+
.chain(iter::once(GoalData::CannotProve(()).intern(interner))),
434434
);
435435
}
436436

@@ -465,7 +465,7 @@ impl<I: Interner> ToProgramClauses<I> for TraitDatum<I> {
465465
.type_parameters()
466466
.map(|ty| DomainGoal::IsUpstream(ty).cast(interner)),
467467
)
468-
.chain(iter::once(GoalData::CannotProve(()).intern())),
468+
.chain(iter::once(GoalData::CannotProve(()).intern(interner))),
469469
);
470470
}
471471

‎chalk-solve/src/coherence/solve.rs

Lines changed: 15 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@ impl<I: Interner> CoherenceSolver<'_, I> {
100100
// to unify the inputs to both impls with one another
101101
let params_goals = lhs_params
102102
.zip(rhs_params)
103-
.map(|(a, b)| GoalData::EqGoal(EqGoal { a, b }).intern());
103+
.map(|(a, b)| GoalData::EqGoal(EqGoal { a, b }).intern(interner));
104104

105105
// Upshift the rhs variables in where clauses
106106
let lhs_where_clauses = lhs.binders.value.where_clauses.iter().cloned();
@@ -119,9 +119,9 @@ impl<I: Interner> CoherenceSolver<'_, I> {
119119
// Join all the goals we've created together with And, then quantify them
120120
// over the joined binders. This is our query.
121121
let goal = Box::new(Goal::all(interner, params_goals.chain(wc_goals)))
122-
.quantify(QuantifierKind::Exists, binders)
122+
.quantify(interner, QuantifierKind::Exists, binders)
123123
.compatible(interner)
124-
.negate();
124+
.negate(interner);
125125

126126
let canonical_goal = &goal.into_closed_goal(interner);
127127
let solution = self
@@ -180,7 +180,7 @@ impl<I: Interner> CoherenceSolver<'_, I> {
180180
.map(|p| p.shifted_in(interner, more_len));
181181
let params_goals = more_special_params
182182
.zip(less_special_params)
183-
.map(|(a, b)| GoalData::EqGoal(EqGoal { a, b }).intern());
183+
.map(|(a, b)| GoalData::EqGoal(EqGoal { a, b }).intern(interner));
184184

185185
// Create the where clause goals.
186186
let more_special_wc = more_special
@@ -200,9 +200,17 @@ impl<I: Interner> CoherenceSolver<'_, I> {
200200

201201
// Join all of the goals together.
202202
let goal = Box::new(Goal::all(interner, params_goals.chain(less_special_wc)))
203-
.quantify(QuantifierKind::Exists, less_special.binders.binders.clone())
204-
.implied_by(more_special_wc)
205-
.quantify(QuantifierKind::ForAll, more_special.binders.binders.clone());
203+
.quantify(
204+
interner,
205+
QuantifierKind::Exists,
206+
less_special.binders.binders.clone(),
207+
)
208+
.implied_by(interner, more_special_wc)
209+
.quantify(
210+
interner,
211+
QuantifierKind::ForAll,
212+
more_special.binders.binders.clone(),
213+
);
206214

207215
let canonical_goal = &goal.into_closed_goal(interner);
208216
let result = match self

‎chalk-solve/src/wf.rs

Lines changed: 14 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -192,8 +192,12 @@ where
192192
// We ask that the above input types are well-formed provided that all the where-clauses
193193
// on the struct definition hold.
194194
let goal = GoalData::Implies(hypotheses, goal)
195-
.intern()
196-
.quantify(QuantifierKind::ForAll, struct_datum.binders.binders.clone());
195+
.intern(interner)
196+
.quantify(
197+
interner,
198+
QuantifierKind::ForAll,
199+
struct_datum.binders.binders.clone(),
200+
);
197201

198202
let is_legal = match self
199203
.solver_choice
@@ -286,8 +290,12 @@ where
286290
.collect();
287291

288292
let goal = GoalData::Implies(hypotheses, goal)
289-
.intern()
290-
.quantify(QuantifierKind::ForAll, impl_datum.binders.binders.clone());
293+
.intern(interner)
294+
.quantify(
295+
interner,
296+
QuantifierKind::ForAll,
297+
impl_datum.binders.binders.clone(),
298+
);
291299

292300
debug!("WF trait goal: {:?}", goal);
293301

@@ -425,7 +433,7 @@ where
425433
.casted(interner)
426434
.collect();
427435

428-
let goal = GoalData::Implies(hypotheses, goal).intern();
436+
let goal = GoalData::Implies(hypotheses, goal).intern(interner);
429437

430438
// Create a composed goal that is universally quantified over
431439
// the parameters from the associated type value (e.g.,
@@ -434,6 +442,6 @@ where
434442
.db
435443
.split_associated_ty_value_parameters(&assoc_ty.value.binders, assoc_ty);
436444

437-
Some(goal.quantify(QuantifierKind::ForAll, value_binders.to_vec()))
445+
Some(goal.quantify(interner, QuantifierKind::ForAll, value_binders.to_vec()))
438446
}
439447
}

0 commit comments

Comments
 (0)