Skip to content

Commit b7ed5e0

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #353 from yaahc/jane/intern-goals-data
Add self paramter to Interner::goals_data
2 parents 030aea8 + d793117 commit b7ed5e0

File tree

16 files changed

+230
-124
lines changed

16 files changed

+230
-124
lines changed

‎chalk-engine/src/context.rs

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -154,16 +154,6 @@ pub trait Context: Clone + Debug {
154154

155155
fn goal_from_goal_in_environment(goal: &Self::GoalInEnvironment) -> &Self::Goal;
156156

157-
/// Convert the context's goal type into the `HhGoal` type that
158-
/// the SLG solver understands. The expectation is that the
159-
/// context's goal type has the same set of variants, but with
160-
/// different names and a different setup. If you inspect
161-
/// `HhGoal`, you will see that this is a "shallow" or "lazy"
162-
/// conversion -- that is, we convert the outermost goal into an
163-
/// `HhGoal`, but the goals contained within are left as context
164-
/// goals.
165-
fn into_hh_goal(goal: Self::Goal) -> HhGoal<Self>;
166-
167157
// Used by: simplify
168158
fn add_clauses(env: &Self::Environment, clauses: Self::ProgramClauses) -> Self::Environment;
169159

@@ -266,6 +256,16 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
266256
u_canon: &C::UCanonicalGoalInEnvironment,
267257
canonical_subst: &C::CanonicalAnswerSubst,
268258
) -> bool;
259+
260+
/// Convert the context's goal type into the `HhGoal` type that
261+
/// the SLG solver understands. The expectation is that the
262+
/// context's goal type has the same set of variants, but with
263+
/// different names and a different setup. If you inspect
264+
/// `HhGoal`, you will see that this is a "shallow" or "lazy"
265+
/// conversion -- that is, we convert the outermost goal into an
266+
/// `HhGoal`, but the goals contained within are left as context
267+
/// goals.
268+
fn into_hh_goal(&self, goal: C::Goal) -> HhGoal<C>;
269269
}
270270

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

‎chalk-engine/src/logic.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -255,7 +255,7 @@ impl<C: Context> Forest<C> {
255255
goal: C::Goal,
256256
) {
257257
let table_ref = &mut self.tables[table];
258-
match C::into_hh_goal(goal) {
258+
match context.into_hh_goal(goal) {
259259
HhGoal::DomainGoal(domain_goal) => {
260260
match context.program_clauses(&environment, &domain_goal, &mut infer) {
261261
Ok(clauses) => {

‎chalk-engine/src/simplify.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -33,20 +33,20 @@ impl<C: Context> Forest<C> {
3333
HhGoal::ForAll(subgoal) => {
3434
let subgoal =
3535
infer.instantiate_binders_universally(context.interner(), &subgoal);
36-
pending_goals.push((environment, C::into_hh_goal(subgoal)));
36+
pending_goals.push((environment, context.into_hh_goal(subgoal)));
3737
}
3838
HhGoal::Exists(subgoal) => {
3939
let subgoal =
4040
infer.instantiate_binders_existentially(context.interner(), &subgoal);
41-
pending_goals.push((environment, C::into_hh_goal(subgoal)))
41+
pending_goals.push((environment, context.into_hh_goal(subgoal)))
4242
}
4343
HhGoal::Implies(wc, subgoal) => {
4444
let new_environment = C::add_clauses(&environment, wc);
45-
pending_goals.push((new_environment, C::into_hh_goal(subgoal)));
45+
pending_goals.push((new_environment, context.into_hh_goal(subgoal)));
4646
}
4747
HhGoal::All(subgoals) => {
4848
for subgoal in subgoals {
49-
pending_goals.push((environment.clone(), C::into_hh_goal(subgoal)));
49+
pending_goals.push((environment.clone(), context.into_hh_goal(subgoal)));
5050
}
5151
}
5252
HhGoal::Not(subgoal) => {

‎chalk-integration/src/program.rs

Lines changed: 70 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ use chalk_ir::debug::Angle;
44
use chalk_ir::interner::ChalkIr;
55
use chalk_ir::tls;
66
use chalk_ir::{
7-
AliasTy, AssocTypeId, ImplId, Lifetime, Parameter, ParameterKind, ProgramClause, StructId,
8-
TraitId, Ty, TyData, TypeName,
7+
AliasTy, AssocTypeId, Goal, GoalData, Goals, ImplId, Lifetime, Parameter, ParameterKind,
8+
ProgramClause, ProgramClauseImplication, StructId, TraitId, Ty, TyData, TypeName,
99
};
1010
use chalk_rust_ir::{
1111
AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum,
@@ -147,6 +147,74 @@ impl tls::DebugContext for Program {
147147
ParameterKind::Lifetime(n) => write!(fmt, "{:?}", n),
148148
}
149149
}
150+
151+
fn debug_goal(
152+
&self,
153+
goal: &Goal<ChalkIr>,
154+
fmt: &mut fmt::Formatter<'_>,
155+
) -> Result<(), fmt::Error> {
156+
let interner = self.interner();
157+
match goal.data(interner) {
158+
GoalData::Quantified(qkind, ref subgoal) => {
159+
write!(fmt, "{:?}<", qkind)?;
160+
for (index, binder) in subgoal.binders.iter().enumerate() {
161+
if index > 0 {
162+
write!(fmt, ", ")?;
163+
}
164+
match *binder {
165+
ParameterKind::Ty(()) => write!(fmt, "type")?,
166+
ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
167+
}
168+
}
169+
write!(fmt, "> {{ {:?} }}", subgoal.value)
170+
}
171+
GoalData::Implies(ref wc, ref g) => write!(fmt, "if ({:?}) {{ {:?} }}", wc, g),
172+
GoalData::All(ref goals) => write!(fmt, "all{:?}", goals),
173+
GoalData::Not(ref g) => write!(fmt, "not {{ {:?} }}", g),
174+
GoalData::EqGoal(ref wc) => write!(fmt, "{:?}", wc),
175+
GoalData::DomainGoal(ref wc) => write!(fmt, "{:?}", wc),
176+
GoalData::CannotProve(()) => write!(fmt, r"¯\_(ツ)_/¯"),
177+
}
178+
}
179+
180+
fn debug_goals(
181+
&self,
182+
goals: &Goals<ChalkIr>,
183+
fmt: &mut fmt::Formatter<'_>,
184+
) -> Result<(), fmt::Error> {
185+
let interner = self.interner();
186+
write!(fmt, "(")?;
187+
for (goal, index) in goals.iter(interner).zip(0..) {
188+
if index > 0 {
189+
write!(fmt, ", ")?;
190+
}
191+
write!(fmt, "{:?}", goal)?;
192+
}
193+
write!(fmt, ")")?;
194+
Ok(())
195+
}
196+
197+
fn debug_program_clause_implication(
198+
&self,
199+
pci: &ProgramClauseImplication<ChalkIr>,
200+
fmt: &mut fmt::Formatter<'_>,
201+
) -> Result<(), fmt::Error> {
202+
let interner = self.interner();
203+
write!(fmt, "{:?}", pci.consequence)?;
204+
205+
let conditions = pci.conditions.as_slice(interner);
206+
207+
let conds = conditions.len();
208+
if conds == 0 {
209+
return Ok(());
210+
}
211+
212+
write!(fmt, " :- ")?;
213+
for cond in &conditions[..conds - 1] {
214+
write!(fmt, "{:?}, ", cond)?;
215+
}
216+
write!(fmt, "{:?}", conditions[conds - 1])
217+
}
150218
}
151219

152220
impl RustIrDatabase<ChalkIr> for Program {

‎chalk-ir/src/debug.rs

Lines changed: 18 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -33,13 +33,30 @@ impl<I: Interner> Debug for Lifetime<I> {
3333
}
3434
}
3535

36-
#[allow(unreachable_code, unused_variables)]
3736
impl<I: Interner> Debug for Parameter<I> {
3837
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
3938
I::debug_parameter(self, fmt).unwrap_or_else(|| unimplemented!())
4039
}
4140
}
4241

42+
impl<I: Interner> Debug for Goal<I> {
43+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
44+
I::debug_goal(self, fmt).unwrap_or_else(|| unimplemented!())
45+
}
46+
}
47+
48+
impl<I: Interner> Debug for Goals<I> {
49+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
50+
I::debug_goals(self, fmt).unwrap_or_else(|| unimplemented!())
51+
}
52+
}
53+
54+
impl<I: Interner> Debug for ProgramClauseImplication<I> {
55+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
56+
I::debug_program_clause_implication(self, fmt).unwrap_or_else(|| unimplemented!())
57+
}
58+
}
59+
4360
impl Display for UniverseIndex {
4461
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
4562
write!(fmt, "U{}", self.counter)
@@ -264,46 +281,6 @@ impl<I: Interner> Debug for EqGoal<I> {
264281
}
265282
}
266283

267-
impl<I: Interner> Debug for Goal<I> {
268-
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
269-
match self.data() {
270-
GoalData::Quantified(qkind, ref subgoal) => {
271-
write!(fmt, "{:?}<", qkind)?;
272-
for (index, binder) in subgoal.binders.iter().enumerate() {
273-
if index > 0 {
274-
write!(fmt, ", ")?;
275-
}
276-
match *binder {
277-
ParameterKind::Ty(()) => write!(fmt, "type")?,
278-
ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
279-
}
280-
}
281-
write!(fmt, "> {{ {:?} }}", subgoal.value)
282-
}
283-
GoalData::Implies(ref wc, ref g) => write!(fmt, "if ({:?}) {{ {:?} }}", wc, g),
284-
GoalData::All(ref goals) => write!(fmt, "all{:?}", goals),
285-
GoalData::Not(ref g) => write!(fmt, "not {{ {:?} }}", g),
286-
GoalData::EqGoal(ref wc) => write!(fmt, "{:?}", wc),
287-
GoalData::DomainGoal(ref wc) => write!(fmt, "{:?}", wc),
288-
GoalData::CannotProve(()) => write!(fmt, r"¯\_(ツ)_/¯"),
289-
}
290-
}
291-
}
292-
293-
impl<I: Interner> Debug for Goals<I> {
294-
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
295-
write!(fmt, "(")?;
296-
for (goal, index) in self.iter().zip(0..) {
297-
if index > 0 {
298-
write!(fmt, ", ")?;
299-
}
300-
write!(fmt, "{:?}", goal)?;
301-
}
302-
write!(fmt, ")")?;
303-
Ok(())
304-
}
305-
}
306-
307284
impl<T: Debug> Debug for Binders<T> {
308285
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
309286
let Binders {
@@ -336,25 +313,6 @@ impl<I: Interner> Debug for ProgramClause<I> {
336313
}
337314
}
338315

339-
impl<I: Interner> Debug for ProgramClauseImplication<I> {
340-
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
341-
write!(fmt, "{:?}", self.consequence)?;
342-
343-
let conditions = self.conditions.as_slice();
344-
345-
let conds = conditions.len();
346-
if conds == 0 {
347-
return Ok(());
348-
}
349-
350-
write!(fmt, " :- ")?;
351-
for cond in &conditions[..conds - 1] {
352-
write!(fmt, "{:?}, ", cond)?;
353-
}
354-
write!(fmt, "{:?}", conditions[conds - 1])
355-
}
356-
}
357-
358316
impl<I: Interner> Debug for Environment<I> {
359317
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
360318
write!(fmt, "Env({:?})", self.clauses)

‎chalk-ir/src/fold.rs

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -413,8 +413,12 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for Goal<I> {
413413
I: 'i,
414414
TI: 'i,
415415
{
416-
let interner = folder.target_interner();
417-
Ok(Goal::new(interner, self.data().fold_with(folder, binders)?))
416+
let interner = folder.interner();
417+
let target_interner = folder.target_interner();
418+
Ok(Goal::new(
419+
target_interner,
420+
self.data(interner).fold_with(folder, binders)?,
421+
))
418422
}
419423
}
420424

‎chalk-ir/src/fold/boring_impls.rs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -158,9 +158,10 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Goals<I> {
158158
I: 'i,
159159
TI: 'i,
160160
{
161-
let interner = folder.target_interner();
162-
let folded = self.iter().map(|p| p.fold_with(folder, binders));
163-
Ok(Goals::from_fallible(interner, folded)?)
161+
let interner = folder.interner();
162+
let target_interner = folder.target_interner();
163+
let folded = self.iter(interner).map(|p| p.fold_with(folder, binders));
164+
Ok(Goals::from_fallible(target_interner, folded)?)
164165
}
165166
}
166167

‎chalk-ir/src/interner.rs

Lines changed: 54 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,12 @@ use crate::AliasTy;
22
use crate::AssocTypeId;
33
use crate::Goal;
44
use crate::GoalData;
5+
use crate::Goals;
56
use crate::Lifetime;
67
use crate::LifetimeData;
78
use crate::Parameter;
89
use crate::ParameterData;
10+
use crate::ProgramClauseImplication;
911
use crate::StructId;
1012
use crate::TraitId;
1113
use crate::Ty;
@@ -167,6 +169,36 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
167169
fmt: &mut fmt::Formatter<'_>,
168170
) -> Option<fmt::Result>;
169171

172+
/// Prints the debug representation of an goal. To get good
173+
/// results, this requires inspecting TLS, and is difficult to
174+
/// code without reference to a specific interner (and hence
175+
/// fully known types).
176+
///
177+
/// Returns `None` to fallback to the default debug output (e.g.,
178+
/// if no info about current program is available from TLS).
179+
fn debug_goal(goal: &Goal<Self>, fmt: &mut fmt::Formatter<'_>) -> Option<fmt::Result>;
180+
181+
/// Prints the debug representation of a list of goals. To get good
182+
/// results, this requires inspecting TLS, and is difficult to
183+
/// code without reference to a specific interner (and hence
184+
/// fully known types).
185+
///
186+
/// Returns `None` to fallback to the default debug output (e.g.,
187+
/// if no info about current program is available from TLS).
188+
fn debug_goals(goals: &Goals<Self>, fmt: &mut fmt::Formatter<'_>) -> Option<fmt::Result>;
189+
190+
/// Prints the debug representation of a ProgramClauseImplication. To get good
191+
/// results, this requires inspecting TLS, and is difficult to
192+
/// code without reference to a specific interner (and hence
193+
/// fully known types).
194+
///
195+
/// Returns `None` to fallback to the default debug output (e.g.,
196+
/// if no info about current program is available from TLS).
197+
fn debug_program_clause_implication(
198+
pci: &ProgramClauseImplication<Self>,
199+
fmt: &mut fmt::Formatter<'_>,
200+
) -> Option<fmt::Result>;
201+
170202
/// Create an "interned" type from `ty`. This is not normally
171203
/// invoked directly; instead, you invoke `TyData::intern` (which
172204
/// will ultimately call this method).
@@ -200,7 +232,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
200232
fn intern_goal(&self, data: GoalData<Self>) -> Self::InternedGoal;
201233

202234
/// Lookup the `GoalData` that was interned to create a `InternedGoal`.
203-
fn goal_data(goal: &Self::InternedGoal) -> &GoalData<Self>;
235+
fn goal_data<'a>(&self, goal: &'a Self::InternedGoal) -> &'a GoalData<Self>;
204236

205237
/// Create an "interned" goals from `data`. This is not
206238
/// normally invoked directly; instead, you invoke
@@ -209,7 +241,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
209241
fn intern_goals(&self, data: impl IntoIterator<Item = Goal<Self>>) -> Self::InternedGoals;
210242

211243
/// Lookup the `GoalsData` that was interned to create a `InternedGoals`.
212-
fn goals_data(goals: &Self::InternedGoals) -> &[Goal<Self>];
244+
fn goals_data<'a>(&self, goals: &'a Self::InternedGoals) -> &'a [Goal<Self>];
213245

214246
/// Create an "interned" substitution from `data`. This is not
215247
/// normally invoked directly; instead, you invoke
@@ -326,6 +358,24 @@ mod default {
326358
tls::with_current_program(|prog| Some(prog?.debug_parameter(parameter, fmt)))
327359
}
328360

361+
fn debug_goal(goal: &Goal<ChalkIr>, fmt: &mut fmt::Formatter<'_>) -> Option<fmt::Result> {
362+
tls::with_current_program(|prog| Some(prog?.debug_goal(goal, fmt)))
363+
}
364+
365+
fn debug_goals(
366+
goals: &Goals<ChalkIr>,
367+
fmt: &mut fmt::Formatter<'_>,
368+
) -> Option<fmt::Result> {
369+
tls::with_current_program(|prog| Some(prog?.debug_goals(goals, fmt)))
370+
}
371+
372+
fn debug_program_clause_implication(
373+
pci: &ProgramClauseImplication<ChalkIr>,
374+
fmt: &mut fmt::Formatter<'_>,
375+
) -> Option<fmt::Result> {
376+
tls::with_current_program(|prog| Some(prog?.debug_program_clause_implication(pci, fmt)))
377+
}
378+
329379
fn intern_ty(&self, ty: TyData<ChalkIr>) -> Arc<TyData<ChalkIr>> {
330380
Arc::new(ty)
331381
}
@@ -360,7 +410,7 @@ mod default {
360410
Arc::new(goal)
361411
}
362412

363-
fn goal_data(goal: &Arc<GoalData<ChalkIr>>) -> &GoalData<ChalkIr> {
413+
fn goal_data<'a>(&self, goal: &'a Arc<GoalData<ChalkIr>>) -> &'a GoalData<ChalkIr> {
364414
goal
365415
}
366416

@@ -371,7 +421,7 @@ mod default {
371421
data.into_iter().collect()
372422
}
373423

374-
fn goals_data(goals: &Vec<Goal<ChalkIr>>) -> &[Goal<ChalkIr>] {
424+
fn goals_data<'a>(&self, goals: &'a Vec<Goal<ChalkIr>>) -> &'a [Goal<ChalkIr>] {
375425
goals
376426
}
377427

0 commit comments

Comments
 (0)