Add new exhaustive covering predicate

& Add additional tests

Author: JulianKnodt

crates/formality-check/src/fns.rs

@@ -3,9 +3,7 @@ use formality_rust::{
     grammar::{Fn, FnBoundData},
     prove::ToWcs,
 };
-use formality_types::{
-    grammar::{Fallible, Wcs},
-};
+use formality_types::grammar::{Fallible, Wcs};
 
 use crate::Check;
 

crates/formality-prove/src/db.rs

@@ -0,0 +1 @@
+

crates/formality-prove/src/prove.rs

@@ -1,3 +1,4 @@
+mod combinators;
 mod constraints;
 mod env;
 mod is_local;
@@ -9,7 +10,6 @@ mod prove_via;
 mod prove_wc;
 mod prove_wc_list;
 mod prove_wf;
-mod combinators;
 
 pub use constraints::Constraints;
 use formality_types::{cast::Upcast, collections::Set, grammar::Wcs, set, visit::Visit};

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

@@ -5,9 +5,7 @@ use formality_types::{
 
 use crate::{
     decls::Decls,
-    prove::{
-        constraints::Constraints, env::Env, prove, prove_after::prove_after, 
-    },
+    prove::{constraints::Constraints, env::Env, prove, prove_after::prove_after},
 };
 
 judgment_fn! {

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

@@ -1,10 +1,12 @@
 use formality_types::{
-    grammar::{Predicate, Relation, Wc, WcData, Wcs},
+    cast::Upcasted,
+    grammar::{Const, ExhaustiveState, Predicate, Relation, Scalar, Ty, Wc, WcData, Wcs},
     judgment_fn,
 };
 
 use crate::{
     decls::Decls,
+    derive_links::Parameter,
     prove::{
         env::Env,
         is_local::{is_local_trait_ref, may_be_remote},
@@ -18,6 +20,23 @@ use crate::{
 
 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(
         decls: Decls,
@@ -48,6 +67,50 @@ judgment_fn! {
             (prove_wc(decls, env, assumptions, WcData::PR(goal)) => c)
         )
 
+        (
+            (decls.impl_decls(&trait_ref.trait_id) => i)
+            (let (env, subst) = env.existential_substitution(&i.binder))
+            (let i = i.binder.instantiate_with(&subst).unwrap())
+            (let co_assumptions = (&assumptions, &trait_ref))
+            (prove(&decls, env, &co_assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c)
+            (let t = decls.trait_decl(&i.trait_ref.trait_id).binder.instantiate_with(&i.trait_ref.parameters).unwrap())
+            (prove_after(&decls, c, &co_assumptions, &i.where_clause) => c)
+            (prove_after(&decls, c, &assumptions, &t.where_clause) => c)
+            ----------------------------- ("positive impl")
+            (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
+        )
+
+        (
+            (let mut covering_consts = vec![ExhaustiveState::ExactMatch; trait_ref.parameters.len()])
+            (let ass = &assumptions)
+            (let d = &decls)
+            (d.impl_decls(&trait_ref.trait_id).flat_map(|i| {
+
+              let (env, subst) = env.clone().existential_substitution(&i.binder);
+              let i = i.binder.instantiate_with(&subst).unwrap();
+              let co_assumptions = (ass, &trait_ref);
+              let cs = prove(
+                &decls, env, &co_assumptions,
+                Wcs::eq_or_cover(
+                  &i.trait_ref.parameters, &trait_ref.parameters, &mut covering_consts
+                )
+              ).into_iter().collect::<Vec<_>>();
+              let cs = cs.into_iter().flat_map(move |c| {
+                prove_after(d, c, &co_assumptions, &i.where_clause)
+                  .into_iter()
+              }).into_iter().collect::<Vec<_>>();
+              let cs :Vec<Constraints> = cs.into_iter().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, ass, &t.where_clause).into_iter()
+               }).collect::<Vec<_>>();
+               cs
+            }).collect::<Vec<_>>().into_iter() => c)
+            (prove_after(d, c, ass, is_covering(&covering_consts, &trait_ref.parameters)) => _c)
+            ----------------------------- ("exhaustive positive impl")
+            (prove_wc(_d, env, _ass, Predicate::IsImplemented(trait_ref)) => Constraints::none(env.clone()))
+        )
+
         (
             (decls.impl_decls(&trait_ref.trait_id) => i)
             (let (env, subst) = env.existential_substitution(&i.binder))
@@ -108,6 +171,24 @@ 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.iter()
+              .enumerate()
+              .flat_map(|(i,v)|
+                prove_after(
+                  &decls, &c, &assumptions,
+                  Relation::eq(Const::valtree(Scalar::new(i as u128), Ty::bool()), v)
+                )
+            ).collect::<Vec<_>>().into_iter() => c)
+            ----------------------------- ("exhausttive 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

@@ -31,6 +31,9 @@ pub enum Predicate {
 
     #[grammar(@ConstHasType($v0, $v1))]
     ConstHasType(Const, Ty),
+
+    #[grammar(@CoveringSet($v0, $v1))]
+    Covers(Vec<Const>, Const),
 }
 
 /// A coinductive predicate is one that can be proven via a cycle.
@@ -88,6 +91,7 @@ pub enum Skeleton {
     Equals,
     Sub,
     Outlives,
+    Covered,
 }
 
 impl Predicate {
@@ -125,6 +129,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

@@ -10,13 +10,19 @@ use crate::{
     set,
 };
 
-use super::{Binder, BoundVar, Parameter, Predicate, Relation, TraitRef};
+use super::{Binder, BoundVar, Const, Parameter, Predicate, Relation, TraitRef};
 
 #[term($set)]
 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()
@@ -33,6 +39,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 Vec<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::eq(a, b))
+                }
+            })
+            .upcasted()
+            .collect()
+    }
 }
 
 impl<'w> IntoIterator for &'w Wcs {

crates/formality-types/src/judgment/test_filtered.rs

@@ -4,7 +4,7 @@ use std::sync::Arc;
 
 use formality_macros::{term, test};
 
-use crate::{judgment_fn};
+use crate::judgment_fn;
 
 #[term($edges)]
 struct Graph {

crates/formality-types/src/matcher.rs

@@ -0,0 +1 @@
+