Skip to content

Commit 30efe09

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #370 from tirr-c/intern-program-clause
Intern Vec<ProgramClause<I>>
2 parents 039fc90 + 6ad46a2 commit 30efe09

File tree

21 files changed

+429
-94
lines changed

21 files changed

+429
-94
lines changed

‎chalk-engine/src/context.rs

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

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

157-
// Used by: simplify
158-
fn add_clauses(env: &Self::Environment, clauses: Self::ProgramClauses) -> Self::Environment;
159-
160157
/// Selects the next appropriate subgoal index for evaluation.
161158
/// Used by: logic
162159
fn next_subgoal_index(ex_clause: &ExClause<Self>) -> usize;
@@ -180,6 +177,9 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
180177
infer: &mut C::InferenceTable,
181178
) -> Result<Vec<C::ProgramClause>, Floundered>;
182179

180+
// Used by: simplify
181+
fn add_clauses(&self, env: &C::Environment, clauses: C::ProgramClauses) -> C::Environment;
182+
183183
/// Create an inference table for processing a new goal and instantiate that goal
184184
/// in that context, returning "all the pieces".
185185
///

‎chalk-engine/src/simplify.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ impl<C: Context> Forest<C> {
4141
pending_goals.push((environment, context.into_hh_goal(subgoal)))
4242
}
4343
HhGoal::Implies(wc, subgoal) => {
44-
let new_environment = C::add_clauses(&environment, wc);
44+
let new_environment = context.add_clauses(&environment, wc);
4545
pending_goals.push((new_environment, context.into_hh_goal(subgoal)));
4646
}
4747
HhGoal::All(subgoals) => {

‎chalk-integration/src/lowering.rs

Lines changed: 5 additions & 4 deletions
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();
@@ -1303,11 +1303,12 @@ impl<'k> LowerGoal<Env<'k>> for Goal {
13031303
// `T: Trait<Assoc = U>` to `FromEnv(T: Trait)` and `FromEnv(T: Trait<Assoc = U>)`
13041304
// in the assumptions of an `if` goal, e.g. `if (T: Trait) { ... }` lowers to
13051305
// `if (FromEnv(T: Trait)) { ... /* this part is untouched */ ... }`.
1306-
let where_clauses: LowerResult<Vec<_>> = hyp
1306+
let where_clauses = hyp
13071307
.into_iter()
13081308
.flat_map(|h| h.lower_clause(env).apply_result())
1309-
.map(|result| result.map(|h| h.into_from_env_clause(interner)))
1310-
.collect();
1309+
.map(|result| result.map(|h| h.into_from_env_clause(interner)));
1310+
let where_clauses =
1311+
chalk_ir::ProgramClauses::from_fallible(interner, where_clauses);
13111312
Ok(chalk_ir::GoalData::Implies(where_clauses?, g.lower(env)?).intern(interner))
13121313
}
13131314
Goal::And(g1, g2s) => {

‎chalk-integration/src/program.rs

Lines changed: 20 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ use chalk_ir::interner::ChalkIr;
55
use chalk_ir::tls;
66
use chalk_ir::{
77
debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplId, Lifetime,
8-
Parameter, ProgramClause, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
9-
TyData, TypeName,
8+
Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, StructId, Substitution,
9+
TraitId, Ty, TyData, TypeName,
1010
};
1111
use chalk_rust_ir::{
1212
AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum,
@@ -173,6 +173,24 @@ 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+
185+
fn debug_program_clauses(
186+
&self,
187+
clauses: &ProgramClauses<ChalkIr>,
188+
fmt: &mut fmt::Formatter<'_>,
189+
) -> Result<(), fmt::Error> {
190+
let interner = self.interner();
191+
write!(fmt, "{:?}", clauses.as_slice(interner))
192+
}
193+
176194
fn debug_application_ty(
177195
&self,
178196
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: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -62,14 +62,22 @@ 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) => {
73+
clause.value.consequence.could_match(interner, other)
74+
}
7375
}
7476
}
7577
}
78+
79+
impl<I: Interner> CouldMatch<DomainGoal<I>> for ProgramClause<I> {
80+
fn could_match(&self, interner: &I, other: &DomainGoal<I>) -> bool {
81+
self.data(interner).could_match(interner, other)
82+
}
83+
}

‎chalk-ir/src/debug.rs

Lines changed: 15 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,18 @@ 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).unwrap_or_else(|| write!(fmt, "{:?}", self.interned))
64+
}
65+
}
66+
67+
impl<I: Interner> Debug for ProgramClauses<I> {
68+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
69+
I::debug_program_clauses(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.interned))
70+
}
71+
}
72+
6173
impl<I: Interner> Debug for ApplicationTy<I> {
6274
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
6375
I::debug_application_ty(self, fmt).unwrap_or_else(|| write!(fmt, "ApplicationTy(?)"))
@@ -520,11 +532,11 @@ impl<T: Debug> Debug for Binders<T> {
520532
}
521533
}
522534

523-
impl<I: Interner> Debug for ProgramClause<I> {
535+
impl<I: Interner> Debug for ProgramClauseData<I> {
524536
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
525537
match self {
526-
ProgramClause::Implies(pc) => write!(fmt, "{:?}", pc),
527-
ProgramClause::ForAll(pc) => write!(fmt, "{:?}", pc),
538+
ProgramClauseData::Implies(pc) => write!(fmt, "{:?}", pc),
539+
ProgramClauseData::ForAll(pc) => write!(fmt, "{:?}", pc),
528540
}
529541
}
530542
}

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

Lines changed: 44 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -172,6 +172,26 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Goals<I> {
172172
}
173173
}
174174

175+
impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for ProgramClauses<I> {
176+
type Result = ProgramClauses<TI>;
177+
fn fold_with<'i>(
178+
&self,
179+
folder: &mut dyn Folder<'i, I, TI>,
180+
outer_binder: DebruijnIndex,
181+
) -> Fallible<Self::Result>
182+
where
183+
I: 'i,
184+
TI: 'i,
185+
{
186+
let interner = folder.interner();
187+
let target_interner = folder.target_interner();
188+
let folded = self
189+
.iter(interner)
190+
.map(|p| p.fold_with(folder, outer_binder));
191+
Ok(ProgramClauses::from_fallible(target_interner, folded)?)
192+
}
193+
}
194+
175195
#[macro_export]
176196
macro_rules! copy_fold {
177197
($t:ty) => {
@@ -228,7 +248,7 @@ id_fold!(StructId);
228248
id_fold!(TraitId);
229249
id_fold!(AssocTypeId);
230250

231-
impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
251+
impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClauseData<I> {
232252
fn super_fold_with<'i>(
233253
&self,
234254
folder: &mut dyn Folder<'i, I, TI>,
@@ -239,16 +259,33 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
239259
TI: 'i,
240260
{
241261
match self {
242-
ProgramClause::Implies(pci) => {
243-
Ok(ProgramClause::Implies(pci.fold_with(folder, outer_binder)?))
244-
}
245-
ProgramClause::ForAll(pci) => {
246-
Ok(ProgramClause::ForAll(pci.fold_with(folder, outer_binder)?))
247-
}
262+
ProgramClauseData::Implies(pci) => Ok(ProgramClauseData::Implies(
263+
pci.fold_with(folder, outer_binder)?,
264+
)),
265+
ProgramClauseData::ForAll(pci) => Ok(ProgramClauseData::ForAll(
266+
pci.fold_with(folder, outer_binder)?,
267+
)),
248268
}
249269
}
250270
}
251271

272+
impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
273+
fn super_fold_with<'i>(
274+
&self,
275+
folder: &mut dyn Folder<'i, I, TI>,
276+
outer_binder: DebruijnIndex,
277+
) -> ::chalk_engine::fallible::Fallible<Self::Result>
278+
where
279+
I: 'i,
280+
TI: 'i,
281+
{
282+
let clause = self.data(folder.interner());
283+
Ok(clause
284+
.super_fold_with(folder, outer_binder)?
285+
.intern(folder.target_interner()))
286+
}
287+
}
288+
252289
impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for PhantomData<I> {
253290
type Result = PhantomData<TI>;
254291

0 commit comments

Comments
 (0)