Skip to content

Commit b828b09

Browse files
tirr-ctirr-c
committed
Intern ProgramClause<I>
1 parent 039fc90 commit b828b09

File tree

13 files changed

+181
-39
lines changed

13 files changed

+181
-39
lines changed

‎chalk-integration/src/lowering.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1198,7 +1198,7 @@ impl LowerClause for Clause {
11981198
.into_iter()
11991199
.map(
12001200
|implication: chalk_ir::Binders<chalk_ir::ProgramClauseImplication<ChalkIr>>| {
1201-
chalk_ir::ProgramClause::ForAll(implication)
1201+
chalk_ir::ProgramClauseData::ForAll(implication).intern(interner)
12021202
},
12031203
)
12041204
.collect();

‎chalk-integration/src/program.rs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -173,6 +173,15 @@ impl tls::DebugContext for Program {
173173
write!(fmt, "{:?}", pci.debug(interner))
174174
}
175175

176+
fn debug_program_clause(
177+
&self,
178+
clause: &ProgramClause<ChalkIr>,
179+
fmt: &mut fmt::Formatter<'_>,
180+
) -> Result<(), fmt::Error> {
181+
let interner = self.interner();
182+
write!(fmt, "{:?}", clause.data(interner))
183+
}
184+
176185
fn debug_application_ty(
177186
&self,
178187
application_ty: &ApplicationTy<ChalkIr>,

‎chalk-ir/src/cast.rs

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -183,10 +183,11 @@ where
183183
I: Interner,
184184
{
185185
fn cast_to(self, interner: &I) -> ProgramClause<I> {
186-
ProgramClause::Implies(ProgramClauseImplication {
186+
ProgramClauseData::Implies(ProgramClauseImplication {
187187
consequence: self.cast(interner),
188188
conditions: Goals::new(interner),
189189
})
190+
.intern(interner)
190191
}
191192
}
192193

@@ -196,22 +197,23 @@ where
196197
I: Interner,
197198
{
198199
fn cast_to(self, interner: &I) -> ProgramClause<I> {
199-
ProgramClause::ForAll(self.map(|bound| ProgramClauseImplication {
200+
ProgramClauseData::ForAll(self.map(|bound| ProgramClauseImplication {
200201
consequence: bound.cast(interner),
201202
conditions: Goals::new(interner),
202203
}))
204+
.intern(interner)
203205
}
204206
}
205207

206208
impl<I: Interner> CastTo<ProgramClause<I>> for ProgramClauseImplication<I> {
207-
fn cast_to(self, _interner: &I) -> ProgramClause<I> {
208-
ProgramClause::Implies(self)
209+
fn cast_to(self, interner: &I) -> ProgramClause<I> {
210+
ProgramClauseData::Implies(self).intern(interner)
209211
}
210212
}
211213

212214
impl<I: Interner> CastTo<ProgramClause<I>> for Binders<ProgramClauseImplication<I>> {
213-
fn cast_to(self, _interner: &I) -> ProgramClause<I> {
214-
ProgramClause::ForAll(self)
215+
fn cast_to(self, interner: &I) -> ProgramClause<I> {
216+
ProgramClauseData::ForAll(self).intern(interner)
215217
}
216218
}
217219

‎chalk-ir/src/could_match.rs

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -62,14 +62,20 @@ where
6262
}
6363
}
6464

65-
impl<I: Interner> CouldMatch<DomainGoal<I>> for ProgramClause<I> {
65+
impl<I: Interner> CouldMatch<DomainGoal<I>> for ProgramClauseData<I> {
6666
fn could_match(&self, interner: &I, other: &DomainGoal<I>) -> bool {
6767
match self {
68-
ProgramClause::Implies(implication) => {
68+
ProgramClauseData::Implies(implication) => {
6969
implication.consequence.could_match(interner, other)
7070
}
7171

72-
ProgramClause::ForAll(clause) => clause.value.consequence.could_match(interner, other),
72+
ProgramClauseData::ForAll(clause) => clause.value.consequence.could_match(interner, other),
7373
}
7474
}
7575
}
76+
77+
impl<I: Interner> CouldMatch<DomainGoal<I>> for ProgramClause<I> {
78+
fn could_match(&self, interner: &I, other: &DomainGoal<I>) -> bool {
79+
self.data(interner).could_match(interner, other)
80+
}
81+
}

‎chalk-ir/src/debug.rs

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,13 @@ impl<I: Interner> Debug for ProgramClauseImplication<I> {
5858
}
5959
}
6060

61+
impl<I: Interner> Debug for ProgramClause<I> {
62+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
63+
I::debug_program_clause(self, fmt)
64+
.unwrap_or_else(|| write!(fmt, "{:?}", self.clause))
65+
}
66+
}
67+
6168
impl<I: Interner> Debug for ApplicationTy<I> {
6269
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
6370
I::debug_application_ty(self, fmt).unwrap_or_else(|| write!(fmt, "ApplicationTy(?)"))
@@ -520,11 +527,11 @@ impl<T: Debug> Debug for Binders<T> {
520527
}
521528
}
522529

523-
impl<I: Interner> Debug for ProgramClause<I> {
530+
impl<I: Interner> Debug for ProgramClauseData<I> {
524531
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
525532
match self {
526-
ProgramClause::Implies(pc) => write!(fmt, "{:?}", pc),
527-
ProgramClause::ForAll(pc) => write!(fmt, "{:?}", pc),
533+
ProgramClauseData::Implies(pc) => write!(fmt, "{:?}", pc),
534+
ProgramClauseData::ForAll(pc) => write!(fmt, "{:?}", pc),
528535
}
529536
}
530537
}

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

Lines changed: 20 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -228,7 +228,7 @@ id_fold!(StructId);
228228
id_fold!(TraitId);
229229
id_fold!(AssocTypeId);
230230

231-
impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
231+
impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClauseData<I> {
232232
fn super_fold_with<'i>(
233233
&self,
234234
folder: &mut dyn Folder<'i, I, TI>,
@@ -239,16 +239,31 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
239239
TI: 'i,
240240
{
241241
match self {
242-
ProgramClause::Implies(pci) => {
243-
Ok(ProgramClause::Implies(pci.fold_with(folder, outer_binder)?))
242+
ProgramClauseData::Implies(pci) => {
243+
Ok(ProgramClauseData::Implies(pci.fold_with(folder, outer_binder)?))
244244
}
245-
ProgramClause::ForAll(pci) => {
246-
Ok(ProgramClause::ForAll(pci.fold_with(folder, outer_binder)?))
245+
ProgramClauseData::ForAll(pci) => {
246+
Ok(ProgramClauseData::ForAll(pci.fold_with(folder, outer_binder)?))
247247
}
248248
}
249249
}
250250
}
251251

252+
impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
253+
fn super_fold_with<'i>(
254+
&self,
255+
folder: &mut dyn Folder<'i, I, TI>,
256+
outer_binder: DebruijnIndex,
257+
) -> ::chalk_engine::fallible::Fallible<Self::Result>
258+
where
259+
I: 'i,
260+
TI: 'i,
261+
{
262+
let clause = self.data(folder.interner());
263+
Ok(clause.super_fold_with(folder, outer_binder)?.intern(folder.target_interner()))
264+
}
265+
}
266+
252267
impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for PhantomData<I> {
253268
type Result = PhantomData<TI>;
254269

‎chalk-ir/src/interner.rs

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ use crate::Lifetime;
88
use crate::LifetimeData;
99
use crate::Parameter;
1010
use crate::ParameterData;
11+
use crate::ProgramClause;
12+
use crate::ProgramClauseData;
1113
use crate::ProgramClauseImplication;
1214
use crate::SeparatorTraitRef;
1315
use crate::StructId;
@@ -94,6 +96,14 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
9496
/// converted back to its underlying data via `substitution_data`.
9597
type InternedSubstitution: Debug + Clone + Eq + Hash;
9698

99+
/// "Interned" representation of a "program clause". In normal user code,
100+
/// `Self::InternedProgramClause` is not referenced. Instead, we refer to
101+
/// `ProgramClause<Self>`, which wraps this type.
102+
///
103+
/// An `InternedProgramClause` is created by `intern_program_clause` and can be
104+
/// converted back to its underlying data via `program_clause_data`.
105+
type InternedProgramClause: Debug + Clone + Eq + Hash;
106+
97107
/// The core "id" type used for struct-ids and the like.
98108
type DefId: Debug + Copy + Eq + Ord + Hash;
99109

@@ -234,6 +244,21 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
234244
None
235245
}
236246

247+
/// Prints the debug representation of a ProgramClause. To get good
248+
/// results, this requires inspecting TLS, and is difficult to
249+
/// code without reference to a specific interner (and hence
250+
/// fully known types).
251+
///
252+
/// Returns `None` to fallback to the default debug output (e.g.,
253+
/// if no info about current program is available from TLS).
254+
#[allow(unused_variables)]
255+
fn debug_program_clause(
256+
clause: &ProgramClause<Self>,
257+
fmt: &mut fmt::Formatter<'_>,
258+
) -> Option<fmt::Result> {
259+
None
260+
}
261+
237262
/// Prints the debug representation of an ApplicationTy. To get good
238263
/// results, this requires inspecting TLS, and is difficult to
239264
/// code without reference to a specific interner (and hence
@@ -337,6 +362,18 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
337362
&self,
338363
substitution: &'a Self::InternedSubstitution,
339364
) -> &'a [Parameter<Self>];
365+
366+
/// Create an "interned" program clause from `data`. This is not
367+
/// normally invoked directly; instead, you invoke
368+
/// `ProgramClauseData::intern` (which will ultimately call this
369+
/// method).
370+
fn intern_program_clause(&self, data: ProgramClauseData<Self>) -> Self::InternedProgramClause;
371+
372+
/// Lookup the `ProgramClauseData` that was interned to create a `ProgramClause`.
373+
fn program_clause_data<'a>(
374+
&self,
375+
clause: &'a Self::InternedProgramClause,
376+
) -> &'a ProgramClauseData<Self>;
340377
}
341378

342379
pub trait TargetInterner<I: Interner>: Interner {
@@ -391,6 +428,7 @@ mod default {
391428
type InternedGoal = Arc<GoalData<ChalkIr>>;
392429
type InternedGoals = Vec<Goal<ChalkIr>>;
393430
type InternedSubstitution = Vec<Parameter<ChalkIr>>;
431+
type InternedProgramClause = ProgramClauseData<ChalkIr>;
394432
type DefId = RawId;
395433
type Identifier = Identifier;
396434

@@ -459,6 +497,13 @@ mod default {
459497
tls::with_current_program(|prog| Some(prog?.debug_program_clause_implication(pci, fmt)))
460498
}
461499

500+
fn debug_program_clause(
501+
clause: &ProgramClause<ChalkIr>,
502+
fmt: &mut fmt::Formatter<'_>,
503+
) -> Option<fmt::Result> {
504+
tls::with_current_program(|prog| Some(prog?.debug_program_clause(clause, fmt)))
505+
}
506+
462507
fn debug_application_ty(
463508
application_ty: &ApplicationTy<ChalkIr>,
464509
fmt: &mut fmt::Formatter<'_>,
@@ -544,6 +589,20 @@ mod default {
544589
) -> &'a [Parameter<ChalkIr>] {
545590
substitution
546591
}
592+
593+
fn intern_program_clause(
594+
&self,
595+
data: ProgramClauseData<Self>,
596+
) -> ProgramClauseData<Self> {
597+
data
598+
}
599+
600+
fn program_clause_data<'a>(
601+
&self,
602+
clause: &'a ProgramClauseData<Self>,
603+
) -> &'a ProgramClauseData<Self> {
604+
clause
605+
}
547606
}
548607

549608
impl HasInterner for ChalkIr {

‎chalk-ir/src/lib.rs

Lines changed: 33 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1208,8 +1208,8 @@ pub struct ProgramClauseImplication<I: Interner> {
12081208
pub conditions: Goals<I>,
12091209
}
12101210

1211-
#[derive(Clone, PartialEq, Eq, Hash, HasInterner)]
1212-
pub enum ProgramClause<I: Interner> {
1211+
#[derive(Clone, PartialEq, Eq, Hash, Fold, HasInterner)]
1212+
pub enum ProgramClauseData<I: Interner> {
12131213
Implies(ProgramClauseImplication<I>),
12141214
ForAll(Binders<ProgramClauseImplication<I>>),
12151215
}
@@ -1227,17 +1227,42 @@ impl<I: Interner> ProgramClauseImplication<I> {
12271227
}
12281228
}
12291229

1230-
impl<I: Interner> ProgramClause<I> {
1231-
pub fn into_from_env_clause(self, interner: &I) -> ProgramClause<I> {
1230+
impl<I: Interner> ProgramClauseData<I> {
1231+
pub fn into_from_env_clause(self, interner: &I) -> ProgramClauseData<I> {
12321232
match self {
1233-
ProgramClause::Implies(implication) => {
1234-
ProgramClause::Implies(implication.into_from_env_clause(interner))
1233+
ProgramClauseData::Implies(implication) => {
1234+
ProgramClauseData::Implies(implication.into_from_env_clause(interner))
12351235
}
1236-
ProgramClause::ForAll(binders_implication) => {
1237-
ProgramClause::ForAll(binders_implication.map(|i| i.into_from_env_clause(interner)))
1236+
ProgramClauseData::ForAll(binders_implication) => {
1237+
ProgramClauseData::ForAll(binders_implication.map(|i| i.into_from_env_clause(interner)))
12381238
}
12391239
}
12401240
}
1241+
1242+
pub fn intern(self, interner: &I) -> ProgramClause<I> {
1243+
ProgramClause {
1244+
clause: interner.intern_program_clause(self),
1245+
}
1246+
}
1247+
}
1248+
1249+
#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
1250+
pub struct ProgramClause<I: Interner> {
1251+
clause: I::InternedProgramClause,
1252+
}
1253+
1254+
impl<I: Interner> ProgramClause<I> {
1255+
pub fn into_from_env_clause(self, interner: &I) -> ProgramClause<I> {
1256+
let program_clause_data = self.data(interner);
1257+
let new_clause = program_clause_data.clone().into_from_env_clause(interner);
1258+
ProgramClause {
1259+
clause: interner.intern_program_clause(new_clause),
1260+
}
1261+
}
1262+
1263+
pub fn data(&self, interner: &I) -> &ProgramClauseData<I> {
1264+
interner.program_clause_data(&self.clause)
1265+
}
12411266
}
12421267

12431268
/// Wraps a "canonicalized item". Items are canonicalized as follows:

‎chalk-ir/src/tls.rs

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
use crate::interner::ChalkIr;
22
use crate::{
33
debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, Lifetime,
4-
Parameter, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
4+
Parameter, ProgramClause, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
55
};
66
use std::cell::RefCell;
77
use std::fmt;
@@ -68,6 +68,12 @@ pub trait DebugContext {
6868
fmt: &mut fmt::Formatter<'_>,
6969
) -> Result<(), fmt::Error>;
7070

71+
fn debug_program_clause(
72+
&self,
73+
clause: &ProgramClause<ChalkIr>,
74+
fmt: &mut fmt::Formatter<'_>,
75+
) -> Result<(), fmt::Error>;
76+
7177
fn debug_application_ty(
7278
&self,
7379
application_ty: &ApplicationTy<ChalkIr>,

‎chalk-ir/src/zip.rs

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -309,7 +309,7 @@ enum_zip!(impl<I> for DomainGoal<I> {
309309
Compatible,
310310
DownstreamType
311311
});
312-
enum_zip!(impl<I> for ProgramClause<I> { Implies, ForAll });
312+
enum_zip!(impl<I> for ProgramClauseData<I> { Implies, ForAll });
313313

314314
impl<I: Interner> Zip<I> for Substitution<I> {
315315
fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()>
@@ -396,3 +396,13 @@ impl<I: Interner> Zip<I> for Parameter<I> {
396396
Zip::zip_with(zipper, a.data(interner), b.data(interner))
397397
}
398398
}
399+
400+
impl<I: Interner> Zip<I> for ProgramClause<I> {
401+
fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()>
402+
where
403+
I: 'i,
404+
{
405+
let interner = zipper.interner();
406+
Zip::zip_with(zipper, a.data(interner), b.data(interner))
407+
}
408+
}

0 commit comments

Comments
 (0)