Skip to content

Commit a0350f2

Browse files
yaahcyaahc
committed
Add self param to intern_goal
1 parent 2e7f4f9 commit a0350f2

File tree

8 files changed

+42
-40
lines changed

8 files changed

+42
-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: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1071,29 +1071,29 @@ 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(self, interner: &I, kind: QuantifierKind, binders: Vec<ParameterKind<()>>) -> Goal<I> {
10841084
GoalData::Quantified(
10851085
kind,
10861086
Binders {
10871087
value: self,
10881088
binders,
10891089
},
10901090
)
1091-
.intern()
1091+
.intern(interner)
10921092
}
10931093

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

10991099
/// Takes a goal `G` and turns it into `compatible { G }`
@@ -1114,14 +1114,14 @@ impl<I: Interner> Goal<I> {
11141114
],
11151115
goal,
11161116
)
1117-
.intern()
1117+
.intern(interner)
11181118
}),
11191119
)
1120-
.intern()
1120+
.intern(interner)
11211121
}
11221122

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

11271127
/// True if this goal is "trivially true" -- i.e., no work is
@@ -1150,14 +1150,14 @@ where
11501150
interner,
11511151
Some(goal0).into_iter().chain(Some(goal1)).chain(iter),
11521152
);
1153-
GoalData::All(goals).intern()
1153+
GoalData::All(goals).intern(interner)
11541154
} else {
11551155
// One goal to prove
11561156
goal0
11571157
}
11581158
} else {
11591159
// No goals to prove, always true
1160-
GoalData::All(Goals::new(interner)).intern()
1160+
GoalData::All(Goals::new(interner)).intern(interner)
11611161
}
11621162
}
11631163
}
@@ -1192,8 +1192,8 @@ pub enum GoalData<I: Interner> {
11921192
}
11931193

11941194
impl<I: Interner> GoalData<I> {
1195-
pub fn intern(self) -> Goal<I> {
1196-
Goal::new(self)
1195+
pub fn intern(self, interner: &I) -> Goal<I> {
1196+
Goal::new(interner, self)
11971197
}
11981198
}
11991199

‎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: 7 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,9 @@ 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(interner, QuantifierKind::Exists, less_special.binders.binders.clone())
204+
.implied_by(interner, more_special_wc)
205+
.quantify(interner, QuantifierKind::ForAll, more_special.binders.binders.clone());
206206

207207
let canonical_goal = &goal.into_closed_goal(interner);
208208
let result = match self

‎chalk-solve/src/wf.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -192,8 +192,8 @@ 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(interner, QuantifierKind::ForAll, struct_datum.binders.binders.clone());
197197

198198
let is_legal = match self
199199
.solver_choice
@@ -286,8 +286,8 @@ where
286286
.collect();
287287

288288
let goal = GoalData::Implies(hypotheses, goal)
289-
.intern()
290-
.quantify(QuantifierKind::ForAll, impl_datum.binders.binders.clone());
289+
.intern(interner)
290+
.quantify(interner, QuantifierKind::ForAll, impl_datum.binders.binders.clone());
291291

292292
debug!("WF trait goal: {:?}", goal);
293293

@@ -425,7 +425,7 @@ where
425425
.casted(interner)
426426
.collect();
427427

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

430430
// Create a composed goal that is universally quantified over
431431
// the parameters from the associated type value (e.g.,
@@ -434,6 +434,6 @@ where
434434
.db
435435
.split_associated_ty_value_parameters(&assoc_ty.value.binders, assoc_ty);
436436

437-
Some(goal.quantify(QuantifierKind::ForAll, value_binders.to_vec()))
437+
Some(goal.quantify(interner, QuantifierKind::ForAll, value_binders.to_vec()))
438438
}
439439
}

0 commit comments

Comments
 (0)