Skip to content

Commit

Permalink
add tests
Browse files Browse the repository at this point in the history
  • Loading branch information
basil-cow committed Jun 6, 2020
1 parent 2cbebf4 commit 1d16b9e
Show file tree
Hide file tree
Showing 13 changed files with 871 additions and 302 deletions.
18 changes: 14 additions & 4 deletions chalk-engine/src/logic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,8 @@ use crate::{
use chalk_ir::interner::Interner;
use chalk_ir::{debug, debug_heading, info, info_heading};
use chalk_ir::{
Canonical, ConstrainedSubst, Floundered, Goal, GoalData, InEnvironment, NoSolution,
Substitution, UCanonical, UniverseMap,
Canonical, ConstrainedSubst, DomainGoal, Floundered, Goal, GoalData, InEnvironment, NoSolution,
Substitution, UCanonical, UniverseMap, WhereClause,
};

type RootSearchResult<T> = Result<T, RootSearchFail>;
Expand Down Expand Up @@ -251,8 +251,18 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
) -> Table<I> {
let mut table = Table::new(goal.clone(), context.is_coinductive(&goal));
let (mut infer, subst, environment, goal) = context.instantiate_ucanonical_goal(&goal);
match goal.data(context.interner()) {
GoalData::DomainGoal(domain_goal) => {
let goal_data = goal.data(context.interner());

let is_outlives_goal = |dg: &DomainGoal<I>| {
if let DomainGoal::Holds(WhereClause::LifetimeOutlives(_)) = dg {
true
} else {
false
}
};

match goal_data {
GoalData::DomainGoal(domain_goal) if !is_outlives_goal(domain_goal) => {
match context.program_clauses(&environment, &domain_goal, &mut infer) {
Ok(clauses) => {
for clause in clauses {
Expand Down
125 changes: 83 additions & 42 deletions chalk-solve/src/clauses/builtin_traits/unsize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,9 @@ use chalk_ir::{
cast::Cast,
interner::HasInterner,
visit::{visitors::FindAny, SuperVisit, Visit, VisitResult, Visitor},
ApplicationTy, Binders, DebruijnIndex, DomainGoal, DynTy, EqGoal, Goal, QuantifiedWhereClauses,
Substitution, TraitId, Ty, TyData, TypeName, WhereClause,
ApplicationTy, Binders, Const, ConstValue, DebruijnIndex, DomainGoal, DynTy, EqGoal, Goal,
LifetimeOutlives, QuantifiedWhereClauses, Substitution, TraitId, Ty, TyData, TypeName,
WhereClause,
};

struct UnsizeParameterCollector<'a, I: Interner> {
Expand All @@ -24,14 +25,12 @@ impl<'a, I: Interner> Visitor<'a, I> for UnsizeParameterCollector<'a, I> {
self
}

// FIXME(areredify) when const generics land, collect const variables too

fn visit_ty(&mut self, ty: &Ty<I>, outer_binder: DebruijnIndex) -> Self::Result {
let interner = self.interner;

match ty.data(interner) {
TyData::BoundVar(bound_var) => {
// check if bound var referse to the outermost binder
// check if bound var refers to the outermost binder
if bound_var.debruijn.shifted_in() == outer_binder {
self.parameters.insert(bound_var.index);
}
Expand All @@ -40,6 +39,20 @@ impl<'a, I: Interner> Visitor<'a, I> for UnsizeParameterCollector<'a, I> {
}
}

fn visit_const(&mut self, constant: &Const<I>, outer_binder: DebruijnIndex) -> Self::Result {
let interner = self.interner;

match constant.data(interner).value {
ConstValue::BoundVar(bound_var) => {
// check if bound var refers to the outermost binder
if bound_var.debruijn.shifted_in() == outer_binder {
self.parameters.insert(bound_var.index);
}
}
_ => (),
}
}

fn interner(&self) -> &'a I {
self.interner
}
Expand Down Expand Up @@ -87,6 +100,23 @@ impl<'a, 'p, I: Interner> Visitor<'a, I> for ParameterOccurenceCheck<'a, 'p, I>
}
}

fn visit_const(&mut self, constant: &Const<I>, outer_binder: DebruijnIndex) -> Self::Result {
let interner = self.interner;

match constant.data(interner).value {
ConstValue::BoundVar(bound_var) => {
if bound_var.debruijn.shifted_in() == outer_binder
&& self.parameters.contains(&bound_var.index)
{
FindAny::FOUND
} else {
FindAny::new()
}
}
_ => FindAny::new(),
}
}

fn interner(&self) -> &'a I {
self.interner
}
Expand All @@ -110,36 +140,25 @@ fn principal_id<'a, I: Interner>(
) -> Option<TraitId<I>> {
let interner = db.interner();

let principal_id = bounds
return bounds
.skip_binders()
.iter(interner)
.next()
.expect("Expected trait object to have at least one trait bound")
.trait_id()?;

if db.trait_datum(principal_id).is_auto_trait() {
None
} else {
Some(principal_id)
}
.filter_map(|b| b.trait_id())
.filter(|&id| !db.trait_datum(id).is_auto_trait())
.next();
}

fn auto_trait_ids<'a, I: Interner>(
db: &dyn RustIrDatabase<I>,
db: &'a dyn RustIrDatabase<I>,
bounds: &'a Binders<QuantifiedWhereClauses<I>>,
) -> impl Iterator<Item = TraitId<I>> + 'a {
let interner = db.interner();
// all trait ref where clauses after the principal are auto traits
let to_skip = if principal_id(db, bounds).is_some() {
1
} else {
0
};

bounds
.skip_binders()
.iter(interner)
.skip(to_skip)
.filter_map(|clause| clause.trait_id())
.filter(move |&id| db.trait_datum(id).is_auto_trait())
}

pub fn add_unsize_program_clauses<I: Interner>(
Expand Down Expand Up @@ -196,10 +215,11 @@ pub fn add_unsize_program_clauses<I: Interner>(
}

// COMMENT FROM RUSTC:
// ------------------
// Require that the traits involved in this upcast are **equal**;
// only the **lifetime bound** is changed.
//
// FIXME: This condition is arguably too strong -- it would
// This condition is arguably too strong -- it would
// suffice for the source trait to be a *subtype* of the target
// trait. In particular, changing from something like
// `for<'a, 'b> Foo<'a, 'b>` to `for<'a> Foo<'a, 'a>` should be
Expand All @@ -211,11 +231,13 @@ pub fn add_unsize_program_clauses<I: Interner>(
// with what our behavior should be there. -nikomatsakis
// ------------------

// Filter out auto traits of source that are not present in target
// and change source lifetime to target lifetime
// Construct a new trait object type by taking the source ty,
// filtering out auto traits of source that are not present in target
// and changing source lifetime to target lifetime.
//
// This new type should be equal to target type.
let source_ty = TyData::Dyn(DynTy {
// In order for the coercion to be valid, this new type
// should be equal to target type.
let new_source_ty = TyData::Dyn(DynTy {
bounds: bounds_a.map_ref(|bounds| {
QuantifiedWhereClauses::from(
interner,
Expand All @@ -238,16 +260,15 @@ pub fn add_unsize_program_clauses<I: Interner>(

// Check that new source is equal to target
let eq_goal = EqGoal {
a: source_ty.cast(interner),
a: new_source_ty.cast(interner),
b: target_ty.clone().cast(interner),
}
.cast(interner);

// FIXME(areredify) change this to outlives once #419 lands
let lifetime_outlives_goal = EqGoal {
a: lifetime_a.clone().cast(interner),
b: lifetime_b.clone().cast(interner),
}
let lifetime_outlives_goal: Goal<I> = WhereClause::LifetimeOutlives(LifetimeOutlives {
a: lifetime_a.clone(),
b: lifetime_b.clone(),
})
.cast(interner);

builder.push_clause(trait_ref.clone(), [eq_goal, lifetime_outlives_goal].iter());
Expand Down Expand Up @@ -294,6 +315,27 @@ pub fn add_unsize_program_clauses<I: Interner>(
);
}

(
TyData::Apply(ApplicationTy {
name: TypeName::Array,
substitution: array_subst,
}),
TyData::Apply(ApplicationTy {
name: TypeName::Slice,
substitution: slice_subst,
}),
) => {
let array_ty = array_subst.at(interner, 0);
let slice_ty = slice_subst.at(interner, 0);

let eq_goal = EqGoal {
a: array_ty.clone(),
b: slice_ty.clone(),
};

builder.push_clause(trait_ref.clone(), iter::once(eq_goal));
}

// Struct<T> -> Struct<U>
// Unsizing of enums is not allowed
(
Expand All @@ -318,19 +360,18 @@ pub fn add_unsize_program_clauses<I: Interner>(
return;
}

let struct_tail_field = struct_datum
let adt_tail_field = struct_datum
.binders
.map_ref(|bound| bound.fields.last().unwrap());

// Collect unsize parameters that last field contains and
// ensure there at least one of them.
let unsize_parameter_candidates =
outer_binder_parameters_used(interner, &struct_tail_field);
outer_binder_parameters_used(interner, &adt_tail_field);

if unsize_parameter_candidates.len() == 0 {
return;
}

// Ensure none of the other fields mention the parameters used
// in unsizing.
if uses_outer_binder_params(
Expand All @@ -345,15 +386,15 @@ pub fn add_unsize_program_clauses<I: Interner>(

let parameters_a = substitution_a.parameters(interner);
let parameters_b = substitution_b.parameters(interner);
// Check that the source struct with the target's
// Check that the source adt with the target's
// unsizing parameters is equal to the target.
let substitution = Substitution::from(
interner,
parameters_a.iter().enumerate().map(|(i, p)| {
if unsize_parameter_candidates.contains(&i) {
p
} else {
&parameters_b[i]
} else {
p
}
}),
);
Expand All @@ -370,8 +411,8 @@ pub fn add_unsize_program_clauses<I: Interner>(
.cast(interner);

// Extract `TailField<T>` and `TailField<U>` from `Struct<T>` and `Struct<U>`.
let source_tail_field = struct_tail_field.substitute(interner, substitution_a);
let target_tail_field = struct_tail_field.substitute(interner, substitution_b);
let source_tail_field = adt_tail_field.substitute(interner, substitution_a);
let target_tail_field = adt_tail_field.substitute(interner, substitution_b);

// Check that `TailField<T>: Unsize<TailField<U>>`
let last_field_unsizing_goal: Goal<I> = TraitRef {
Expand Down
4 changes: 2 additions & 2 deletions tests/test/auto_traits.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,15 +6,15 @@ use super::*;
fn auto_semantics() {
test! {
program {
#[lang(sized)] trait Sized { }
trait Sized { }
#[auto] trait Send { }

struct TypeA { }

struct Ptr<T> { }
impl<T> Send for Ptr<T> where T: Send { }

struct List<T> where T: Sized {
struct List<T> {
data: T,
next: Ptr<List<T>>
}
Expand Down
4 changes: 4 additions & 0 deletions tests/test/builtin_impls.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
mod clone;
mod copy;
mod sized;
mod unsize;
64 changes: 64 additions & 0 deletions tests/test/builtin_impls/clone.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
use crate::test::*;

#[test]
fn tuples_are_clone() {
test! {
program {
#[non_enumerable] // see above
#[lang(clone)]
trait Clone { }

struct S {}

impl Clone for u8 {}
}

goal {
([u8],): Clone
} yields {
"No possible solution"
}

goal {
(u8, [u8]): Clone
} yields {
"No possible solution"
}

goal {
([u8], u8): Clone
} yields {
"No possible solution"
}

goal {
(): Clone
} yields {
"Unique; substitution [], lifetime constraints []"
}

goal {
(u8,): Clone
} yields {
"Unique; substitution [], lifetime constraints []"
}

goal {
(u8, u8): Clone
} yields {
"Unique; substitution [], lifetime constraints []"
}

goal {
exists<T> { (T, u8): Clone }
} yields {
"Ambiguous"
}

goal {
forall<T> { if (T: Clone) { (T, u8): Clone } }
} yields {
"Unique; substitution [], lifetime constraints []"
}
}
}
Loading

0 comments on commit 1d16b9e

Please sign in to comment.