Skip to content

Commit

Permalink
Add WF requirements for projection types
Browse files Browse the repository at this point in the history
  • Loading branch information
@scalexm
scalexm committed Feb 6, 2018
1 parent 9d4f4cb commit a640bea
Show file tree
Hide file tree
Showing 5 changed files with 140 additions and 52 deletions.
7 changes: 1 addition & 6 deletions src/ir/could_match.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,7 @@ impl<T: Zip> CouldMatch<T> for T {
fn zip_tys(&mut self, a: &Ty, b: &Ty) -> Fallible<()> {
let could_match = match (a, b) {
(&Ty::Apply(ref a), &Ty::Apply(ref b)) => {
let names_could_match = match (a.name, b.name) {
(TypeName::ItemId(item_a), TypeName::ItemId(item_b)) => {
item_a == item_b
}
_ => true,
};
let names_could_match = a.name == b.name;

names_could_match
&& a.parameters
Expand Down
7 changes: 7 additions & 0 deletions src/ir/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -296,6 +296,13 @@ impl Ty {
_ => panic!("{:?} is not a projection", self),
}
}

pub fn is_projection(&self) -> bool {
match *self {
Ty::Projection(..) | Ty::UnselectedProjection(..) => true,
_ => false,
}
}
}

/// for<'a...'z> X -- all binders are instantiated at once,
Expand Down
97 changes: 57 additions & 40 deletions src/lower/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1407,34 +1407,42 @@ impl ir::AssociatedTyDatum {
}
};

// Construct an application from the projection. So if we have `<T as Iterator>::Item`,
// we would produce `(Iterator::Item)<T>`.
let app = ir::ApplicationTy {
name: ir::TypeName::AssociatedType(self.id),
parameters,
};
let app_ty = ir::Ty::Apply(app);

let mut clauses = vec![];

// forall<T> {
// ProjectionEq(<T as Foo>::Assoc = (Foo::Assoc)<T>) :-
// T: Foo
// }
let fallback_clause = {
// Construct an application from the projection. So if we have `<T as Iterator>::Item`,
// we would produce `(Iterator::Item)<T>`.
let app = ir::ApplicationTy {
name: ir::TypeName::AssociatedType(self.id),
parameters,
};
let app_ty = ir::Ty::Apply(app);

ir::ProgramClause {
implication: ir::Binders {
binders: binders.clone(),
value: ir::ProgramClauseImplication {
consequence: ir::ProjectionEq {
projection: projection.clone(),
ty: app_ty,
}.cast(),
conditions: vec![
trait_ref.clone().cast(),
],
},
clauses.push(ir::ProgramClause {
implication: ir::Binders {
binders: binders.clone(),
value: ir::ProgramClauseImplication {
consequence: ir::ProjectionEq {
projection: projection.clone(),
ty: app_ty.clone(),
}.cast(),
conditions: vec![trait_ref.clone().cast()],
},
},
});

clauses.push(ir::ProgramClause {
implication: ir::Binders {
binders: binders.clone(),
value: ir::ProgramClauseImplication {
consequence: ir::WellFormed::Ty(app_ty).cast(),
conditions: vec![],
}
}
};
});

// add new type parameter U
let mut binders = binders;
Expand All @@ -1448,22 +1456,21 @@ impl ir::AssociatedTyDatum {
// ProjectionEq(<T as Foo>::Assoc = U) :-
// Normalize(<T as Foo>::Assoc -> U)
// }
let normalize_clause =
ir::ProgramClause {
implication: ir::Binders {
binders: binders.clone(),
value: ir::ProgramClauseImplication {
consequence: ir::ProjectionEq {
projection: projection.clone(),
ty,
}.cast(),
conditions: vec![normalize.clone().cast()],
},
clauses.push(ir::ProgramClause {
implication: ir::Binders {
binders: binders.clone(),
value: ir::ProgramClauseImplication {
consequence: ir::ProjectionEq {
projection: projection.clone(),
ty,
}.cast(),
conditions: vec![normalize.clone().cast()],
},
};
},
});


let well_formed_clause = ir::ProgramClause {
clauses.push(ir::ProgramClause {
implication: ir::Binders {
binders: binders.clone(),
value: ir::ProgramClauseImplication {
Expand All @@ -1474,18 +1481,28 @@ impl ir::AssociatedTyDatum {
],
}
}
};
});

let from_env_clause = ir::ProgramClause {
clauses.push(ir::ProgramClause {
implication: ir::Binders {
binders,
binders: binders.clone(),
value: ir::ProgramClauseImplication {
consequence: ir::FromEnv::TraitRef(trait_ref).cast(),
conditions: vec![ir::FromEnv::Normalize(normalize.clone()).cast()],
},
}
});

clauses.push(ir::ProgramClause {
implication: ir::Binders {
binders: binders,
value: ir::ProgramClauseImplication {
consequence: normalize.clone().cast(),
conditions: vec![ir::FromEnv::Normalize(normalize).cast()],
},
}
};
});

vec![fallback_clause, normalize_clause, well_formed_clause, from_env_clause]
clauses
}
}
68 changes: 67 additions & 1 deletion src/lower/test.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -605,7 +605,7 @@ fn cyclic_traits_error() {
}

#[test]
fn cyclic_wf_requirement() {
fn cyclic_wf_requirements() {
lowering_success! {
program {
trait Foo where <Self as Foo>::Value: Foo {
Expand Down Expand Up @@ -694,3 +694,69 @@ fn implied_bounds_on_ty_decl() {
}
}
}

#[test]
fn wf_requiremements_for_projection() {
lowering_error! {
program {
trait Foo {
type Value;
}

trait Iterator {
type Item;
}

impl<T> Foo for T {
type Value = <T as Iterator>::Item;
}
} error_msg {
"trait impl for \"Foo\" does not meet well-formedness requirements"
}
}

lowering_success! {
program {
trait Foo {
type Value;
}

trait Iterator {
type Item;
}

impl<T> Foo for T where T: Iterator {
type Value = <T as Iterator>::Item;
}
}
}
}

#[test]
fn projection_type_in_header() {
lowering_error! {
program {
trait Foo {
type Value;
}

trait Bar { }

impl<T> Bar for <T as Foo>::Value { }
} error_msg {
"trait impl for \"Bar\" does not meet well-formedness requirements"
}
}

lowering_success! {
program {
trait Foo {
type Value;
}

trait Bar { }

impl<T> Bar for <T as Foo>::Value where T: Foo { }
}
}
}
13 changes: 8 additions & 5 deletions src/lower/wf.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -176,26 +176,29 @@ impl WfSolver {
.iter()
.filter_map(compute_assoc_ty_goal);

let mut header_input_types = Vec::new();
trait_ref.fold(&mut header_input_types);
let (header_projection_types, header_other_types): (Vec<_>, Vec<_>) =
header_input_types.into_iter()
.partition(|ty| ty.is_projection());

let goals =
input_types.into_iter()
.chain(header_projection_types.into_iter())
.map(|ty| WellFormed::Ty(ty).cast())
.chain(assoc_ty_goals)
.chain(Some(WellFormed::TraitRef(trait_ref.clone())).cast());

let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)))
.expect("at least one goal");

let mut input_types = Vec::new();
trait_ref.fold(&mut input_types);

let hypotheses =
impl_datum.binders
.value
.where_clauses
.iter()
.cloned()
.map(|wc| wc.into_from_env_clause())
.chain(input_types.into_iter().map(|ty| FromEnv::Ty(ty).cast()))
.chain(header_other_types.into_iter().map(|ty| FromEnv::Ty(ty).cast()))
.collect();

let goal = Goal::Implies(hypotheses, Box::new(goal))
Expand Down

0 comments on commit a640bea

Please sign in to comment.