Skip to content

Commit a090028

Browse files
committed
Start working on intern goal_data
1 parent e97cbed commit a090028

File tree

15 files changed

+109
-75
lines changed

15 files changed

+109
-75
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: 31 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, ImplId, Lifetime, Parameter, ParameterKind,
8+
ProgramClause, StructId, TraitId, Ty, TyData, TypeName,
99
};
1010
use chalk_rust_ir::{
1111
AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum,
@@ -147,6 +147,35 @@ 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+
}
150179
}
151180

152181
impl RustIrDatabase<ChalkIr> for Program {

chalk-ir/src/debug.rs

Lines changed: 6 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -33,13 +33,18 @@ 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+
4348
impl Display for UniverseIndex {
4449
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
4550
write!(fmt, "U{}", self.counter)
@@ -264,32 +269,6 @@ impl<I: Interner> Debug for EqGoal<I> {
264269
}
265270
}
266271

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-
293272
impl<I: Interner> Debug for Goals<I> {
294273
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
295274
write!(fmt, "(")?;

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/interner.rs

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -167,6 +167,15 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
167167
fmt: &mut fmt::Formatter<'_>,
168168
) -> Option<fmt::Result>;
169169

170+
/// Prints the debug representation of an goal. To get good
171+
/// results, this requires inspecting TLS, and is difficult to
172+
/// code without reference to a specific interner (and hence
173+
/// fully known types).
174+
///
175+
/// Returns `None` to fallback to the default debug output (e.g.,
176+
/// if no info about current program is available from TLS).
177+
fn debug_goal(goal: &Goal<Self>, fmt: &mut fmt::Formatter<'_>) -> Option<fmt::Result>;
178+
170179
/// Create an "interned" type from `ty`. This is not normally
171180
/// invoked directly; instead, you invoke `TyData::intern` (which
172181
/// will ultimately call this method).
@@ -200,7 +209,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
200209
fn intern_goal(&self, data: GoalData<Self>) -> Self::InternedGoal;
201210

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

205214
/// Create an "interned" goals from `data`. This is not
206215
/// normally invoked directly; instead, you invoke
@@ -326,6 +335,10 @@ mod default {
326335
tls::with_current_program(|prog| Some(prog?.debug_parameter(parameter, fmt)))
327336
}
328337

338+
fn debug_goal(goal: &Goal<ChalkIr>, fmt: &mut fmt::Formatter<'_>) -> Option<fmt::Result> {
339+
tls::with_current_program(|prog| Some(prog?.debug_goal(goal, fmt)))
340+
}
341+
329342
fn intern_ty(&self, ty: TyData<ChalkIr>) -> Arc<TyData<ChalkIr>> {
330343
Arc::new(ty)
331344
}
@@ -360,7 +373,7 @@ mod default {
360373
Arc::new(goal)
361374
}
362375

363-
fn goal_data(goal: &Arc<GoalData<ChalkIr>>) -> &GoalData<ChalkIr> {
376+
fn goal_data<'a>(&self, goal: &'a Arc<GoalData<ChalkIr>>) -> &'a GoalData<ChalkIr> {
364377
goal
365378
}
366379

chalk-ir/src/lib.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1083,8 +1083,8 @@ impl<I: Interner> Goal<I> {
10831083
Self { interned }
10841084
}
10851085

1086-
pub fn data(&self) -> &GoalData<I> {
1087-
I::goal_data(&self.interned)
1086+
pub fn data(&self, interner: &I) -> &GoalData<I> {
1087+
interner.goal_data(&self.interned)
10881088
}
10891089

10901090
pub fn quantify(
@@ -1138,8 +1138,8 @@ impl<I: Interner> Goal<I> {
11381138

11391139
/// True if this goal is "trivially true" -- i.e., no work is
11401140
/// required to prove it.
1141-
pub fn is_trivially_true(&self) -> bool {
1142-
match self.data() {
1141+
pub fn is_trivially_true(&self, interner: &I) -> bool {
1142+
match self.data(interner) {
11431143
GoalData::All(goals) => goals.is_empty(),
11441144
_ => false,
11451145
}

chalk-ir/src/tls.rs

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
use crate::interner::ChalkIr;
2-
use crate::{AliasTy, AssocTypeId, Lifetime, Parameter, StructId, TraitId, Ty};
2+
use crate::{AliasTy, AssocTypeId, Goal, Lifetime, Parameter, StructId, TraitId, Ty};
33
use std::cell::RefCell;
44
use std::fmt;
55
use std::sync::Arc;
@@ -46,6 +46,12 @@ pub trait DebugContext {
4646
parameter: &Parameter<ChalkIr>,
4747
fmt: &mut fmt::Formatter<'_>,
4848
) -> Result<(), fmt::Error>;
49+
50+
fn debug_goal(
51+
&self,
52+
goal: &Goal<ChalkIr>,
53+
fmt: &mut fmt::Formatter<'_>,
54+
) -> Result<(), fmt::Error>;
4955
}
5056

5157
pub fn with_current_program<R>(op: impl FnOnce(Option<&Arc<dyn DebugContext>>) -> R) -> R {

chalk-ir/src/zip.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -327,7 +327,8 @@ impl<I: Interner> Zip<I> for Goal<I> {
327327
where
328328
I: 'i,
329329
{
330-
Zip::zip_with(zipper, a.data(), b.data())
330+
let interner = zipper.interner();
331+
Zip::zip_with(zipper, a.data(interner), b.data(interner))
331332
}
332333
}
333334

0 commit comments

Comments
 (0)