Skip to content

Commit

Permalink
Merge pull request #54 from scalexm/cologic
Browse files Browse the repository at this point in the history
Auto traits
  • Loading branch information
nikomatsakis authored Jul 17, 2017
2 parents bb32a14 + 72e6553 commit 7eb0f08
Show file tree
Hide file tree
Showing 13 changed files with 640 additions and 51 deletions.
18 changes: 17 additions & 1 deletion chalk-parse/src/ast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ pub struct TraitDefn {
pub parameter_kinds: Vec<ParameterKind>,
pub where_clauses: Vec<WhereClause>,
pub assoc_ty_defns: Vec<AssocTyDefn>,
pub auto: bool,
}

pub struct AssocTyDefn {
Expand Down Expand Up @@ -93,7 +94,7 @@ impl Kinded for Parameter {

pub struct Impl {
pub parameter_kinds: Vec<ParameterKind>,
pub trait_ref: TraitRef,
pub trait_ref: PolarizedTraitRef,
pub where_clauses: Vec<WhereClause>,
pub assoc_ty_values: Vec<AssocTyValue>,
}
Expand Down Expand Up @@ -139,6 +140,21 @@ pub struct TraitRef {
pub args: Vec<Parameter>,
}

pub enum PolarizedTraitRef {
Positive(TraitRef),
Negative(TraitRef),
}

impl PolarizedTraitRef {
pub fn from_bool(polarity: bool, trait_ref: TraitRef) -> PolarizedTraitRef {
if polarity {
PolarizedTraitRef::Positive(trait_ref)
} else {
PolarizedTraitRef::Negative(trait_ref)
}
}
}

#[derive(Copy, Clone, Debug)]
pub struct Identifier {
pub str: InternedString,
Expand Down
16 changes: 12 additions & 4 deletions chalk-parse/src/parser.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -47,12 +47,17 @@ StructDefn: StructDefn = {
}
};

AutoKeyword: () = "#" "[" "auto" "]";

TraitDefn: TraitDefn = {
"trait" <n:Id><p:Angle<ParameterKind>> <w:WhereClauses> "{" <a:AssocTyDefn*> "}" => TraitDefn {
<auto:AutoKeyword?> "trait" <n:Id><p:Angle<ParameterKind>> <w:WhereClauses> "{"
<a:AssocTyDefn*> "}" =>
TraitDefn {
name: n,
parameter_kinds: p,
where_clauses: w,
assoc_ty_defns: a,
auto: auto.is_some(),
}
};

Expand All @@ -64,14 +69,17 @@ AssocTyDefn: AssocTyDefn = {
};

Impl: Impl = {
"impl" <p:Angle<ParameterKind>> <t:Id> <a:Angle<Parameter>> "for" <s:Ty> <w:WhereClauses> "{"
<assoc:AssocTyValue*>"}" =>
"impl" <p:Angle<ParameterKind>> <mark:"!"?> <t:Id> <a:Angle<Parameter>> "for" <s:Ty> <w:WhereClauses> "{"
<assoc:AssocTyValue*> "}" =>
{
let mut args = vec![Parameter::Ty(s)];
args.extend(a);
Impl {
parameter_kinds: p,
trait_ref: TraitRef { trait_name: t, args: args },
trait_ref: PolarizedTraitRef::from_bool(mark.is_none(), TraitRef {
trait_name: t,
args: args,
}),
where_clauses: w,
assoc_ty_values: assoc,
}
Expand Down
16 changes: 13 additions & 3 deletions src/coherence/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,12 @@ impl Program {

// Create a vector of references to impl datums, sorted by trait ref
let impl_data = self.impl_data.iter().sorted_by(|&(_, lhs), &(_, rhs)| {
lhs.binders.value.trait_ref.trait_id.cmp(&rhs.binders.value.trait_ref.trait_id)
lhs.binders.value.trait_ref.trait_ref().trait_id.cmp(&rhs.binders.value.trait_ref.trait_ref().trait_id)
});

// Group impls by trait.
let impl_groupings = impl_data.into_iter().group_by(|&(_, impl_datum)| {
impl_datum.binders.value.trait_ref.trait_id
impl_datum.binders.value.trait_ref.trait_ref().trait_id
});


Expand All @@ -31,6 +31,11 @@ impl Program {
let impls: Vec<(&ItemId, &ImplDatum)> = impls.collect();

for ((&l_id, lhs), (&r_id, rhs)) in impls.into_iter().tuple_combinations() {
// Two negative impls never overlap.
if !lhs.binders.value.trait_ref.is_positive() && !rhs.binders.value.trait_ref.is_positive() {
continue;
}

// Check if the impls overlap, then if they do, check if one specializes
// the other. Note that specialization can only run one way - if both
// specialization checks return *either* true or false, that's an error.
Expand Down Expand Up @@ -133,6 +138,11 @@ impl Solver {
// }
// }
fn specializes(&mut self, less_special: &ImplDatum, more_special: &ImplDatum) -> bool {
// Negative impls cannot specialize.
if !less_special.binders.value.trait_ref.is_positive() || !more_special.binders.value.trait_ref.is_positive() {
return false;
}

let more_len = more_special.binders.len();

// Create parameter equality goals.
Expand Down Expand Up @@ -160,5 +170,5 @@ impl Solver {
}

fn params(impl_datum: &ImplDatum) -> &[Parameter] {
&impl_datum.binders.value.trait_ref.parameters
&impl_datum.binders.value.trait_ref.trait_ref().parameters
}
1 change: 1 addition & 0 deletions src/fold/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -195,6 +195,7 @@ macro_rules! enum_fold {
}
}

enum_fold!(PolarizedTraitRef[] { Positive(a), Negative(a) });
enum_fold!(ParameterKind[T,L] { Ty(a), Lifetime(a) } where T: Fold, L: Fold);
enum_fold!(DomainGoal[] { Implemented(a), Normalize(a), WellFormed(a) });
enum_fold!(WellFormed[] { Ty(a), TraitRef(a) });
Expand Down
76 changes: 69 additions & 7 deletions src/ir/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ use cast::Cast;
use chalk_parse::ast;
use lalrpop_intern::InternedString;
use solve::infer::{TyInferenceVariable, LifetimeInferenceVariable};
use std::collections::{HashMap, BTreeMap};
use std::collections::{HashSet, HashMap, BTreeMap};
use std::sync::Arc;

pub type Identifier = InternedString;
Expand All @@ -24,8 +24,11 @@ pub struct Program {
/// For each trait:
pub trait_data: HashMap<ItemId, TraitDatum>,

/// For each trait:
/// For each associated ty:
pub associated_ty_data: HashMap<ItemId, AssociatedTyDatum>,

/// For each default impl (automatically generated for auto traits):
pub default_impl_data: Vec<DefaultImplDatum>,
}

impl Program {
Expand Down Expand Up @@ -85,7 +88,8 @@ impl Environment {
where I: IntoIterator<Item = DomainGoal>
{
let mut env = self.clone();
env.clauses.extend(clauses);
let env_clauses: HashSet<_> = env.clauses.into_iter().chain(clauses).collect();
env.clauses = env_clauses.into_iter().collect();
Arc::new(env)
}

Expand Down Expand Up @@ -182,12 +186,23 @@ pub struct ImplDatum {

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct ImplDatumBound {
pub trait_ref: TraitRef,
pub trait_ref: PolarizedTraitRef,
pub where_clauses: Vec<DomainGoal>,
pub associated_ty_values: Vec<AssociatedTyValue>,
pub specialization_priority: usize,
}

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct DefaultImplDatum {
pub binders: Binders<DefaultImplDatumBound>,
}

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct DefaultImplDatumBound {
pub trait_ref: TraitRef,
pub accessible_tys: Vec<Ty>,
}

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct StructDatum {
pub binders: Binders<StructDatumBound>,
Expand All @@ -209,6 +224,7 @@ pub struct TraitDatum {
pub struct TraitDatumBound {
pub trait_ref: TraitRef,
pub where_clauses: Vec<DomainGoal>,
pub auto: bool,
}

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
Expand Down Expand Up @@ -343,6 +359,28 @@ pub struct TraitRef {
pub parameters: Vec<Parameter>,
}

#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
pub enum PolarizedTraitRef {
Positive(TraitRef),
Negative(TraitRef),
}

impl PolarizedTraitRef {
pub fn is_positive(&self) -> bool {
match *self {
PolarizedTraitRef::Positive(_) => true,
PolarizedTraitRef::Negative(_) => false,
}
}

pub fn trait_ref(&self) -> &TraitRef {
match *self {
PolarizedTraitRef::Positive(ref tr) |
PolarizedTraitRef::Negative(ref tr) => tr
}
}
}

/// A "domain goal" is a goal that is directly about Rust, rather than a pure
/// logical statement. As much as possible, the Chalk solver should avoid
/// decomposing this enum, and instead treat its values opaquely.
Expand Down Expand Up @@ -374,9 +412,8 @@ impl DomainGoal {
pub fn expanded(self, program: &Program) -> impl Iterator<Item = DomainGoal> {
let mut expanded = vec![];
match self {
DomainGoal::Implemented(ref trait_ref) => {
expanded.push(WellFormed::TraitRef(trait_ref.clone()).cast());
}
DomainGoal::Implemented(ref trait_ref) =>
expanded.push(WellFormed::TraitRef(trait_ref.clone()).cast()),
DomainGoal::Normalize(Normalize { ref projection, .. }) => {
let (associated_ty_data, trait_params, _) = program.split_projection(&projection);
let trait_ref = TraitRef {
Expand Down Expand Up @@ -500,6 +537,31 @@ pub enum FullyReducedGoal {
DomainGoal(Canonical<InEnvironment<DomainGoal>>),
}

impl FullyReducedGoal {
pub fn into_binders(self) -> Vec<ParameterKind<UniverseIndex>> {
match self {
FullyReducedGoal::EqGoal(Canonical { binders, .. }) |
FullyReducedGoal::DomainGoal(Canonical { binders, ..}) => binders,
}
}

/// A goal has coinductive semantics if it is of the form `T: AutoTrait`.
pub fn is_coinductive(&self, program: &ProgramEnvironment) -> bool {
if let FullyReducedGoal::DomainGoal(Canonical {
value: InEnvironment {
goal: DomainGoal::Implemented(ref tr),
..
},
..
}) = *self {
let trait_datum = &program.trait_data[&tr.trait_id];
return trait_datum.binders.value.auto;
}

false
}
}

impl<T> Canonical<T> {
pub fn map<OP, U>(self, op: OP) -> Canonical<U>
where OP: FnOnce(T) -> U
Expand Down
80 changes: 80 additions & 0 deletions src/lower/default.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
use ir::*;
use solve::infer::InferenceTable;
use cast::Cast;

impl Program {
pub(super) fn add_default_impls(&mut self) {
// For each auto trait `MyAutoTrait` and for each struct/type `MyStruct`
for auto_trait in self.trait_data.values().filter(|t| t.binders.value.auto) {
for struct_datum in self.struct_data.values() {

// `MyStruct: MyAutoTrait`
let trait_ref = TraitRef {
trait_id: auto_trait.binders.value.trait_ref.trait_id,
parameters: vec![
ParameterKind::Ty(Ty::Apply(struct_datum.binders.value.self_ty.clone()))
]
};

// If a positive or negative impl is already provided for a type family
// which includes `MyStruct`, we do not generate a default impl.
if self.impl_provided_for(trait_ref.clone(), struct_datum) {
continue;
}

self.default_impl_data.push(DefaultImplDatum {
binders: Binders {
binders: struct_datum.binders.binders.clone(),
value: DefaultImplDatumBound {
trait_ref,
accessible_tys: struct_datum.binders.value.fields.clone(),
}
}
});
}
}
}

fn impl_provided_for(&self, trait_ref: TraitRef, struct_datum: &StructDatum) -> bool {
let goal: DomainGoal = trait_ref.cast();

let env = Environment::new();
let mut infer = InferenceTable::new();

let goal = infer.instantiate_in(env.universe, struct_datum.binders.binders.clone(), &goal);

for impl_datum in self.impl_data.values() {
// We retrieve the trait ref given by the positive impl (even if the actual impl is negative)
let impl_goal: DomainGoal = impl_datum.binders.value.trait_ref.trait_ref().clone().cast();

let impl_goal = infer.instantiate_in(env.universe, impl_datum.binders.binders.clone(), &impl_goal);

// We check whether the impl `MyStruct: (!)MyAutoTrait` unifies with an existing impl.
// Examples:
//
// ```
// struct MyStruct;
// impl<T> Send for T where T: Foo { }
// ```
// `MyStruct: Send` unifies with `T: Send` so no default impl is generated for `MyStruct`.
//
// ```
// struct MyStruct;
// impl<T> Send for Vec<T> where T: Foo { }
// ```
// `Vec<i32>: Send` unifies with `Vec<T>: Send` so no default impl is generated for `Vec<i32>`.
// But a default impl is generated for `MyStruct`.
//
// ```
// struct MyStruct;
// impl<T> !Send for T where T: Foo { }
// ```
// `MyStruct: !Send` unifies with `T: !Send` so no default impl is generated for `MyStruct`.
if infer.unify(&Environment::new(), &goal, &impl_goal).is_ok() {
return true;
}
}

false
}
}
Loading

0 comments on commit 7eb0f08

Please sign in to comment.