Replace type params with bound vars in rustc_traits::lowering

This commit is contained in:
scalexm 2018-10-31 15:16:46 +01:00
parent 485397e49a
commit 64aac8d4c1
4 changed files with 143 additions and 61 deletions

View File

@ -687,7 +687,7 @@ define_queries! { <'tcx>
) -> Clauses<'tcx>,
// Get the chalk-style environment of the given item.
[] fn environment: Environment(DefId) -> traits::Environment<'tcx>,
[] fn environment: Environment(DefId) -> ty::Binder<traits::Environment<'tcx>>,
},
Linking {

View File

@ -179,6 +179,30 @@ impl<'a, 'gcx, 'tcx> Substs<'tcx> {
})
}
pub fn bound_vars_for_item(
tcx: TyCtxt<'a, 'gcx, 'tcx>,
def_id: DefId
) -> &'tcx Substs<'tcx> {
Substs::for_item(tcx, def_id, |param, _| {
match param.kind {
ty::GenericParamDefKind::Type { .. } => {
tcx.mk_ty(ty::Bound(ty::BoundTy {
index: ty::INNERMOST,
var: ty::BoundVar::from(param.index),
kind: ty::BoundTyKind::Param(param.name),
})).into()
}
ty::GenericParamDefKind::Lifetime => {
tcx.mk_region(ty::RegionKind::ReLateBound(
ty::INNERMOST,
ty::BoundRegion::BrNamed(param.def_id, param.name)
)).into()
}
}
})
}
/// Creates a `Substs` for generic parameter definitions,
/// by calling closures to obtain each kind.
/// The closures get to observe the `Substs` as they're

View File

@ -88,12 +88,12 @@ impl ClauseVisitor<'set, 'a, 'tcx> {
ty::FnPtr(..) |
ty::Tuple(..) |
ty::Never |
ty::Param(..) => (),
ty::Infer(..) |
ty::Bound(..) => (),
ty::GeneratorWitness(..) |
ty::UnnormalizedProjection(..) |
ty::Infer(..) |
ty::Bound(..) |
ty::Param(..) |
ty::Error => {
bug!("unexpected type {:?}", ty);
}
@ -173,21 +173,28 @@ crate fn program_clauses_for_env<'a, 'tcx>(
);
}
crate fn environment<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> Environment<'tcx> {
crate fn environment<'a, 'tcx>(
tcx: TyCtxt<'a, 'tcx, 'tcx>,
def_id: DefId
) -> ty::Binder<Environment<'tcx>> {
use super::{Lower, IntoFromEnvGoal};
use rustc::hir::{Node, TraitItemKind, ImplItemKind, ItemKind, ForeignItemKind};
use rustc::ty::subst::{Subst, Substs};
// The environment of an impl Trait type is its defining function's environment.
if let Some(parent) = ty::is_impl_trait_defn(tcx, def_id) {
return environment(tcx, parent);
}
let bound_vars = Substs::bound_vars_for_item(tcx, def_id);
// Compute the bounds on `Self` and the type parameters.
let ty::InstantiatedPredicates { predicates } =
tcx.predicates_of(def_id).instantiate_identity(tcx);
let ty::InstantiatedPredicates { predicates } = tcx.predicates_of(def_id)
.instantiate_identity(tcx);
let clauses = predicates.into_iter()
.map(|predicate| predicate.lower())
.map(|predicate| predicate.subst(tcx, bound_vars))
.map(|domain_goal| domain_goal.map_bound(|bound| bound.into_from_env_goal()))
.map(|domain_goal| domain_goal.map_bound(|bound| bound.into_program_clause()))
@ -228,33 +235,43 @@ crate fn environment<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> En
let mut input_tys = FxHashSet::default();
// In an impl, we assume that the receiver type and all its constituents
// In an impl, we assume that the header trait ref and all its constituents
// are well-formed.
if is_impl {
let trait_ref = tcx.impl_trait_ref(def_id).expect("not an impl");
input_tys.extend(trait_ref.self_ty().walk());
let trait_ref = tcx.impl_trait_ref(def_id)
.expect("not an impl")
.subst(tcx, bound_vars);
input_tys.extend(
trait_ref.substs.types().flat_map(|ty| ty.walk())
);
}
// In an fn, we assume that the arguments and all their constituents are
// well-formed.
if is_fn {
let fn_sig = tcx.fn_sig(def_id);
// `skip_binder` because we move late bound regions to the root binder,
// restored in the return type
let fn_sig = tcx.fn_sig(def_id).skip_binder().subst(tcx, bound_vars);
input_tys.extend(
// FIXME: `skip_binder` seems ok for now? In a real setting,
// the late bound regions would next be instantiated with things
// in the inference table.
fn_sig.skip_binder().inputs().iter().flat_map(|ty| ty.walk())
fn_sig.inputs().iter().flat_map(|ty| ty.walk())
);
}
let clauses = clauses.chain(
input_tys.into_iter()
// Filter out type parameters
.filter(|ty| match ty.sty {
ty::Bound(..) => false,
_ => true,
})
.map(|ty| DomainGoal::FromEnv(FromEnv::Ty(ty)))
.map(|domain_goal| domain_goal.into_program_clause())
.map(Clause::Implies)
);
Environment {
ty::Binder::bind(Environment {
clauses: tcx.mk_clauses(clauses),
}
})
}

View File

@ -28,6 +28,7 @@ use rustc::traits::{
};
use rustc::ty::query::Providers;
use rustc::ty::{self, List, TyCtxt};
use rustc::ty::subst::{Subst, Substs};
use syntax::ast;
use std::iter;
@ -189,9 +190,14 @@ fn program_clauses_for_trait<'a, 'tcx>(
// }
// ```
let bound_vars = Substs::bound_vars_for_item(tcx, def_id);
// `Self: Trait<P1..Pn>`
let trait_pred = ty::TraitPredicate {
trait_ref: ty::TraitRef::identity(tcx, def_id),
trait_ref: ty::TraitRef {
def_id,
substs: bound_vars,
},
};
// `Implemented(Self: Trait<P1..Pn>)`
@ -208,11 +214,12 @@ fn program_clauses_for_trait<'a, 'tcx>(
category: ProgramClauseCategory::ImpliedBound,
};
let clauses = iter::once(Clause::ForAll(ty::Binder::dummy(implemented_from_env)));
let implemented_from_env = Clause::ForAll(ty::Binder::bind(implemented_from_env));
let where_clauses = &tcx.predicates_defined_on(def_id).predicates
.into_iter()
.map(|(wc, _)| wc.lower())
.map(|wc| wc.subst(tcx, bound_vars))
.collect::<Vec<_>>();
// Rule Implied-Bound-From-Trait
@ -230,11 +237,21 @@ fn program_clauses_for_trait<'a, 'tcx>(
.cloned()
// `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`
.map(|wc| wc.map_bound(|goal| ProgramClause {
goal: goal.into_from_env_goal(),
hypotheses,
category: ProgramClauseCategory::ImpliedBound,
}))
.map(|wc| {
// we move binders to the left
wc.map_bound(|goal| ProgramClause {
goal: goal.into_from_env_goal(),
// FIXME: As where clauses can only bind lifetimes for now,
// and that named bound regions have a def-id, it is safe
// to just inject `hypotheses` (which contains named vars bound at index `0`)
// into this binding level. This may change if we ever allow where clauses
// to bind types (e.g. for GATs things).
hypotheses,
category: ProgramClauseCategory::ImpliedBound,
})
})
.map(Clause::ForAll);
// Rule WellFormed-TraitRef
@ -246,28 +263,27 @@ fn program_clauses_for_trait<'a, 'tcx>(
// }
// ```
// `Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)`
let wf_conditions = iter::once(ty::Binder::dummy(trait_pred.lower()))
.chain(
where_clauses
.into_iter()
.map(|wc| wc.map_bound(|goal| goal.into_well_formed_goal()))
);
// `WellFormed(WC)`
let wf_conditions = where_clauses
.into_iter()
.map(|wc| wc.map_bound(|goal| goal.into_well_formed_goal()));
// `WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)`
let wf_clause = ProgramClause {
goal: DomainGoal::WellFormed(WellFormed::Trait(trait_pred)),
hypotheses: tcx.mk_goals(
wf_conditions.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
iter::once(tcx.mk_goal(GoalKind::DomainGoal(impl_trait))).chain(
wf_conditions.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx)))
)
),
category: ProgramClauseCategory::WellFormed,
};
let wf_clause = iter::once(Clause::ForAll(ty::Binder::dummy(wf_clause)));
let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
tcx.mk_clauses(
clauses
iter::once(implemented_from_env)
.chain(implied_bound_clauses)
.chain(wf_clause)
.chain(iter::once(wf_clause))
)
}
@ -286,7 +302,11 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
// }
// ```
let trait_ref = tcx.impl_trait_ref(def_id).expect("not an impl");
let bound_vars = Substs::bound_vars_for_item(tcx, def_id);
let trait_ref = tcx.impl_trait_ref(def_id)
.expect("not an impl")
.subst(tcx, bound_vars);
// `Implemented(A0: Trait<A1..An>)`
let trait_pred = ty::TraitPredicate { trait_ref }.lower();
@ -294,7 +314,8 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
// `WC`
let where_clauses = tcx.predicates_of(def_id).predicates
.into_iter()
.map(|(wc, _)| wc.lower());
.map(|(wc, _)| wc.lower())
.map(|wc| wc.subst(tcx, bound_vars));
// `Implemented(A0: Trait<A1..An>) :- WC`
let clause = ProgramClause {
@ -305,7 +326,7 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
),
category: ProgramClauseCategory::Other,
};
tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause))))
tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::bind(clause))))
}
pub fn program_clauses_for_type_def<'a, 'tcx>(
@ -322,17 +343,20 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
// }
// ```
let bound_vars = Substs::bound_vars_for_item(tcx, def_id);
// `Ty<...>`
let ty = tcx.type_of(def_id);
let ty = tcx.type_of(def_id).subst(tcx, bound_vars);
// `WC`
let where_clauses = tcx.predicates_of(def_id).predicates
.into_iter()
.map(|(wc, _)| wc.lower())
.map(|wc| wc.subst(tcx, bound_vars))
.collect::<Vec<_>>();
// `WellFormed(Ty<...>) :- WC1, ..., WCm`
let well_formed = ProgramClause {
let well_formed_clause = ProgramClause {
goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
hypotheses: tcx.mk_goals(
where_clauses
@ -342,8 +366,7 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
),
category: ProgramClauseCategory::WellFormed,
};
let well_formed_clause = iter::once(Clause::ForAll(ty::Binder::dummy(well_formed)));
let well_formed_clause = Clause::ForAll(ty::Binder::bind(well_formed_clause));
// Rule FromEnv-Type
//
@ -363,15 +386,23 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
.into_iter()
// `FromEnv(WC) :- FromEnv(Ty<...>)`
.map(|wc| wc.map_bound(|goal| ProgramClause {
goal: goal.into_from_env_goal(),
hypotheses,
category: ProgramClauseCategory::ImpliedBound,
}))
.map(|wc| {
// move the binders to the left
wc.map_bound(|goal| ProgramClause {
goal: goal.into_from_env_goal(),
// FIXME: we inject `hypotheses` into this binding level,
// which may be incorrect in the future: see the FIXME in
// `program_clauses_for_trait`
hypotheses,
category: ProgramClauseCategory::ImpliedBound,
})
})
.map(Clause::ForAll);
tcx.mk_clauses(well_formed_clause.chain(from_env_clauses))
tcx.mk_clauses(iter::once(well_formed_clause).chain(from_env_clauses))
}
pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
@ -403,7 +434,12 @@ pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
ty::AssociatedItemContainer::TraitContainer(trait_id) => trait_id,
_ => bug!("not an trait container"),
};
let trait_ref = ty::TraitRef::identity(tcx, trait_id);
let trait_bound_vars = Substs::bound_vars_for_item(tcx, trait_id);
let trait_ref = ty::TraitRef {
def_id: trait_id,
substs: trait_bound_vars,
};
let projection_ty = ty::ProjectionTy::from_ref_and_name(tcx, trait_ref, item.ident);
let placeholder_ty = tcx.mk_ty(ty::UnnormalizedProjection(projection_ty));
@ -417,6 +453,7 @@ pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
hypotheses: ty::List::empty(),
category: ProgramClauseCategory::Other,
};
let projection_eq_clause = Clause::ForAll(ty::Binder::bind(projection_eq_clause));
// Rule WellFormed-AssocTy
// ```
@ -430,11 +467,13 @@ pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
let hypothesis = tcx.mk_goal(
DomainGoal::Holds(WhereClause::Implemented(trait_predicate)).into_goal()
);
let wf_clause = ProgramClause {
goal: DomainGoal::WellFormed(WellFormed::Ty(placeholder_ty)),
hypotheses: tcx.mk_goals(iter::once(hypothesis)),
category: ProgramClauseCategory::WellFormed,
};
let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
// Rule Implied-Trait-From-AssocTy
// ```
@ -447,16 +486,17 @@ pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
let hypothesis = tcx.mk_goal(
DomainGoal::FromEnv(FromEnv::Ty(placeholder_ty)).into_goal()
);
let from_env_clause = ProgramClause {
goal: DomainGoal::FromEnv(FromEnv::Trait(trait_predicate)),
hypotheses: tcx.mk_goals(iter::once(hypothesis)),
category: ProgramClauseCategory::ImpliedBound,
};
let from_env_clause = Clause::ForAll(ty::Binder::bind(from_env_clause));
let clauses = iter::once(projection_eq_clause)
.chain(iter::once(wf_clause))
.chain(iter::once(from_env_clause));
let clauses = clauses.map(|clause| Clause::ForAll(ty::Binder::dummy(clause)));
tcx.mk_clauses(clauses)
}
@ -490,17 +530,18 @@ pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
_ => bug!("not an impl container"),
};
let impl_bound_vars = Substs::bound_vars_for_item(tcx, impl_id);
// `A0 as Trait<A1..An>`
let trait_ref = tcx.impl_trait_ref(impl_id).unwrap();
let trait_ref = tcx.impl_trait_ref(impl_id)
.unwrap()
.subst(tcx, impl_bound_vars);
// `T`
let ty = tcx.type_of(item_id);
// `Implemented(A0: Trait<A1..An>)`
let trait_implemented = ty::Binder::dummy(ty::TraitPredicate { trait_ref }.lower());
// `Implemented(A0: Trait<A1..An>)`
let hypotheses = vec![trait_implemented];
let trait_implemented: DomainGoal = ty::TraitPredicate { trait_ref }.lower();
// `<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm>`
let projection_ty = ty::ProjectionTy::from_ref_and_name(tcx, trait_ref, item.ident);
@ -509,16 +550,16 @@ pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
let normalize_goal = DomainGoal::Normalize(ty::ProjectionPredicate { projection_ty, ty });
// `Normalize(... -> T) :- ...`
let clause = ProgramClause {
let normalize_clause = ProgramClause {
goal: normalize_goal,
hypotheses: tcx.mk_goals(
hypotheses
.into_iter()
.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
iter::once(tcx.mk_goal(GoalKind::DomainGoal(trait_implemented)))
),
category: ProgramClauseCategory::Other,
};
tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause))))
let normalize_clause = Clause::ForAll(ty::Binder::bind(normalize_clause));
tcx.mk_clauses(iter::once(normalize_clause))
}
pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) {
@ -548,7 +589,7 @@ impl<'a, 'tcx> ClauseDumper<'a, 'tcx> {
if attr.check_name("rustc_dump_env_program_clauses") {
let environment = self.tcx.environment(def_id);
clauses = Some(self.tcx.program_clauses_for_env(environment));
clauses = Some(self.tcx.program_clauses_for_env(*environment.skip_binder()));
}
if let Some(clauses) = clauses {