diff --git a/crates/formality-check/src/fns.rs b/crates/formality-check/src/fns.rs index b9858ce5..15f2357a 100644 --- a/crates/formality-check/src/fns.rs +++ b/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; diff --git a/crates/formality-prove/src/db.rs b/crates/formality-prove/src/db.rs index e69de29b..8b137891 100644 --- a/crates/formality-prove/src/db.rs +++ b/crates/formality-prove/src/db.rs @@ -0,0 +1 @@ + diff --git a/crates/formality-prove/src/prove.rs b/crates/formality-prove/src/prove.rs index ed9e7a04..1c168353 100644 --- a/crates/formality-prove/src/prove.rs +++ b/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}; diff --git a/crates/formality-prove/src/prove/prove_via.rs b/crates/formality-prove/src/prove/prove_via.rs index 666a68cc..612500d6 100644 --- a/crates/formality-prove/src/prove/prove_via.rs +++ b/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! { diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index 17b364fc..595ef7f7 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/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::>(); + let cs = cs.into_iter().flat_map(move |c| { + prove_after(d, c, &co_assumptions, &i.where_clause) + .into_iter() + }).into_iter().collect::>(); + let cs :Vec = 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::>(); + cs + }).collect::>().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::>().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) diff --git a/crates/formality-types/src/grammar/consts.rs b/crates/formality-types/src/grammar/consts.rs index e032cc1a..c636e333 100644 --- a/crates/formality-types/src/grammar/consts.rs +++ b/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 { match self.data() { ConstData::Value(_, _) => None, diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index e5558fd1..6a356b3c 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/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), } /// 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::>(), + ), } } } diff --git a/crates/formality-types/src/grammar/wc.rs b/crates/formality-types/src/grammar/wc.rs index 37e1741a..20dfd9a5 100644 --- a/crates/formality-types/src/grammar/wc.rs +++ b/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, } +#[derive(Debug, Clone, PartialEq)] +pub enum ExhaustiveState { + ExactMatch, + ConstCover(Vec), +} + 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>, + trait_impl: impl Upcast>, + covering_items: &mut Vec, + ) -> Wcs { + let a: Vec = candidate.upcast(); + let b: Vec = 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 { diff --git a/crates/formality-types/src/judgment/test_filtered.rs b/crates/formality-types/src/judgment/test_filtered.rs index 458c5971..83483a18 100644 --- a/crates/formality-types/src/judgment/test_filtered.rs +++ b/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 { diff --git a/crates/formality-types/src/matcher.rs b/crates/formality-types/src/matcher.rs index e69de29b..8b137891 100644 --- a/crates/formality-types/src/matcher.rs +++ b/crates/formality-types/src/matcher.rs @@ -0,0 +1 @@ + diff --git a/crates/formality-types/src/parse.rs b/crates/formality-types/src/parse.rs index ce0c58ac..a8513966 100644 --- a/crates/formality-types/src/parse.rs +++ b/crates/formality-types/src/parse.rs @@ -115,7 +115,11 @@ impl<'t> ParseError<'t> { /// Offset of this error relative to the starting point `text` pub fn offset(&self, text: &str) -> usize { - assert!(text.ends_with(self.text)); + assert!( + text.ends_with(self.text), + "text={text}, \nself.text={}", + self.text + ); text.len() - self.text.len() } diff --git a/tests/consts.rs b/tests/consts.rs deleted file mode 100644 index c6d324d2..00000000 --- a/tests/consts.rs +++ /dev/null @@ -1,183 +0,0 @@ -use formality::test_program_ok; -use formality_macros::test; - -#[test] -fn test_ok() { - expect_test::expect![[r#" - Ok( - (), - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool] {} - trait Bar where [type_of_const C is u32] {} - - impl Foo for u32 where [type_of_const C is bool] {} - } - ]", - )); -} - -#[test] -fn test_holds() { - expect_test::expect![[r#" - Ok( - (), - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool] {} - - impl<> Foo for u32 where [] {} - } - ]", - )); -} - -#[test] -fn test_mismatch() { - expect_test::expect![[r#" - Err( - Error { - context: "check_trait_impl(impl <> Foo < const 42_(rigid (scalar u32)) > for (rigid (scalar u32)) where [] { })", - source: "failed to prove {Foo((rigid (scalar u32)), const 42_(rigid (scalar u32)))} given {}, got {}", - }, - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool] {} - - impl<> Foo for u32 where [] {} - } - ]", - )); -} - -#[test] -fn test_generic_mismatch() { - expect_test::expect![[r#" - Err( - Error { - context: "check_trait_impl(impl Foo < const ^const0_0 > for (rigid (scalar u32)) where [type_of_const ^const0_0 is (rigid (scalar u32))] { })", - source: "failed to prove {Foo((rigid (scalar u32)), const !const_1)} given {@ ConstHasType(!const_1 , (rigid (scalar u32)))}, got {}", - }, - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool] {} - - impl Foo for u32 where [type_of_const C is u32] {} - } - ]", - )); -} - -#[test] -fn test_trait_with_const() { - expect_test::expect![[r#" - Ok( - (), - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool] {} - - trait Bar where [T: Foo] {} - - impl<> Foo for u32 where [] {} - impl<> Bar for u32 where [] {} - } - ]", - )); -} - -#[test] -fn test_trait_with_generic_const() { - expect_test::expect![[r#" - Ok( - (), - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool] {} - - trait Bar where [T: Foo, type_of_const C is bool] {} - - impl Foo for u32 where [type_of_const C is bool] {} - impl Bar for u32 where [type_of_const C is bool] {} - } - ]", - )); -} - -#[test] -/// This test is the short version of `test_holds`, skipping -/// substituting and directly going to a rigid constant. -fn test_rigid_const_bound() { - expect_test::expect![[r#" - Ok( - (), - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo<> where [type_of_const true is bool] {} - } - ]", - )); -} - -#[test] -/// This test is the short version of `test_generic_mismatch`, skipping -/// substituting and directly going to a wrong constant. -fn test_nonsense_rigid_const_bound() { - expect_test::expect![[r#" - Err( - Error { - context: "check_trait(Foo)", - source: Error { - context: "prove_where_clause_well_formed(type_of_const 0_(rigid (scalar bool)) is (rigid (scalar u32)))", - source: "failed to prove {(rigid (scalar u32)) = (rigid (scalar bool))} given {@ ConstHasType(0_(rigid (scalar bool)) , (rigid (scalar u32)))}, got {}", - }, - }, - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo<> where [type_of_const true is u32] {} - } - ]", - )); -} - -#[test] -/// This test is wrong, but it's also not something rustc ever generates. -/// Types on const generics only get exactly one `type_of_const` bound. -fn test_multiple_type_of_const() { - expect_test::expect![[r#" - Ok( - (), - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool, type_of_const C is u32] {} - } - ]", - )); -} diff --git "a/tests/ui/consts/double.\360\237\224\254" "b/tests/ui/consts/double.\360\237\224\254" new file mode 100644 index 00000000..c97b7f9d --- /dev/null +++ "b/tests/ui/consts/double.\360\237\224\254" @@ -0,0 +1,8 @@ +//@check-pass +[ + crate Foo { + trait Foo where [type_of_const C is bool, type_of_const D is bool] {} + + impl Foo for u32 where [type_of_const C is bool] {} + } +] diff --git "a/tests/ui/consts/exhaustive.\360\237\224\254" "b/tests/ui/consts/exhaustive.\360\237\224\254" new file mode 100644 index 00000000..bd8fb5b1 --- /dev/null +++ "b/tests/ui/consts/exhaustive.\360\237\224\254" @@ -0,0 +1,12 @@ +//@check-pass +[ + crate Foo { + trait Foo where [type_of_const C is bool] {} + + trait Bar where [T: Foo, type_of_const C is bool] {} + + impl<> Foo for u32 where [] {} + impl<> Foo for u32 where [] {} + impl Bar for u32 where [type_of_const C is bool] {} + } +] diff --git a/tests/ui/consts/not_covering.stderr b/tests/ui/consts/not_covering.stderr new file mode 100644 index 00000000..bd1406b7 --- /dev/null +++ b/tests/ui/consts/not_covering.stderr @@ -0,0 +1,4 @@ +Error: check_trait_impl(impl Bar < (rigid (scalar u32)), const ^const0_0 > for (rigid (scalar u32)) where [type_of_const ^const0_0 is (rigid (scalar bool))] { }) + +Caused by: + failed to prove {Bar((rigid (scalar u32)), (rigid (scalar u32)), const !const_1)} given {@ ConstHasType(!const_1 , (rigid (scalar bool)))}, got {} diff --git "a/tests/ui/consts/not_covering.\360\237\224\254" "b/tests/ui/consts/not_covering.\360\237\224\254" new file mode 100644 index 00000000..acbe2b75 --- /dev/null +++ "b/tests/ui/consts/not_covering.\360\237\224\254" @@ -0,0 +1,10 @@ +[ + crate Foo { + trait Foo where [type_of_const C is bool] {} + + trait Bar where [T: Foo, type_of_const C is bool] {} + + impl<> Foo for u32 where [] {} + impl Bar for u32 where [type_of_const C is bool] {} + } +] diff --git "a/tests/ui/consts/trait_with_const.\360\237\224\254" "b/tests/ui/consts/trait_with_const.\360\237\224\254" new file mode 100644 index 00000000..c74576e9 --- /dev/null +++ "b/tests/ui/consts/trait_with_const.\360\237\224\254" @@ -0,0 +1,11 @@ +//@check-pass +[ + crate Foo { + trait Foo where [type_of_const C is bool] {} + + trait Bar where [T: Foo] {} + + impl<> Foo for u32 where [] {} + impl<> Bar for u32 where [] {} + } +] diff --git "a/tests/ui/consts/trait_with_generic_const.\360\237\224\254" "b/tests/ui/consts/trait_with_generic_const.\360\237\224\254" new file mode 100644 index 00000000..680f0ae1 --- /dev/null +++ "b/tests/ui/consts/trait_with_generic_const.\360\237\224\254" @@ -0,0 +1,11 @@ +//@check-pass +[ + crate Foo { + trait Foo where [type_of_const C is bool] {} + + trait Bar where [T: Foo, type_of_const C is bool] {} + + impl Foo for u32 where [type_of_const C is bool] {} + impl Bar for u32 where [type_of_const C is bool] {} + } +]