Skip to content

Commit 31ea6d8

Browse files
authored
Merge pull request #379 from crlf0710/master
Intern `Vec<QuantifiedWhereClause<I>>`.
2 parents fd8cd45 + c94f055 commit 31ea6d8

File tree

11 files changed

+195
-11
lines changed

11 files changed

+195
-11
lines changed

chalk-integration/src/lowering.rs

+7-7
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
11
use chalk_ir::cast::{Cast, Caster};
22
use chalk_ir::interner::ChalkIr;
33
use chalk_ir::{
4-
self, AssocTypeId, BoundVar, DebruijnIndex, ImplId, StructId, Substitution, TraitId,
4+
self, AssocTypeId, BoundVar, DebruijnIndex, ImplId, QuantifiedWhereClauses, StructId,
5+
Substitution, TraitId,
56
};
67
use chalk_parse::ast::*;
78
use chalk_rust_ir as rust_ir;
@@ -1000,10 +1001,9 @@ impl LowerTy for Ty {
10001001
// FIXME: Figure out a proper name for this type parameter
10011002
Some(chalk_ir::ParameterKind::Ty(intern(FIXME_SELF))),
10021003
|env| {
1003-
Ok(bounds
1004-
.lower(env)?
1005-
.iter()
1006-
.flat_map(|qil| {
1004+
Ok(QuantifiedWhereClauses::from(
1005+
interner,
1006+
bounds.lower(env)?.iter().flat_map(|qil| {
10071007
qil.into_where_clauses(
10081008
interner,
10091009
chalk_ir::TyData::BoundVar(BoundVar::new(
@@ -1012,8 +1012,8 @@ impl LowerTy for Ty {
10121012
))
10131013
.intern(interner),
10141014
)
1015-
})
1016-
.collect())
1015+
}),
1016+
))
10171017
},
10181018
)?,
10191019
})

chalk-integration/src/program.rs

+9
Original file line numberDiff line numberDiff line change
@@ -217,6 +217,15 @@ impl tls::DebugContext for Program {
217217
let interner = self.interner();
218218
write!(fmt, "{:?}", separator_trait_ref.debug(interner))
219219
}
220+
221+
fn debug_quantified_where_clauses(
222+
&self,
223+
clauses: &chalk_ir::QuantifiedWhereClauses<ChalkIr>,
224+
fmt: &mut fmt::Formatter<'_>,
225+
) -> Result<(), fmt::Error> {
226+
let interner = self.interner();
227+
write!(fmt, "{:?}", clauses.as_slice(interner))
228+
}
220229
}
221230

222231
impl RustIrDatabase<ChalkIr> for Program {

chalk-ir/src/cast.rs

+1
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,7 @@ reflexive_impl!(for(I: Interner) DomainGoal<I>);
8181
reflexive_impl!(for(I: Interner) Goal<I>);
8282
reflexive_impl!(for(I: Interner) WhereClause<I>);
8383
reflexive_impl!(for(I: Interner) ProgramClause<I>);
84+
reflexive_impl!(for(I: Interner) QuantifiedWhereClause<I>);
8485

8586
impl<I: Interner> CastTo<WhereClause<I>> for TraitRef<I> {
8687
fn cast_to(self, _interner: &I) -> WhereClause<I> {

chalk-ir/src/debug.rs

+7
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,13 @@ impl<I: Interner> Debug for AliasTy<I> {
8989
}
9090
}
9191

92+
impl<I: Interner> Debug for QuantifiedWhereClauses<I> {
93+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
94+
I::debug_quantified_where_clauses(self, fmt)
95+
.unwrap_or_else(|| write!(fmt, "{:?}", self.interned))
96+
}
97+
}
98+
9299
impl<I: Interner> Display for Substitution<I> {
93100
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
94101
I::debug_substitution(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.parameters))

chalk-ir/src/fold/boring_impls.rs

+23
Original file line numberDiff line numberDiff line change
@@ -192,6 +192,29 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for ProgramClauses<I> {
192192
}
193193
}
194194

195+
impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for QuantifiedWhereClauses<I> {
196+
type Result = QuantifiedWhereClauses<TI>;
197+
fn fold_with<'i>(
198+
&self,
199+
folder: &mut dyn Folder<'i, I, TI>,
200+
outer_binder: DebruijnIndex,
201+
) -> Fallible<Self::Result>
202+
where
203+
I: 'i,
204+
TI: 'i,
205+
{
206+
let interner = folder.interner();
207+
let target_interner = folder.target_interner();
208+
let folded = self
209+
.iter(interner)
210+
.map(|p| p.fold_with(folder, outer_binder));
211+
Ok(QuantifiedWhereClauses::from_fallible(
212+
target_interner,
213+
folded,
214+
)?)
215+
}
216+
}
217+
195218
#[macro_export]
196219
macro_rules! copy_fold {
197220
($t:ty) => {

chalk-ir/src/interner.rs

+65
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@ use crate::ProgramClause;
1212
use crate::ProgramClauseData;
1313
use crate::ProgramClauseImplication;
1414
use crate::ProgramClauses;
15+
use crate::QuantifiedWhereClause;
16+
use crate::QuantifiedWhereClauses;
1517
use crate::SeparatorTraitRef;
1618
use crate::StructId;
1719
use crate::Substitution;
@@ -113,6 +115,14 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
113115
/// converted back to its underlying data via `program_clause_data`.
114116
type InternedProgramClause: Debug + Clone + Eq + Hash;
115117

118+
/// "Interned" representation of a list of quantified where clauses.
119+
/// In normal user code, `Self::InternedQuantifiedWhereClauses` is not referenced.
120+
/// Instead, we refer to `QuantifiedWhereClauses<Self>`, which wraps this type.
121+
///
122+
/// An `InternedQuantifiedWhereClauses` is created by `intern_quantified_where_clauses`
123+
/// and can be converted back to its underlying data via `quantified_where_clauses_data`.
124+
type InternedQuantifiedWhereClauses: Debug + Clone + Eq + Hash;
125+
116126
/// The core "id" type used for struct-ids and the like.
117127
type DefId: Debug + Copy + Eq + Ord + Hash;
118128

@@ -328,6 +338,21 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
328338
None
329339
}
330340

341+
/// Prints the debug representation of a QuantifiedWhereClauses. To get good
342+
/// results, this requires inspecting TLS, and is difficult to
343+
/// code without reference to a specific interner (and hence
344+
/// fully known types).
345+
///
346+
/// Returns `None` to fallback to the default debug output (e.g.,
347+
/// if no info about current program is available from TLS).
348+
#[allow(unused_variables)]
349+
fn debug_quantified_where_clauses(
350+
clauses: &QuantifiedWhereClauses<Self>,
351+
fmt: &mut fmt::Formatter<'_>,
352+
) -> Option<fmt::Result> {
353+
None
354+
}
355+
331356
/// Create an "interned" type from `ty`. This is not normally
332357
/// invoked directly; instead, you invoke `TyData::intern` (which
333358
/// will ultimately call this method).
@@ -413,6 +438,22 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
413438
&self,
414439
clauses: &'a Self::InternedProgramClauses,
415440
) -> &'a [ProgramClause<Self>];
441+
442+
/// Create an "interned" quantified where clauses from `data`. This is not
443+
/// normally invoked directly; instead, you invoke
444+
/// `QuantifiedWhereClauses::from` (which will ultimately call this
445+
/// method).
446+
fn intern_quantified_where_clauses(
447+
&self,
448+
data: impl IntoIterator<Item = QuantifiedWhereClause<Self>>,
449+
) -> Self::InternedQuantifiedWhereClauses;
450+
451+
/// Lookup the slice of `QuantifiedWhereClause` that was interned to
452+
/// create a `QuantifiedWhereClauses`.
453+
fn quantified_where_clauses_data<'a>(
454+
&self,
455+
clauses: &'a Self::InternedQuantifiedWhereClauses,
456+
) -> &'a [QuantifiedWhereClause<Self>];
416457
}
417458

418459
pub trait TargetInterner<I: Interner>: Interner {
@@ -469,6 +510,7 @@ mod default {
469510
type InternedSubstitution = Vec<Parameter<ChalkIr>>;
470511
type InternedProgramClause = ProgramClauseData<ChalkIr>;
471512
type InternedProgramClauses = Vec<ProgramClause<ChalkIr>>;
513+
type InternedQuantifiedWhereClauses = Vec<QuantifiedWhereClause<ChalkIr>>;
472514
type DefId = RawId;
473515
type Identifier = Identifier;
474516

@@ -574,6 +616,15 @@ mod default {
574616
})
575617
}
576618

619+
fn debug_quantified_where_clauses(
620+
clauses: &QuantifiedWhereClauses<Self>,
621+
fmt: &mut fmt::Formatter<'_>,
622+
) -> Option<fmt::Result> {
623+
tls::with_current_program(|prog| {
624+
Some(prog?.debug_quantified_where_clauses(clauses, fmt))
625+
})
626+
}
627+
577628
fn intern_ty(&self, ty: TyData<ChalkIr>) -> Arc<TyData<ChalkIr>> {
578629
Arc::new(ty)
579630
}
@@ -661,6 +712,20 @@ mod default {
661712
) -> &'a [ProgramClause<Self>] {
662713
clauses
663714
}
715+
716+
fn intern_quantified_where_clauses(
717+
&self,
718+
data: impl IntoIterator<Item = QuantifiedWhereClause<Self>>,
719+
) -> Self::InternedQuantifiedWhereClauses {
720+
data.into_iter().collect()
721+
}
722+
723+
fn quantified_where_clauses_data<'a>(
724+
&self,
725+
clauses: &'a Self::InternedQuantifiedWhereClauses,
726+
) -> &'a [QuantifiedWhereClause<Self>] {
727+
clauses
728+
}
664729
}
665730

666731
impl HasInterner for ChalkIr {

chalk-ir/src/lib.rs

+57-1
Original file line numberDiff line numberDiff line change
@@ -543,7 +543,7 @@ impl DebruijnIndex {
543543
/// level of binder).
544544
#[derive(Clone, PartialEq, Eq, Hash, Fold)]
545545
pub struct DynTy<I: Interner> {
546-
pub bounds: Binders<Vec<QuantifiedWhereClause<I>>>,
546+
pub bounds: Binders<QuantifiedWhereClauses<I>>,
547547
}
548548

549549
#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
@@ -1033,6 +1033,62 @@ impl<I: Interner> QuantifiedWhereClause<I> {
10331033
}
10341034
}
10351035

1036+
#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
1037+
pub struct QuantifiedWhereClauses<I: Interner> {
1038+
interned: I::InternedQuantifiedWhereClauses,
1039+
}
1040+
1041+
impl<I: Interner> QuantifiedWhereClauses<I> {
1042+
pub fn new(interner: &I) -> Self {
1043+
Self::from(interner, None::<QuantifiedWhereClause<I>>)
1044+
}
1045+
1046+
pub fn interned(&self) -> &I::InternedQuantifiedWhereClauses {
1047+
&self.interned
1048+
}
1049+
1050+
pub fn from(
1051+
interner: &I,
1052+
clauses: impl IntoIterator<Item = impl CastTo<QuantifiedWhereClause<I>>>,
1053+
) -> Self {
1054+
use crate::cast::Caster;
1055+
QuantifiedWhereClauses {
1056+
interned: I::intern_quantified_where_clauses(
1057+
interner,
1058+
clauses.into_iter().casted(interner),
1059+
),
1060+
}
1061+
}
1062+
1063+
pub fn from_fallible<E>(
1064+
interner: &I,
1065+
clauses: impl IntoIterator<Item = Result<impl CastTo<QuantifiedWhereClause<I>>, E>>,
1066+
) -> Result<Self, E> {
1067+
use crate::cast::Caster;
1068+
let clauses = clauses
1069+
.into_iter()
1070+
.casted(interner)
1071+
.collect::<Result<Vec<QuantifiedWhereClause<I>>, _>>()?;
1072+
Ok(Self::from(interner, clauses))
1073+
}
1074+
1075+
pub fn iter(&self, interner: &I) -> std::slice::Iter<'_, QuantifiedWhereClause<I>> {
1076+
self.as_slice(interner).iter()
1077+
}
1078+
1079+
pub fn is_empty(&self, interner: &I) -> bool {
1080+
self.as_slice(interner).is_empty()
1081+
}
1082+
1083+
pub fn len(&self, interner: &I) -> usize {
1084+
self.as_slice(interner).len()
1085+
}
1086+
1087+
pub fn as_slice(&self, interner: &I) -> &[QuantifiedWhereClause<I>] {
1088+
interner.quantified_where_clauses_data(&self.interned)
1089+
}
1090+
}
1091+
10361092
impl<I: Interner> DomainGoal<I> {
10371093
/// Convert `Implemented(...)` into `FromEnv(...)`, but leave other
10381094
/// goals unchanged.

chalk-ir/src/tls.rs

+8-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
use crate::interner::ChalkIr;
22
use crate::{
33
debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, Lifetime,
4-
Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, StructId, Substitution,
5-
TraitId, Ty,
4+
Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, QuantifiedWhereClauses,
5+
StructId, Substitution, TraitId, Ty,
66
};
77
use std::cell::RefCell;
88
use std::fmt;
@@ -98,6 +98,12 @@ pub trait DebugContext {
9898
separator_trait_ref: &SeparatorTraitRef<'_, ChalkIr>,
9999
fmt: &mut fmt::Formatter<'_>,
100100
) -> Result<(), fmt::Error>;
101+
102+
fn debug_quantified_where_clauses(
103+
&self,
104+
clauses: &QuantifiedWhereClauses<ChalkIr>,
105+
fmt: &mut fmt::Formatter<'_>,
106+
) -> Result<(), fmt::Error>;
101107
}
102108

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

chalk-ir/src/zip.rs

+11
Original file line numberDiff line numberDiff line change
@@ -283,6 +283,17 @@ impl<I: Interner> Zip<I> for ProgramClauses<I> {
283283
}
284284
}
285285

286+
impl<I: Interner> Zip<I> for QuantifiedWhereClauses<I> {
287+
fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()>
288+
where
289+
I: 'i,
290+
{
291+
let interner = zipper.interner();
292+
Zip::zip_with(zipper, a.as_slice(interner), b.as_slice(interner))?;
293+
Ok(())
294+
}
295+
}
296+
286297
/// Generates a Zip impl that requires the two enums be the same
287298
/// variant, then zips each field of the variant in turn. Only works
288299
/// if all variants have a single parenthesized value right now.

chalk-solve/src/clauses.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -222,7 +222,7 @@ fn program_clauses_that_could_match<I: Interner>(
222222
// and `bounded_ty` is the `exists<T> { .. }`
223223
// clauses shown above.
224224

225-
for exists_qwc in &dyn_ty.bounds {
225+
for exists_qwc in dyn_ty.bounds.map_ref(|r| r.iter(interner)) {
226226
// Replace the `T` from `exists<T> { .. }` with `self_ty`,
227227
// yielding clases like
228228
//

chalk-solve/src/wf.rs

+6
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,12 @@ impl<I: Interner> FoldInputTypes for Substitution<I> {
7878
}
7979
}
8080

81+
impl<I: Interner> FoldInputTypes for QuantifiedWhereClauses<I> {
82+
fn fold(&self, interner: &I, accumulator: &mut Vec<Ty<I>>) {
83+
self.as_slice(interner).fold(interner, accumulator)
84+
}
85+
}
86+
8187
impl<I: Interner> FoldInputTypes for Ty<I> {
8288
fn fold(&self, interner: &I, accumulator: &mut Vec<Ty<I>>) {
8389
match self.data(interner) {

0 commit comments

Comments
 (0)