Add new exhaustive covering predicate

& Add additional tests

Author: JulianKnodt

crates/formality-core/src/judgment/proven_set.rs

@@ -99,6 +99,17 @@ impl<T: Ord + Debug> ProvenSet<T> {
         }
     }
 
+    /// Convert to a non-empty set of proven results (if ok) or an error (otherwise).
+    pub fn into_iter(self) -> Box<dyn Iterator<Item = T>>
+    where
+        T: 'static,
+    {
+        match self.data {
+            Data::Failure(_) => Box::new(std::iter::empty()),
+            Data::Success(s) => Box::new(s.into_iter()),
+        }
+    }
+
     /// For each item `t` that was proven,
     /// invoke `op(t)` to yield a new set of proven results
     /// and then flatten those into a new proven set.

crates/formality-prove/src/prove.rs

@@ -49,7 +49,11 @@ pub fn prove(
         return ProvenSet::singleton(Constraints::none(env).ambiguous());
     }
 
-    assert!(env.encloses(term_in));
+    assert!(
+        env.encloses(term_in),
+        "{env:?} does not enclose {term_in:?}: {:?}",
+        term_in.free_variables()
+    );
 
     let result_set = prove_wc_list(decls, &env, assumptions, goal);
 

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

@@ -1,20 +1,35 @@
-use formality_core::judgment_fn;
-use formality_types::grammar::{Predicate, Relation, Wc, WcData, Wcs};
-
-use crate::{
-    decls::Decls,
-    prove::{
-        env::Env,
-        is_local::{is_local_trait_ref, may_be_remote},
-        prove,
-        prove_after::prove_after,
-        prove_eq::prove_eq,
-        prove_via::prove_via,
-        prove_wf::prove_wf,
-    },
+use crate::prove;
+use crate::prove::is_local::is_local_trait_ref;
+use crate::prove::is_local::may_be_remote;
+use crate::prove::prove_after::prove_after;
+use crate::prove::prove_eq::prove_eq;
+use crate::prove::prove_via::prove_via;
+use crate::prove::prove_wf::prove_wf;
+use crate::Decls;
+use crate::Env;
+
+use crate::Constraints;
+use formality_core::{judgment_fn, ProvenSet, Upcasted};
+use formality_types::grammar::{
+    Const, ExhaustiveState, Parameter, Predicate, Relation, Scalar, Ty, Wc, WcData, Wcs,
 };
 
-use super::constraints::Constraints;
+pub fn is_covering(vals: &[ExhaustiveState], params: &[Parameter]) -> Wcs {
+    assert_eq!(vals.len(), params.len());
+    vals.iter()
+        .zip(params.iter())
+        .filter_map(|(a, b)| match a {
+            ExhaustiveState::ExactMatch => None,
+            ExhaustiveState::ConstCover(cs) => {
+                let Parameter::Const(c) = b else {
+                    todo!();
+                };
+                Some(Predicate::Covers(cs.clone(), c.clone()))
+            }
+        })
+        .upcasted()
+        .collect()
+}
 
 judgment_fn! {
     pub fn prove_wc(
@@ -46,6 +61,34 @@ judgment_fn! {
             (prove_wc(decls, env, assumptions, WcData::PR(goal)) => c)
         )
 
+        (
+            (let mut covering_consts = vec![ExhaustiveState::ExactMatch; trait_ref.parameters.len()])
+            (let asmp = &assumptions)
+            (let d = &decls)
+            (d.impl_decls(&trait_ref.trait_id).flat_map(|i| {
+
+              let (env, subst) = env.clone().universal_substitution(&i.binder);
+              let i = i.binder.instantiate_with(&subst).unwrap();
+              let co_assumptions = (asmp, &trait_ref);
+              let cs = prove(
+                &decls, env, &co_assumptions,
+                Wcs::eq_or_cover(
+                  &i.trait_ref.parameters, &trait_ref.parameters, &mut covering_consts
+                )
+              );
+              let cs = cs.flat_map(move |c| prove_after(d, c, &co_assumptions, &i.where_clause));
+              let cs = cs.flat_map(move |c| {
+                  let t = d.trait_decl(&i.trait_ref.trait_id)
+                    .binder.instantiate_with(&i.trait_ref.parameters).unwrap();
+                  prove_after(d, c, asmp, &t.where_clause)
+               });
+               cs.into_iter()
+            }).into_iter().collect::<ProvenSet<_>>() => c)
+            (prove_after(d, c, asmp, is_covering(&covering_consts, &trait_ref.parameters)) => c)
+            ----------------------------- ("exhaustive positive impl")
+            (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c)
+        )
+
         (
             (decls.impl_decls(&trait_ref.trait_id) => i)!
             (let (env, subst) = env.existential_substitution(&i.binder))
@@ -112,6 +155,23 @@ judgment_fn! {
             (prove_wc(decls, env, assumptions, Predicate::IsLocal(trait_ref)) => c)
         )
 
+        (
+            (let () = vals.sort_unstable())
+            (prove(&decls, env, &assumptions, Predicate::ConstHasType(var, Ty::bool())) => c)
+            (vals.iter().cloned() => v)
+            (prove_after(&decls, &c, &assumptions, Predicate::ConstHasType(v, Ty::bool())) => c)
+            (if vals.len() == 2)
+            (vals.clone().into_iter().enumerate().flat_map(|(i, v)| {
+                prove_after(
+                  &decls, &c, &assumptions,
+                  Relation::Equals(Parameter::Const(Const::valtree(Scalar::new(i as u128),
+                  Ty::bool())), Parameter::Const(v))
+                ).into_iter()
+            }).collect::<ProvenSet<_>>() => c)
+            ----------------------------- ("exhaustive bool values cover variable")
+            (prove_wc(decls, env, assumptions, Predicate::Covers(mut vals, var)) => c)
+        )
+
 
         (
             (prove_wf(decls, env, assumptions, p) => c)

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

@@ -26,6 +26,10 @@ impl Const {
         Self::new(ConstData::Value(vt.upcast(), ty.upcast()))
     }
 
+    pub fn is_variable(&self) -> bool {
+        matches!(self.data(), ConstData::Variable(_))
+    }
+
     pub fn as_variable(&self) -> Option<Variable> {
         match self.data() {
             ConstData::Value(_, _) => None,

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

@@ -36,6 +36,9 @@ pub enum Predicate {
 
     #[grammar(@ConstHasType($v0, $v1))]
     ConstHasType(Const, Ty),
+
+    #[grammar(@Covers($v0, $v1))]
+    Covers(Vec<Const>, Const),
 }
 
 /// A coinductive predicate is one that can be proven via a cycle.
@@ -94,6 +97,7 @@ pub enum Skeleton {
     Equals,
     Sub,
     Outlives,
+    Covered,
 }
 
 impl Predicate {
@@ -136,6 +140,15 @@ impl Predicate {
                 Skeleton::ConstHasType,
                 vec![ct.clone().upcast(), ty.clone().upcast()],
             ),
+            Predicate::Covers(consts, c) => (
+                Skeleton::Covered,
+                consts
+                    .iter()
+                    .cloned()
+                    .chain(std::iter::once(c.clone()))
+                    .map(|c| Parameter::Const(c))
+                    .collect::<Vec<_>>(),
+            ),
         }
     }
 }

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

@@ -6,14 +6,20 @@ use formality_core::{
 
 use crate::grammar::PR;
 
-use super::{Binder, BoundVar, Parameter, Predicate, Relation, TraitRef};
+use super::{Binder, BoundVar, Const, Parameter, Predicate, Relation, TraitRef};
 
 #[term($set)]
 #[derive(Default)]
 pub struct Wcs {
     set: Set<Wc>,
 }
 
+#[derive(Debug, Clone, PartialEq)]
+pub enum ExhaustiveState {
+    ExactMatch,
+    ConstCover(Vec<Const>),
+}
+
 impl Wcs {
     pub fn t() -> Self {
         set![].upcast()
@@ -30,6 +36,37 @@ impl Wcs {
             .upcasted()
             .collect()
     }
+    /// Goal(s) to prove `a` and `b` are equal (they must have equal length)
+    pub fn eq_or_cover(
+        candidate: impl Upcast<Vec<Parameter>>,
+        trait_impl: impl Upcast<Vec<Parameter>>,
+        covering_items: &mut [ExhaustiveState],
+    ) -> Wcs {
+        let a: Vec<Parameter> = candidate.upcast();
+        let b: Vec<Parameter> = trait_impl.upcast();
+        assert_eq!(a.len(), b.len());
+        a.into_iter()
+            .zip(b)
+            .enumerate()
+            .filter_map(|(i, (a, b))| match (&a, &b) {
+                (Parameter::Const(ct), Parameter::Const(param)) if param.is_variable() => {
+                    if covering_items[i] == ExhaustiveState::ExactMatch {
+                        covering_items[i] = ExhaustiveState::ConstCover(vec![]);
+                    }
+                    let ExhaustiveState::ConstCover(ref mut c) = &mut covering_items[i] else {
+                        panic!();
+                    };
+                    c.push(ct.clone());
+                    None
+                }
+                _ => {
+                    assert!(matches!(covering_items[i], ExhaustiveState::ExactMatch));
+                    Some(Relation::equals(a, b))
+                }
+            })
+            .upcasted()
+            .collect()
+    }
 }
 
 impl<'w> IntoIterator for &'w Wcs {

tests/coherence_overlap.rs

@@ -47,13 +47,11 @@ fn test_overlap_normalize_alias_to_LocalType() {
     // ...but it's an error if LocalType implements Iterator (figuring *this* out also
     // requires normalizing).
 
-    test_program_ok(&gen_program(
-        "impl Iterator for LocalType {}",
-    )).assert_err(
+    test_program_ok(&gen_program("impl Iterator for LocalType {}")).assert_err(
         expect_test::expect![[r#"
             impls may overlap:
             impl <ty> LocalTrait for ^ty0_0 where ^ty0_0 : Iterator { }
-            impl LocalTrait for <LocalType as Mirror>::T { }"#]]
+            impl LocalTrait for <LocalType as Mirror>::T { }"#]],
     );
 }
 
@@ -103,12 +101,10 @@ fn test_overlap_alias_not_normalizable() {
 
     // ...as long as there is at least one Iterator impl, however, we do flag an error.
 
-    test_program_ok(&gen_program(
-        "impl Iterator for u32 {}",
-    )).assert_err(
-        expect_test::expect![[r#"
+    test_program_ok(&gen_program("impl Iterator for u32 {}")).assert_err(expect_test::expect![[
+        r#"
             impls may overlap:
             impl <ty> LocalTrait for ^ty0_0 where ^ty0_0 : Iterator { }
-            impl <ty> LocalTrait for <^ty0_0 as Mirror>::T where ^ty0_0 : Mirror { }"#]]
-    ); // FIXME
+            impl <ty> LocalTrait for <^ty0_0 as Mirror>::T where ^ty0_0 : Mirror { }"#
+    ]]); // FIXME
 }