Skip to content

Commit

Permalink
Correctly instantiate where clauses / bounds on GATs in wf.rs
Browse files Browse the repository at this point in the history
  • Loading branch information
@scalexm @tmandry
scalexm authored and tmandry committed May 23, 2018
1 parent 6f4ce28 commit 8bd16f5
Show file tree
Hide file tree
Showing 6 changed files with 106 additions and 137 deletions.
13 changes: 13 additions & 0 deletions src/fold.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -431,6 +431,7 @@ enum_fold!(Constraint[] { LifetimeEq(a, b) });
enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g),
Leaf(wc), CannotProve(a) });
enum_fold!(ProgramClause[] { Implies(a), ForAll(a) });
enum_fold!(InlineBound[] { TraitBound(a), ProjectionEqBound(a) });

macro_rules! struct_fold {
($s:ident $([$($tt_args:tt)*])? { $($name:ident),* $(,)* } $($w:tt)*) => {
Expand Down Expand Up @@ -582,4 +583,16 @@ struct_fold!(ConstrainedSubst {
constraints,
});

struct_fold!(TraitBound {
trait_id,
args_no_self,
});

struct_fold!(ProjectionEqBound {
trait_bound,
associated_ty_id,
parameters,
value,
});

// struct_fold!(ApplicationTy { name, parameters }); -- intentionally omitted, folded through Ty
4 changes: 3 additions & 1 deletion src/ir.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -688,7 +688,9 @@ impl DomainGoal {
/// Same as `into_well_formed_goal` but with the `FromEnv` predicate instead of `WellFormed`.
crate fn into_from_env_goal(self) -> DomainGoal {
match self {
DomainGoal::Holds(wca) => DomainGoal::FromEnv(wca),
DomainGoal::Holds(wca @ WhereClauseAtom::Implemented(..)) => {
DomainGoal::FromEnv(wca)
}
goal => goal,
}
}
Expand Down
28 changes: 28 additions & 0 deletions src/ir/lowering/test.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -378,3 +378,31 @@ fn duplicate_parameters() {
}
}
}

#[test]
fn external_items() {
lowering_success! {
program {
extern trait Send { }
extern struct Vec<T> { }
}
}
}

#[test]
fn deref_trait() {
lowering_success! {
program {
#[lang_deref] trait Deref { type Target; }
}
}

lowering_error! {
program {
#[lang_deref] trait Deref { }
#[lang_deref] trait DerefDupe { }
} error_msg {
"Duplicate lang item `DerefTrait`"
}
}
}
54 changes: 3 additions & 51 deletions src/rules.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -496,11 +496,12 @@ impl ir::AssociatedTyDatum {
// FromEnv(WC) :- FromEnv((Foo::Assoc)<Self>).
// }
clauses.extend(self.where_clauses.iter().map(|wc| {
let shift = wc.binders.len();
ir::Binders {
binders: binders.iter().chain(wc.binders.iter()).cloned().collect(),
binders: wc.binders.iter().chain(binders.iter()).cloned().collect(),
value: ir::ProgramClauseImplication {
consequence: wc.value.clone().into_from_env_goal(),
conditions: vec![ir::DomainGoal::FromEnvTy(app_ty.clone()).cast()],
conditions: vec![ir::DomainGoal::FromEnvTy(app_ty.clone()).up_shift(shift).cast()],
}
}.cast()
}));
Expand Down Expand Up @@ -539,55 +540,6 @@ impl ir::AssociatedTyDatum {
},
}.cast());


let projection_wc = ir::WhereClauseAtom::ProjectionEq(projection_eq.clone());
let trait_ref_wc = ir::WhereClauseAtom::Implemented(trait_ref.clone());

// We generate a proxy rule for the well-formedness of `T: Foo<Assoc = U>` which really
// means two things: `T: Foo` and `Normalize(<T as Foo>::Assoc -> U)`. So we have the
// following rule:
//
// forall<T> {
// WellFormed(T: Foo<Assoc = U>) :-
// WellFormed(T: Foo), ProjectionEq(<T as Foo>::Assoc = U)
// }
clauses.push(ir::Binders {
binders: binders.clone(),
value: ir::ProgramClauseImplication {
consequence: ir::DomainGoal::WellFormed(projection_wc.clone()),
conditions: vec![
ir::DomainGoal::WellFormed(trait_ref_wc.clone()).cast(),
projection_eq.clone().cast()
],
}
}.cast());

// We also have three proxy reverse rules, the first one being:
//
// forall<T> {
// FromEnv(T: Foo) :- FromEnv(T: Foo<Assoc = U>)
// }
clauses.push(ir::Binders {
binders: binders.clone(),
value: ir::ProgramClauseImplication {
consequence: ir::DomainGoal::FromEnv(trait_ref_wc).cast(),
conditions: vec![ir::DomainGoal::FromEnv(projection_wc.clone()).cast()],
},
}.cast());

// The second:
//
// forall<T> {
// ProjectionEq(<T as Foo>::Assoc = U) :- FromEnv(T: Foo<Assoc = U>)
// }
clauses.push(ir::Binders {
binders: binders.clone(),
value: ir::ProgramClauseImplication {
consequence: projection_eq.clone().cast(),
conditions: vec![ir::DomainGoal::FromEnv(projection_wc).cast()],
},
}.cast());

// And the third:
//
// forall<T> {
Expand Down
98 changes: 41 additions & 57 deletions src/rules/wf.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@ use errors::*;
use cast::*;
use solve::SolverChoice;
use itertools::Itertools;
use fold::*;
use fold::shift::Shift;

mod test;

Expand Down Expand Up @@ -207,38 +209,20 @@ impl WfSolver {
let mut input_types = Vec::new();
impl_datum.binders.value.where_clauses.fold(&mut input_types);

// We partition the input types of the type on which we implement the trait in two categories:
// * projection types, e.g. `<T as Iterator>::Item`: we will have to prove that these types
// are well-formed, e.g. that we can show that `T: Iterator` holds
// * any other types, e.g. `HashSet<K>`: we will *assume* that these types are well-formed, e.g.
// we will be able to derive that `K: Hash` holds without writing any where clause.
// We retrieve all the input types of the type on which we implement the trait: we will
// *assume* that these types are well-formed, e.g. we will be able to derive that
// `K: Hash` holds without writing any where clause.
//
// Examples:
// Example:
// ```
// struct HashSet<K> where K: Hash { ... }
//
// impl<K> Foo for HashSet<K> {
// // Inside here, we can rely on the fact that `K: Hash` holds
// }
// ```
//
// ```
// impl<T> Foo for <T as Iterator>::Item {
// // The impl is not well-formed, as an exception we do not assume that
// // `<T as Iterator>::Item` is well-formed and instead want to prove it.
// }
// ```
//
// ```
// impl<T> Foo for <T as Iterator>::Item where T: Iterator {
// // Now ok.
// }
// ```
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());

// Associated type values are special because they can be parametric (independently of
// the impl), so we issue a special goal which is quantified using the binders of the
Expand All @@ -257,49 +241,48 @@ impl WfSolver {
let assoc_ty_datum = &self.env.associated_ty_data[&assoc_ty.associated_ty_id];
let bounds = &assoc_ty_datum.bounds;

let trait_datum = &self.env.trait_data[&assoc_ty_datum.trait_id];

let mut input_types = Vec::new();
assoc_ty.value.value.ty.fold(&mut input_types);

let goals = input_types.into_iter()
.map(|ty| DomainGoal::WellFormedTy(ty).cast());
//.chain(bounds.iter()
// .flat_map(|b| b.clone()
// .lower_with_self(assoc_ty.value.value.ty.clone()))
// .map(|g| g.into_well_formed_goal().cast()));
let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)));
//.expect("at least one goal");
let goal = goal //Goal::Implies(hypotheses, Box::new(goal))
.map(|goal| goal.quantify(QuantifierKind::ForAll, assoc_ty.value.binders.clone()));//binders);

// FIXME this is wrong (and test)!
let mut bound_binders = assoc_ty.value.binders.clone();
bound_binders.extend(trait_datum.binders.binders.iter());
let wf_goals =
input_types.into_iter()
.map(|ty| DomainGoal::WellFormedTy(ty));

let trait_ref = trait_ref.up_shift(assoc_ty.value.binders.len());

let all_parameters: Vec<_> =
assoc_ty.value.binders.iter()
.zip(0..)
.map(|p| p.to_parameter())
.chain(trait_ref.parameters.iter().cloned())
.collect();

let bound_goals =
bounds.iter()
.map(|b| Subst::apply(&all_parameters, b))
.flat_map(|b| b.lower_with_self(assoc_ty.value.value.ty.clone()))
.map(|g| g.into_well_formed_goal());

let goals = wf_goals.chain(bound_goals).casted();
let goal = match goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) {
Some(goal) => goal,
None => return None,
};

let hypotheses =
assoc_ty_datum.where_clauses
.iter()
.chain(impl_datum.binders.value.where_clauses.iter()) // FIXME binders (and test)!
.cloned()
.map(|wc| Subst::apply(&all_parameters, wc))
.map(|wc| wc.map(|bound| bound.into_from_env_goal()))
.casted()
.collect();
let bound_goal = bounds.iter()
.flat_map(|b| b.clone()
.lower_with_self(assoc_ty.value.value.ty.clone()))
.map(|g| g.into_well_formed_goal().cast())
.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)));
let bound_goal = bound_goal.map(|g| {
Goal::Implies(hypotheses, Box::new(g)).quantify(QuantifierKind::ForAll, bound_binders)
});

let goal = goal.into_iter()
.chain(bound_goal.into_iter())
.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)));
println!("{:?}", goal);

goal

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

Some(goal.quantify(QuantifierKind::ForAll, assoc_ty.value.binders.clone()))
};

let assoc_ty_goals =
Expand All @@ -316,7 +299,6 @@ impl WfSolver {
);
let goals =
input_types.into_iter()
.chain(header_projection_types.into_iter())
.map(|ty| DomainGoal::WellFormedTy(ty).cast())
.chain(assoc_ty_goals)
.chain(Some(trait_ref_wf).cast());
Expand All @@ -335,12 +317,14 @@ impl WfSolver {
.cloned()
.map(|wc| wc.map(|bound| bound.into_from_env_goal()))
.casted()
.chain(header_other_types.into_iter().map(|ty| DomainGoal::FromEnvTy(ty).cast()))
.chain(header_input_types.into_iter().map(|ty| DomainGoal::FromEnvTy(ty).cast()))
.collect();

let goal = Goal::Implies(hypotheses, Box::new(goal))
.quantify(QuantifierKind::ForAll, impl_datum.binders.binders.clone());

println!("{:?}", goal);

match self.solver_choice.solve_root_goal(&self.env, &goal.into_closed_goal()).unwrap() {
Some(sol) => sol.is_unique(),
None => false,
Expand Down
46 changes: 18 additions & 28 deletions src/rules/wf/test.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -438,16 +438,6 @@ fn generic_projection_bound() {
}
}

#[test]
fn external_items() {
lowering_success! {
program {
extern trait Send { }
extern struct Vec<T> { }
}
}
}

#[test]
fn higher_ranked_trait_bounds() {
lowering_error! {
Expand All @@ -474,6 +464,24 @@ fn higher_ranked_trait_bounds() {
}
}

#[test]
fn higher_ranked_trait_bound_on_gat() {
lowering_success! {
program {
trait Foo<'a> { }
struct i32 { }

trait Bar<'a> {
type Item<V>: Foo<'a> where forall<'b> V: Foo<'b>;
}

impl<'a> Bar<'a> for i32 {
type Item<V> = V;
}
}
}
}

// See `cyclic_traits`, this is essentially the same but with higher-ranked co-inductive WF goals.
#[test]
fn higher_ranked_cyclic_requirements() {
Expand Down Expand Up @@ -511,21 +519,3 @@ fn higher_ranked_cyclic_requirements() {
}
}
}

#[test]
fn deref_trait() {
lowering_success! {
program {
#[lang_deref] trait Deref { type Target; }
}
}

lowering_error! {
program {
#[lang_deref] trait Deref { }
#[lang_deref] trait DerefDupe { }
} error_msg {
"Duplicate lang item `DerefTrait`"
}
}
}

0 comments on commit 8bd16f5

Please sign in to comment.