Skip to content
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

Auto traits #54

Merged
merged 14 commits into from
Jul 17, 2017
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" "]";
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

if you wanted to make auto usable as an identifier, you could do this:

Id: Identifier = {
    <l:@L> <s:RawIdent> <r:@R> => Identifier {
        str: intern(s),
        span: Span::new(l, r),
    }
};

RawIdent: &'input str = {
    "auto",
    r"([A-Za-z]|_)([A-Za-z0-9]|_)*",
};

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah I see, but actually I think #[auto] is fine now :)


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