Skip to content

Commit

Permalink
Merge pull request #134 from tmandry/GAT-step3
Browse files Browse the repository at this point in the history
Finish implementing GATs
  • Loading branch information
nikomatsakis committed May 24, 2018
2 parents 7b21259 + 4061896 commit 38856d0
Show file tree
Hide file tree
Showing 11 changed files with 1,074 additions and 189 deletions.
2 changes: 1 addition & 1 deletion chalk-parse/src/ast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ pub struct TraitBound {
pub struct ProjectionEqBound {
pub trait_bound: TraitBound,
pub name: Identifier,
pub parameters: Vec<Parameter>,
pub args: Vec<Parameter>,
pub value: Ty,
}

Expand Down
2 changes: 1 addition & 1 deletion chalk-parse/src/parser.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,7 @@ ProjectionEqBound: ProjectionEqBound = {
args_no_self: a.unwrap_or(vec![]),
},
name,
parameters: a2,
args: a2,
value: ty,
}
};
Expand Down
13 changes: 13 additions & 0 deletions src/fold.rs
Original file line number Diff line number Diff line change
Expand Up @@ -431,6 +431,7 @@ enum_fold!(Constraint[] { LifetimeEq(a, b) });
enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g),
Leaf(wc), CannotProve(a) });
enum_fold!(ProgramClause[] { Implies(a), ForAll(a) });
enum_fold!(InlineBound[] { TraitBound(a), ProjectionEqBound(a) });

macro_rules! struct_fold {
($s:ident $([$($tt_args:tt)*])? { $($name:ident),* $(,)* } $($w:tt)*) => {
Expand Down Expand Up @@ -582,4 +583,16 @@ struct_fold!(ConstrainedSubst {
constraints,
});

struct_fold!(TraitBound {
trait_id,
args_no_self,
});

struct_fold!(ProjectionEqBound {
trait_bound,
associated_ty_id,
parameters,
value,
});

// struct_fold!(ApplicationTy { name, parameters }); -- intentionally omitted, folded through Ty
108 changes: 105 additions & 3 deletions src/ir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ use fold::shift::Shift;
use lalrpop_intern::InternedString;
use std::collections::{BTreeMap, BTreeSet};
use std::sync::Arc;
use std::iter;

#[macro_use]
mod macros;
Expand Down Expand Up @@ -259,6 +260,80 @@ pub struct TraitFlags {
pub deref: bool,
}

/// An inline bound, e.g. `: Foo<K>` in `impl<K, T: Foo<K>> SomeType<T>`.
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub enum InlineBound {
TraitBound(TraitBound),
ProjectionEqBound(ProjectionEqBound),
}

impl InlineBound {
/// Applies the `InlineBound` to `self_ty` and lowers to a [`DomainGoal`].
///
/// Because an `InlineBound` does not know anything about what it's binding,
/// you must provide that type as `self_ty`.
crate fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
match self {
InlineBound::TraitBound(b) => b.lower_with_self(self_ty),
InlineBound::ProjectionEqBound(b) => b.lower_with_self(self_ty),
}
}
}

/// Represents a trait bound on e.g. a type or type parameter.
/// Does not know anything about what it's binding.
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct TraitBound {
crate trait_id: ItemId,
crate args_no_self: Vec<Parameter>,
}

impl TraitBound {
crate fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
let trait_ref = self.as_trait_ref(self_ty);
vec![DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref))]
}

fn as_trait_ref(&self, self_ty: Ty) -> TraitRef {
let self_ty = ParameterKind::Ty(self_ty);
TraitRef {
trait_id: self.trait_id,
parameters: iter::once(self_ty).chain(self.args_no_self.iter().cloned()).collect(),
}
}
}

/// Represents a projection equality bound on e.g. a type or type parameter.
/// Does not know anything about what it's binding.
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct ProjectionEqBound {
crate trait_bound: TraitBound,
crate associated_ty_id: ItemId,
/// Does not include trait parameters.
crate parameters: Vec<Parameter>,
crate value: Ty,
}

impl ProjectionEqBound {
crate fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
let trait_ref = self.trait_bound.as_trait_ref(self_ty);

let mut parameters = self.parameters.clone();
parameters.extend(trait_ref.parameters.clone());

vec![
DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref)),
DomainGoal::Holds(WhereClauseAtom::ProjectionEq(ProjectionEq {
projection: ProjectionTy {
associated_ty_id: self.associated_ty_id,
parameters: parameters,
},
ty: self.value.clone(),
}))
]
}
}

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct AssociatedTyDatum {
/// The trait this associated type is defined in.
Expand All @@ -274,12 +349,37 @@ pub struct AssociatedTyDatum {
/// but possibly including more.
crate parameter_kinds: Vec<ParameterKind<Identifier>>,

// FIXME: inline bounds on the associated ty need to be implemented
/// Bounds on the associated type itself.
///
/// These must be proven by the implementer, for all possible parameters that
/// would result in a well-formed projection.
crate bounds: Vec<InlineBound>,

/// Where clauses that must hold for the projection be well-formed.
/// Where clauses that must hold for the projection to be well-formed.
crate where_clauses: Vec<QuantifiedDomainGoal>,
}

impl AssociatedTyDatum {
/// Returns the associated ty's bounds applied to the projection type, e.g.:
///
/// ```notrust
/// Implemented(<?0 as Foo>::Item<?1>: Sized)
/// ```
crate fn bounds_on_self(&self) -> Vec<DomainGoal> {
let parameters = self.parameter_kinds
.anonymize()
.iter()
.zip(0..)
.map(|p| p.to_parameter())
.collect();
let self_ty = Ty::Projection(ProjectionTy {
associated_ty_id: self.id,
parameters
});
self.bounds.iter().flat_map(|b| b.lower_with_self(self_ty.clone())).collect()
}
}

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct AssociatedTyValue {
crate associated_ty_id: ItemId,
Expand Down Expand Up @@ -612,7 +712,9 @@ impl DomainGoal {
/// Same as `into_well_formed_goal` but with the `FromEnv` predicate instead of `WellFormed`.
crate fn into_from_env_goal(self) -> DomainGoal {
match self {
DomainGoal::Holds(wca) => DomainGoal::FromEnv(wca),
DomainGoal::Holds(wca @ WhereClauseAtom::Implemented(..)) => {
DomainGoal::FromEnv(wca)
}
goal => goal,
}
}
Expand Down
147 changes: 127 additions & 20 deletions src/ir/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -191,6 +191,7 @@ impl LowerProgram for Program {
id: info.id,
name: defn.name.str,
parameter_kinds: parameter_kinds,
bounds: defn.bounds.lower(&env)?,
where_clauses: defn.where_clauses.lower(&env)?,
},
);
Expand Down Expand Up @@ -441,32 +442,37 @@ trait LowerWhereClause<T> {
/// type in Rust and well-formedness checks.
impl LowerWhereClause<ir::DomainGoal> for WhereClause {
fn lower(&self, env: &Env) -> Result<Vec<ir::DomainGoal>> {
let goal = match self {
let goals = match self {
WhereClause::Implemented { trait_ref } => {
ir::DomainGoal::Holds(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?))
vec![ir::DomainGoal::Holds(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?))]
}
WhereClause::ProjectionEq {
projection,
ty,
} => ir::DomainGoal::Holds(ir::WhereClauseAtom::ProjectionEq(ir::ProjectionEq {
projection: projection.lower(env)?,
ty: ty.lower(env)?,
})),
} => vec![
ir::DomainGoal::Holds(ir::WhereClauseAtom::ProjectionEq(ir::ProjectionEq {
projection: projection.lower(env)?,
ty: ty.lower(env)?,
})),
ir::DomainGoal::Holds(ir::WhereClauseAtom::Implemented(
projection.trait_ref.lower(env)?
)),
],
WhereClause::Normalize {
projection,
ty,
} => ir::DomainGoal::Normalize(ir::Normalize {
} => vec![ir::DomainGoal::Normalize(ir::Normalize {
projection: projection.lower(env)?,
ty: ty.lower(env)?,
}),
WhereClause::TyWellFormed { ty } => ir::DomainGoal::WellFormedTy(ty.lower(env)?),
WhereClause::TraitRefWellFormed { trait_ref } => {
})],
WhereClause::TyWellFormed { ty } => vec![ir::DomainGoal::WellFormedTy(ty.lower(env)?)],
WhereClause::TraitRefWellFormed { trait_ref } => vec![
ir::DomainGoal::WellFormed(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?))
}
WhereClause::TyFromEnv { ty } => ir::DomainGoal::FromEnvTy(ty.lower(env)?),
WhereClause::TraitRefFromEnv { trait_ref } => {
],
WhereClause::TyFromEnv { ty } => vec![ir::DomainGoal::FromEnvTy(ty.lower(env)?)],
WhereClause::TraitRefFromEnv { trait_ref } => vec![
ir::DomainGoal::FromEnv(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?))
}
],
WhereClause::UnifyTys { .. } | WhereClause::UnifyLifetimes { .. } => {
bail!("this form of where-clause not allowed here")
}
Expand All @@ -480,19 +486,19 @@ impl LowerWhereClause<ir::DomainGoal> for WhereClause {
bail!(ErrorKind::NotTrait(trait_name));
}

ir::DomainGoal::InScope(id)
vec![ir::DomainGoal::InScope(id)]
}
WhereClause::Derefs { source, target } => {
WhereClause::Derefs { source, target } => vec![
ir::DomainGoal::Derefs(ir::Derefs {
source: source.lower(env)?,
target: target.lower(env)?
})
}
WhereClause::TyIsLocal { ty } => {
],
WhereClause::TyIsLocal { ty } => vec![
ir::DomainGoal::IsLocalTy(ty.lower(env)?)
}
],
};
Ok(vec![goal])
Ok(goals)
}
}

Expand Down Expand Up @@ -638,6 +644,107 @@ impl LowerTraitRef for TraitRef {
}
}

trait LowerTraitBound {
fn lower_trait_bound(&self, env: &Env) -> Result<ir::TraitBound>;
}

impl LowerTraitBound for TraitBound {
fn lower_trait_bound(&self, env: &Env) -> Result<ir::TraitBound> {
let id = match env.lookup(self.trait_name)? {
NameLookup::Type(id) => id,
NameLookup::Parameter(_) => bail!(ErrorKind::NotTrait(self.trait_name)),
};

let k = env.type_kind(id);
if k.sort != ir::TypeSort::Trait {
bail!(ErrorKind::NotTrait(self.trait_name));
}

let parameters = self.args_no_self
.iter()
.map(|a| Ok(a.lower(env)?))
.collect::<Result<Vec<_>>>()?;

if parameters.len() != k.binders.len() {
bail!(
"wrong number of parameters, expected `{:?}`, got `{:?}`",
k.binders.len(),
parameters.len()
)
}

for (binder, param) in k.binders.binders.iter().zip(parameters.iter()) {
check_type_kinds("incorrect kind for trait parameter", binder, param)?;
}

Ok(ir::TraitBound {
trait_id: id,
args_no_self: parameters,
})
}
}

trait LowerInlineBound {
fn lower(&self, env: &Env) -> Result<ir::InlineBound>;
}

impl LowerInlineBound for TraitBound {
fn lower(&self, env: &Env) -> Result<ir::InlineBound> {
Ok(ir::InlineBound::TraitBound(self.lower_trait_bound(&env)?))
}
}

impl LowerInlineBound for ProjectionEqBound {
fn lower(&self, env: &Env) -> Result<ir::InlineBound> {
let trait_bound = self.trait_bound.lower_trait_bound(env)?;
let info = match env.associated_ty_infos.get(&(trait_bound.trait_id, self.name.str)) {
Some(info) => info,
None => bail!("no associated type `{}` defined in trait", self.name.str),
};
let args: Vec<_> = try!(self.args.iter().map(|a| a.lower(env)).collect());

if args.len() != info.addl_parameter_kinds.len() {
bail!(
"wrong number of parameters for associated type (expected {}, got {})",
info.addl_parameter_kinds.len(),
args.len()
)
}

for (param, arg) in info.addl_parameter_kinds.iter().zip(args.iter()) {
check_type_kinds("incorrect kind for associated type parameter", param, arg)?;
}

Ok(ir::InlineBound::ProjectionEqBound(ir::ProjectionEqBound {
trait_bound,
associated_ty_id: info.id,
parameters: args,
value: self.value.lower(env)?,
}))
}
}

impl LowerInlineBound for InlineBound {
fn lower(&self, env: &Env) -> Result<ir::InlineBound> {
match self {
InlineBound::TraitBound(b) => b.lower(&env),
InlineBound::ProjectionEqBound(b) => b.lower(&env),
}
}
}

trait LowerInlineBounds {
fn lower(&self, env: &Env) -> Result<Vec<ir::InlineBound>>;
}

impl LowerInlineBounds for Vec<InlineBound> {
fn lower(&self, env: &Env) -> Result<Vec<ir::InlineBound>> {
self.iter()
.map(|b| b.lower(env))
.collect()
}
}

trait LowerPolarizedTraitRef {
fn lower(&self, env: &Env) -> Result<ir::PolarizedTraitRef>;
}
Expand Down
Loading

0 comments on commit 38856d0

Please sign in to comment.