Skip to content

Commit 822a388

Browse files
tmandrytmandry
committed
Lower bounds on associated types
Adds reverse rule and WF rules for associated type bounds. The WF rules aren't quite right, but they'll be fixed in a later commit.
1 parent d8d6fc5 commit 822a388

File tree

5 files changed

+136
-13
lines changed

5 files changed

+136
-13
lines changed

‎chalk-parse/src/ast.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,7 @@ pub struct TraitBound {
8686
pub struct ProjectionEqBound {
8787
pub trait_bound: TraitBound,
8888
pub name: Identifier,
89-
pub parameters: Vec<Parameter>,
89+
pub args: Vec<Parameter>,
9090
pub value: Ty,
9191
}
9292

‎chalk-parse/src/parser.lalrpop

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,7 @@ ProjectionEqBound: ProjectionEqBound = {
107107
args_no_self: a.unwrap_or(vec![]),
108108
},
109109
name,
110-
parameters: a2,
110+
args: a2,
111111
value: ty,
112112
}
113113
};

‎src/ir.rs

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ use fold::shift::Shift;
55
use lalrpop_intern::InternedString;
66
use std::collections::{BTreeMap, BTreeSet};
77
use std::sync::Arc;
8+
use std::iter;
89

910
#[macro_use]
1011
mod macros;
@@ -284,6 +285,60 @@ pub struct ProjectionEqBound {
284285
crate value: Ty,
285286
}
286287

288+
trait AsTraitRef {
289+
fn as_trait_ref(&self, self_ty: Ty) -> TraitRef;
290+
}
291+
292+
impl AsTraitRef for TraitBound {
293+
fn as_trait_ref(&self, self_ty: Ty) -> TraitRef {
294+
let self_ty = ParameterKind::Ty(self_ty);
295+
TraitRef {
296+
trait_id: self.trait_id,
297+
parameters: iter::once(self_ty).chain(self.args_no_self.iter().cloned()).collect(),
298+
}
299+
}
300+
}
301+
302+
pub trait LowerWithSelf {
303+
fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal>;
304+
}
305+
306+
impl LowerWithSelf for TraitBound {
307+
fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
308+
let trait_ref = self.as_trait_ref(self_ty);
309+
vec![DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref))]
310+
}
311+
}
312+
313+
impl LowerWithSelf for ProjectionEqBound {
314+
fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
315+
let trait_ref = self.trait_bound.as_trait_ref(self_ty);
316+
317+
let mut parameters = self.parameters.clone();
318+
parameters.extend(trait_ref.parameters.clone());
319+
320+
vec![
321+
DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref)),
322+
DomainGoal::Holds(WhereClauseAtom::ProjectionEq(ProjectionEq {
323+
projection: ProjectionTy {
324+
associated_ty_id: self.associated_ty_id,
325+
parameters: parameters,
326+
},
327+
ty: self.value.clone(),
328+
}))
329+
]
330+
}
331+
}
332+
333+
impl LowerWithSelf for InlineBound {
334+
fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
335+
match self {
336+
InlineBound::TraitBound(b) => b.lower_with_self(self_ty),
337+
InlineBound::ProjectionEqBound(b) => b.lower_with_self(self_ty),
338+
}
339+
}
340+
}
341+
287342
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
288343
pub struct AssociatedTyDatum {
289344
/// The trait this associated type is defined in.
@@ -309,6 +364,22 @@ pub struct AssociatedTyDatum {
309364
crate where_clauses: Vec<QuantifiedDomainGoal>,
310365
}
311366

367+
impl AssociatedTyDatum {
368+
pub fn bounds_on_self(&self) -> Vec<DomainGoal> {
369+
let parameters = self.parameter_kinds
370+
.anonymize()
371+
.iter()
372+
.zip(0..)
373+
.map(|p| p.to_parameter())
374+
.collect();
375+
let self_ty = Ty::Projection(ProjectionTy {
376+
associated_ty_id: self.id,
377+
parameters
378+
});
379+
self.bounds.iter().flat_map(|b| b.lower_with_self(self_ty.clone())).collect()
380+
}
381+
}
382+
312383
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
313384
pub struct AssociatedTyValue {
314385
crate associated_ty_id: ItemId,

‎src/rules.rs

Lines changed: 20 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -562,7 +562,7 @@ impl ir::AssociatedTyDatum {
562562
}
563563
}.cast());
564564

565-
// We also have two proxy reverse rules, the first one being:
565+
// We also have three proxy reverse rules, the first one being:
566566
//
567567
// forall<T> {
568568
// FromEnv(T: Foo) :- FromEnv(T: Foo<Assoc = U>)
@@ -575,19 +575,36 @@ impl ir::AssociatedTyDatum {
575575
},
576576
}.cast());
577577

578-
// And the other one being:
578+
// The second:
579579
//
580580
// forall<T> {
581581
// ProjectionEq(<T as Foo>::Assoc = U) :- FromEnv(T: Foo<Assoc = U>)
582582
// }
583583
clauses.push(ir::Binders {
584-
binders,
584+
binders: binders.clone(),
585585
value: ir::ProgramClauseImplication {
586586
consequence: projection_eq.clone().cast(),
587587
conditions: vec![ir::DomainGoal::FromEnv(projection_wc).cast()],
588588
},
589589
}.cast());
590590

591+
// And the third:
592+
//
593+
// forall<T> {
594+
// FromEnv(<T as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo)
595+
// }
596+
clauses.extend(self.bounds_on_self().into_iter().map(|bound| {
597+
ir::Binders {
598+
binders: binders.clone(),
599+
value: ir::ProgramClauseImplication {
600+
consequence: bound.into_from_env_goal(),
601+
conditions: vec![
602+
ir::DomainGoal::FromEnv(trait_ref.clone().cast()).cast()
603+
],
604+
}
605+
}.cast()
606+
}));
607+
591608
clauses
592609
}
593610
}

‎src/rules/wf.rs

Lines changed: 43 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -254,17 +254,52 @@ impl WfSolver {
254254
// ```
255255
// we would issue the following subgoal: `forall<'a> { WellFormed(Box<&'a T>) }`.
256256
let compute_assoc_ty_goal = |assoc_ty: &AssociatedTyValue| {
257+
let assoc_ty_datum = &self.env.associated_ty_data[&assoc_ty.associated_ty_id];
258+
let bounds = &assoc_ty_datum.bounds;
259+
260+
let trait_datum = &self.env.trait_data[&assoc_ty_datum.trait_id];
261+
257262
let mut input_types = Vec::new();
258263
assoc_ty.value.value.ty.fold(&mut input_types);
259264

260-
if input_types.is_empty() {
261-
return None;
262-
}
263-
264-
let goals = input_types.into_iter().map(|ty| DomainGoal::WellFormedTy(ty).cast());
265-
let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)))
266-
.expect("at least one goal");
267-
Some(goal.quantify(QuantifierKind::ForAll, assoc_ty.value.binders.clone()))
265+
let goals = input_types.into_iter()
266+
.map(|ty| DomainGoal::WellFormedTy(ty).cast());
267+
//.chain(bounds.iter()
268+
// .flat_map(|b| b.clone()
269+
// .lower_with_self(assoc_ty.value.value.ty.clone()))
270+
// .map(|g| g.into_well_formed_goal().cast()));
271+
let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)));
272+
//.expect("at least one goal");
273+
let goal = goal //Goal::Implies(hypotheses, Box::new(goal))
274+
.map(|goal| goal.quantify(QuantifierKind::ForAll, assoc_ty.value.binders.clone()));//binders);
275+
276+
// FIXME this is wrong (and test)!
277+
let mut bound_binders = assoc_ty.value.binders.clone();
278+
bound_binders.extend(trait_datum.binders.binders.iter());
279+
280+
let hypotheses =
281+
assoc_ty_datum.where_clauses
282+
.iter()
283+
.chain(impl_datum.binders.value.where_clauses.iter()) // FIXME binders (and test)!
284+
.cloned()
285+
.map(|wc| wc.map(|bound| bound.into_from_env_goal()))
286+
.casted()
287+
.collect();
288+
let bound_goal = bounds.iter()
289+
.flat_map(|b| b.clone()
290+
.lower_with_self(assoc_ty.value.value.ty.clone()))
291+
.map(|g| g.into_well_formed_goal().cast())
292+
.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)));
293+
let bound_goal = bound_goal.map(|g| {
294+
Goal::Implies(hypotheses, Box::new(g)).quantify(QuantifierKind::ForAll, bound_binders)
295+
});
296+
297+
let goal = goal.into_iter()
298+
.chain(bound_goal.into_iter())
299+
.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)));
300+
println!("{:?}", goal);
301+
302+
goal
268303
};
269304

270305
let assoc_ty_goals =

0 commit comments

Comments
 (0)