Skip to content

Commit eea51d7

Browse files
basil-cowbasil-cow
committed
alias eq goals
1 parent 95a5e08 commit eea51d7

File tree

4 files changed

+72
-69
lines changed

4 files changed

+72
-69
lines changed

‎chalk-solve/src/clauses/builder.rs‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,11 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
8080
let clause = if self.binders.len() == 0 {
8181
ProgramClauseData::Implies(clause).intern(interner)
8282
} else {
83-
ProgramClauseData::ForAll(Binders::new(ParameterKinds::from(interner, self.binders.clone()), clause)).intern(interner)
83+
ProgramClauseData::ForAll(Binders::new(
84+
ParameterKinds::from(interner, self.binders.clone()),
85+
clause,
86+
))
87+
.intern(interner)
8488
};
8589

8690
self.clauses.push(syn_eq_lower(interner, &clause));

‎chalk-solve/src/clauses/program_clauses.rs‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -735,6 +735,7 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
735735

736736
// add new type parameter U
737737
builder.push_bound_ty(|builder, ty| {
738+
let alias = AliasTy::Projection(projection.clone());
738739
// `Normalize(<T as Foo>::Assoc -> U)`
739740
let normalize = Normalize {
740741
alias: AliasTy::Projection(projection.clone()),
@@ -743,8 +744,8 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
743744

744745
// `AliasEq(<T as Foo>::Assoc = U)`
745746
let projection_eq = AliasEq {
746-
alias: AliasTy::Projection(projection),
747-
ty,
747+
alias: alias.clone(),
748+
ty: ty.clone(),
748749
};
749750

750751
// Projection equality rule from above.
@@ -753,7 +754,7 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
753754
// AliasEq(<T as Foo>::Assoc = U) :-
754755
// Normalize(<T as Foo>::Assoc -> U).
755756
// }
756-
builder.push_clause(projection_eq, Some(normalize));
757+
builder.push_clause(projection_eq.clone(), Some(normalize));
757758
});
758759
});
759760
}

‎chalk-solve/src/clauses/syntactic_eq.rs‎

Lines changed: 59 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -2,49 +2,34 @@ use std::{iter, mem::replace};
22

33
use chalk_engine::fallible::Fallible;
44
use chalk_ir::{
5+
cast::Cast,
56
fold::{shift::Shift, Fold, Folder, SuperFold},
67
interner::Interner,
7-
Binders, BoundVar, DebruijnIndex, EqGoal, Goal, GoalData, Goals, Parameter, ProgramClause,
8-
ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty, TyData, ParameterKind, ApplicationTy, TypeName,
9-
ParameterKinds,
8+
AliasEq, Binders, BoundVar, DebruijnIndex, Goal, GoalData, Goals, ParameterKind,
9+
ParameterKinds, ProgramClause, ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty,
10+
TyData, AliasTy
1011
};
1112

12-
pub fn syn_eq_lower<I: Interner>(interner: &I, clause: &ProgramClause<I>) -> ProgramClause<I> {
13+
pub fn syn_eq_lower<I: Interner, T: Fold<I>>(interner: &I, clause: &T) -> <T as Fold<I>>::Result {
1314
let mut folder = SynEqFolder {
1415
interner,
1516
new_params: vec![],
17+
new_goals: vec![],
1618
binders_len: 0,
1719
};
1820

19-
clause.fold_with(&mut folder, DebruijnIndex::INNERMOST).unwrap()
21+
clause
22+
.fold_with(&mut folder, DebruijnIndex::INNERMOST)
23+
.unwrap()
2024
}
2125

2226
struct SynEqFolder<'i, I: Interner> {
2327
interner: &'i I,
24-
new_params: Vec<Parameter<I>>,
28+
new_params: Vec<ParameterKind<()>>,
29+
new_goals: Vec<Goal<I>>,
2530
binders_len: usize,
2631
}
2732

28-
impl<'i, I: Interner> SynEqFolder<'i, I>
29-
where
30-
I: 'i,
31-
{
32-
fn to_eq_goals(&self, new_params: Vec<Parameter<I>>, old_len: usize) -> impl Iterator<Item = Goal<I>> + 'i {
33-
let interner = self.interner;
34-
new_params.into_iter().enumerate().map(move |(i, p)| {
35-
let var = BoundVar {
36-
debruijn: DebruijnIndex::INNERMOST,
37-
index: i + old_len,
38-
};
39-
GoalData::EqGoal(EqGoal {
40-
a: p.replace_bound(var, interner),
41-
b: p,
42-
})
43-
.intern(interner)
44-
})
45-
}
46-
}
47-
4833
impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> {
4934
fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> {
5035
self
@@ -54,14 +39,23 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> {
5439
let interner = self.interner;
5540
let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, self.binders_len);
5641

57-
let folded = ty.super_fold_with(self, outer_binder)?;
58-
match folded.data(interner) {
59-
TyData::Apply(ApplicationTy { name: TypeName::AssociatedType(_), .. }) => {
60-
self.new_params.push(ParameterKind::Ty(ty.clone()).intern(interner));
42+
let new_ty = TyData::BoundVar(bound_var).intern(interner);
43+
match ty.data(interner) {
44+
TyData::Alias(alias @ AliasTy::Projection(_)) => {
45+
self.new_params.push(ParameterKind::Ty(()));
46+
self.new_goals.push(
47+
AliasEq {
48+
alias: alias.clone(),
49+
ty: new_ty.clone(),
50+
}
51+
.cast(interner),
52+
);
6153
self.binders_len += 1;
62-
Ok(TyData::BoundVar(bound_var).intern(interner))
54+
ty.super_fold_with(self, outer_binder)?;
55+
Ok(new_ty)
6356
}
64-
_ => ty.super_fold_with(self, outer_binder),
57+
TyData::Function(_) => Ok(ty.clone()),
58+
_ => Ok(ty.super_fold_with(self, outer_binder)?),
6559
}
6660
}
6761

@@ -73,42 +67,46 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> {
7367
let interner = self.interner;
7468

7569
let ((binders, implication), in_binders) = match clause.data(interner) {
76-
ProgramClauseData::ForAll(for_all) => {
77-
(for_all.clone().into(), true)
78-
}
70+
ProgramClauseData::ForAll(for_all) => (for_all.clone().into(), true),
7971
// introduce a dummy binder and shift implication through it
80-
ProgramClauseData::Implies(implication) => ((ParameterKinds::new(interner), implication.shifted_in(interner)), false),
72+
ProgramClauseData::Implies(implication) => (
73+
(
74+
ParameterKinds::new(interner),
75+
implication.shifted_in(interner),
76+
),
77+
false,
78+
),
8179
};
8280
let mut binders: Vec<_> = binders.as_slice(interner).clone().into();
83-
81+
8482
let outer_binder = outer_binder.shifted_in();
8583

8684
self.binders_len = binders.len();
8785
let consequence = implication.consequence.fold_with(self, outer_binder)?;
8886
// Immediately move `new_params` out of of the folder struct so it's safe
8987
// to call `.fold_with` again
9088
let new_params = replace(&mut self.new_params, vec![]);
91-
89+
let new_goals = replace(&mut self.new_goals, vec![]);
90+
9291
let mut conditions = implication.conditions.fold_with(self, outer_binder)?;
9392
if new_params.is_empty() && !in_binders {
9493
// shift the clause out since we didn't use the dummy binder
95-
return Ok(ProgramClauseData::Implies(ProgramClauseImplication {
96-
consequence,
97-
conditions,
98-
priority: implication.priority,
99-
}.shifted_out(interner)?)
94+
return Ok(ProgramClauseData::Implies(
95+
ProgramClauseImplication {
96+
consequence,
97+
conditions,
98+
priority: implication.priority,
99+
}
100+
.shifted_out(interner)?,
101+
)
100102
.intern(interner));
101103
}
102104

103-
let old_len = binders.len();
104-
binders.extend(new_params.iter().map(|p| p.data(interner).anonymize()));
105+
binders.extend(new_params.into_iter());
105106

106107
conditions = Goals::from(
107108
interner,
108-
conditions
109-
.iter(interner)
110-
.cloned()
111-
.chain(self.to_eq_goals(new_params, old_len)),
109+
conditions.iter(interner).cloned().chain(new_goals),
112110
);
113111

114112
Ok(ProgramClauseData::ForAll(Binders::new(
@@ -126,37 +124,35 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> {
126124
assert!(self.new_params.is_empty(), true);
127125

128126
let interner = self.interner;
129-
let domain_goal = match goal.data(interner) {
130-
GoalData::DomainGoal(dg) => dg,
127+
match goal.data(interner) {
128+
GoalData::DomainGoal(_) | GoalData::EqGoal(_) => (),
131129
_ => return goal.super_fold_with(self, outer_binder),
132130
};
133131

134132
self.binders_len = 0;
135133
// shifted in because we introduce a new binder
136134
let outer_binder = outer_binder.shifted_in();
137-
let domain_goal =
138-
GoalData::DomainGoal(domain_goal.shifted_in(interner).fold_with(self, outer_binder)?).intern(interner);
135+
let syn_goal = goal
136+
.shifted_in(interner)
137+
.super_fold_with(self, outer_binder)?;
139138
let new_params = replace(&mut self.new_params, vec![]);
139+
let new_goals = replace(&mut self.new_goals, vec![]);
140140

141-
let binders: Vec<_> = new_params
142-
.iter()
143-
.map(|p| p.data(interner).anonymize())
144-
.collect();
145-
146-
if binders.is_empty() {
141+
if new_params.is_empty() {
147142
return Ok(goal.clone());
148143
}
149144

150145
let goal = GoalData::All(Goals::from(
151146
interner,
152-
iter::once(domain_goal).chain(self.to_eq_goals(new_params, 0)),
147+
iter::once(syn_goal).into_iter().chain(new_goals),
153148
))
154149
.intern(interner);
155150

156-
Ok(
157-
GoalData::Quantified(QuantifierKind::Exists, Binders::new(ParameterKinds::from(interner, binders), goal))
158-
.intern(interner),
151+
Ok(GoalData::Quantified(
152+
QuantifierKind::Exists,
153+
Binders::new(ParameterKinds::from(interner, new_params), goal),
159154
)
155+
.intern(interner))
160156
}
161157

162158
fn interner(&self) -> &'i I {

‎chalk-solve/src/ext.rs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
use crate::infer::InferenceTable;
2+
use crate::clauses::syntactic_eq::syn_eq_lower;
23
use chalk_ir::fold::Fold;
34
use chalk_ir::interner::{HasInterner, Interner};
45
use chalk_ir::*;
@@ -89,7 +90,7 @@ impl<I: Interner> GoalExt<I> for Goal<I> {
8990
}
9091
}
9192
};
92-
let canonical = infer.canonicalize(interner, &peeled_goal).quantified;
93+
let canonical = infer.canonicalize(interner, &syn_eq_lower(interner, &peeled_goal)).quantified;
9394
infer.u_canonicalize(interner, &canonical).quantified
9495
}
9596

@@ -104,7 +105,8 @@ impl<I: Interner> GoalExt<I> for Goal<I> {
104105
/// Will panic if this goal does in fact contain free variables.
105106
fn into_closed_goal(self, interner: &I) -> UCanonical<InEnvironment<Goal<I>>> {
106107
let mut infer = InferenceTable::new();
107-
let env_goal = InEnvironment::new(&Environment::new(interner), self);
108+
let lowered_goal = syn_eq_lower(interner, &self);
109+
let env_goal = InEnvironment::new(&Environment::new(interner), &lowered_goal);
108110
let canonical_goal = infer.canonicalize(interner, &env_goal).quantified;
109111
infer.u_canonicalize(interner, &canonical_goal).quantified
110112
}

0 commit comments

Comments
 (0)