Skip to content

Commit 446df30

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 d109ff0 commit 446df30

File tree

5 files changed

+132
-59
lines changed

5 files changed

+132
-59
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: 70 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;
@@ -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

Lines changed: 17 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -545,6 +545,23 @@ impl ir::AssociatedTyDatum {
545545
}.cast()
546546
}));
547547

548+
// Reverse rule for implied bounds.
549+
//
550+
// forall<T> {
551+
// FromEnv(<T as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo)
552+
// }
553+
clauses.extend(self.bounds_on_self().into_iter().map(|bound| {
554+
ir::Binders {
555+
binders: binders.clone(),
556+
value: ir::ProgramClauseImplication {
557+
consequence: bound.into_from_env_goal(),
558+
conditions: vec![
559+
ir::DomainGoal::FromEnv(trait_ref.clone().cast()).cast()
560+
],
561+
}
562+
}.cast()
563+
}));
564+
548565
// add new type parameter U
549566
let mut binders = binders;
550567
binders.push(ir::ParameterKind::Ty(()));
@@ -570,55 +587,6 @@ impl ir::AssociatedTyDatum {
570587
},
571588
}.cast());
572589

573-
574-
let projection_wc = ir::WhereClauseAtom::ProjectionEq(projection_eq.clone());
575-
let trait_ref_wc = ir::WhereClauseAtom::Implemented(trait_ref.clone());
576-
577-
// We generate a proxy rule for the well-formedness of `T: Foo<Assoc = U>` which really
578-
// means two things: `T: Foo` and `Normalize(<T as Foo>::Assoc -> U)`. So we have the
579-
// following rule:
580-
//
581-
// forall<T> {
582-
// WellFormed(T: Foo<Assoc = U>) :-
583-
// WellFormed(T: Foo), ProjectionEq(<T as Foo>::Assoc = U)
584-
// }
585-
clauses.push(ir::Binders {
586-
binders: binders.clone(),
587-
value: ir::ProgramClauseImplication {
588-
consequence: ir::DomainGoal::WellFormed(projection_wc.clone()),
589-
conditions: vec![
590-
ir::DomainGoal::WellFormed(trait_ref_wc.clone()).cast(),
591-
projection_eq.clone().cast()
592-
],
593-
}
594-
}.cast());
595-
596-
// We also have two proxy reverse rules, the first one being:
597-
//
598-
// forall<T> {
599-
// FromEnv(T: Foo) :- FromEnv(T: Foo<Assoc = U>)
600-
// }
601-
clauses.push(ir::Binders {
602-
binders: binders.clone(),
603-
value: ir::ProgramClauseImplication {
604-
consequence: ir::DomainGoal::FromEnv(trait_ref_wc).cast(),
605-
conditions: vec![ir::DomainGoal::FromEnv(projection_wc.clone()).cast()],
606-
},
607-
}.cast());
608-
609-
// And the other one being:
610-
//
611-
// forall<T> {
612-
// ProjectionEq(<T as Foo>::Assoc = U) :- FromEnv(T: Foo<Assoc = U>)
613-
// }
614-
clauses.push(ir::Binders {
615-
binders,
616-
value: ir::ProgramClauseImplication {
617-
consequence: projection_eq.clone().cast(),
618-
conditions: vec![ir::DomainGoal::FromEnv(projection_wc).cast()],
619-
},
620-
}.cast());
621-
622590
clauses
623591
}
624592
}

‎src/rules/wf.rs

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

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

272307
let assoc_ty_goals =

0 commit comments

Comments
 (0)