limit to supertraits, first test working

Author: nikomatsakis

crates/formality-prove/src/decls.rs

@@ -1,7 +1,11 @@
 use formality_macros::term;
 use formality_types::{
+    cast::Upcast,
     collections::Set,
-    grammar::{AliasName, AliasTy, Binder, TraitId, TraitRef, Ty, Wc, Wcs},
+    grammar::{
+        AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, Wcs,
+        PR,
+    },
 };
 
 #[term]
@@ -90,8 +94,27 @@ impl TraitDecl {
     /// this would return the set `{trait_invariant(<ty Self> Ord(Self) => PartialOrd(Self)}`
     pub fn trait_invariants(&self) -> Set<TraitInvariant> {
         let (variables, TraitDeclBoundData { where_clause }) = self.binder.open();
+        let self_var: Parameter = variables[0].upcast();
+
+        fn is_supertrait(self_var: &Parameter, wc: &Wc) -> bool {
+            match wc.data() {
+                formality_types::grammar::WcData::PR(PR::Predicate(Predicate::IsImplemented(
+                    trait_ref,
+                ))) => trait_ref.parameters[0] == *self_var,
+                formality_types::grammar::WcData::PR(PR::Relation(Relation::Outlives(a, _))) => {
+                    *a == *self_var
+                }
+                formality_types::grammar::WcData::PR(_) => false,
+                formality_types::grammar::WcData::ForAll(binder) => {
+                    is_supertrait(self_var, binder.peek())
+                }
+                formality_types::grammar::WcData::Implies(_, c) => is_supertrait(self_var, c),
+            }
+        }
+
         where_clause
             .into_iter()
+            .filter(|where_clause| is_supertrait(&self_var, where_clause))
             .map(|where_clause| TraitInvariant {
                 binder: Binder::new(
                     &variables,

crates/formality-prove/src/prove/prove_wc.rs

@@ -74,5 +74,14 @@ judgment_fn! {
             ----------------------------- ("eq")
             (prove_wc(decls, env, assumptions, Relation::Equals(a, b)) => c)
         )
+
+
+        (
+            (let t = decls.trait_decl(&trait_ref.trait_id))
+            (let t = t.binder.instantiate_with(&trait_ref.parameters).unwrap())
+            (prove(decls, env, assumptions, t.where_clause) => c)
+            ----------------------------- ("trait well formed")
+            (prove_wc(decls, env, assumptions, Predicate::WellFormedTraitRef(trait_ref)) => c)
+        )
     }
 }

crates/formality-types/src/grammar/formulas.rs

@@ -22,16 +22,6 @@ pub enum Predicate {
     #[cast]
     IsImplemented(TraitRef),
 
-    /// True if an alias normalizes to the given type.
-    #[grammar(@NormalizesTo($v0 -> $v1))]
-    NormalizesTo(AliasTy, Ty),
-
-    #[grammar(@WellFormedAdt($v0, $v1))]
-    WellFormedAdt(AdtId, Parameters),
-
-    #[grammar(@WellFormedAlias($v0, $v1))]
-    WellFormedAlias(AliasName, Parameters),
-
     #[grammar(@WellFormedTraitRef($v0))]
     WellFormedTraitRef(TraitRef),
 }
@@ -53,32 +43,6 @@ impl std::ops::BitAnd for Coinductive {
     }
 }
 
-impl Predicate {
-    /// True if this goal can be proven via a cycle. For example,
-    /// it is ok for a `T: Debug` impl to require `T: Debug`.
-    pub fn is_coinductive(&self) -> Coinductive {
-        match self {
-            Predicate::IsImplemented(_) => Coinductive::Yes,
-            Predicate::NormalizesTo(_, _) => Coinductive::No,
-            Predicate::WellFormedAlias(_, _)
-            | Predicate::WellFormedAdt(_, _)
-            | Predicate::WellFormedTraitRef(_) => Coinductive::Yes,
-        }
-    }
-}
-
-impl AliasName {
-    pub fn well_formed(&self, t: impl Upcast<Vec<Parameter>>) -> Predicate {
-        Predicate::WellFormedAlias(self.clone(), t.upcast())
-    }
-}
-
-impl AliasTy {
-    pub fn normalizes_to(&self, t: impl Upcast<Ty>) -> Predicate {
-        Predicate::NormalizesTo(self.clone(), t.upcast())
-    }
-}
-
 impl Ty {
     pub fn well_formed(&self) -> Relation {
         Relation::WellFormed(self.upcast())
@@ -102,10 +66,7 @@ impl Parameter {
 #[term]
 pub enum Skeleton {
     IsImplemented(TraitId),
-    NormalizesTo(AliasName),
     WellFormed,
-    WellFormedAdt(AdtId),
-    WellFormedAlias(AliasName),
     WellFormedTraitRef(TraitId),
 
     Equals,
@@ -125,20 +86,6 @@ impl Predicate {
                 Skeleton::IsImplemented(trait_id.clone()),
                 parameters.clone(),
             ),
-            Predicate::NormalizesTo(AliasTy { name, parameters }, ty) => (
-                Skeleton::NormalizesTo(name.clone()),
-                parameters
-                    .iter()
-                    .cloned()
-                    .chain(Some(ty.to_parameter()))
-                    .collect(),
-            ),
-            Predicate::WellFormedAdt(id, parameters) => {
-                (Skeleton::WellFormedAdt(id.clone()), parameters.clone())
-            }
-            Predicate::WellFormedAlias(id, parameters) => {
-                (Skeleton::WellFormedAlias(id.clone()), parameters.clone())
-            }
             Predicate::WellFormedTraitRef(TraitRef {
                 trait_id,
                 parameters,
@@ -160,12 +107,6 @@ impl TraitRef {
     }
 }
 
-impl AdtId {
-    pub fn well_formed(&self, parameters: impl Upcast<Vec<Parameter>>) -> Predicate {
-        Predicate::WellFormedAdt(self.clone(), parameters.upcast())
-    }
-}
-
 /// Relations are built-in goals which are implemented in custom Rust logic.
 #[term]
 pub enum Relation {

crates/formality-types/src/grammar/wc.rs

@@ -10,7 +10,7 @@ use crate::{
     set,
 };
 
-use super::{Binder, BoundVar, Predicate, Relation, TraitRef};
+use super::{Binder, BoundVar, Parameter, Predicate, Relation, TraitRef, Ty};
 
 #[term($set)]
 pub struct Wcs {

tests/basic--hello_world.rs

@@ -1,5 +1,4 @@
 #![allow(non_snake_case)]
-#![cfg(FIXME)]
 
 use formality::test_program_ok;
 
@@ -29,10 +28,7 @@ fn test_broken() {
         Err(
             Error {
                 context: "check_trait(Foo)",
-                source: Error {
-                    context: "prove_where_clause_well_formed([Bar(!tyU(1)_1, !tyU(1)_0)] => Bar(!tyU(1)_1, !tyU(1)_0)",
-                    source: "could not prove `well_formed_trait_ref(Bar(!tyU(1)_1, !tyU(1)_0))` given `[\n    Bar(!tyU(1)_1, !tyU(1)_0),\n]`",
-                },
+                source: "failed to prove {@ WellFormedTraitRef(Bar(!ty_2, !ty_1))} given [!ty_2 : Bar < !ty_1 >], got {}",
             },
         )
     "#]].assert_debug_eq(&test_program_ok(PROGRAM_BROKEN));