From f7c4c26d644bb6bc6aed09dfde51ba4a8d1f42ca Mon Sep 17 00:00:00 2001 From: scalexm Date: Sun, 27 May 2018 13:42:41 +0200 Subject: [PATCH 1/2] Replace `WhereClauseAtom` with `WhereClause` --- chalk-parse/src/ast.rs | 20 ++-- chalk-parse/src/parser.lalrpop | 79 +++++++------- src/cast.rs | 64 +++++++----- src/fold.rs | 6 +- src/ir.rs | 122 ++++++++++++---------- src/ir/debug.rs | 24 ++--- src/ir/lowering.rs | 174 ++++++++++++++++--------------- src/rules.rs | 185 +++++++++++++++++---------------- src/rules/wf.rs | 58 +++-------- src/zip.rs | 6 +- 10 files changed, 378 insertions(+), 360 deletions(-) diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index fef01ed186c..bd597bfae4f 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -208,19 +208,27 @@ pub struct Identifier { pub enum WhereClause { Implemented { trait_ref: TraitRef }, - Normalize { projection: ProjectionTy, ty: Ty }, ProjectionEq { projection: ProjectionTy, ty: Ty }, - TyWellFormed { ty: Ty }, +} + +pub enum DomainGoal { + Holds { where_clause: WhereClause }, + Normalize { projection: ProjectionTy, ty: Ty }, TraitRefWellFormed { trait_ref: TraitRef }, + TyWellFormed { ty: Ty }, TyFromEnv { ty: Ty }, TraitRefFromEnv { trait_ref: TraitRef }, - UnifyTys { a: Ty, b: Ty }, - UnifyLifetimes { a: Lifetime, b: Lifetime }, TraitInScope { trait_name: Identifier }, Derefs { source: Ty, target: Ty }, IsLocal { ty: Ty }, } +pub enum LeafGoal { + DomainGoal { goal: DomainGoal }, + UnifyTys { a: Ty, b: Ty }, + UnifyLifetimes { a: Lifetime, b: Lifetime }, +} + pub struct QuantifiedWhereClause { pub parameter_kinds: Vec, pub where_clause: WhereClause, @@ -235,7 +243,7 @@ pub struct Field { /// logic; it has no equivalent in Rust, but it's useful for testing. pub struct Clause { pub parameter_kinds: Vec, - pub consequence: WhereClause, + pub consequence: DomainGoal, pub conditions: Vec>, } @@ -247,5 +255,5 @@ pub enum Goal { Not(Box), // Additional kinds of goals: - Leaf(WhereClause), + Leaf(LeafGoal), } diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index 899c8310409..3516afbc7e6 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -29,9 +29,9 @@ pub Goal: Box = { Goal1: Box = { "forall" "<" > ">" "{" "}" => Box::new(Goal::ForAll(p, g)), "exists" "<" > ">" "{" "}" => Box::new(Goal::Exists(p, g)), - "if" "(" > ")" "{" "}" => Box::new(Goal::Implies(w, g)), + "if" "(" > ")" "{" "}" => Box::new(Goal::Implies(h, g)), "not" "{" "}" => Box::new(Goal::Not(g)), - => Box::new(Goal::Leaf(w)), + => Box::new(Goal::Leaf(leaf)), "(" ")", }; @@ -199,29 +199,29 @@ Field: Field = { }; Clause: Clause = { - "forall" > "{" "if" > "}" => Clause { + "forall" > "{" "if" > "}" => Clause { parameter_kinds: pk, - consequence: wc, + consequence: dg, conditions: g, }, - "forall" > "{" "}" => Clause { + "forall" > "{" "}" => Clause { parameter_kinds: pk, - consequence: wc, + consequence: dg, conditions: vec![], }, }; InlineClause1: Clause = { - => Clause { + => Clause { parameter_kinds: vec![], - consequence: wc, + consequence: dg, conditions: vec![], }, - ":" "-" > => Clause { + ":" "-" > => Clause { parameter_kinds: vec![], - consequence: wc, + consequence: dg, conditions: g, }, }; @@ -236,29 +236,9 @@ InlineClause: Clause = { } }; -QuantifiedWhereClauses: Vec = { - "where" >, - () => vec![], -}; - WhereClause: WhereClause = { > => WhereClause::Implemented { trait_ref: t }, - "WellFormed" "(" ")" => WhereClause::TyWellFormed { ty: t }, - - "WellFormed" "(" > ")" => WhereClause::TraitRefWellFormed { trait_ref: t }, - - "FromEnv" "(" ")" => WhereClause::TyFromEnv { ty: t }, - - "FromEnv" "(" > ")" => WhereClause::TraitRefFromEnv { trait_ref: t }, - - "=" => WhereClause::UnifyTys { a, b }, - - "=" => WhereClause::UnifyLifetimes { a, b }, - - // `::U -> Bar` -- a normalization - "Normalize" "(" "->" ")" => WhereClause::Normalize { projection: s, ty: t }, - // `T: Foo` -- projection equality ":" "<" > ",")?> > "=" ">" => @@ -269,11 +249,6 @@ WhereClause: WhereClause = { let projection = ProjectionTy { trait_ref, name, args: a2 }; WhereClause::ProjectionEq { projection, ty } }, - - "InScope" "(" ")" => WhereClause::TraitInScope { trait_name: t }, - "Derefs" "(" "," ")" => WhereClause::Derefs { source, target }, - - "IsLocal" "(" ")" => WhereClause::IsLocal { ty }, }; QuantifiedWhereClause: QuantifiedWhereClause = { @@ -288,6 +263,40 @@ QuantifiedWhereClause: QuantifiedWhereClause = { }, }; +QuantifiedWhereClauses: Vec = { + "where" >, + () => vec![], +}; + +DomainGoal: DomainGoal = { + => DomainGoal::Holds { where_clause: wc }, + + "WellFormed" "(" ")" => DomainGoal::TyWellFormed { ty: t }, + + "WellFormed" "(" > ")" => DomainGoal::TraitRefWellFormed { trait_ref: t }, + + "FromEnv" "(" ")" => DomainGoal::TyFromEnv { ty: t }, + + "FromEnv" "(" > ")" => DomainGoal::TraitRefFromEnv { trait_ref: t }, + + // `::U -> Bar` -- a normalization + "Normalize" "(" "->" ")" => DomainGoal::Normalize { projection: s, ty: t }, + + "InScope" "(" ")" => DomainGoal::TraitInScope { trait_name: t }, + + "Derefs" "(" "," ")" => DomainGoal::Derefs { source, target }, + + "IsLocal" "(" ")" => DomainGoal::IsLocal { ty }, +}; + +LeafGoal: LeafGoal = { + => LeafGoal::DomainGoal { goal: dg }, + + "=" => LeafGoal::UnifyTys { a, b }, + + "=" => LeafGoal::UnifyLifetimes { a, b }, +}; + TraitRef: TraitRef = { S > => { let mut args = vec![Parameter::Ty(s)]; diff --git a/src/cast.rs b/src/cast.rs index 6ef3aead167..4cb149ad13a 100644 --- a/src/cast.rs +++ b/src/cast.rs @@ -50,21 +50,21 @@ macro_rules! reflexive_impl { reflexive_impl!(TraitRef); reflexive_impl!(LeafGoal); reflexive_impl!(DomainGoal); -reflexive_impl!(WhereClauseAtom); +reflexive_impl!(WhereClause); -impl Cast for TraitRef { - fn cast(self) -> WhereClauseAtom { - WhereClauseAtom::Implemented(self) +impl Cast for TraitRef { + fn cast(self) -> WhereClause { + WhereClause::Implemented(self) } } -impl Cast for ProjectionEq { - fn cast(self) -> WhereClauseAtom { - WhereClauseAtom::ProjectionEq(self) +impl Cast for ProjectionEq { + fn cast(self) -> WhereClause { + WhereClause::ProjectionEq(self) } } -impl Cast for T where T: Cast { +impl Cast for T where T: Cast { fn cast(self) -> DomainGoal { DomainGoal::Holds(self.cast()) } @@ -94,13 +94,25 @@ impl Cast for UnselectedNormalize { } } +impl Cast for WellFormed { + fn cast(self) -> DomainGoal { + DomainGoal::WellFormed(self) + } +} + +impl Cast for FromEnv { + fn cast(self) -> DomainGoal { + DomainGoal::FromEnv(self) + } +} + impl Cast for EqGoal { fn cast(self) -> LeafGoal { LeafGoal::EqGoal(self) } } -impl Cast for QuantifiedDomainGoal { +impl> Cast for Binders { fn cast(self) -> Goal { if self.binders.is_empty() { self.value.cast() @@ -113,21 +125,6 @@ impl Cast for QuantifiedDomainGoal { } } -impl Cast for QuantifiedDomainGoal { - fn cast(self) -> ProgramClause { - if self.binders.is_empty() { - self.value.cast() - } else { - ProgramClause::ForAll( - self.map(|bound| ProgramClauseImplication { - consequence: bound, - conditions: vec![], - }) - ) - } - } -} - impl Cast for ApplicationTy { fn cast(self) -> Ty { Ty::Apply(self) @@ -152,15 +149,30 @@ impl Cast for Lifetime { } } -impl Cast for DomainGoal { +impl Cast for T where T: Cast { fn cast(self) -> ProgramClause { ProgramClause::Implies(ProgramClauseImplication { - consequence: self, + consequence: self.cast(), conditions: vec![], }) } } +impl> Cast for Binders { + fn cast(self) -> ProgramClause { + if self.binders.is_empty() { + Cast::::cast(self.value) + } else { + ProgramClause::ForAll( + self.map(|bound| ProgramClauseImplication { + consequence: bound.cast(), + conditions: vec![], + }) + ) + } + } +} + impl Cast for ProgramClauseImplication { fn cast(self) -> ProgramClause { ProgramClause::Implies(self) diff --git a/src/fold.rs b/src/fold.rs index 0b1d7b74627..9ae1c5f5e58 100644 --- a/src/fold.rs +++ b/src/fold.rs @@ -423,9 +423,11 @@ 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!(WhereClauseAtom[] { Implemented(a), ProjectionEq(a) }); +enum_fold!(WhereClause[] { Implemented(a), ProjectionEq(a) }); +enum_fold!(WellFormed[] { Trait(a), Ty(a) }); +enum_fold!(FromEnv[] { Trait(a), Ty(a) }); enum_fold!(DomainGoal[] { Holds(a), WellFormed(a), FromEnv(a), Normalize(a), UnselectedNormalize(a), - WellFormedTy(a), FromEnvTy(a), InScope(a), Derefs(a), IsLocal(a), LocalImplAllowed(a) }); + InScope(a), Derefs(a), IsLocal(a), LocalImplAllowed(a) }); enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) }); enum_fold!(Constraint[] { LifetimeEq(a, b) }); enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g), diff --git a/src/ir.rs b/src/ir.rs index 05b1832e302..d334dde566b 100644 --- a/src/ir.rs +++ b/src/ir.rs @@ -6,6 +6,7 @@ use lalrpop_intern::InternedString; use std::collections::{BTreeMap, BTreeSet}; use std::sync::Arc; use std::iter; +use cast::Cast; #[macro_use] mod macros; @@ -205,7 +206,7 @@ pub struct ImplDatum { #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct ImplDatumBound { crate trait_ref: PolarizedTraitRef, - crate where_clauses: Vec, + crate where_clauses: Vec, crate associated_ty_values: Vec, crate specialization_priority: usize, } @@ -230,7 +231,7 @@ pub struct StructDatum { pub struct StructDatumBound { crate self_ty: ApplicationTy, crate fields: Vec, - crate where_clauses: Vec, + crate where_clauses: Vec, crate flags: StructFlags, } @@ -248,7 +249,7 @@ pub struct TraitDatum { #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct TraitDatumBound { crate trait_ref: TraitRef, - crate where_clauses: Vec, + crate where_clauses: Vec, crate flags: TraitFlags, } @@ -272,10 +273,10 @@ impl InlineBound { /// /// 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 { + crate fn into_where_clauses(&self, self_ty: Ty) -> Vec { match self { - InlineBound::TraitBound(b) => b.lower_with_self(self_ty), - InlineBound::ProjectionEqBound(b) => b.lower_with_self(self_ty), + InlineBound::TraitBound(b) => b.into_where_clauses(self_ty), + InlineBound::ProjectionEqBound(b) => b.into_where_clauses(self_ty), } } } @@ -289,9 +290,9 @@ pub struct TraitBound { } impl TraitBound { - crate fn lower_with_self(&self, self_ty: Ty) -> Vec { + crate fn into_where_clauses(&self, self_ty: Ty) -> Vec { let trait_ref = self.as_trait_ref(self_ty); - vec![DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref))] + vec![WhereClause::Implemented(trait_ref)] } fn as_trait_ref(&self, self_ty: Ty) -> TraitRef { @@ -315,21 +316,21 @@ pub struct ProjectionEqBound { } impl ProjectionEqBound { - crate fn lower_with_self(&self, self_ty: Ty) -> Vec { + crate fn into_where_clauses(&self, self_ty: Ty) -> Vec { 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 { + WhereClause::Implemented(trait_ref), + WhereClause::ProjectionEq(ProjectionEq { projection: ProjectionTy { associated_ty_id: self.associated_ty_id, parameters: parameters, }, ty: self.value.clone(), - })) + }), ] } } @@ -356,7 +357,7 @@ pub struct AssociatedTyDatum { crate bounds: Vec, /// Where clauses that must hold for the projection to be well-formed. - crate where_clauses: Vec, + crate where_clauses: Vec, } impl AssociatedTyDatum { @@ -365,7 +366,7 @@ impl AssociatedTyDatum { /// ```notrust /// Implemented(::Item: Sized) /// ``` - crate fn bounds_on_self(&self) -> Vec { + crate fn bounds_on_self(&self) -> Vec { let parameters = self.parameter_kinds .anonymize() .iter() @@ -376,7 +377,7 @@ impl AssociatedTyDatum { associated_ty_id: self.id, parameters }); - self.bounds.iter().flat_map(|b| b.lower_with_self(self_ty.clone())).collect() + self.bounds.iter().flat_map(|b| b.into_where_clauses(self_ty.clone())).collect() } } @@ -605,9 +606,9 @@ impl PolarizedTraitRef { } } -/// "Basic" where clauses which have a WF/FromEnv version of themselves. +/// Where clauses that can be written by a Rust programmer. #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] -pub enum WhereClauseAtom { +pub enum WhereClause { Implemented(TraitRef), ProjectionEq(ProjectionEq), } @@ -618,13 +619,8 @@ pub struct Derefs { pub target: Ty, } -/// 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. -#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] -pub enum DomainGoal { - Holds(WhereClauseAtom), - +#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)] +pub enum WellFormed { /// A predicate which is true is some trait ref is well-formed. /// For example, given the following trait definitions: /// @@ -635,8 +631,23 @@ pub enum DomainGoal { /// /// then we have the following rule: /// `WellFormed(?Self: Copy) :- ?Self: Copy, WellFormed(?Self: Clone)`. - WellFormed(WhereClauseAtom), + Trait(TraitRef), + + /// A predicate which is true is some type is well-formed. + /// For example, given the following type definition: + /// + /// ```notrust + /// struct Set where K: Hash { + /// ... + /// } + /// ``` + /// + /// then we have the following rule: `WellFormedTy(Set) :- Implemented(K: Hash)`. + Ty(Ty), +} +#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)] +pub enum FromEnv { /// A predicate which enables deriving everything which should be true if we *know* that /// some trait ref is well-formed. For example given the above trait definitions, we can use /// `FromEnv(T: Copy)` to derive that `T: Clone`, like in: @@ -648,23 +659,7 @@ pub enum DomainGoal { /// } /// } /// ``` - FromEnv(WhereClauseAtom), - - - Normalize(Normalize), - UnselectedNormalize(UnselectedNormalize), - - /// A predicate which is true is some type is well-formed. - /// For example, given the following type definition: - /// - /// ```notrust - /// struct Set where K: Hash { - /// ... - /// } - /// ``` - /// - /// then we have the following rule: `WellFormedTy(Set) :- Implemented(K: Hash)`. - WellFormedTy(Ty), + Trait(TraitRef), /// A predicate which enables deriving everything which should be true if we *know* that /// some type is well-formed. For example given the above type definition, we can use @@ -677,7 +672,21 @@ pub enum DomainGoal { /// } /// } /// ``` - FromEnvTy(Ty), + Ty(Ty), +} + +/// 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. +#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] +pub enum DomainGoal { + Holds(WhereClause), + WellFormed(WellFormed), + FromEnv(FromEnv), + + + Normalize(Normalize), + UnselectedNormalize(UnselectedNormalize), InScope(ItemId), @@ -703,26 +712,33 @@ pub enum DomainGoal { LocalImplAllowed(TraitRef), } -pub type QuantifiedDomainGoal = Binders; +pub type QuantifiedWhereClause = Binders; -impl DomainGoal { +impl WhereClause { /// Turn a where clause into the WF version of it i.e.: /// * `Implemented(T: Trait)` maps to `WellFormed(T: Trait)` /// * `ProjectionEq(::Item = Foo)` maps to `WellFormed(::Item = Foo)` /// * any other clause maps to itself crate fn into_well_formed_goal(self) -> DomainGoal { match self { - DomainGoal::Holds(wca) => DomainGoal::WellFormed(wca), - goal => goal, + WhereClause::Implemented(trait_ref) => WellFormed::Trait(trait_ref).cast(), + wc => wc.cast(), } } /// 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 @ WhereClauseAtom::Implemented(..)) => { - DomainGoal::FromEnv(wca) - } + WhereClause::Implemented(trait_ref) => FromEnv::Trait(trait_ref).cast(), + wc => wc.cast(), + } + } +} + +impl DomainGoal { + crate fn into_from_env_goal(self) -> DomainGoal { + match self { + DomainGoal::Holds(wc) => wc.into_from_env_goal(), goal => goal, } } @@ -1055,14 +1071,14 @@ impl Goal { match self { Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::Holds(wca))) => { match wca { - WhereClauseAtom::Implemented(tr) => { + WhereClause::Implemented(tr) => { let trait_datum = &program.trait_data[&tr.trait_id]; trait_datum.binders.value.flags.auto } - WhereClauseAtom::ProjectionEq(..) => false, + WhereClause::ProjectionEq(..) => false, } } - Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::WellFormed(..))) => { + Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..)))) => { true } Goal::Quantified(QuantifierKind::ForAll, goal) => goal.value.is_coinductive(program), diff --git a/src/ir/debug.rs b/src/ir/debug.rs index 4e07925eb59..70210007de7 100644 --- a/src/ir/debug.rs +++ b/src/ir/debug.rs @@ -169,17 +169,17 @@ impl Debug for UnselectedNormalize { } } -impl Debug for WhereClauseAtom { +impl Debug for WhereClause { fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> { match self { - WhereClauseAtom::Implemented(tr) => write!( + WhereClause::Implemented(tr) => write!( fmt, "Implemented({:?}: {:?}{:?})", tr.parameters[0], tr.trait_id, Angle(&tr.parameters[1..]) ), - WhereClauseAtom::ProjectionEq(p) => write!(fmt, "{:?}", p), + WhereClause::ProjectionEq(p) => write!(fmt, "{:?}", p), } } } @@ -187,23 +187,11 @@ impl Debug for WhereClauseAtom { impl Debug for DomainGoal { fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> { match self { - DomainGoal::Holds(wca) => write!(fmt, "{:?}", wca), - DomainGoal::WellFormed(WhereClauseAtom::Implemented(tr)) => { - write!(fmt, "WellFormed({:?})", tr) - } - DomainGoal::WellFormed(WhereClauseAtom::ProjectionEq(p)) => { - write!(fmt, "WellFormed({:?})", p) - } - DomainGoal::FromEnv(WhereClauseAtom::Implemented(tr)) => { - write!(fmt, "FromEnv({:?})", tr) - } - DomainGoal::FromEnv(WhereClauseAtom::ProjectionEq(p)) => { - write!(fmt, "FromEnv({:?})", p) - } + DomainGoal::Holds(n) => write!(fmt, "{:?}", n), + DomainGoal::WellFormed(n) => write!(fmt, "{:?}", n), + DomainGoal::FromEnv(n) => write!(fmt, "{:?}", n), DomainGoal::Normalize(n) => write!(fmt, "{:?}", n), DomainGoal::UnselectedNormalize(n) => write!(fmt, "{:?}", n), - DomainGoal::WellFormedTy(t) => write!(fmt, "WellFormed({:?})", t), - DomainGoal::FromEnvTy(t) => write!(fmt, "FromEnv({:?})", t), DomainGoal::InScope(n) => write!(fmt, "InScope({:?})", n), DomainGoal::Derefs(n) => write!(fmt, "Derefs({:?})", n), DomainGoal::IsLocal(n) => write!(fmt, "IsLocal({:?})", n), diff --git a/src/ir/lowering.rs b/src/ir/lowering.rs index ef56e0f158c..43c972592a1 100644 --- a/src/ir/lowering.rs +++ b/src/ir/lowering.rs @@ -361,7 +361,7 @@ impl LowerParameterKind for ParameterKind { trait LowerWhereClauses { fn where_clauses(&self) -> &[QuantifiedWhereClause]; - fn lower_where_clauses(&self, env: &Env) -> Result> { + fn lower_where_clauses(&self, env: &Env) -> Result> { self.where_clauses().lower(env) } } @@ -416,16 +416,16 @@ trait LowerWhereClauseVec { fn lower(&self, env: &Env) -> Result>; } -impl LowerWhereClauseVec for [WhereClause] { - fn lower(&self, env: &Env) -> Result> { - self.iter().flat_map(|wc| wc.lower(env).apply_result()).collect() +impl LowerWhereClauseVec for [WhereClause] { + fn lower(&self, env: &Env) -> Result> { + self.iter().flat_map(|wc| LowerWhereClause::lower(wc, env).apply_result()).collect() } } -impl LowerWhereClauseVec for [QuantifiedWhereClause] { - fn lower(&self, env: &Env) -> Result> { +impl LowerWhereClauseVec for [QuantifiedWhereClause] { + fn lower(&self, env: &Env) -> Result> { self.iter() - .flat_map(|wc| match wc.lower(env) { + .flat_map(|wc| match LowerWhereClause::lower(wc, env) { Ok(v) => v.into_iter().map(Ok).collect(), Err(e) => vec![Err(e)], }) @@ -437,64 +437,95 @@ trait LowerWhereClause { fn lower(&self, env: &Env) -> Result>; } -/// Lowers a where-clause in the context of a clause (i.e. in "negative" -/// position); this is limited to the kinds of where-clauses users can actually -/// type in Rust and well-formedness checks. -impl LowerWhereClause for WhereClause { - fn lower(&self, env: &Env) -> Result> { - let goals = match self { +impl LowerWhereClause for WhereClause { + fn lower(&self, env: &Env) -> Result> { + let where_clauses = match self { WhereClause::Implemented { trait_ref } => { - vec![ir::DomainGoal::Holds(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?))] + vec![ir::WhereClause::Implemented(trait_ref.lower(env)?)] } WhereClause::ProjectionEq { projection, ty, } => vec![ - ir::DomainGoal::Holds(ir::WhereClauseAtom::ProjectionEq(ir::ProjectionEq { + ir::WhereClause::ProjectionEq(ir::ProjectionEq { projection: projection.lower(env)?, ty: ty.lower(env)?, - })), - ir::DomainGoal::Holds(ir::WhereClauseAtom::Implemented( + }), + ir::WhereClause::Implemented( projection.trait_ref.lower(env)? - )), + ), ], - WhereClause::Normalize { + }; + Ok(where_clauses) + } +} + +impl LowerWhereClause for QuantifiedWhereClause { + fn lower(&self, env: &Env) -> Result> { + let parameter_kinds = self.parameter_kinds.iter().map(|pk| pk.lower()); + let binders = env.in_binders(parameter_kinds, |env| { + Ok(LowerWhereClause::lower(&self.where_clause, env)?) + })?; + Ok(binders.into_iter().collect()) + } +} + +trait LowerDomainGoal { + fn lower(&self, env: &Env) -> Result>; +} + +/// Lowers a where-clause in the context of a clause (i.e. in "negative" +/// position); this is limited to the kinds of where-clauses users can actually +/// type in Rust and well-formedness checks. +/// +/// Lowers a where-clause in the context of a goal (i.e. in "positive" +/// position); this is richer in terms of the legal sorts of where-clauses that +/// can appear, because it includes all the sorts of things that the compiler +/// must verify. +impl LowerDomainGoal for DomainGoal { + fn lower(&self, env: &Env) -> Result> { + let goals = match self { + DomainGoal::Holds { where_clause } => { + where_clause.lower(env)?.into_iter().casted().collect() + }, + DomainGoal::Normalize { projection, ty, } => vec![ir::DomainGoal::Normalize(ir::Normalize { projection: projection.lower(env)?, ty: ty.lower(env)?, })], - 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 } => 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") - } - &WhereClause::TraitInScope { trait_name } => { - let id = match env.lookup(trait_name)? { + DomainGoal::TyWellFormed { ty } => vec![ir::DomainGoal::WellFormed( + ir::WellFormed::Ty(ty.lower(env)?) + )], + DomainGoal::TraitRefWellFormed { trait_ref } => vec![ir::DomainGoal::WellFormed( + ir::WellFormed::Trait(trait_ref.lower(env)?) + )], + DomainGoal::TyFromEnv { ty } => vec![ir::DomainGoal::FromEnv( + ir::FromEnv::Ty(ty.lower(env)?) + )], + DomainGoal::TraitRefFromEnv { trait_ref } => vec![ir::DomainGoal::FromEnv( + ir::FromEnv::Trait(trait_ref.lower(env)?) + )], + DomainGoal::TraitInScope { trait_name } => { + let id = match env.lookup(*trait_name)? { NameLookup::Type(id) => id, - NameLookup::Parameter(_) => bail!(ErrorKind::NotTrait(trait_name)), + NameLookup::Parameter(_) => bail!(ErrorKind::NotTrait(*trait_name)), }; if env.type_kind(id).sort != ir::TypeSort::Trait { - bail!(ErrorKind::NotTrait(trait_name)); + bail!(ErrorKind::NotTrait(*trait_name)); } vec![ir::DomainGoal::InScope(id)] } - WhereClause::Derefs { source, target } => vec![ - ir::DomainGoal::Derefs(ir::Derefs { + DomainGoal::Derefs { source, target } => vec![ir::DomainGoal::Derefs( + ir::Derefs { source: source.lower(env)?, target: target.lower(env)? - }) - ], - WhereClause::IsLocal { ty } => vec![ + } + )], + DomainGoal::IsLocal { ty } => vec![ ir::DomainGoal::IsLocal(ty.lower(env)?) ], }; @@ -502,56 +533,29 @@ impl LowerWhereClause for WhereClause { } } -impl LowerWhereClause for QuantifiedWhereClause { - fn lower(&self, env: &Env) -> Result> { - let parameter_kinds = self.parameter_kinds.iter().map(|pk| pk.lower()); - let binders = env.in_binders(parameter_kinds, |env| { - Ok(self.where_clause.lower(env)?) - })?; - Ok(binders.into_iter().collect()) - } +trait LowerLeafGoal { + fn lower(&self, env: &Env) -> Result>; } -/// Lowers a where-clause in the context of a goal (i.e. in "positive" -/// position); this is richer in terms of the legal sorts of where-clauses that -/// can appear, because it includes all the sorts of things that the compiler -/// must verify. -impl LowerWhereClause for WhereClause { +impl LowerLeafGoal for LeafGoal { fn lower(&self, env: &Env) -> Result> { - Ok(match *self { - WhereClause::Implemented { .. } - | WhereClause::ProjectionEq { .. } - | WhereClause::Normalize { .. } - | WhereClause::TyWellFormed { .. } - | WhereClause::TraitRefWellFormed { .. } - | WhereClause::TyFromEnv { .. } - | WhereClause::TraitRefFromEnv { .. } - | WhereClause::Derefs { .. } - | WhereClause::IsLocal { .. } => { - let goals: Vec = self.lower(env)?; - goals.into_iter().casted().collect() + let goals = match self { + LeafGoal::DomainGoal { goal } => { + goal.lower(env)? + .into_iter() + .map(|goal| ir::LeafGoal::DomainGoal(goal)) + .collect() } - WhereClause::UnifyTys { ref a, ref b } => vec![ir::EqGoal { + LeafGoal::UnifyTys { a, b } => vec![ir::EqGoal { a: ir::ParameterKind::Ty(a.lower(env)?), b: ir::ParameterKind::Ty(b.lower(env)?), }.cast()], - WhereClause::UnifyLifetimes { ref a, ref b } => vec![ir::EqGoal { + LeafGoal::UnifyLifetimes { ref a, ref b } => vec![ir::EqGoal { a: ir::ParameterKind::Lifetime(a.lower(env)?), b: ir::ParameterKind::Lifetime(b.lower(env)?), }.cast()], - WhereClause::TraitInScope { trait_name } => { - let id = match env.lookup(trait_name)? { - NameLookup::Type(id) => id, - NameLookup::Parameter(_) => bail!(ErrorKind::NotTrait(trait_name)), - }; - - if env.type_kind(id).sort != ir::TypeSort::Trait { - bail!(ErrorKind::NotTrait(trait_name)); - } - - vec![ir::DomainGoal::InScope(id).cast()] - } - }) + }; + Ok(goals) } } @@ -1098,15 +1102,15 @@ impl<'k> LowerGoal> for Goal { Goal::Exists(ids, g) => { g.lower_quantified(env, ir::QuantifierKind::Exists, ids) } - Goal::Implies(wc, g) => { + Goal::Implies(hyp, g) => { // We "elaborate" implied bounds by lowering goals like `T: Trait` and // `T: Trait` to `FromEnv(T: Trait)` and `FromEnv(T: Trait)` // in the assumptions of an `if` goal, e.g. `if (T: Trait) { ... }` lowers to // `if (FromEnv(T: Trait)) { ... /* this part is untouched */ ... }`. let where_clauses: Result> = - wc.into_iter() - .flat_map(|wc| wc.lower_clause(env).apply_result()) - .map(|result| result.map(|wc| wc.into_from_env_clause())) + hyp.into_iter() + .flat_map(|h| h.lower_clause(env).apply_result()) + .map(|result| result.map(|h| h.into_from_env_clause())) .collect(); Ok(Box::new(ir::Goal::Implies(where_clauses?, g.lower(env)?))) } @@ -1114,9 +1118,9 @@ impl<'k> LowerGoal> for Goal { Ok(Box::new(ir::Goal::And(g1.lower(env)?, g2.lower(env)?))) } Goal::Not(g) => Ok(Box::new(ir::Goal::Not(g.lower(env)?))), - Goal::Leaf(wc) => { + Goal::Leaf(leaf) => { // A where clause can lower to multiple leaf goals; wrap these in Goal::And. - let leaves = wc.lower(env)?.into_iter().map(ir::Goal::Leaf); + let leaves = leaf.lower(env)?.into_iter().map(ir::Goal::Leaf); let goal = leaves.fold1(|goal, leaf| ir::Goal::And(Box::new(goal), Box::new(leaf))) .expect("at least one goal"); Ok(Box::new(goal)) diff --git a/src/rules.rs b/src/rules.rs index 01c80b212af..c79d10e0f33 100644 --- a/src/rules.rs +++ b/src/rules.rs @@ -1,14 +1,14 @@ use cast::{Cast, Caster}; use fold::shift::Shift; use fold::Subst; -use ir::{self, ToParameter}; +use ir::*; use std::iter; mod default; mod wf; -impl ir::Program { - pub fn environment(&self) -> ir::ProgramEnvironment { +impl Program { + pub fn environment(&self) -> ProgramEnvironment { // Construct the set of *clauses*; these are sort of a compiled form // of the data above that always has the form: // @@ -36,20 +36,20 @@ impl ir::Program { // Adds clause that defines the Derefs domain goal: // forall { Derefs(T, U) :- ProjectionEq(::Target = U>) } - if let Some(trait_id) = self.lang_items.get(&ir::LangItem::DerefTrait) { + if let Some(trait_id) = self.lang_items.get(&LangItem::DerefTrait) { // Find `Deref::Target`. let associated_ty_id = self.associated_ty_data.values() .find(|d| d.trait_id == *trait_id) .expect("Deref has no assoc item") .id; - let t = || ir::Ty::Var(0); - let u = || ir::Ty::Var(1); - program_clauses.push(ir::Binders { - binders: vec![ir::ParameterKind::Ty(()), ir::ParameterKind::Ty(())], - value: ir::ProgramClauseImplication { - consequence: ir::DomainGoal::Derefs(ir::Derefs { source: t(), target: u() }), - conditions: vec![ir::ProjectionEq { - projection: ir::ProjectionTy { + let t = || Ty::Var(0); + let u = || Ty::Var(1); + program_clauses.push(Binders { + binders: vec![ParameterKind::Ty(()), ParameterKind::Ty(())], + value: ProgramClauseImplication { + consequence: DomainGoal::Derefs(Derefs { source: t(), target: u() }), + conditions: vec![ProjectionEq { + projection: ProjectionTy { associated_ty_id, parameters: vec![t().cast()] }, @@ -78,7 +78,7 @@ impl ir::Program { let trait_data = self.trait_data.clone(); let associated_ty_data = self.associated_ty_data.clone(); - ir::ProgramEnvironment { + ProgramEnvironment { trait_data, associated_ty_data, program_clauses, @@ -86,15 +86,15 @@ impl ir::Program { } } -impl ir::ImplDatum { +impl ImplDatum { /// Given `impl Clone for Vec`, generate: /// /// ```notrust /// forall { (Vec: Clone) :- (T: Clone) } /// ``` - fn to_program_clause(&self) -> ir::ProgramClause { + fn to_program_clause(&self) -> ProgramClause { self.binders.map_ref(|bound| { - ir::ProgramClauseImplication { + ProgramClauseImplication { consequence: bound.trait_ref.trait_ref().clone().cast(), conditions: bound .where_clauses @@ -107,7 +107,7 @@ impl ir::ImplDatum { } } -impl ir::DefaultImplDatum { +impl DefaultImplDatum { /// For each accessible type `T` in a struct which needs a default implementation for the auto /// trait `Foo` (accessible types are the struct fields types), we add a bound `T: Foo` (which /// is then expanded with `WF(T: Foo)`). For example, given: @@ -131,15 +131,15 @@ impl ir::DefaultImplDatum { /// (Box>>: Send) /// } /// ``` - fn to_program_clause(&self) -> ir::ProgramClause { + fn to_program_clause(&self) -> ProgramClause { self.binders.map_ref(|bound| { - ir::ProgramClauseImplication { + ProgramClauseImplication { consequence: bound.trait_ref.clone().cast(), conditions: { let wc = bound.accessible_tys.iter().cloned().map(|ty| { - ir::TraitRef { + TraitRef { trait_id: bound.trait_ref.trait_id, - parameters: vec![ir::ParameterKind::Ty(ty)], + parameters: vec![ParameterKind::Ty(ty)], } }); @@ -150,7 +150,7 @@ impl ir::DefaultImplDatum { } } -impl ir::AssociatedTyValue { +impl AssociatedTyValue { /// Given: /// /// ```notrust @@ -180,9 +180,9 @@ impl ir::AssociatedTyValue { /// ``` fn to_program_clauses( &self, - program: &ir::Program, - impl_datum: &ir::ImplDatum, - ) -> Vec { + program: &Program, + impl_datum: &ImplDatum, + ) -> Vec { let associated_ty = &program.associated_ty_data[&self.associated_ty_id]; // Begin with the innermost parameters (`'a`) and then add those from impl (`T`). @@ -218,7 +218,7 @@ impl ir::AssociatedTyValue { .map(|wc| Subst::apply(&all_parameters, wc)) .casted(); - let conditions: Vec = + let conditions: Vec = where_clauses .chain(Some(impl_trait_ref.clone().cast())) .collect(); @@ -234,7 +234,7 @@ impl ir::AssociatedTyValue { .collect() }; - let projection = ir::ProjectionTy { + let projection = ProjectionTy { associated_ty_id: self.associated_ty_id, // Add the remaining parameters of the trait-ref, if any @@ -244,35 +244,35 @@ impl ir::AssociatedTyValue { .collect(), }; - let normalize_goal = ir::DomainGoal::Normalize(ir::Normalize { + let normalize_goal = DomainGoal::Normalize(Normalize { projection: projection.clone(), ty: self.value.value.ty.clone(), }); // Determine the normalization - let normalization = ir::Binders { + let normalization = Binders { binders: all_binders.clone(), - value: ir::ProgramClauseImplication { + value: ProgramClauseImplication { consequence: normalize_goal.clone(), conditions: conditions, }, }.cast(); - let unselected_projection = ir::UnselectedProjectionTy { + let unselected_projection = UnselectedProjectionTy { type_name: associated_ty.name.clone(), parameters: parameters, }; - let unselected_normalization = ir::Binders { + let unselected_normalization = Binders { binders: all_binders.clone(), - value: ir::ProgramClauseImplication { - consequence: ir::DomainGoal::UnselectedNormalize(ir::UnselectedNormalize { + value: ProgramClauseImplication { + consequence: DomainGoal::UnselectedNormalize(UnselectedNormalize { projection: unselected_projection, ty: self.value.value.ty.clone(), }), conditions: vec![ normalize_goal.cast(), - ir::DomainGoal::InScope(impl_trait_ref.trait_id).cast(), + DomainGoal::InScope(impl_trait_ref.trait_id).cast(), ], }, }.cast(); @@ -281,8 +281,8 @@ impl ir::AssociatedTyValue { } } -impl ir::StructDatum { - fn to_program_clauses(&self) -> Vec { +impl StructDatum { + fn to_program_clauses(&self) -> Vec { // Given: // // struct Foo { } @@ -306,8 +306,8 @@ impl ir::StructDatum { // forall { IsLocal(Box) :- IsLocal(T) } let wf = self.binders.map_ref(|bound_datum| { - ir::ProgramClauseImplication { - consequence: ir::DomainGoal::WellFormedTy(bound_datum.self_ty.clone().cast()), + ProgramClauseImplication { + consequence: WellFormed::Ty(bound_datum.self_ty.clone().cast()).cast(), conditions: { bound_datum.where_clauses @@ -323,9 +323,9 @@ impl ir::StructDatum { // Types that are not marked `extern` satisfy IsLocal(TypeName) if !self.binders.value.flags.external { - // `IsLocal(Ty)` depends *only* on whether the type is marked extern and nothing else - let is_local = self.binders.map_ref(|bound_datum| ir::ProgramClauseImplication { - consequence: ir::DomainGoal::IsLocal(bound_datum.self_ty.clone().cast()), + // `IsLocalTy(Ty)` depends *only* on whether the type is marked extern and nothing else + let is_local = self.binders.map_ref(|bound_datum| ProgramClauseImplication { + consequence: DomainGoal::IsLocal(bound_datum.self_ty.clone().cast()), conditions: Vec::new(), }).cast(); @@ -342,10 +342,10 @@ impl ir::StructDatum { assert_eq!(self.binders.value.self_ty.len_type_parameters(), 1, "Only fundamental types with a single parameter are supported"); - let local_fundamental = self.binders.map_ref(|bound_datum| ir::ProgramClauseImplication { - consequence: ir::DomainGoal::IsLocal(bound_datum.self_ty.clone().cast()), + let local_fundamental = self.binders.map_ref(|bound_datum| ProgramClauseImplication { + consequence: DomainGoal::IsLocal(bound_datum.self_ty.clone().cast()), conditions: vec![ - ir::DomainGoal::IsLocal( + DomainGoal::IsLocal( // This unwrap is safe because we asserted above for the presence of a type // parameter bound_datum.self_ty.first_type_parameter().unwrap() @@ -356,7 +356,9 @@ impl ir::StructDatum { clauses.push(local_fundamental); } - let condition = ir::DomainGoal::FromEnvTy(self.binders.value.self_ty.clone().cast()); + let condition = DomainGoal::FromEnv( + FromEnv::Ty(self.binders.value.self_ty.clone().cast()) + ); for wc in self.binders .value @@ -374,9 +376,9 @@ impl ir::StructDatum { // `forall<'a, T> { FromEnv(T: Fn(&'a i32)) :- FromEnv(Foo) }` // let shift = wc.binders.len(); - clauses.push(ir::Binders { + clauses.push(Binders { binders: wc.binders.into_iter().chain(self.binders.binders.clone()).collect(), - value: ir::ProgramClauseImplication { + value: ProgramClauseImplication { consequence: wc.value, conditions: vec![condition.clone().up_shift(shift).cast()], } @@ -387,8 +389,8 @@ impl ir::StructDatum { } } -impl ir::TraitDatum { - fn to_program_clauses(&self) -> Vec { +impl TraitDatum { + fn to_program_clauses(&self) -> Vec { // Given: // // trait Ord where Self: Eq { ... } @@ -404,27 +406,30 @@ impl ir::TraitDatum { // forall { (Self: Ord) :- FromEnv(Self: Ord) } // forall { FromEnv(Self: Eq) :- FromEnv(Self: Ord) } - let trait_ref_impl = ir::WhereClauseAtom::Implemented( + let trait_ref = self.binders.value.trait_ref.clone(); + + let trait_ref_impl = WhereClause::Implemented( self.binders.value.trait_ref.clone() ); let wf = self.binders.map_ref(|bound| { - ir::ProgramClauseImplication { - consequence: ir::DomainGoal::WellFormed(trait_ref_impl.clone()), + ProgramClauseImplication { + consequence: WellFormed::Trait(trait_ref.clone()).cast(), conditions: { bound.where_clauses .iter() .cloned() - .map(|wc| wc.map(|bound| bound.into_well_formed_goal()).cast()) - .chain(Some(ir::DomainGoal::Holds(trait_ref_impl.clone()).cast())) + .map(|wc| wc.map(|bound| bound.into_well_formed_goal())) + .casted() + .chain(Some(DomainGoal::Holds(trait_ref_impl.clone()).cast())) .collect() }, } }).cast(); let mut clauses = vec![wf]; - let condition = ir::DomainGoal::FromEnv(trait_ref_impl.clone()); + let condition = DomainGoal::FromEnv(FromEnv::Trait(trait_ref.clone())); for wc in self.binders .value @@ -436,9 +441,9 @@ impl ir::TraitDatum { // We move the binders of the where-clause to the left for the reverse rules, // cf `StructDatum::to_program_clauses`. let shift = wc.binders.len(); - clauses.push(ir::Binders { + clauses.push(Binders { binders: wc.binders.into_iter().chain(self.binders.binders.clone()).collect(), - value: ir::ProgramClauseImplication { + value: ProgramClauseImplication { consequence: wc.value, conditions: vec![condition.clone().up_shift(shift).cast()], } @@ -446,8 +451,8 @@ impl ir::TraitDatum { } clauses.push(self.binders.map_ref(|_| { - ir::ProgramClauseImplication { - consequence: ir::DomainGoal::Holds(trait_ref_impl), + ProgramClauseImplication { + consequence: DomainGoal::Holds(trait_ref_impl), conditions: vec![condition.cast()], } }).cast()); @@ -456,8 +461,8 @@ impl ir::TraitDatum { } } -impl ir::AssociatedTyDatum { - fn to_program_clauses(&self, program: &ir::Program) -> Vec { +impl AssociatedTyDatum { + fn to_program_clauses(&self, program: &Program) -> Vec { // For each associated type, we define the "projection // equality" rules. There are always two; one for a successful normalization, // and one for the "fallback" notion of equality. @@ -502,7 +507,7 @@ impl ir::AssociatedTyDatum { .map(|pk| pk.map(|_| ())) .collect(); let parameters: Vec<_> = binders.iter().zip(0..).map(|p| p.to_parameter()).collect(); - let projection = ir::ProjectionTy { + let projection = ProjectionTy { associated_ty_id: self.id, parameters: parameters.clone(), }; @@ -510,7 +515,7 @@ impl ir::AssociatedTyDatum { // Retrieve the trait ref embedding the associated type let trait_ref = { let (associated_ty_data, trait_params, _) = program.split_projection(&projection); - ir::TraitRef { + TraitRef { trait_id: associated_ty_data.trait_id, parameters: trait_params.to_owned(), } @@ -518,13 +523,13 @@ impl ir::AssociatedTyDatum { // Construct an application from the projection. So if we have `::Item`, // we would produce `(Iterator::Item)`. - let app = ir::ApplicationTy { - name: ir::TypeName::AssociatedType(self.id), + let app = ApplicationTy { + name: TypeName::AssociatedType(self.id), parameters, }; - let app_ty = ir::Ty::Apply(app); + let app_ty = Ty::Apply(app); - let projection_eq = ir::ProjectionEq { + let projection_eq = ProjectionEq { projection: projection.clone(), ty: app_ty.clone(), }; @@ -537,9 +542,9 @@ impl ir::AssociatedTyDatum { // forall { // ProjectionEq(::Assoc = (Foo::Assoc)). // } - clauses.push(ir::Binders { + clauses.push(Binders { binders: binders.clone(), - value: ir::ProgramClauseImplication { + value: ProgramClauseImplication { consequence: projection_eq.clone().cast(), conditions: vec![], }, @@ -550,10 +555,10 @@ impl ir::AssociatedTyDatum { // forall { // WellFormed((Foo::Assoc)) :- Self: Foo, WC. // } - clauses.push(ir::Binders { + clauses.push(Binders { binders: binders.clone(), - value: ir::ProgramClauseImplication { - consequence: ir::DomainGoal::WellFormedTy(app_ty.clone()).cast(), + value: ProgramClauseImplication { + consequence: WellFormed::Ty(app_ty.clone()).cast(), conditions: iter::once(trait_ref.clone().cast()) .chain(self.where_clauses.iter().cloned().casted()) .collect(), @@ -566,11 +571,11 @@ impl ir::AssociatedTyDatum { // forall { // FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)). // } - clauses.push(ir::Binders { + clauses.push(Binders { binders: binders.clone(), - value: ir::ProgramClauseImplication { - consequence: ir::DomainGoal::FromEnv(trait_ref.clone().cast()), - conditions: vec![ir::DomainGoal::FromEnvTy(app_ty.clone()).cast()], + value: ProgramClauseImplication { + consequence: FromEnv::Trait(trait_ref.clone()).cast(), + conditions: vec![FromEnv::Ty(app_ty.clone()).cast()], } }.cast()); @@ -583,11 +588,13 @@ impl ir::AssociatedTyDatum { // This is really a family of clauses, one for each where clause. clauses.extend(self.where_clauses.iter().map(|wc| { let shift = wc.binders.len(); - ir::Binders { + Binders { binders: wc.binders.iter().chain(binders.iter()).cloned().collect(), - value: ir::ProgramClauseImplication { + value: ProgramClauseImplication { consequence: wc.value.clone().into_from_env_goal(), - conditions: vec![ir::DomainGoal::FromEnvTy(app_ty.clone()).up_shift(shift).cast()], + conditions: vec![ + FromEnv::Ty(app_ty.clone()).up_shift(shift).cast() + ], } }.cast() })); @@ -598,12 +605,12 @@ impl ir::AssociatedTyDatum { // FromEnv(::Assoc: Bounds) :- FromEnv(Self: Foo) // } clauses.extend(self.bounds_on_self().into_iter().map(|bound| { - ir::Binders { + Binders { binders: binders.clone(), - value: ir::ProgramClauseImplication { + value: ProgramClauseImplication { consequence: bound.into_from_env_goal(), conditions: vec![ - ir::DomainGoal::FromEnv(trait_ref.clone().cast()).cast() + FromEnv::Trait(trait_ref.clone()).cast() ], } }.cast() @@ -611,14 +618,14 @@ impl ir::AssociatedTyDatum { // add new type parameter U let mut binders = binders; - binders.push(ir::ParameterKind::Ty(())); - let ty = ir::Ty::Var(binders.len() - 1); + binders.push(ParameterKind::Ty(())); + let ty = Ty::Var(binders.len() - 1); // `Normalize(::Assoc -> U)` - let normalize = ir::Normalize { projection: projection.clone(), ty: ty.clone() }; + let normalize = Normalize { projection: projection.clone(), ty: ty.clone() }; // `ProjectionEq(::Assoc = U)` - let projection_eq = ir::ProjectionEq { projection: projection.clone(), ty }; + let projection_eq = ProjectionEq { projection: projection.clone(), ty }; // Projection equality rule from above. // @@ -626,9 +633,9 @@ impl ir::AssociatedTyDatum { // ProjectionEq(::Assoc = U) :- // Normalize(::Assoc -> U). // } - clauses.push(ir::Binders { + clauses.push(Binders { binders: binders.clone(), - value: ir::ProgramClauseImplication { + value: ProgramClauseImplication { consequence: projection_eq.clone().cast(), conditions: vec![normalize.clone().cast()], }, diff --git a/src/rules/wf.rs b/src/rules/wf.rs index a9a7519be2e..a0c0f11e34b 100644 --- a/src/rules/wf.rs +++ b/src/rules/wf.rs @@ -109,45 +109,11 @@ impl FoldInputTypes for ProjectionEq { } } -impl FoldInputTypes for WhereClauseAtom { +impl FoldInputTypes for WhereClause { fn fold(&self, accumulator: &mut Vec) { match self { - WhereClauseAtom::Implemented(tr) => tr.fold(accumulator), - WhereClauseAtom::ProjectionEq(p) => p.fold(accumulator), - } - } -} - -impl FoldInputTypes for Normalize { - fn fold(&self, accumulator: &mut Vec) { - self.projection.parameters.fold(accumulator); - self.ty.fold(accumulator); - } -} - -impl FoldInputTypes for UnselectedNormalize { - fn fold(&self, accumulator: &mut Vec) { - self.projection.parameters.fold(accumulator); - self.ty.fold(accumulator); - } -} - -impl FoldInputTypes for DomainGoal { - fn fold(&self, accumulator: &mut Vec) { - match self { - DomainGoal::Holds(wca) => wca.fold(accumulator), - DomainGoal::Normalize(n) => n.fold(accumulator), - DomainGoal::UnselectedNormalize(n) => n.fold(accumulator), - - DomainGoal::WellFormed(..) | - DomainGoal::FromEnv(..) | - DomainGoal::WellFormedTy(..) | - DomainGoal::FromEnvTy(..) | - DomainGoal::IsLocal(..) | - DomainGoal::LocalImplAllowed(..) | - DomainGoal::Derefs(..) => panic!("unexpected where clause"), - - DomainGoal::InScope(..) => (), + WhereClause::Implemented(tr) => tr.fold(accumulator), + WhereClause::ProjectionEq(p) => p.fold(accumulator), } } } @@ -169,7 +135,9 @@ impl WfSolver { return true; } - let goals = input_types.into_iter().map(|ty| DomainGoal::WellFormedTy(ty).cast()); + let goals = input_types.into_iter() + .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty))) + .casted(); let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) .expect("at least one goal"); @@ -248,7 +216,7 @@ impl WfSolver { let wf_goals = input_types.into_iter() - .map(|ty| DomainGoal::WellFormedTy(ty)); + .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty))); let trait_ref = trait_ref.up_shift(assoc_ty.value.binders.len()); @@ -264,7 +232,7 @@ impl WfSolver { let bound_goals = bounds.iter() .map(|b| Subst::apply(&all_parameters, b)) - .flat_map(|b| b.lower_with_self(assoc_ty.value.value.ty.clone())) + .flat_map(|b| b.into_where_clauses(assoc_ty.value.value.ty.clone())) .map(|g| g.into_well_formed_goal()); let goals = wf_goals.chain(bound_goals).casted(); @@ -301,11 +269,11 @@ impl WfSolver { // Things to prove well-formed: input types of the where-clauses, projection types // appearing in the header, associated type values, and of course the trait ref. let trait_ref_wf = DomainGoal::WellFormed( - WhereClauseAtom::Implemented(trait_ref.clone()) + WellFormed::Trait(trait_ref.clone()) ); let goals = input_types.into_iter() - .map(|ty| DomainGoal::WellFormedTy(ty).cast()) + .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty)).cast()) .chain(assoc_ty_goals) .chain(Some(trait_ref_wf).cast()); @@ -323,7 +291,11 @@ impl WfSolver { .cloned() .map(|wc| wc.map(|bound| bound.into_from_env_goal())) .casted() - .chain(header_input_types.into_iter().map(|ty| DomainGoal::FromEnvTy(ty).cast())) + .chain( + header_input_types.into_iter() + .map(|ty| DomainGoal::FromEnv(FromEnv::Ty(ty))) + .casted() + ) .collect(); let goal = Goal::Implies(hypotheses, Box::new(goal)) diff --git a/src/zip.rs b/src/zip.rs index 17b3ab237d6..d1d1e78ec7b 100644 --- a/src/zip.rs +++ b/src/zip.rs @@ -216,15 +216,15 @@ macro_rules! enum_zip { /// variant, then zips each field of the variant in turn. Only works /// if all variants have a single parenthesized value right now. enum_zip!(PolarizedTraitRef { Positive, Negative }); -enum_zip!(WhereClauseAtom { Implemented, ProjectionEq }); +enum_zip!(WhereClause { Implemented, ProjectionEq }); +enum_zip!(WellFormed { Trait, Ty }); +enum_zip!(FromEnv { Trait, Ty }); enum_zip!(DomainGoal { Holds, WellFormed, FromEnv, Normalize, UnselectedNormalize, - WellFormedTy, - FromEnvTy, InScope, Derefs, IsLocal, From 5607fc91431b39e6fe0815ec8be75774ca0713e7 Mon Sep 17 00:00:00 2001 From: scalexm Date: Sun, 27 May 2018 14:34:24 +0200 Subject: [PATCH 2/2] Update doc and refactor some parts of the lowering process --- chalk-parse/src/ast.rs | 33 +++++++++++++-- src/ir.rs | 2 +- src/ir/lowering.rs | 95 ++++++++++++++++-------------------------- src/rules.rs | 19 ++++++--- src/rules/wf/test.rs | 6 +-- 5 files changed, 83 insertions(+), 72 deletions(-) diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index bd597bfae4f..762c1ee366f 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -1,7 +1,7 @@ use lalrpop_intern::InternedString; use std::fmt; -#[derive(Copy, Clone, Debug, PartialEq, Eq)] +#[derive(Copy, Clone, PartialEq, Eq, Debug)] pub struct Span { pub lo: usize, pub hi: usize, @@ -13,10 +13,12 @@ impl Span { } } +#[derive(Clone, PartialEq, Eq, Debug)] pub struct Program { pub items: Vec } +#[derive(Clone, PartialEq, Eq, Debug)] pub enum Item { StructDefn(StructDefn), TraitDefn(TraitDefn), @@ -24,6 +26,7 @@ pub enum Item { Clause(Clause), } +#[derive(Clone, PartialEq, Eq, Debug)] pub struct StructDefn { pub name: Identifier, pub parameter_kinds: Vec, @@ -32,11 +35,13 @@ pub struct StructDefn { pub flags: StructFlags, } +#[derive(Clone, PartialEq, Eq, Debug)] pub struct StructFlags { pub external: bool, pub fundamental: bool, } +#[derive(Clone, PartialEq, Eq, Debug)] pub struct TraitDefn { pub name: Identifier, pub parameter_kinds: Vec, @@ -45,6 +50,7 @@ pub struct TraitDefn { pub flags: TraitFlags, } +#[derive(Clone, PartialEq, Eq, Debug)] pub struct TraitFlags { pub auto: bool, pub marker: bool, @@ -52,6 +58,7 @@ pub struct TraitFlags { pub deref: bool, } +#[derive(Clone, PartialEq, Eq, Debug)] pub struct AssocTyDefn { pub name: Identifier, pub parameter_kinds: Vec, @@ -59,22 +66,26 @@ pub struct AssocTyDefn { pub where_clauses: Vec, } +#[derive(Copy, Clone, PartialEq, Eq, Debug)] pub enum ParameterKind { Ty(Identifier), Lifetime(Identifier), } +#[derive(Clone, PartialEq, Eq, Debug)] pub enum Parameter { Ty(Ty), Lifetime(Lifetime), } +#[derive(Clone, PartialEq, Eq, Debug)] /// An inline bound, e.g. `: Foo` in `impl> SomeType`. pub enum InlineBound { TraitBound(TraitBound), ProjectionEqBound(ProjectionEqBound), } +#[derive(Clone, PartialEq, Eq, Debug)] /// Represents a trait bound on e.g. a type or type parameter. /// Does not know anything about what it's binding. pub struct TraitBound { @@ -82,6 +93,7 @@ pub struct TraitBound { pub args_no_self: Vec, } +#[derive(Clone, PartialEq, Eq, Debug)] /// Represents a projection equality bound on e.g. a type or type parameter. /// Does not know anything about what it's binding. pub struct ProjectionEqBound { @@ -91,7 +103,7 @@ pub struct ProjectionEqBound { pub value: Ty, } -#[derive(Copy, Clone, Debug, Eq, PartialEq)] +#[derive(Copy, Clone, PartialEq, Eq, Debug)] pub enum Kind { Ty, Lifetime, @@ -130,6 +142,7 @@ impl Kinded for Parameter { } } +#[derive(Clone, PartialEq, Eq, Debug)] pub struct Impl { pub parameter_kinds: Vec, pub trait_ref: PolarizedTraitRef, @@ -137,12 +150,14 @@ pub struct Impl { pub assoc_ty_values: Vec, } +#[derive(Clone, PartialEq, Eq, Debug)] pub struct AssocTyValue { pub name: Identifier, pub parameter_kinds: Vec, pub value: Ty, } +#[derive(Clone, PartialEq, Eq, Debug)] pub enum Ty { Id { name: Identifier, @@ -163,28 +178,33 @@ pub enum Ty { } } +#[derive(Copy, Clone, PartialEq, Eq, Debug)] pub enum Lifetime { Id { name: Identifier, } } +#[derive(Clone, PartialEq, Eq, Debug)] pub struct ProjectionTy { pub trait_ref: TraitRef, pub name: Identifier, pub args: Vec, } +#[derive(Clone, PartialEq, Eq, Debug)] pub struct UnselectedProjectionTy { pub name: Identifier, pub args: Vec, } +#[derive(Clone, PartialEq, Eq, Debug)] pub struct TraitRef { pub trait_name: Identifier, pub args: Vec, } +#[derive(Clone, PartialEq, Eq, Debug)] pub enum PolarizedTraitRef { Positive(TraitRef), Negative(TraitRef), @@ -200,17 +220,19 @@ impl PolarizedTraitRef { } } -#[derive(Copy, Clone, Debug)] +#[derive(Copy, Clone, PartialEq, Eq, Debug)] pub struct Identifier { pub str: InternedString, pub span: Span, } +#[derive(Clone, PartialEq, Eq, Debug)] pub enum WhereClause { Implemented { trait_ref: TraitRef }, ProjectionEq { projection: ProjectionTy, ty: Ty }, } +#[derive(Clone, PartialEq, Eq, Debug)] pub enum DomainGoal { Holds { where_clause: WhereClause }, Normalize { projection: ProjectionTy, ty: Ty }, @@ -223,22 +245,26 @@ pub enum DomainGoal { IsLocal { ty: Ty }, } +#[derive(Clone, PartialEq, Eq, Debug)] pub enum LeafGoal { DomainGoal { goal: DomainGoal }, UnifyTys { a: Ty, b: Ty }, UnifyLifetimes { a: Lifetime, b: Lifetime }, } +#[derive(Clone, PartialEq, Eq, Debug)] pub struct QuantifiedWhereClause { pub parameter_kinds: Vec, pub where_clause: WhereClause, } +#[derive(Clone, PartialEq, Eq, Debug)] pub struct Field { pub name: Identifier, pub ty: Ty, } +#[derive(Clone, PartialEq, Eq, Debug)] /// This allows users to add arbitrary `A :- B` clauses into the /// logic; it has no equivalent in Rust, but it's useful for testing. pub struct Clause { @@ -247,6 +273,7 @@ pub struct Clause { pub conditions: Vec>, } +#[derive(Clone, PartialEq, Eq, Debug)] pub enum Goal { ForAll(Vec, Box), Exists(Vec, Box), diff --git a/src/ir.rs b/src/ir.rs index d334dde566b..66fcfb5a970 100644 --- a/src/ir.rs +++ b/src/ir.rs @@ -295,7 +295,7 @@ impl TraitBound { vec![WhereClause::Implemented(trait_ref)] } - fn as_trait_ref(&self, self_ty: Ty) -> TraitRef { + crate fn as_trait_ref(&self, self_ty: Ty) -> TraitRef { let self_ty = ParameterKind::Ty(self_ty); TraitRef { trait_id: self.trait_id, diff --git a/src/ir/lowering.rs b/src/ir/lowering.rs index 43c972592a1..7636e013a70 100644 --- a/src/ir/lowering.rs +++ b/src/ir/lowering.rs @@ -418,14 +418,14 @@ trait LowerWhereClauseVec { impl LowerWhereClauseVec for [WhereClause] { fn lower(&self, env: &Env) -> Result> { - self.iter().flat_map(|wc| LowerWhereClause::lower(wc, env).apply_result()).collect() + self.iter().flat_map(|wc| wc.lower(env).apply_result()).collect() } } impl LowerWhereClauseVec for [QuantifiedWhereClause] { fn lower(&self, env: &Env) -> Result> { self.iter() - .flat_map(|wc| match LowerWhereClause::lower(wc, env) { + .flat_map(|wc| match wc.lower(env) { Ok(v) => v.into_iter().map(Ok).collect(), Err(e) => vec![Err(e)], }) @@ -434,6 +434,10 @@ impl LowerWhereClauseVec for [QuantifiedWhereClause] } trait LowerWhereClause { + /// Lower from an AST `where` clause to an internal IR. + /// Some AST `where` clauses can lower to multiple ones, this is why we return a `Vec`. + /// As for now, this is the only the case for `where T: Foo` which lowers to + /// `Implemented(T: Foo)` and `ProjectionEq(::Item = U)`. fn lower(&self, env: &Env) -> Result>; } @@ -464,7 +468,7 @@ impl LowerWhereClause for QuantifiedWhereClause { fn lower(&self, env: &Env) -> Result> { let parameter_kinds = self.parameter_kinds.iter().map(|pk| pk.lower()); let binders = env.in_binders(parameter_kinds, |env| { - Ok(LowerWhereClause::lower(&self.where_clause, env)?) + Ok(self.where_clause.lower(env)?) })?; Ok(binders.into_iter().collect()) } @@ -474,14 +478,6 @@ trait LowerDomainGoal { fn lower(&self, env: &Env) -> Result>; } -/// Lowers a where-clause in the context of a clause (i.e. in "negative" -/// position); this is limited to the kinds of where-clauses users can actually -/// type in Rust and well-formedness checks. -/// -/// Lowers a where-clause in the context of a goal (i.e. in "positive" -/// position); this is richer in terms of the legal sorts of where-clauses that -/// can appear, because it includes all the sorts of things that the compiler -/// must verify. impl LowerDomainGoal for DomainGoal { fn lower(&self, env: &Env) -> Result> { let goals = match self { @@ -614,46 +610,22 @@ trait LowerTraitRef { impl LowerTraitRef for TraitRef { fn lower(&self, env: &Env) -> Result { - 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 - .iter() - .map(|a| Ok(a.lower(env)?)) - .collect::>>()?; - - if parameters.len() != k.binders.len() + 1 { - bail!( - "wrong number of parameters, expected `{:?}`, got `{:?}`", - k.binders.len() + 1, - parameters.len() - ) - } - - for (binder, param) in k.binders.binders.iter().zip(parameters.iter().skip(1)) { - check_type_kinds("incorrect kind for trait parameter", binder, param)?; - } + let without_self = TraitBound { + trait_name: self.trait_name, + args_no_self: self.args.iter().cloned().skip(1).collect(), + }.lower(env)?; - Ok(ir::TraitRef { - trait_id: id, - parameters: parameters, - }) + let self_parameter = self.args[0].lower(env)?; + Ok(without_self.as_trait_ref(self_parameter.ty().unwrap())) } } trait LowerTraitBound { - fn lower_trait_bound(&self, env: &Env) -> Result; + fn lower(&self, env: &Env) -> Result; } impl LowerTraitBound for TraitBound { - fn lower_trait_bound(&self, env: &Env) -> Result { + fn lower(&self, env: &Env) -> Result { let id = match env.lookup(self.trait_name)? { NameLookup::Type(id) => id, NameLookup::Parameter(_) => bail!(ErrorKind::NotTrait(self.trait_name)), @@ -688,19 +660,13 @@ impl LowerTraitBound for TraitBound { } } -trait LowerInlineBound { - fn lower(&self, env: &Env) -> Result; -} - -impl LowerInlineBound for TraitBound { - fn lower(&self, env: &Env) -> Result { - Ok(ir::InlineBound::TraitBound(self.lower_trait_bound(&env)?)) - } +trait LowerProjectionEqBound { + fn lower(&self, env: &Env) -> Result; } -impl LowerInlineBound for ProjectionEqBound { - fn lower(&self, env: &Env) -> Result { - let trait_bound = self.trait_bound.lower_trait_bound(env)?; +impl LowerProjectionEqBound for ProjectionEqBound { + fn lower(&self, env: &Env) -> Result { + let trait_bound = self.trait_bound.lower(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), @@ -719,21 +685,30 @@ impl LowerInlineBound for ProjectionEqBound { check_type_kinds("incorrect kind for associated type parameter", param, arg)?; } - Ok(ir::InlineBound::ProjectionEqBound(ir::ProjectionEqBound { + Ok(ir::ProjectionEqBound { trait_bound, associated_ty_id: info.id, parameters: args, value: self.value.lower(env)?, - })) + }) } } +trait LowerInlineBound { + fn lower(&self, env: &Env) -> Result; +} + impl LowerInlineBound for InlineBound { fn lower(&self, env: &Env) -> Result { - match self { - InlineBound::TraitBound(b) => b.lower(&env), - InlineBound::ProjectionEqBound(b) => b.lower(&env), - } + let bound = match self { + InlineBound::TraitBound(b) => ir::InlineBound::TraitBound( + b.lower(&env)? + ), + InlineBound::ProjectionEqBound(b) => ir::InlineBound::ProjectionEqBound( + b.lower(&env)? + ), + }; + Ok(bound) } } diff --git a/src/rules.rs b/src/rules.rs index c79d10e0f33..0789e65e5b5 100644 --- a/src/rules.rs +++ b/src/rules.rs @@ -151,21 +151,28 @@ impl DefaultImplDatum { } impl AssociatedTyValue { - /// Given: + /// Given the following trait: /// /// ```notrust + /// trait Iterable { + /// type IntoIter<'a>: 'a; + /// } + /// ``` + /// + /// Then for the following impl: + /// ```notrust /// impl Iterable for Vec { - /// type IntoIter<'a> where T: 'a = Iter<'a, T>; + /// type IntoIter<'a> = Iter<'a, T>; /// } /// ``` /// - /// generate: + /// we generate: /// /// ```notrust /// forall<'a, T> { /// Normalize( as Iterable>::IntoIter<'a> -> Iter<'a, T>>) :- /// (Vec: Iterable), // (1) - /// (T: 'a) // (2) + /// (Iter<'a, T>: 'a) // (2) /// } /// ``` /// @@ -211,7 +218,8 @@ impl AssociatedTyValue { // This comes in two parts, marked as (1) and (2) in example above: // // 1. require that the trait is implemented - // 2. any where-clauses from the `type` declaration in the impl + // 2. any where-clauses from the `type` declaration in the trait: the + // parameters must be substituted with those of the impl let where_clauses = associated_ty.where_clauses .iter() @@ -587,6 +595,7 @@ impl AssociatedTyDatum { // // This is really a family of clauses, one for each where clause. clauses.extend(self.where_clauses.iter().map(|wc| { + // Don't forget to move the binders to the left in case of higher-ranked where clauses. let shift = wc.binders.len(); Binders { binders: wc.binders.iter().chain(binders.iter()).cloned().collect(), diff --git a/src/rules/wf/test.rs b/src/rules/wf/test.rs index befb4214e89..3e1a3a6317d 100644 --- a/src/rules/wf/test.rs +++ b/src/rules/wf/test.rs @@ -206,7 +206,7 @@ fn wf_requiremements_for_projection() { } #[test] -fn projection_type_in_header() { +fn ill_formed_type_in_header() { lowering_error! { program { trait Foo { @@ -215,8 +215,8 @@ fn projection_type_in_header() { trait Bar { } - // Projection types in an impl header are not assumed to be well-formed, - // an explicit where clause is needed (see below). + // Types in where clauses are not assumed to be well-formed, + // an explicit where clause would be needed (see below). impl Bar for T where ::Value: Bar { } } error_msg { "trait impl for \"Bar\" does not meet well-formedness requirements"