Merge pull request #107 from scalexm/assoc-types

Add higher-ranked trait bounds

Author: nikomatsakis

chalk-parse/src/ast.rs

@@ -27,7 +27,7 @@ pub enum Item {
 pub struct StructDefn {
     pub name: Identifier,
     pub parameter_kinds: Vec<ParameterKind>,
-    pub where_clauses: Vec<WhereClause>,
+    pub where_clauses: Vec<QuantifiedWhereClause>,
     pub fields: Vec<Field>,
     pub flags: StructFlags,
 }
@@ -39,7 +39,7 @@ pub struct StructFlags {
 pub struct TraitDefn {
     pub name: Identifier,
     pub parameter_kinds: Vec<ParameterKind>,
-    pub where_clauses: Vec<WhereClause>,
+    pub where_clauses: Vec<QuantifiedWhereClause>,
     pub assoc_ty_defns: Vec<AssocTyDefn>,
     pub flags: TraitFlags,
 }
@@ -107,7 +107,7 @@ impl Kinded for Parameter {
 pub struct Impl {
     pub parameter_kinds: Vec<ParameterKind>,
     pub trait_ref: PolarizedTraitRef,
-    pub where_clauses: Vec<WhereClause>,
+    pub where_clauses: Vec<QuantifiedWhereClause>,
     pub assoc_ty_values: Vec<AssocTyValue>,
 }
 
@@ -194,6 +194,11 @@ pub enum WhereClause {
     TraitInScope { trait_name: Identifier },
 }
 
+pub struct QuantifiedWhereClause {
+    pub parameter_kinds: Vec<ParameterKind>,
+    pub where_clause: WhereClause,
+}
+
 pub struct Field {
     pub name: Identifier,
     pub ty: Ty,

chalk-parse/src/parser.lalrpop

@@ -40,7 +40,9 @@ AutoKeyword: () = "#" "[" "auto" "]";
 MarkerKeyword: () = "#" "[" "marker" "]";
 
 StructDefn: StructDefn = {
-    <external:ExternalKeyword?> "struct" <n:Id><p:Angle<ParameterKind>> <w:WhereClauses> "{" <f:Fields> "}" => StructDefn {
+    <external:ExternalKeyword?> "struct" <n:Id><p:Angle<ParameterKind>>
+        <w:QuantifiedWhereClauses> "{" <f:Fields> "}" => StructDefn
+    {
         name: n,
         parameter_kinds: p,
         where_clauses: w,
@@ -52,9 +54,9 @@ StructDefn: StructDefn = {
 };
 
 TraitDefn: TraitDefn = {
-    <external:ExternalKeyword?> <auto:AutoKeyword?> <marker:MarkerKeyword?> "trait" <n:Id><p:Angle<ParameterKind>> <w:WhereClauses> "{"
-        <a:AssocTyDefn*> "}" =>
-    TraitDefn {
+    <external:ExternalKeyword?> <auto:AutoKeyword?> <marker:MarkerKeyword?> "trait" <n:Id><p:Angle<ParameterKind>>
+        <w:QuantifiedWhereClauses> "{" <a:AssocTyDefn*> "}" => TraitDefn
+    {
         name: n,
         parameter_kinds: p,
         where_clauses: w,
@@ -75,8 +77,8 @@ AssocTyDefn: AssocTyDefn = {
 };
 
 Impl: Impl = {
-    "impl" <p:Angle<ParameterKind>> <mark:"!"?> <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:QuantifiedWhereClauses> "{" <assoc:AssocTyValue*> "}" =>
     {
         let mut args = vec![Parameter::Ty(s)];
         args.extend(a);
@@ -160,58 +162,53 @@ Field: Field = {
 };
 
 Clause: Clause = {
-    "forall" <pk:Angle<ParameterKind>> "{" <wc:WhereClause> "if" <g:Comma<Goal1>> "}" => {
-        Clause {
-            parameter_kinds: pk,
-            consequence: wc,
-            conditions: g,
-        }
+    "forall" <pk:Angle<ParameterKind>> "{" <wc:WhereClause> "if" <g:Comma<Goal1>> "}" => Clause {
+        parameter_kinds: pk,
+        consequence: wc,
+        conditions: g,
     },
 
-    "forall" <pk:Angle<ParameterKind>> "{" <wc:WhereClause> "}" => {
-        Clause {
-            parameter_kinds: pk,
-            consequence: wc,
-            conditions: vec![],
-        }
+    "forall" <pk:Angle<ParameterKind>> "{" <wc:WhereClause> "}" => Clause {
+        parameter_kinds: pk,
+        consequence: wc,
+        conditions: vec![],
     },
 };
 
 InlineClause1: Clause = {
-    <wc:WhereClause> => {
-        Clause {
-            parameter_kinds: vec![],
-            consequence: wc,
-            conditions: vec![],
-        }
+    <wc:WhereClause> => Clause {
+        parameter_kinds: vec![],
+        consequence: wc,
+        conditions: vec![],
     },
 
-    <wc:WhereClause> ":" "-" <g:Comma<Goal1>> => {
-        Clause {
-            parameter_kinds: vec![],
-            consequence: wc,
-            conditions: g,
-        }
+    <wc:WhereClause> ":" "-" <g:Comma<Goal1>> => Clause {
+        parameter_kinds: vec![],
+        consequence: wc,
+        conditions: g,
     },
 };
 
 InlineClause: Clause = {
     <InlineClause1>,
 
-    "forall" "<" <pk:Comma<ParameterKind>> ">" "{" <c:InlineClause1> "}" => {
-        Clause {
-            parameter_kinds: pk,
-            consequence: c.consequence,
-            conditions: c.conditions,
-        }
-    },
+    "forall" "<" <pk:Comma<ParameterKind>> ">" "{" <c:InlineClause1> "}" => Clause {
+        parameter_kinds: pk,
+        consequence: c.consequence,
+        conditions: c.conditions,
+    }
 };
 
 WhereClauses: Vec<WhereClause> = {
     "where" <Comma<WhereClause>>,
     () => vec![],
 };
 
+QuantifiedWhereClauses: Vec<QuantifiedWhereClause> = {
+    "where" <Comma<QuantifiedWhereClause>>,
+    () => vec![],
+};
+
 WhereClause: WhereClause = {
     <t:TraitRef<":">> => WhereClause::Implemented { trait_ref: t },
 
@@ -244,6 +241,18 @@ WhereClause: WhereClause = {
     "InScope" "(" <t:Id> ")" => WhereClause::TraitInScope { trait_name: t },
 };
 
+QuantifiedWhereClause: QuantifiedWhereClause = {
+    <wc:WhereClause> => QuantifiedWhereClause {
+        parameter_kinds: vec![],
+        where_clause: wc,
+    },
+
+    "forall" "<" <pk:Comma<ParameterKind>> ">" <wc:WhereClause> => QuantifiedWhereClause {
+        parameter_kinds: pk,
+        where_clause: wc,
+    },
+};
+
 TraitRef<S>: TraitRef = {
     <s:Ty> S <t:Id> <a:Angle<Parameter>> => {
         let mut args = vec![Parameter::Ty(s)];

src/bin/chalki.rs

@@ -1,5 +1,3 @@
-#![feature(match_default_bindings)]
-
 extern crate chalk;
 extern crate chalk_parse;
 extern crate docopt;

src/cast.rs

@@ -100,6 +100,34 @@ impl Cast<LeafGoal> for EqGoal {
     }
 }
 
+impl Cast<Goal> for QuantifiedDomainGoal {
+    fn cast(self) -> Goal {
+        if self.binders.is_empty() {
+            self.value.cast()
+        } else {
+            Goal::Quantified(
+                QuantifierKind::ForAll,
+                self.map(|bound| Box::new(bound.cast()))
+            )
+        }
+    }
+}
+
+impl Cast<ProgramClause> 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<Ty> for ApplicationTy {
     fn cast(self) -> Ty {
         Ty::Apply(self)

src/coherence/solve.rs

@@ -143,7 +143,7 @@ impl OverlapSolver {
         // Create a goal for each clause in both where clauses
         let wc_goals = lhs_where_clauses
             .chain(rhs_where_clauses)
-            .map(|wc| Goal::Leaf(LeafGoal::DomainGoal(wc)));
+            .map(|wc| wc.cast());
 
         // Join all the goals we've created together with And, then quantify them
         // over the joined binders. This is our query.
@@ -216,7 +216,7 @@ impl OverlapSolver {
             .value
             .where_clauses
             .iter()
-            .map(|wc| Goal::Leaf(LeafGoal::DomainGoal(wc.up_shift(more_len))));
+            .map(|wc| wc.up_shift(more_len).cast());
 
         // Join all of the goals together.
         let goal = params_goals

src/ir/mod.rs

@@ -193,7 +193,7 @@ pub struct ImplDatum {
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub struct ImplDatumBound {
     crate trait_ref: PolarizedTraitRef,
-    crate where_clauses: Vec<DomainGoal>,
+    crate where_clauses: Vec<QuantifiedDomainGoal>,
     crate associated_ty_values: Vec<AssociatedTyValue>,
     crate specialization_priority: usize,
 }
@@ -218,7 +218,7 @@ pub struct StructDatum {
 pub struct StructDatumBound {
     crate self_ty: ApplicationTy,
     crate fields: Vec<Ty>,
-    crate where_clauses: Vec<DomainGoal>,
+    crate where_clauses: Vec<QuantifiedDomainGoal>,
     crate flags: StructFlags,
 }
 
@@ -235,7 +235,7 @@ pub struct TraitDatum {
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub struct TraitDatumBound {
     crate trait_ref: TraitRef,
-    crate where_clauses: Vec<DomainGoal>,
+    crate where_clauses: Vec<QuantifiedDomainGoal>,
     crate flags: TraitFlags,
 }
 
@@ -518,6 +518,8 @@ pub enum DomainGoal {
     InScope(ItemId),
 }
 
+pub type QuantifiedDomainGoal = Binders<DomainGoal>;
+
 impl DomainGoal {
     /// Turn a where clause into the WF version of it i.e.:
     /// * `Implemented(T: Trait)` maps to `WellFormed(T: Trait)`
@@ -610,14 +612,19 @@ pub struct Binders<T> {
 }
 
 impl<T> Binders<T> {
-    crate fn map_ref<U, OP>(&self, op: OP) -> Binders<U>
-    where
-        OP: FnOnce(&T) -> U,
-    {
+    crate fn map<U, OP>(self, op: OP) -> Binders<U> where OP: FnOnce(T) -> U {
+        let value = op(self.value);
+        Binders {
+            binders: self.binders,
+            value,
+        }
+    }
+
+    crate fn map_ref<U, OP>(&self, op: OP) -> Binders<U> where OP: FnOnce(&T) -> U {
         let value = op(&self.value);
         Binders {
             binders: self.binders.clone(),
-            value: value,
+            value,
         }
     }
 
@@ -730,21 +737,7 @@ impl UCanonical<InEnvironment<Goal>> {
     /// with WF requirements and cyclic traits, which generates cycles in the proof tree which must
     /// not be rejected but instead must be treated as a success.
     crate fn is_coinductive(&self, program: &ProgramEnvironment) -> bool {
-        match &self.canonical.value.goal {
-            Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::Holds(wca))) => {
-                match wca {
-                    WhereClauseAtom::Implemented(tr) => {
-                        let trait_datum = &program.trait_data[&tr.trait_id];
-                        trait_datum.binders.value.flags.auto
-                    }
-                    WhereClauseAtom::ProjectionEq(..) => false,
-                }
-            }
-            Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::WellFormed(..))) => {
-                true
-            }
-            _ => false,
-        }
+        self.canonical.value.goal.is_coinductive(program)
     }
 }
 
@@ -843,6 +836,25 @@ impl Goal {
         let canonical_goal = infer.canonicalize(&env_goal).quantified;
         infer.u_canonicalize(&canonical_goal).quantified
     }
+
+    crate fn is_coinductive(&self, program: &ProgramEnvironment) -> bool {
+        match self {
+            Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::Holds(wca))) => {
+                match wca {
+                    WhereClauseAtom::Implemented(tr) => {
+                        let trait_datum = &program.trait_data[&tr.trait_id];
+                        trait_datum.binders.value.flags.auto
+                    }
+                    WhereClauseAtom::ProjectionEq(..) => false,
+                }
+            }
+            Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::WellFormed(..))) => {
+                true
+            }
+            Goal::Quantified(QuantifierKind::ForAll, goal) => goal.value.is_coinductive(program),
+            _ => false,
+        }
+    }
 }
 
 #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]