Skip to content

Commit 95a5e08

Browse files
basil-cowbasil-cow
committed
mvp with eq goals
1 parent 15daa1a commit 95a5e08

File tree

4 files changed

+196
-11
lines changed

4 files changed

+196
-11
lines changed

‎chalk-ir/src/lib.rs

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -817,6 +817,13 @@ impl<T, L> ParameterKind<T, L> {
817817
_ => None,
818818
}
819819
}
820+
821+
pub fn anonymize(&self) -> ParameterKind<()> {
822+
match self {
823+
ParameterKind::Ty(_) => ParameterKind::Ty(()),
824+
ParameterKind::Lifetime(_) => ParameterKind::Lifetime(()),
825+
}
826+
}
820827
}
821828

822829
#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
@@ -853,6 +860,18 @@ impl<I: Interner> Parameter<I> {
853860
}
854861
}
855862

863+
pub fn replace_bound(&self, bound_var: BoundVar, interner: &I) -> Self {
864+
match self.data(interner) {
865+
ParameterKind::Ty(_) => {
866+
ParameterKind::Ty(TyData::BoundVar(bound_var).intern(interner)).intern(interner)
867+
}
868+
ParameterKind::Lifetime(_) => {
869+
ParameterKind::Lifetime(LifetimeData::BoundVar(bound_var).intern(interner))
870+
.intern(interner)
871+
}
872+
}
873+
}
874+
856875
pub fn is_ty(&self, interner: &I) -> bool {
857876
match self.data(interner) {
858877
ParameterKind::Ty(_) => true,

‎chalk-solve/src/clauses.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ mod builtin_traits;
1515
mod env_elaborator;
1616
mod generalize;
1717
pub mod program_clauses;
18+
pub mod syntactic_eq;
1819

1920
/// For auto-traits, we generate a default rule for every struct,
2021
/// unless there is a manual impl for that struct given explicitly.

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

Lines changed: 7 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
use crate::cast::{Cast, CastTo};
2+
use crate::clauses::syntactic_eq::syn_eq_lower;
23
use crate::RustIrDatabase;
34
use chalk_ir::fold::Fold;
45
use chalk_ir::interner::{HasInterner, Interner};
@@ -76,18 +77,13 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
7677
priority,
7778
};
7879

79-
if self.binders.len() == 0 {
80-
self.clauses
81-
.push(ProgramClauseData::Implies(clause).intern(interner));
80+
let clause = if self.binders.len() == 0 {
81+
ProgramClauseData::Implies(clause).intern(interner)
8282
} else {
83-
self.clauses.push(
84-
ProgramClauseData::ForAll(Binders::new(
85-
ParameterKinds::from(interner, self.binders.clone()),
86-
clause,
87-
))
88-
.intern(interner),
89-
);
90-
}
83+
ProgramClauseData::ForAll(Binders::new(ParameterKinds::from(interner, self.binders.clone()), clause)).intern(interner)
84+
};
85+
86+
self.clauses.push(syn_eq_lower(interner, &clause));
9187

9288
debug!("pushed clause {:?}", self.clauses.last());
9389
}

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

Lines changed: 169 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,169 @@
1+
use std::{iter, mem::replace};
2+
3+
use chalk_engine::fallible::Fallible;
4+
use chalk_ir::{
5+
fold::{shift::Shift, Fold, Folder, SuperFold},
6+
interner::Interner,
7+
Binders, BoundVar, DebruijnIndex, EqGoal, Goal, GoalData, Goals, Parameter, ProgramClause,
8+
ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty, TyData, ParameterKind, ApplicationTy, TypeName,
9+
ParameterKinds,
10+
};
11+
12+
pub fn syn_eq_lower<I: Interner>(interner: &I, clause: &ProgramClause<I>) -> ProgramClause<I> {
13+
let mut folder = SynEqFolder {
14+
interner,
15+
new_params: vec![],
16+
binders_len: 0,
17+
};
18+
19+
clause.fold_with(&mut folder, DebruijnIndex::INNERMOST).unwrap()
20+
}
21+
22+
struct SynEqFolder<'i, I: Interner> {
23+
interner: &'i I,
24+
new_params: Vec<Parameter<I>>,
25+
binders_len: usize,
26+
}
27+
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+
48+
impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> {
49+
fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> {
50+
self
51+
}
52+
53+
fn fold_ty(&mut self, ty: &Ty<I>, outer_binder: DebruijnIndex) -> Fallible<Ty<I>> {
54+
let interner = self.interner;
55+
let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, self.binders_len);
56+
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));
61+
self.binders_len += 1;
62+
Ok(TyData::BoundVar(bound_var).intern(interner))
63+
}
64+
_ => ty.super_fold_with(self, outer_binder),
65+
}
66+
}
67+
68+
fn fold_program_clause(
69+
&mut self,
70+
clause: &ProgramClause<I>,
71+
outer_binder: DebruijnIndex,
72+
) -> Fallible<ProgramClause<I>> {
73+
let interner = self.interner;
74+
75+
let ((binders, implication), in_binders) = match clause.data(interner) {
76+
ProgramClauseData::ForAll(for_all) => {
77+
(for_all.clone().into(), true)
78+
}
79+
// introduce a dummy binder and shift implication through it
80+
ProgramClauseData::Implies(implication) => ((ParameterKinds::new(interner), implication.shifted_in(interner)), false),
81+
};
82+
let mut binders: Vec<_> = binders.as_slice(interner).clone().into();
83+
84+
let outer_binder = outer_binder.shifted_in();
85+
86+
self.binders_len = binders.len();
87+
let consequence = implication.consequence.fold_with(self, outer_binder)?;
88+
// Immediately move `new_params` out of of the folder struct so it's safe
89+
// to call `.fold_with` again
90+
let new_params = replace(&mut self.new_params, vec![]);
91+
92+
let mut conditions = implication.conditions.fold_with(self, outer_binder)?;
93+
if new_params.is_empty() && !in_binders {
94+
// 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)?)
100+
.intern(interner));
101+
}
102+
103+
let old_len = binders.len();
104+
binders.extend(new_params.iter().map(|p| p.data(interner).anonymize()));
105+
106+
conditions = Goals::from(
107+
interner,
108+
conditions
109+
.iter(interner)
110+
.cloned()
111+
.chain(self.to_eq_goals(new_params, old_len)),
112+
);
113+
114+
Ok(ProgramClauseData::ForAll(Binders::new(
115+
ParameterKinds::from(interner, binders),
116+
ProgramClauseImplication {
117+
consequence,
118+
conditions,
119+
priority: implication.priority,
120+
},
121+
))
122+
.intern(interner))
123+
}
124+
125+
fn fold_goal(&mut self, goal: &Goal<I>, outer_binder: DebruijnIndex) -> Fallible<Goal<I>> {
126+
assert!(self.new_params.is_empty(), true);
127+
128+
let interner = self.interner;
129+
let domain_goal = match goal.data(interner) {
130+
GoalData::DomainGoal(dg) => dg,
131+
_ => return goal.super_fold_with(self, outer_binder),
132+
};
133+
134+
self.binders_len = 0;
135+
// shifted in because we introduce a new binder
136+
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);
139+
let new_params = replace(&mut self.new_params, vec![]);
140+
141+
let binders: Vec<_> = new_params
142+
.iter()
143+
.map(|p| p.data(interner).anonymize())
144+
.collect();
145+
146+
if binders.is_empty() {
147+
return Ok(goal.clone());
148+
}
149+
150+
let goal = GoalData::All(Goals::from(
151+
interner,
152+
iter::once(domain_goal).chain(self.to_eq_goals(new_params, 0)),
153+
))
154+
.intern(interner);
155+
156+
Ok(
157+
GoalData::Quantified(QuantifierKind::Exists, Binders::new(ParameterKinds::from(interner, binders), goal))
158+
.intern(interner),
159+
)
160+
}
161+
162+
fn interner(&self) -> &'i I {
163+
self.interner
164+
}
165+
166+
fn target_interner(&self) -> &'i I {
167+
self.interner
168+
}
169+
}

0 commit comments

Comments
 (0)