Skip to content

Migrate Vec<ParameterKinds<()>> and Vec<ParameterKinds<UniverseIndex>> to interned #386

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Apr 17, 2020
Merged
Show file tree
Hide file tree
Changes from 7 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 17 additions & 0 deletions chalk-engine/src/forest.rs
Original file line number Diff line number Diff line change
Expand Up @@ -113,6 +113,23 @@ pub enum SubstitutionResult<S> {
Floundered,
}

impl<S> SubstitutionResult<S> {
pub fn as_ref(&self) -> SubstitutionResult<&S> {
match self {
SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(subst),
SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(subst),
SubstitutionResult::Floundered => SubstitutionResult::Floundered,
}
}
pub fn map<U, F: FnOnce(S) -> U>(self, f: F) -> SubstitutionResult<U> {
match self {
SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(f(subst)),
SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(f(subst)),
SubstitutionResult::Floundered => SubstitutionResult::Floundered,
}
}
}

impl<S: Display> Display for SubstitutionResult<S> {
fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
Expand Down
10 changes: 9 additions & 1 deletion chalk-integration/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ pub mod program;
pub mod program_environment;
pub mod query;

use chalk_ir::interner::{ChalkIr, HasInterner};
pub use chalk_ir::interner::{Identifier, RawId};
use chalk_ir::Binders;

Expand All @@ -21,9 +22,16 @@ pub enum TypeSort {
Opaque,
}

#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
pub struct Unit;

impl HasInterner for Unit {
type Interner = ChalkIr;
}

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct TypeKind {
pub sort: TypeSort,
pub name: Identifier,
pub binders: Binders<()>,
pub binders: Binders<Unit>,
}
53 changes: 35 additions & 18 deletions chalk-integration/src/lowering.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use chalk_ir::cast::{Cast, Caster};
use chalk_ir::interner::ChalkIr;
use chalk_ir::interner::{ChalkIr, HasInterner};
use chalk_ir::{
self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId,
self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId, ParameterKinds,
QuantifiedWhereClauses, StructId, Substitution, TraitId,
};
use chalk_parse::ast::*;
Expand Down Expand Up @@ -174,11 +174,16 @@ impl<'k> Env<'k> {
where
I: IntoIterator<Item = chalk_ir::ParameterKind<Ident>>,
I::IntoIter: ExactSizeIterator,
T: HasInterner<Interner = ChalkIr>,
OP: FnOnce(&Self) -> LowerResult<T>,
{
let interner = &ChalkIr;
let binders: Vec<_> = binders.into_iter().collect();
let env = self.introduce(binders.iter().cloned())?;
Ok(chalk_ir::Binders::new(binders.anonymize(), op(&env)?))
Ok(chalk_ir::Binders::new(
ParameterKinds::from(interner, binders.anonymize()),
op(&env)?,
))
}
}

Expand Down Expand Up @@ -594,10 +599,14 @@ trait LowerWhereClauses {

impl LowerTypeKind for StructDefn {
fn lower_type_kind(&self) -> LowerResult<TypeKind> {
let interner = &ChalkIr;
Ok(TypeKind {
sort: TypeSort::Struct,
name: self.name.str,
binders: chalk_ir::Binders::new(self.all_parameters().anonymize(), ()),
binders: chalk_ir::Binders::new(
ParameterKinds::from(interner, self.all_parameters().anonymize()),
crate::Unit,
),
})
}
}
Expand All @@ -610,26 +619,31 @@ impl LowerWhereClauses for StructDefn {

impl LowerTypeKind for TraitDefn {
fn lower_type_kind(&self) -> LowerResult<TypeKind> {
let interner = &ChalkIr;
let binders: Vec<_> = self.parameter_kinds.iter().map(|p| p.lower()).collect();
Ok(TypeKind {
sort: TypeSort::Trait,
name: self.name.str,
binders: chalk_ir::Binders::new(
// for the purposes of the *type*, ignore `Self`:
binders.anonymize(),
(),
ParameterKinds::from(interner, binders.anonymize()),
crate::Unit,
),
})
}
}

impl LowerTypeKind for OpaqueTyDefn {
fn lower_type_kind(&self) -> LowerResult<TypeKind> {
let interner = &ChalkIr;
let binders: Vec<_> = self.parameter_kinds.iter().map(|p| p.lower()).collect();
Ok(TypeKind {
sort: TypeSort::Opaque,
name: self.identifier.str,
binders: chalk_ir::Binders::new(binders.anonymize(), ()),
binders: chalk_ir::Binders::new(
ParameterKinds::from(interner, binders.anonymize()),
crate::Unit,
),
})
}
}
Expand Down Expand Up @@ -835,6 +849,7 @@ trait LowerTraitBound {

impl LowerTraitBound for TraitBound {
fn lower(&self, env: &Env) -> LowerResult<rust_ir::TraitBound<ChalkIr>> {
let interner = &ChalkIr;
let trait_id = env.lookup_trait(self.trait_name)?;

let k = env.trait_kind(trait_id);
Expand All @@ -848,15 +863,15 @@ impl LowerTraitBound for TraitBound {
.map(|a| Ok(a.lower(env)?))
.collect::<LowerResult<Vec<_>>>()?;

if parameters.len() != k.binders.len() {
if parameters.len() != k.binders.len(interner) {
Err(RustIrError::IncorrectNumberOfTypeParameters {
identifier: self.trait_name,
expected: k.binders.len(),
expected: k.binders.len(interner),
actual: parameters.len(),
})?;
}

for (binder, param) in k.binders.binders.iter().zip(parameters.iter()) {
for (binder, param) in k.binders.binders.iter(interner).zip(parameters.iter()) {
if binder.kind() != param.kind() {
Err(RustIrError::IncorrectTraitParameterKind {
identifier: self.trait_name,
Expand Down Expand Up @@ -1062,10 +1077,10 @@ impl LowerTy for Ty {
Ty::Id { name } => match env.lookup_type(name)? {
TypeLookup::Struct(id) => {
let k = env.struct_kind(id);
if k.binders.len() > 0 {
if k.binders.len(interner) > 0 {
Err(RustIrError::IncorrectNumberOfTypeParameters {
identifier: name,
expected: k.binders.len(),
expected: k.binders.len(interner),
actual: 0,
})
} else {
Expand Down Expand Up @@ -1118,10 +1133,10 @@ impl LowerTy for Ty {
};

let k = env.struct_kind(id);
if k.binders.len() != args.len() {
if k.binders.len(interner) != args.len() {
Err(RustIrError::IncorrectNumberOfTypeParameters {
identifier: name,
expected: k.binders.len(),
expected: k.binders.len(interner),
actual: args.len(),
})?;
}
Expand All @@ -1131,7 +1146,7 @@ impl LowerTy for Ty {
args.iter().map(|t| Ok(t.lower(env)?)),
)?;

for (param, arg) in k.binders.binders.iter().zip(args.iter()) {
for (param, arg) in k.binders.binders.iter(interner).zip(args.iter()) {
if param.kind() != arg.kind() {
Err(RustIrError::IncorrectParameterKind {
identifier: name,
Expand Down Expand Up @@ -1362,14 +1377,16 @@ pub trait LowerGoal<A> {

impl LowerGoal<LoweredProgram> for Goal {
fn lower(&self, program: &LoweredProgram) -> LowerResult<chalk_ir::Goal<ChalkIr>> {
let interner = &ChalkIr;
let associated_ty_lookups: BTreeMap<_, _> = program
.associated_ty_data
.iter()
.map(|(&associated_ty_id, datum)| {
let trait_datum = &program.trait_data[&datum.trait_id];
let num_trait_params = trait_datum.binders.len();
let num_addl_params = datum.binders.len() - num_trait_params;
let addl_parameter_kinds = datum.binders.binders[..num_addl_params].to_owned();
let num_trait_params = trait_datum.binders.len(interner);
let num_addl_params = datum.binders.len(interner) - num_trait_params;
let addl_parameter_kinds =
datum.binders.binders.as_slice(interner)[..num_addl_params].to_owned();
let lookup = AssociatedTyLookup {
id: associated_ty_id,
addl_parameter_kinds,
Expand Down
27 changes: 27 additions & 0 deletions chalk-integration/src/program.rs
Original file line number Diff line number Diff line change
Expand Up @@ -188,6 +188,33 @@ impl tls::DebugContext for Program {
write!(fmt, "{:?}", parameter.data(interner).inner_debug())
}

fn debug_parameter_kinds(
&self,
parameter_kinds: &chalk_ir::ParameterKinds<ChalkIr>,
fmt: &mut fmt::Formatter<'_>,
) -> Result<(), fmt::Error> {
let interner = self.interner();
write!(fmt, "{:?}", parameter_kinds.as_slice(interner))
}

fn debug_parameter_kinds_with_angles(
&self,
parameter_kinds: &chalk_ir::ParameterKinds<ChalkIr>,
fmt: &mut fmt::Formatter<'_>,
) -> Result<(), fmt::Error> {
let interner = self.interner();
write!(fmt, "{:?}", parameter_kinds.inner_debug(interner))
}

fn debug_canonical_var_kinds(
&self,
parameter_kinds: &chalk_ir::CanonicalVarKinds<ChalkIr>,
fmt: &mut fmt::Formatter<'_>,
) -> Result<(), fmt::Error> {
let interner = self.interner();
write!(fmt, "{:?}", parameter_kinds.as_slice(interner))
}

fn debug_goal(
&self,
goal: &Goal<ChalkIr>,
Expand Down
14 changes: 8 additions & 6 deletions chalk-ir/src/cast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,8 @@ reflexive_impl!(for(I: Interner) Goal<I>);
reflexive_impl!(for(I: Interner) WhereClause<I>);
reflexive_impl!(for(I: Interner) ProgramClause<I>);
reflexive_impl!(for(I: Interner) QuantifiedWhereClause<I>);
reflexive_impl!(for(I: Interner) ParameterKinds<I>);
reflexive_impl!(for(I: Interner) CanonicalVarKinds<I>);

impl<I: Interner> CastTo<WhereClause<I>> for TraitRef<I> {
fn cast_to(self, _interner: &I) -> WhereClause<I> {
Expand Down Expand Up @@ -138,7 +140,7 @@ impl<I: Interner> CastTo<Goal<I>> for EqGoal<I> {
}
}

impl<T: CastTo<Goal<I>>, I: Interner> CastTo<Goal<I>> for Binders<T> {
impl<I: Interner, T: HasInterner<Interner = I> + CastTo<Goal<I>>> CastTo<Goal<I>> for Binders<T> {
fn cast_to(self, interner: &I) -> Goal<I> {
GoalData::Quantified(
QuantifierKind::ForAll,
Expand Down Expand Up @@ -193,10 +195,10 @@ where
}
}

impl<T, I> CastTo<ProgramClause<I>> for Binders<T>
impl<I, T> CastTo<ProgramClause<I>> for Binders<T>
where
T: CastTo<DomainGoal<I>>,
I: Interner,
T: HasInterner<Interner = I> + CastTo<DomainGoal<I>>,
{
fn cast_to(self, interner: &I) -> ProgramClause<I> {
ProgramClauseData::ForAll(self.map(|bound| ProgramClauseImplication {
Expand Down Expand Up @@ -268,16 +270,16 @@ where
impl<T, U> CastTo<Canonical<U>> for Canonical<T>
where
T: CastTo<U> + HasInterner,
U: HasInterner,
U: HasInterner<Interner = T::Interner>,
{
fn cast_to(self, interner: &U::Interner) -> Canonical<U> {
fn cast_to(self, interner: &T::Interner) -> Canonical<U> {
// Subtle point: It should be ok to re-use the binders here,
// because `cast()` never introduces new inference variables,
// nor changes the "substance" of the type we are working
// with. It just introduces new wrapper types.
Canonical {
value: self.value.cast(interner),
binders: self.binders,
binders: self.binders.cast(interner),
}
}
}
Expand Down
2 changes: 1 addition & 1 deletion chalk-ir/src/could_match.rs
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ where

fn zip_binders<T>(&mut self, a: &Binders<T>, b: &Binders<T>) -> Fallible<()>
where
T: Zip<I>,
T: HasInterner + Zip<I>,
{
Zip::zip_with(self, &a.value, &b.value)
}
Expand Down
Loading