Skip to content

Commit 480403c

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 c34a43e commit 480403c

File tree

5 files changed

+132
-59
lines changed

5 files changed

+132
-59
lines changed

‎chalk-parse/src/ast.rs

+1-1
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

+1-1
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

+70
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;
@@ -265,6 +266,19 @@ pub enum InlineBound {
265266
ProjectionEqBound(ProjectionEqBound),
266267
}
267268

269+
impl InlineBound {
270+
/// Applies the `InlineBound` to `self_ty` and lowers to a [`DomainGoal`].
271+
///
272+
/// Because an `InlineBound` not know anything about what it's binding, you
273+
/// must provide that type as `self_ty`.
274+
pub fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
275+
match self {
276+
InlineBound::TraitBound(b) => b.lower_with_self(self_ty),
277+
InlineBound::ProjectionEqBound(b) => b.lower_with_self(self_ty),
278+
}
279+
}
280+
}
281+
268282
/// Represents a trait bound on e.g. a type or type parameter.
269283
/// Does not know anything about what it's binding.
270284
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
@@ -273,6 +287,21 @@ pub struct TraitBound {
273287
crate args_no_self: Vec<Parameter>,
274288
}
275289

290+
impl TraitBound {
291+
pub fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
292+
let trait_ref = self.as_trait_ref(self_ty);
293+
vec![DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref))]
294+
}
295+
296+
fn as_trait_ref(&self, self_ty: Ty) -> TraitRef {
297+
let self_ty = ParameterKind::Ty(self_ty);
298+
TraitRef {
299+
trait_id: self.trait_id,
300+
parameters: iter::once(self_ty).chain(self.args_no_self.iter().cloned()).collect(),
301+
}
302+
}
303+
}
304+
276305
/// Represents a projection equality bound on e.g. a type or type parameter.
277306
/// Does not know anything about what it's binding.
278307
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
@@ -284,6 +313,26 @@ pub struct ProjectionEqBound {
284313
crate value: Ty,
285314
}
286315

316+
impl ProjectionEqBound {
317+
pub fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
318+
let trait_ref = self.trait_bound.as_trait_ref(self_ty);
319+
320+
let mut parameters = self.parameters.clone();
321+
parameters.extend(trait_ref.parameters.clone());
322+
323+
vec![
324+
DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref)),
325+
DomainGoal::Holds(WhereClauseAtom::ProjectionEq(ProjectionEq {
326+
projection: ProjectionTy {
327+
associated_ty_id: self.associated_ty_id,
328+
parameters: parameters,
329+
},
330+
ty: self.value.clone(),
331+
}))
332+
]
333+
}
334+
}
335+
287336
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
288337
pub struct AssociatedTyDatum {
289338
/// The trait this associated type is defined in.
@@ -309,6 +358,27 @@ pub struct AssociatedTyDatum {
309358
crate where_clauses: Vec<QuantifiedDomainGoal>,
310359
}
311360

361+
impl AssociatedTyDatum {
362+
/// Returns the associated ty's bounds applied to the projection type, e.g.:
363+
///
364+
/// ```notrust
365+
/// Implemented(<?0 as Foo>::Item<?1>: Sized)
366+
/// ```
367+
pub fn bounds_on_self(&self) -> Vec<DomainGoal> {
368+
let parameters = self.parameter_kinds
369+
.anonymize()
370+
.iter()
371+
.zip(0..)
372+
.map(|p| p.to_parameter())
373+
.collect();
374+
let self_ty = Ty::Projection(ProjectionTy {
375+
associated_ty_id: self.id,
376+
parameters
377+
});
378+
self.bounds.iter().flat_map(|b| b.lower_with_self(self_ty.clone())).collect()
379+
}
380+
}
381+
312382
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
313383
pub struct AssociatedTyValue {
314384
crate associated_ty_id: ItemId,

‎src/rules.rs

+17-49
Original file line numberDiff line numberDiff line change
@@ -529,6 +529,23 @@ impl ir::AssociatedTyDatum {
529529
}.cast()
530530
}));
531531

532+
// Reverse rule for implied bounds.
533+
//
534+
// forall<T> {
535+
// FromEnv(<T as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo)
536+
// }
537+
clauses.extend(self.bounds_on_self().into_iter().map(|bound| {
538+
ir::Binders {
539+
binders: binders.clone(),
540+
value: ir::ProgramClauseImplication {
541+
consequence: bound.into_from_env_goal(),
542+
conditions: vec![
543+
ir::DomainGoal::FromEnv(trait_ref.clone().cast()).cast()
544+
],
545+
}
546+
}.cast()
547+
}));
548+
532549
// add new type parameter U
533550
let mut binders = binders;
534551
binders.push(ir::ParameterKind::Ty(()));
@@ -554,55 +571,6 @@ impl ir::AssociatedTyDatum {
554571
},
555572
}.cast());
556573

557-
558-
let projection_wc = ir::WhereClauseAtom::ProjectionEq(projection_eq.clone());
559-
let trait_ref_wc = ir::WhereClauseAtom::Implemented(trait_ref.clone());
560-
561-
// We generate a proxy rule for the well-formedness of `T: Foo<Assoc = U>` which really
562-
// means two things: `T: Foo` and `Normalize(<T as Foo>::Assoc -> U)`. So we have the
563-
// following rule:
564-
//
565-
// forall<T> {
566-
// WellFormed(T: Foo<Assoc = U>) :-
567-
// WellFormed(T: Foo), ProjectionEq(<T as Foo>::Assoc = U)
568-
// }
569-
clauses.push(ir::Binders {
570-
binders: binders.clone(),
571-
value: ir::ProgramClauseImplication {
572-
consequence: ir::DomainGoal::WellFormed(projection_wc.clone()),
573-
conditions: vec![
574-
ir::DomainGoal::WellFormed(trait_ref_wc.clone()).cast(),
575-
projection_eq.clone().cast()
576-
],
577-
}
578-
}.cast());
579-
580-
// We also have two proxy reverse rules, the first one being:
581-
//
582-
// forall<T> {
583-
// FromEnv(T: Foo) :- FromEnv(T: Foo<Assoc = U>)
584-
// }
585-
clauses.push(ir::Binders {
586-
binders: binders.clone(),
587-
value: ir::ProgramClauseImplication {
588-
consequence: ir::DomainGoal::FromEnv(trait_ref_wc).cast(),
589-
conditions: vec![ir::DomainGoal::FromEnv(projection_wc.clone()).cast()],
590-
},
591-
}.cast());
592-
593-
// And the other one being:
594-
//
595-
// forall<T> {
596-
// ProjectionEq(<T as Foo>::Assoc = U) :- FromEnv(T: Foo<Assoc = U>)
597-
// }
598-
clauses.push(ir::Binders {
599-
binders,
600-
value: ir::ProgramClauseImplication {
601-
consequence: projection_eq.clone().cast(),
602-
conditions: vec![ir::DomainGoal::FromEnv(projection_wc).cast()],
603-
},
604-
}.cast());
605-
606574
clauses
607575
}
608576
}

‎src/rules/wf.rs

+43-8
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)