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

Finish implementing GATs #134

Merged
merged 11 commits into from
May 24, 2018
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