//! variables from the current `Binder`.
use rustc_middle::traits::{
- ChalkEnvironmentAndGoal, ChalkEnvironmentClause, ChalkRustDefId as RustDefId,
- ChalkRustInterner as RustInterner,
+ ChalkEnvironmentAndGoal, ChalkEnvironmentClause, ChalkRustInterner as RustInterner,
};
use rustc_middle::ty::fold::TypeFolder;
use rustc_middle::ty::subst::{GenericArg, GenericArgKind, SubstsRef};
impl<'tcx> LowerInto<'tcx, chalk_ir::AliasTy<RustInterner<'tcx>>> for ty::ProjectionTy<'tcx> {
fn lower_into(self, interner: &RustInterner<'tcx>) -> chalk_ir::AliasTy<RustInterner<'tcx>> {
chalk_ir::AliasTy::Projection(chalk_ir::ProjectionTy {
- associated_ty_id: chalk_ir::AssocTypeId(RustDefId::AssocTy(self.item_def_id)),
+ associated_ty_id: chalk_ir::AssocTypeId(self.item_def_id),
substitution: self.substs.lower_into(interner),
})
}
.intern(interner),
)
}
- // FIXME(chalk): need to add RegionOutlives/TypeOutlives
- ty::PredicateKind::RegionOutlives(_) => None,
+ ty::PredicateKind::RegionOutlives(predicate) => {
+ let (predicate, binders, _named_regions) =
+ collect_bound_vars(interner, interner.tcx, predicate);
+
+ Some(
+ chalk_ir::ProgramClauseData::ForAll(chalk_ir::Binders::new(
+ binders,
+ chalk_ir::ProgramClauseImplication {
+ consequence: chalk_ir::DomainGoal::Holds(
+ chalk_ir::WhereClause::LifetimeOutlives(chalk_ir::LifetimeOutlives {
+ a: predicate.0.lower_into(interner),
+ b: predicate.1.lower_into(interner),
+ })
+ ),
+ conditions: chalk_ir::Goals::new(interner),
+ priority: chalk_ir::ClausePriority::High,
+ },
+ ))
+ .intern(interner),
+ )
+ },
+ // FIXME(chalk): need to add TypeOutlives
ty::PredicateKind::TypeOutlives(_) => None,
ty::PredicateKind::Projection(predicate) => {
let (predicate, binders, _named_regions) =
fn lower_into(self, interner: &RustInterner<'tcx>) -> chalk_ir::GoalData<RustInterner<'tcx>> {
match self.kind() {
ty::PredicateKind::Trait(predicate, _) => predicate.lower_into(interner),
- // FIXME(chalk): we need to register constraints.
- ty::PredicateKind::RegionOutlives(_predicate) => {
- chalk_ir::GoalData::All(chalk_ir::Goals::new(interner))
+ ty::PredicateKind::RegionOutlives(predicate) => {
+ let (predicate, binders, _named_regions) =
+ collect_bound_vars(interner, interner.tcx, predicate);
+
+ chalk_ir::GoalData::Quantified(
+ chalk_ir::QuantifierKind::ForAll,
+ chalk_ir::Binders::new(
+ binders,
+ chalk_ir::GoalData::DomainGoal(chalk_ir::DomainGoal::Holds(
+ chalk_ir::WhereClause::LifetimeOutlives(chalk_ir::LifetimeOutlives {
+ a: predicate.0.lower_into(interner),
+ b: predicate.1.lower_into(interner),
+ })
+ )).intern(interner)
+ )
+ )
}
+ // FIXME(chalk): TypeOutlives
ty::PredicateKind::TypeOutlives(_predicate) => {
chalk_ir::GoalData::All(chalk_ir::Goals::new(interner))
}
ty::PredicateKind::Projection(predicate) => predicate.lower_into(interner),
ty::PredicateKind::WellFormed(arg) => match arg.unpack() {
GenericArgKind::Type(ty) => match ty.kind {
- // These types are always WF.
- ty::Str | ty::Placeholder(..) | ty::Error(_) | ty::Never => {
- chalk_ir::GoalData::All(chalk_ir::Goals::new(interner))
- }
+ // FIXME(chalk): In Chalk, a placeholder is WellFormed if it
+ // `FromEnv`. However, when we "lower" Params, we don't update
+ // the environment.
+ ty::Placeholder(..) => chalk_ir::GoalData::All(chalk_ir::Goals::new(interner)),
- // FIXME(chalk): Well-formed only if ref lifetime outlives type
- ty::Ref(..) => chalk_ir::GoalData::All(chalk_ir::Goals::new(interner)),
-
- ty::Param(..) => panic!("No Params expected."),
-
- // FIXME(chalk) -- ultimately I think this is what we
- // want to do, and we just have rules for how to prove
- // `WellFormed` for everything above, instead of
- // inlining a bit the rules of the proof here.
_ => chalk_ir::GoalData::DomainGoal(chalk_ir::DomainGoal::WellFormed(
chalk_ir::WellFormed::Ty(ty.lower_into(interner)),
)),
GenericArgKind::Lifetime(lt) => bug!("unexpect well formed predicate: {:?}", lt),
},
+ ty::PredicateKind::ObjectSafe(t) => {
+ chalk_ir::GoalData::DomainGoal(chalk_ir::DomainGoal::ObjectSafe(chalk_ir::TraitId(*t)))
+ }
+
// FIXME(chalk): other predicates
//
// We can defer this, but ultimately we'll want to express
// some of these in terms of chalk operations.
- ty::PredicateKind::ObjectSafe(..)
- | ty::PredicateKind::ClosureKind(..)
+ ty::PredicateKind::ClosureKind(..)
| ty::PredicateKind::Subtype(..)
| ty::PredicateKind::ConstEvaluatable(..)
| ty::PredicateKind::ConstEquate(..) => {
{
fn lower_into(self, interner: &RustInterner<'tcx>) -> chalk_ir::TraitRef<RustInterner<'tcx>> {
chalk_ir::TraitRef {
- trait_id: chalk_ir::TraitId(RustDefId::Trait(self.def_id)),
+ trait_id: chalk_ir::TraitId(self.def_id),
substitution: self.substs.lower_into(interner),
}
}
ast::FloatTy::F32 => float(chalk_ir::FloatTy::F32),
ast::FloatTy::F64 => float(chalk_ir::FloatTy::F64),
},
- Adt(def, substs) => {
- apply(struct_ty(RustDefId::Adt(def.did)), substs.lower_into(interner))
- }
+ Adt(def, substs) => apply(struct_ty(def.did), substs.lower_into(interner)),
Foreign(_def_id) => unimplemented!(),
Str => apply(chalk_ir::TypeName::Str, empty()),
Array(ty, _) => apply(
- struct_ty(RustDefId::Array),
- chalk_ir::Substitution::from1(
+ chalk_ir::TypeName::Array,
+ chalk_ir::Substitution::from(
interner,
- chalk_ir::GenericArgData::Ty(ty.lower_into(interner)).intern(interner),
+ &[
+ chalk_ir::GenericArgData::Ty(ty.lower_into(interner)).intern(interner),
+ chalk_ir::GenericArgData::Const(
+ chalk_ir::ConstData {
+ ty: apply(chalk_ir::TypeName::Tuple(0), empty()),
+ value: chalk_ir::ConstValue::Concrete(chalk_ir::ConcreteConst {
+ interned: 0,
+ }),
+ }
+ .intern(interner),
+ )
+ .intern(interner),
+ ],
),
),
Slice(ty) => apply(
),
)
}
- FnDef(def_id, _) => apply(struct_ty(RustDefId::FnDef(def_id)), empty()),
+ FnDef(def_id, substs) => apply(
+ chalk_ir::TypeName::FnDef(chalk_ir::FnDefId(def_id)),
+ substs.lower_into(interner),
+ ),
FnPtr(sig) => {
let (inputs_and_outputs, binders, _named_regions) =
collect_bound_vars(interner, interner.tcx, &sig.inputs_and_output());
Closure(_def_id, _) => unimplemented!(),
Generator(_def_id, _substs, _) => unimplemented!(),
GeneratorWitness(_) => unimplemented!(),
- Never => apply(struct_ty(RustDefId::Never), empty()),
+ Never => apply(chalk_ir::TypeName::Never, empty()),
Tuple(substs) => {
apply(chalk_ir::TypeName::Tuple(substs.len()), substs.lower_into(interner))
}
Projection(proj) => TyData::Alias(proj.lower_into(interner)).intern(interner),
Opaque(def_id, substs) => {
TyData::Alias(chalk_ir::AliasTy::Opaque(chalk_ir::OpaqueTy {
- opaque_ty_id: chalk_ir::OpaqueTyId(RustDefId::Opaque(def_id)),
+ opaque_ty_id: chalk_ir::OpaqueTyId(def_id),
substitution: substs.lower_into(interner),
}))
.intern(interner)
chalk_ir::WhereClause::Implemented(predicate.trait_ref.lower_into(interner)),
))
}
- ty::PredicateKind::RegionOutlives(_predicate) => None,
+ ty::PredicateKind::RegionOutlives(predicate) => {
+ let (predicate, binders, _named_regions) =
+ collect_bound_vars(interner, interner.tcx, predicate);
+
+ Some(chalk_ir::Binders::new(
+ binders,
+ chalk_ir::WhereClause::LifetimeOutlives(chalk_ir::LifetimeOutlives {
+ a: predicate.0.lower_into(interner),
+ b: predicate.1.lower_into(interner),
+ }),
+ ))
+
+ },
ty::PredicateKind::TypeOutlives(_predicate) => None,
ty::PredicateKind::Projection(_predicate) => None,
ty::PredicateKind::WellFormed(_ty) => None,
chalk_ir::Binders::new(
chalk_ir::VariableKinds::new(interner),
chalk_ir::WhereClause::Implemented(chalk_ir::TraitRef {
- trait_id: chalk_ir::TraitId(RustDefId::Trait(*def_id)),
+ trait_id: chalk_ir::TraitId(*def_id),
substitution: substs.lower_into(interner),
}),
)
ty::ExistentialPredicate::AutoTrait(def_id) => chalk_ir::Binders::new(
chalk_ir::VariableKinds::new(interner),
chalk_ir::WhereClause::Implemented(chalk_ir::TraitRef {
- trait_id: chalk_ir::TraitId(RustDefId::Trait(*def_id)),
+ trait_id: chalk_ir::TraitId(*def_id),
substitution: chalk_ir::Substitution::empty(interner),
}),
),
projects / rust.git / blobdiff