From 1bcdbdf2406912c615080db303f5994a7980159a Mon Sep 17 00:00:00 2001 From: tiif Date: Wed, 5 Feb 2025 00:46:53 +0800 Subject: [PATCH 01/65] Currently passed normal trait --- tests/const_trait.rs | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 tests/const_trait.rs diff --git a/tests/const_trait.rs b/tests/const_trait.rs new file mode 100644 index 00000000..13e76598 --- /dev/null +++ b/tests/const_trait.rs @@ -0,0 +1,25 @@ +#![allow(non_snake_case)] // we embed type names into the names for our test functions + +use a_mir_formality::test_program_ok; +use formality_core::test_util::ResultTestExt; +use formality_macros::test; + +#[test] +fn test_const() { + let gen_program = |addl: &str| { + const BASE_PROGRAM: &str = "[ + crate core { + trait Default { + } + + impl Default for () { + } + } + + ]"; + + BASE_PROGRAM.replace("ADDITIONAL", addl) + }; + + test_program_ok(&gen_program("")).assert_ok(expect_test::expect!["()"]); +} From 699d2726811401c2aa4dc5edd79a54fd16faab40 Mon Sep 17 00:00:00 2001 From: tiif Date: Wed, 5 Feb 2025 23:45:13 +0800 Subject: [PATCH 02/65] Support const trait declaration --- crates/formality-check/src/traits.rs | 1 + crates/formality-rust/src/grammar.rs | 13 ++++++++++++- crates/formality-rust/src/prove.rs | 3 ++- 3 files changed, 15 insertions(+), 2 deletions(-) diff --git a/crates/formality-check/src/traits.rs b/crates/formality-check/src/traits.rs index d319f652..a8ab7144 100644 --- a/crates/formality-check/src/traits.rs +++ b/crates/formality-check/src/traits.rs @@ -14,6 +14,7 @@ impl super::Check<'_> { safety: _, id: _, binder, + .. } = t; let mut env = Env::default(); diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 5efda3da..33b490a1 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -174,9 +174,20 @@ pub struct Variant { pub fields: Vec, } -#[term($?safety trait $id $binder)] +#[term] +#[derive(Default)] +pub enum Constness { + #[default] + NotConst, + MaybeConst, + Const, +} + + +#[term($?safety $?constness trait $id $binder)] pub struct Trait { pub safety: Safety, + pub constness: Constness, pub id: TraitId, pub binder: TraitBinder, } diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index e62cbd4d..15453a66 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -80,7 +80,7 @@ impl Crate { self.items .iter() .flat_map(|item| match item { - CrateItem::Trait(Trait { id, binder, safety }) => { + CrateItem::Trait(Trait { id, binder, safety, ..}) => { let ( vars, TraitBoundData { @@ -232,6 +232,7 @@ impl Crate { safety: _, id: trait_id, binder, + .. }) => { let ( trait_vars, From 3a2f82f971e66a4ba45f96db12f8bba7aa378392 Mon Sep 17 00:00:00 2001 From: tiif Date: Wed, 5 Feb 2025 23:55:42 +0800 Subject: [PATCH 03/65] Support impl const trait in parser --- crates/formality-check/src/impls.rs | 1 + crates/formality-rust/src/grammar.rs | 3 ++- crates/formality-rust/src/prove.rs | 2 ++ tests/const_trait.rs | 4 ++-- 4 files changed, 7 insertions(+), 3 deletions(-) diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index aa0cb294..24fdc536 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -24,6 +24,7 @@ impl super::Check<'_> { let mut env = Env::default(); let TraitImplBoundData { + constness: _, trait_id, self_ty, trait_parameters, diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 33b490a1..c3331f84 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -279,8 +279,9 @@ impl TraitImpl { } } -#[term($trait_id $ for $self_ty $:where $,where_clauses { $*impl_items })] +#[term($?constness $trait_id $ for $self_ty $:where $,where_clauses { $*impl_items })] pub struct TraitImplBoundData { + pub constness: Constness, pub trait_id: TraitId, pub self_ty: Ty, pub trait_parameters: Vec, diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index 15453a66..d9863e5f 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -115,6 +115,7 @@ impl Crate { let ( vars, TraitImplBoundData { + constness: _, trait_id, self_ty, trait_parameters, @@ -176,6 +177,7 @@ impl Crate { let ( impl_vars, TraitImplBoundData { + constness: _, trait_id, self_ty, trait_parameters, diff --git a/tests/const_trait.rs b/tests/const_trait.rs index 13e76598..f0297096 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -9,10 +9,10 @@ fn test_const() { let gen_program = |addl: &str| { const BASE_PROGRAM: &str = "[ crate core { - trait Default { + const trait Default { } - impl Default for () { + impl const Default for () { } } From 37c56c2eb83db87f7443f0617d36552b1ae70e72 Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 6 Feb 2025 00:11:15 +0800 Subject: [PATCH 04/65] Failed attempt: requires a lot of other impl --- crates/formality-types/src/grammar/formulas.rs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index d9522c21..edc4f7de 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -190,9 +190,19 @@ impl Relation { } } } +// TODO: this is also defined in formality-rust, haven't found a nice place to put it... +// why this requires so many impl?? +#[derive(Default, Clone, PartialEq, Eq, Ord, Hash, Debug, PartialOrd)] +pub enum Constness { + #[default] + NotConst, + MaybeConst, + Const, +} -#[term($trait_id ( $,parameters ))] +#[term($?constness $trait_id ( $,parameters ))] pub struct TraitRef { + pub constness: Constness, pub trait_id: TraitId, pub parameters: Parameters, } From c83d3fbc12ccd1da941f0ff4ce5cd5bf4e5d6ec6 Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 6 Feb 2025 23:00:26 +0800 Subject: [PATCH 05/65] Get constness in TraitRef somewhat work --- crates/formality-check/src/impls.rs | 9 +++++---- crates/formality-prove/src/decls.rs | 7 +++++-- crates/formality-rust/src/grammar.rs | 19 +++++-------------- crates/formality-rust/src/prove.rs | 13 +++++++------ .../formality-types/src/grammar/formulas.rs | 14 ++++++++++---- 5 files changed, 32 insertions(+), 30 deletions(-) diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index 24fdc536..06860a46 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -12,7 +12,7 @@ use formality_rust::{ prove::ToWcs, }; use formality_types::{ - grammar::{Binder, Fallible, Relation, Substitution, Wcs}, + grammar::{Binder, Constness, Fallible, Relation, Substitution, Wcs}, rust::Term, }; @@ -24,7 +24,7 @@ impl super::Check<'_> { let mut env = Env::default(); let TraitImplBoundData { - constness: _, + constness, trait_id, self_ty, trait_parameters, @@ -32,7 +32,7 @@ impl super::Check<'_> { impl_items, } = env.instantiate_universally(binder); - let trait_ref = trait_id.with(self_ty, trait_parameters); + let trait_ref = trait_id.with(&constness, self_ty, trait_parameters); self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?; @@ -61,6 +61,7 @@ impl super::Check<'_> { let mut env = Env::default(); + // TODO: add constness to NegTraitImpl if necessary let NegTraitImplBoundData { trait_id, self_ty, @@ -68,7 +69,7 @@ impl super::Check<'_> { where_clauses, } = env.instantiate_universally(binder); - let trait_ref = trait_id.with(self_ty, trait_parameters); + let trait_ref = trait_id.with(&Constness::NotConst, self_ty, trait_parameters); // Negative impls are always safe (rustc E0198) regardless of the trait's safety. if *safety == Safety::Unsafe { diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 00bd5222..718d210f 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -4,6 +4,7 @@ use formality_types::grammar::{ AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, Wcs, }; +use formality_types::grammar::Constness; #[term] pub struct Decls { @@ -140,6 +141,7 @@ pub struct NegImplDeclBoundData { pub where_clause: Wcs, } + /// Mark a trait or trait impl as `unsafe`. #[term] #[derive(Default)] @@ -153,8 +155,9 @@ pub enum Safety { /// It doesn't capture the trait items, which will be transformed into other sorts of rules. /// /// In Rust syntax, it covers the `trait Foo: Bar` part of the declaration, but not what appears in the `{...}`. -#[term($?safety trait $id $binder)] +#[term($?constness $?safety trait $id $binder)] pub struct TraitDecl { + pub constness: Constness, /// The name of the trait pub id: TraitId, @@ -197,7 +200,7 @@ impl TraitDecl { binder: Binder::new( &variables, TraitInvariantBoundData { - trait_ref: TraitRef::new(&self.id, &variables), + trait_ref: TraitRef::new(Constness::Const, &self.id, &variables), where_clause, }, ), diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index c3331f84..f8c54fb9 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -2,6 +2,7 @@ use std::sync::Arc; use formality_core::{term, Upcast}; use formality_prove::Safety; +use formality_types::grammar::Constness; use formality_types::{ grammar::{ AdtId, AliasTy, AssociatedItemId, Binder, Const, ConstData, CrateId, Fallible, FieldId, @@ -174,16 +175,6 @@ pub struct Variant { pub fields: Vec, } -#[term] -#[derive(Default)] -pub enum Constness { - #[default] - NotConst, - MaybeConst, - Const, -} - - #[term($?safety $?constness trait $id $binder)] pub struct Trait { pub safety: Safety, @@ -291,7 +282,7 @@ pub struct TraitImplBoundData { impl TraitImplBoundData { pub fn trait_ref(&self) -> TraitRef { - self.trait_id.with(&self.self_ty, &self.trait_parameters) + self.trait_id.with(&self.constness, &self.self_ty, &self.trait_parameters) } } @@ -311,7 +302,7 @@ pub struct NegTraitImplBoundData { impl NegTraitImplBoundData { pub fn trait_ref(&self) -> TraitRef { - self.trait_id.with(&self.self_ty, &self.trait_parameters) + self.trait_id.with(&Constness::NotConst, &self.self_ty, &self.trait_parameters) } } @@ -349,7 +340,7 @@ impl WhereClause { match self.data() { WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => Some( trait_id - .with(self_ty, parameters) + .with(&Constness::NotConst, self_ty, parameters) .not_implemented() .upcast(), ), @@ -367,7 +358,7 @@ impl WhereClause { pub fn well_formed(&self) -> Wcs { match self.data() { WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => { - trait_id.with(self_ty, parameters).well_formed().upcast() + trait_id.with(&Constness::NotConst, self_ty, parameters).well_formed().upcast() } WhereClauseData::AliasEq(alias_ty, ty) => { let alias_param: Parameter = alias_ty.upcast(); diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index d9863e5f..2d0dcd25 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -7,7 +7,7 @@ use crate::grammar::{ use formality_core::{seq, Set, To, Upcast, Upcasted}; use formality_prove as prove; use formality_types::grammar::{ - AdtId, AliasTy, Binder, BoundVar, ParameterKind, Predicate, Relation, TraitId, Ty, Wc, Wcs, + AdtId, AliasTy, Binder, BoundVar, Constness, ParameterKind, Predicate, Relation, TraitId, Ty, Wc, Wcs, }; impl Program { @@ -80,7 +80,7 @@ impl Crate { self.items .iter() .flat_map(|item| match item { - CrateItem::Trait(Trait { id, binder, safety, ..}) => { + CrateItem::Trait(Trait { id, binder, safety, constness}) => { let ( vars, TraitBoundData { @@ -89,6 +89,7 @@ impl Crate { }, ) = binder.open(); Some(prove::TraitDecl { + constness: constness.clone(), safety: safety.clone(), id: id.clone(), binder: Binder::new( @@ -128,7 +129,7 @@ impl Crate { binder: Binder::new( vars, prove::ImplDeclBoundData { - trait_ref: trait_id.with(self_ty, trait_parameters), + trait_ref: trait_id.with(&Constness::NotConst, self_ty, trait_parameters), where_clause: where_clauses.to_wcs(), }, ), @@ -158,7 +159,7 @@ impl Crate { binder: Binder::new( vars, prove::NegImplDeclBoundData { - trait_ref: trait_id.with(self_ty, trait_parameters), + trait_ref: trait_id.with(&Constness::NotConst, self_ty, trait_parameters), where_clause: where_clauses.to_wcs(), }, ), @@ -413,7 +414,7 @@ impl ToWcs for WhereClause { fn to_wcs(&self) -> Wcs { match self.data() { WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => { - trait_id.with(self_ty, parameters).upcast() + trait_id.with(&Constness::NotConst, self_ty, parameters).upcast() } WhereClauseData::AliasEq(alias_ty, ty) => { Predicate::AliasEq(alias_ty.clone(), ty.clone()).upcast() @@ -439,7 +440,7 @@ impl WhereBound { match self.data() { WhereBoundData::IsImplemented(trait_id, parameters) => { - trait_id.with(self_ty, parameters).upcast() + trait_id.with(&Constness::NotConst, self_ty, parameters).upcast() } WhereBoundData::Outlives(lt) => Relation::outlives(self_ty, lt).upcast(), WhereBoundData::ForAll(binder) => { diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index edc4f7de..c9d2be59 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -110,6 +110,7 @@ impl Predicate { pub fn debone(&self) -> (Skeleton, Vec) { match self { Predicate::IsImplemented(TraitRef { + constness: _, trait_id, parameters, }) => ( @@ -117,6 +118,7 @@ impl Predicate { parameters.clone(), ), Predicate::NotImplemented(TraitRef { + constness: _, trait_id, parameters, }) => ( @@ -129,6 +131,7 @@ impl Predicate { (Skeleton::AliasEq(name.clone()), params) } Predicate::WellFormedTraitRef(TraitRef { + constness: _, trait_id, parameters, }) => ( @@ -136,6 +139,7 @@ impl Predicate { parameters.clone(), ), Predicate::IsLocal(TraitRef { + constness: _, trait_id, parameters, }) => (Skeleton::IsLocal(trait_id.clone()), parameters.clone()), @@ -190,9 +194,9 @@ impl Relation { } } } -// TODO: this is also defined in formality-rust, haven't found a nice place to put it... -// why this requires so many impl?? -#[derive(Default, Clone, PartialEq, Eq, Ord, Hash, Debug, PartialOrd)] + +#[term] +#[derive(Default)] pub enum Constness { #[default] NotConst, @@ -200,6 +204,7 @@ pub enum Constness { Const, } + #[term($?constness $trait_id ( $,parameters ))] pub struct TraitRef { pub constness: Constness, @@ -210,12 +215,13 @@ pub struct TraitRef { impl TraitId { pub fn with( &self, + constness: &Constness, self_ty: impl Upcast, parameters: impl Upcast>, ) -> TraitRef { let self_ty: Ty = self_ty.upcast(); let parameters: Vec = parameters.upcast(); - TraitRef::new(self, (Some(self_ty), parameters)) + TraitRef::new(constness, self, (Some(self_ty), parameters)) } } From f7b3f479b6f5652e2f7cb770fc1a36bd84f819cb Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 7 Feb 2025 22:23:33 +0800 Subject: [PATCH 06/65] Use ~const for maybe-const --- crates/formality-types/src/grammar/formulas.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index c9d2be59..6f91b106 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -200,6 +200,7 @@ impl Relation { pub enum Constness { #[default] NotConst, + #[grammar(~const)] MaybeConst, Const, } From 9521e7a27928179c5b1cd9a2d96fbc9aa313fc7a Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 7 Feb 2025 22:32:40 +0800 Subject: [PATCH 07/65] Add constness somewhere --- .../formality-prove/src/test/eq_partial_eq.rs | 12 ++++----- crates/formality-prove/src/test/magic_copy.rs | 26 +++++++++---------- crates/formality-rust/src/test.rs | 2 ++ 3 files changed, 21 insertions(+), 19 deletions(-) diff --git a/crates/formality-prove/src/test/eq_partial_eq.rs b/crates/formality-prove/src/test/eq_partial_eq.rs index 7216d505..6dcebde6 100644 --- a/crates/formality-prove/src/test/eq_partial_eq.rs +++ b/crates/formality-prove/src/test/eq_partial_eq.rs @@ -77,15 +77,15 @@ fn universals_not_eq() { the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because judgment had no applicable rules: `prove_via { goal: PartialEq(!ty_2), via: Eq(!ty_1), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness } }` the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, !ty_2, ?ty_3], bias: Soundness }, known_true: true, substitution: {?ty_3 => !ty_2} }, goal: {Eq(?ty_3)}, assumptions: {Eq(!ty_1)} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, !ty_2, ?ty_3], bias: Soundness }, known_true: true, substitution: {?ty_3 => !ty_2} }, goal: {const Eq(?ty_3)}, assumptions: {Eq(!ty_1)} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {const Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {const Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Eq(!ty_1), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: const Eq(!ty_1), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_via { goal: Eq(!ty_1), via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_via { goal: const Eq(!ty_1), via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): the rule "predicate-congruence-axiom" failed at step #3 (src/file.rs:LL:CC) because judgment `prove { goal: {!ty_0 = !ty_1}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because @@ -109,5 +109,5 @@ fn universals_not_eq() { the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because cyclic proof attempt: `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], bias: Soundness } }`"#]]); + judgment had no applicable rules: `prove_via { goal: const Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], bias: Soundness } }`"#]]); } diff --git a/crates/formality-prove/src/test/magic_copy.rs b/crates/formality-prove/src/test/magic_copy.rs index 4ab17a3c..6d55d7c1 100644 --- a/crates/formality-prove/src/test/magic_copy.rs +++ b/crates/formality-prove/src/test/magic_copy.rs @@ -63,13 +63,13 @@ fn all_t_not_magic() { the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {const Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {const Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {const Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: const Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): the rule "positive impl" failed at step #7 (src/file.rs:LL:CC) because judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because @@ -77,7 +77,7 @@ fn all_t_not_magic() { failed at (src/file.rs:LL:CC) because cyclic proof attempt: `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness } }` + judgment had no applicable rules: `prove_via { goal: const Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness } }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because judgment had no applicable rules: `prove_via { goal: Magic(!ty_1), via: Copy(?ty_2), assumptions: {}, env: Env { variables: [!ty_1, ?ty_2], bias: Soundness } }`"#]]); } @@ -116,13 +116,13 @@ fn all_t_not_copy() { the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Magic(?ty_2)}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {const Magic(?ty_2)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {const Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {const Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: const Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): the rule "positive impl" failed at step #7 (src/file.rs:LL:CC) because judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because @@ -154,11 +154,11 @@ fn all_t_not_copy() { the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {const Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {const Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` + cyclic proof attempt: `prove_wc_list { goal: {const Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness } }`"#]]); + judgment had no applicable rules: `prove_via { goal: const Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness } }`"#]]); } diff --git a/crates/formality-rust/src/test.rs b/crates/formality-rust/src/test.rs index cc2c0001..8bdfd91d 100644 --- a/crates/formality-rust/src/test.rs +++ b/crates/formality-rust/src/test.rs @@ -33,6 +33,7 @@ fn test_parse_rust_like_trait_impl_syntax() { Ty, ], term: TraitImplBoundData { + constness: NotConst, trait_id: PartialEq, self_ty: Ty { data: Variable( @@ -84,6 +85,7 @@ fn test_parse_rust_like_trait_syntax() { Trait( Trait { safety: Safe, + constness: NotConst, id: Foo, binder: where ^ty0_1 : Bar <^ty0_0> { }, }, From d73d4f3cb0a81e63d51bd4e13f70751e116b0b38 Mon Sep 17 00:00:00 2001 From: tiif Date: Mon, 10 Feb 2025 13:08:59 +0800 Subject: [PATCH 08/65] Fix the test --- crates/formality-prove/src/decls.rs | 2 +- .../formality-prove/src/test/eq_partial_eq.rs | 12 ++++----- crates/formality-prove/src/test/magic_copy.rs | 26 +++++++++---------- 3 files changed, 20 insertions(+), 20 deletions(-) diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 718d210f..d7120163 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -200,7 +200,7 @@ impl TraitDecl { binder: Binder::new( &variables, TraitInvariantBoundData { - trait_ref: TraitRef::new(Constness::Const, &self.id, &variables), + trait_ref: TraitRef::new(Constness::NotConst, &self.id, &variables), where_clause, }, ), diff --git a/crates/formality-prove/src/test/eq_partial_eq.rs b/crates/formality-prove/src/test/eq_partial_eq.rs index 6dcebde6..7216d505 100644 --- a/crates/formality-prove/src/test/eq_partial_eq.rs +++ b/crates/formality-prove/src/test/eq_partial_eq.rs @@ -77,15 +77,15 @@ fn universals_not_eq() { the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because judgment had no applicable rules: `prove_via { goal: PartialEq(!ty_2), via: Eq(!ty_1), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness } }` the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, !ty_2, ?ty_3], bias: Soundness }, known_true: true, substitution: {?ty_3 => !ty_2} }, goal: {const Eq(?ty_3)}, assumptions: {Eq(!ty_1)} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, !ty_2, ?ty_3], bias: Soundness }, known_true: true, substitution: {?ty_3 => !ty_2} }, goal: {Eq(?ty_3)}, assumptions: {Eq(!ty_1)} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {const Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {const Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: const Eq(!ty_1), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: Eq(!ty_1), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_via { goal: const Eq(!ty_1), via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_via { goal: Eq(!ty_1), via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): the rule "predicate-congruence-axiom" failed at step #3 (src/file.rs:LL:CC) because judgment `prove { goal: {!ty_0 = !ty_1}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because @@ -109,5 +109,5 @@ fn universals_not_eq() { the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because cyclic proof attempt: `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: const Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], bias: Soundness } }`"#]]); + judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], bias: Soundness } }`"#]]); } diff --git a/crates/formality-prove/src/test/magic_copy.rs b/crates/formality-prove/src/test/magic_copy.rs index 6d55d7c1..4ab17a3c 100644 --- a/crates/formality-prove/src/test/magic_copy.rs +++ b/crates/formality-prove/src/test/magic_copy.rs @@ -63,13 +63,13 @@ fn all_t_not_magic() { the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {const Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {const Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {const Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: const Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): the rule "positive impl" failed at step #7 (src/file.rs:LL:CC) because judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because @@ -77,7 +77,7 @@ fn all_t_not_magic() { failed at (src/file.rs:LL:CC) because cyclic proof attempt: `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: const Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness } }` + judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness } }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because judgment had no applicable rules: `prove_via { goal: Magic(!ty_1), via: Copy(?ty_2), assumptions: {}, env: Env { variables: [!ty_1, ?ty_2], bias: Soundness } }`"#]]); } @@ -116,13 +116,13 @@ fn all_t_not_copy() { the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {const Magic(?ty_2)}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Magic(?ty_2)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {const Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {const Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: const Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): the rule "positive impl" failed at step #7 (src/file.rs:LL:CC) because judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because @@ -154,11 +154,11 @@ fn all_t_not_copy() { the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {const Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {const Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_wc_list { goal: {const Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` + cyclic proof attempt: `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: const Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness } }`"#]]); + judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness } }`"#]]); } From 783a44deded27c13eff9a18570bc323cc2b590af Mon Sep 17 00:00:00 2001 From: tiif Date: Mon, 10 Feb 2025 23:11:59 +0800 Subject: [PATCH 09/65] Add const impl test --- tests/const_trait.rs | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/tests/const_trait.rs b/tests/const_trait.rs index f0297096..e2cff838 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -5,7 +5,7 @@ use formality_core::test_util::ResultTestExt; use formality_macros::test; #[test] -fn test_const() { +fn test_const_syntax() { let gen_program = |addl: &str| { const BASE_PROGRAM: &str = "[ crate core { @@ -23,3 +23,25 @@ fn test_const() { test_program_ok(&gen_program("")).assert_ok(expect_test::expect!["()"]); } + +// Check if the impl is const, then the trait should also be declared as const. +#[test] +fn test_const_trait_impl() { + let gen_program = |addl: &str| { + const BASE_PROGRAM: &str = "[ + crate core { + trait Default { + } + + impl const Default for () { + } + } + + ]"; + + BASE_PROGRAM.replace("ADDITIONAL", addl) + }; + + test_program_ok(&gen_program("")).assert_ok(expect_test::expect!["()"]); +} + From 79697f381974459914d9cfaedb7749e5a541329c Mon Sep 17 00:00:00 2001 From: tiif Date: Mon, 10 Feb 2025 23:52:27 +0800 Subject: [PATCH 10/65] Add const trait impl check --- crates/formality-check/src/impls.rs | 23 +++++++++++++++++++++++ crates/formality-rust/src/grammar.rs | 3 +++ tests/const_trait.rs | 6 +++++- 3 files changed, 31 insertions(+), 1 deletion(-) diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index 06860a46..988cf0ba 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -48,6 +48,8 @@ impl super::Check<'_> { self.check_safety_matches(trait_decl, trait_impl)?; + self.check_constness_matches(trait_decl, trait_impl)?; + for impl_item in &impl_items { self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item)?; } @@ -97,6 +99,27 @@ impl super::Check<'_> { Ok(()) } + + /// + fn check_constness_matches(&self, trait_decl: &Trait, trait_impl: &TraitImpl) -> Fallible<()> { + // TODO: should bail out earlier if there is ~const trait declaration / impl ~const instead of here, + // then perhaps reduce it to assert + let trait_impl_constness = trait_impl.constness(); + if trait_impl_constness == Constness::MaybeConst { + bail!("`impl ~const {:?}` is not supported", trait_decl.id) + } + match trait_decl.constness { + Constness::Const => {}, + Constness::MaybeConst => bail!("`~const {:?}` declaration is not supported", trait_decl.id), + Constness::NotConst => { + if trait_impl.constness() != Constness::NotConst { + bail!("implementing the trait `{:?}` is not const", trait_decl.id) + } + } + } + Ok(()) + } + fn check_trait_impl_item( &self, env: &Env, diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index f8c54fb9..399e4583 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -268,6 +268,9 @@ impl TraitImpl { pub fn trait_id(&self) -> &TraitId { &self.binder.peek().trait_id } + pub fn constness(&self) -> Constness { + self.binder.peek().constness.clone() + } } #[term($?constness $trait_id $ for $self_ty $:where $,where_clauses { $*impl_items })] diff --git a/tests/const_trait.rs b/tests/const_trait.rs index e2cff838..ac7e8f08 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -42,6 +42,10 @@ fn test_const_trait_impl() { BASE_PROGRAM.replace("ADDITIONAL", addl) }; - test_program_ok(&gen_program("")).assert_ok(expect_test::expect!["()"]); + test_program_ok(&gen_program("")).assert_err(expect_test::expect![[r#" + check_trait_impl(impl const Default for () { }) + + Caused by: + implementing the trait `Default` is not const"#]]); } From a59024b98ad9a31f0a5bab953a875a6b2ab588a4 Mon Sep 17 00:00:00 2001 From: tiif Date: Mon, 17 Feb 2025 21:51:43 +0800 Subject: [PATCH 11/65] Add ConstEffect --- crates/formality-rust/src/grammar.rs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 399e4583..7b44da0d 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -196,6 +196,17 @@ impl TraitBinder { } } +pub struct ConstEffects { + pub effect_items: Vec, +} + +pub enum ConstEffect { + Const, + NotConst, + // For >::E, TraitRef can uniquely identify an impl, and an impl has only one effect. + FullyQualified(TraitRef), } + + #[term($:where $,where_clauses { $*trait_items })] pub struct TraitBoundData { pub where_clauses: Vec, From 1e2d04fb09cc526fe4be77fc918947a4f0e467fc Mon Sep 17 00:00:00 2001 From: tiif Date: Mon, 17 Feb 2025 22:10:20 +0800 Subject: [PATCH 12/65] Add effect_items to TraitBoundData --- crates/formality-check/src/impls.rs | 1 + crates/formality-check/src/traits.rs | 1 + crates/formality-rust/src/grammar.rs | 11 +++++------ crates/formality-rust/src/prove.rs | 2 ++ 4 files changed, 9 insertions(+), 6 deletions(-) diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index 988cf0ba..acb80532 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -44,6 +44,7 @@ impl super::Check<'_> { let TraitBoundData { where_clauses: _, trait_items, + effect_items: _, } = trait_decl.binder.instantiate_with(&trait_ref.parameters)?; self.check_safety_matches(trait_decl, trait_impl)?; diff --git a/crates/formality-check/src/traits.rs b/crates/formality-check/src/traits.rs index a8ab7144..163a5c7c 100644 --- a/crates/formality-check/src/traits.rs +++ b/crates/formality-check/src/traits.rs @@ -21,6 +21,7 @@ impl super::Check<'_> { let TraitBoundData { where_clauses, trait_items, + effect_items: _, } = env.instantiate_universally(&binder.explicit_binder); self.check_trait_items_have_unique_names(&trait_items)?; diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 7b44da0d..8373f97d 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -196,21 +196,20 @@ impl TraitBinder { } } -pub struct ConstEffects { - pub effect_items: Vec, -} - +#[term] pub enum ConstEffect { Const, NotConst, // For >::E, TraitRef can uniquely identify an impl, and an impl has only one effect. - FullyQualified(TraitRef), } + FullyQualified(TraitRef), +} -#[term($:where $,where_clauses { $*trait_items })] +#[term($:where $,where_clauses { $*effect_items $*trait_items })] pub struct TraitBoundData { pub where_clauses: Vec, pub trait_items: Vec, + pub effect_items: Vec, } #[term] diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index 2d0dcd25..ed246416 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -86,6 +86,7 @@ impl Crate { TraitBoundData { where_clauses, trait_items: _, + effect_items: _, // TODO: might depend on the constness of the trait decl }, ) = binder.open(); Some(prove::TraitDecl { @@ -242,6 +243,7 @@ impl Crate { TraitBoundData { where_clauses: trait_wc, trait_items, + effect_items: _, }, ) = binder.open(); From 85edbe4211f26afcf2710b5cf0a1b27a17d007a1 Mon Sep 17 00:00:00 2001 From: tiif Date: Mon, 17 Feb 2025 22:22:33 +0800 Subject: [PATCH 13/65] Add a bunch of todos for now --- crates/formality-check/src/impls.rs | 1 + crates/formality-rust/src/grammar.rs | 1 + crates/formality-rust/src/prove.rs | 5 +++-- 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index acb80532..2b4eedad 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -138,6 +138,7 @@ impl super::Check<'_> { ImplItem::AssociatedTyValue(v) => { self.check_associated_ty_value(env, assumptions, trait_items, v) } + ImplItem::ConstEffect => todo!() } } diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 8373f97d..7b53d9f0 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -325,6 +325,7 @@ pub enum ImplItem { Fn(Fn), #[cast] AssociatedTyValue(AssociatedTyValue), + ConstEffect, } #[term(type $id $binder ;)] diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index ed246416..ff92da56 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -135,7 +135,7 @@ impl Crate { }, ), }) - } + }, _ => None, }) .collect() @@ -220,7 +220,8 @@ impl Crate { }, ), }) - } + }, + ImplItem::ConstEffect => todo!(), })) } _ => vec![], From fa35d874288e133dc9cbf41aee02133ff6ca4559 Mon Sep 17 00:00:00 2001 From: tiif Date: Mon, 17 Feb 2025 22:39:39 +0800 Subject: [PATCH 14/65] Clean up a little bit --- crates/formality-check/src/impls.rs | 3 --- crates/formality-check/src/traits.rs | 2 +- crates/formality-prove/src/decls.rs | 1 - crates/formality-rust/src/grammar.rs | 1 - 4 files changed, 1 insertion(+), 6 deletions(-) diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index 2b4eedad..c03d9941 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -64,7 +64,6 @@ impl super::Check<'_> { let mut env = Env::default(); - // TODO: add constness to NegTraitImpl if necessary let NegTraitImplBoundData { trait_id, self_ty, @@ -103,8 +102,6 @@ impl super::Check<'_> { /// fn check_constness_matches(&self, trait_decl: &Trait, trait_impl: &TraitImpl) -> Fallible<()> { - // TODO: should bail out earlier if there is ~const trait declaration / impl ~const instead of here, - // then perhaps reduce it to assert let trait_impl_constness = trait_impl.constness(); if trait_impl_constness == Constness::MaybeConst { bail!("`impl ~const {:?}` is not supported", trait_decl.id) diff --git a/crates/formality-check/src/traits.rs b/crates/formality-check/src/traits.rs index 163a5c7c..9dc5d478 100644 --- a/crates/formality-check/src/traits.rs +++ b/crates/formality-check/src/traits.rs @@ -14,7 +14,7 @@ impl super::Check<'_> { safety: _, id: _, binder, - .. + constness: _, } = t; let mut env = Env::default(); diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index d7120163..1b78ad0a 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -141,7 +141,6 @@ pub struct NegImplDeclBoundData { pub where_clause: Wcs, } - /// Mark a trait or trait impl as `unsafe`. #[term] #[derive(Default)] diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 7b53d9f0..4f80b55a 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -204,7 +204,6 @@ pub enum ConstEffect { FullyQualified(TraitRef), } - #[term($:where $,where_clauses { $*effect_items $*trait_items })] pub struct TraitBoundData { pub where_clauses: Vec, From 02a0d15387d345c19ce5a4d77075f82ee3226445 Mon Sep 17 00:00:00 2001 From: tiif Date: Mon, 17 Feb 2025 22:50:31 +0800 Subject: [PATCH 15/65] Clean up --- crates/formality-rust/src/prove.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index ff92da56..5958235d 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -86,7 +86,7 @@ impl Crate { TraitBoundData { where_clauses, trait_items: _, - effect_items: _, // TODO: might depend on the constness of the trait decl + effect_items: _, }, ) = binder.open(); Some(prove::TraitDecl { From 4bf7bf5de17ed966313b2a4d35fb1e4d6c2ea48a Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 21 Feb 2025 21:36:10 +0800 Subject: [PATCH 16/65] Cleanup --- crates/formality-check/src/impls.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index c03d9941..588625a6 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -99,8 +99,6 @@ impl super::Check<'_> { Ok(()) } - - /// fn check_constness_matches(&self, trait_decl: &Trait, trait_impl: &TraitImpl) -> Fallible<()> { let trait_impl_constness = trait_impl.constness(); if trait_impl_constness == Constness::MaybeConst { From 33f156fc768367d54bb5e8a4f50fd9362f106313 Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 25 Feb 2025 00:26:50 +0800 Subject: [PATCH 17/65] Remove ConstEffect from impl item --- crates/formality-check/src/impls.rs | 1 - crates/formality-rust/src/grammar.rs | 1 - crates/formality-rust/src/prove.rs | 1 - 3 files changed, 3 deletions(-) diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index 588625a6..1009dc31 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -133,7 +133,6 @@ impl super::Check<'_> { ImplItem::AssociatedTyValue(v) => { self.check_associated_ty_value(env, assumptions, trait_items, v) } - ImplItem::ConstEffect => todo!() } } diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 4f80b55a..77e5a817 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -324,7 +324,6 @@ pub enum ImplItem { Fn(Fn), #[cast] AssociatedTyValue(AssociatedTyValue), - ConstEffect, } #[term(type $id $binder ;)] diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index 5958235d..3bb5ff6f 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -221,7 +221,6 @@ impl Crate { ), }) }, - ImplItem::ConstEffect => todo!(), })) } _ => vec![], From 2e15fb37c20e468221b4868a0cc4ab8ef3c37045 Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 25 Feb 2025 01:18:40 +0800 Subject: [PATCH 18/65] Substitute all constness with effect, then remove the syntax check --- crates/formality-check/src/impls.rs | 27 +++-------------- crates/formality-check/src/traits.rs | 2 +- crates/formality-prove/src/decls.rs | 8 ++--- crates/formality-rust/src/grammar.rs | 24 +++++++-------- crates/formality-rust/src/prove.rs | 18 ++++++------ .../formality-types/src/grammar/formulas.rs | 29 ++++++++++--------- 6 files changed, 46 insertions(+), 62 deletions(-) diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index 1009dc31..a534a053 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -12,7 +12,7 @@ use formality_rust::{ prove::ToWcs, }; use formality_types::{ - grammar::{Binder, Constness, Fallible, Relation, Substitution, Wcs}, + grammar::{Binder, Effect, Fallible, Relation, Substitution, Wcs}, rust::Term, }; @@ -24,7 +24,7 @@ impl super::Check<'_> { let mut env = Env::default(); let TraitImplBoundData { - constness, + effect, trait_id, self_ty, trait_parameters, @@ -32,7 +32,7 @@ impl super::Check<'_> { impl_items, } = env.instantiate_universally(binder); - let trait_ref = trait_id.with(&constness, self_ty, trait_parameters); + let trait_ref = trait_id.with(&effect, self_ty, trait_parameters); self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?; @@ -49,8 +49,6 @@ impl super::Check<'_> { self.check_safety_matches(trait_decl, trait_impl)?; - self.check_constness_matches(trait_decl, trait_impl)?; - for impl_item in &impl_items { self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item)?; } @@ -71,7 +69,7 @@ impl super::Check<'_> { where_clauses, } = env.instantiate_universally(binder); - let trait_ref = trait_id.with(&Constness::NotConst, self_ty, trait_parameters); + let trait_ref = trait_id.with(&Effect::Runtime, self_ty, trait_parameters); // Negative impls are always safe (rustc E0198) regardless of the trait's safety. if *safety == Safety::Unsafe { @@ -99,23 +97,6 @@ impl super::Check<'_> { Ok(()) } - fn check_constness_matches(&self, trait_decl: &Trait, trait_impl: &TraitImpl) -> Fallible<()> { - let trait_impl_constness = trait_impl.constness(); - if trait_impl_constness == Constness::MaybeConst { - bail!("`impl ~const {:?}` is not supported", trait_decl.id) - } - match trait_decl.constness { - Constness::Const => {}, - Constness::MaybeConst => bail!("`~const {:?}` declaration is not supported", trait_decl.id), - Constness::NotConst => { - if trait_impl.constness() != Constness::NotConst { - bail!("implementing the trait `{:?}` is not const", trait_decl.id) - } - } - } - Ok(()) - } - fn check_trait_impl_item( &self, env: &Env, diff --git a/crates/formality-check/src/traits.rs b/crates/formality-check/src/traits.rs index 9dc5d478..4fa9873f 100644 --- a/crates/formality-check/src/traits.rs +++ b/crates/formality-check/src/traits.rs @@ -14,7 +14,7 @@ impl super::Check<'_> { safety: _, id: _, binder, - constness: _, + effect: _, } = t; let mut env = Env::default(); diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 1b78ad0a..13ce23ff 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -4,7 +4,7 @@ use formality_types::grammar::{ AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, Wcs, }; -use formality_types::grammar::Constness; +use formality_types::grammar::Effect; #[term] pub struct Decls { @@ -154,9 +154,9 @@ pub enum Safety { /// It doesn't capture the trait items, which will be transformed into other sorts of rules. /// /// In Rust syntax, it covers the `trait Foo: Bar` part of the declaration, but not what appears in the `{...}`. -#[term($?constness $?safety trait $id $binder)] +#[term($?effect $?safety trait $id $binder)] pub struct TraitDecl { - pub constness: Constness, + pub effect: Effect, /// The name of the trait pub id: TraitId, @@ -199,7 +199,7 @@ impl TraitDecl { binder: Binder::new( &variables, TraitInvariantBoundData { - trait_ref: TraitRef::new(Constness::NotConst, &self.id, &variables), + trait_ref: TraitRef::new(Effect::Runtime, &self.id, &variables), where_clause, }, ), diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 77e5a817..c9fdd21e 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -2,7 +2,7 @@ use std::sync::Arc; use formality_core::{term, Upcast}; use formality_prove::Safety; -use formality_types::grammar::Constness; +use formality_types::grammar::Effect; use formality_types::{ grammar::{ AdtId, AliasTy, AssociatedItemId, Binder, Const, ConstData, CrateId, Fallible, FieldId, @@ -175,10 +175,10 @@ pub struct Variant { pub fields: Vec, } -#[term($?safety $?constness trait $id $binder)] +#[term($?safety $?effect trait $id $binder)] pub struct Trait { pub safety: Safety, - pub constness: Constness, + pub effect: Effect, pub id: TraitId, pub binder: TraitBinder, } @@ -199,7 +199,7 @@ impl TraitBinder { #[term] pub enum ConstEffect { Const, - NotConst, + Runtime, // For >::E, TraitRef can uniquely identify an impl, and an impl has only one effect. FullyQualified(TraitRef), } @@ -277,14 +277,14 @@ impl TraitImpl { pub fn trait_id(&self) -> &TraitId { &self.binder.peek().trait_id } - pub fn constness(&self) -> Constness { - self.binder.peek().constness.clone() + pub fn effect(&self) -> Effect { + self.binder.peek().effect.clone() } } -#[term($?constness $trait_id $ for $self_ty $:where $,where_clauses { $*impl_items })] +#[term($?effect $trait_id $ for $self_ty $:where $,where_clauses { $*impl_items })] pub struct TraitImplBoundData { - pub constness: Constness, + pub effect: Effect, pub trait_id: TraitId, pub self_ty: Ty, pub trait_parameters: Vec, @@ -294,7 +294,7 @@ pub struct TraitImplBoundData { impl TraitImplBoundData { pub fn trait_ref(&self) -> TraitRef { - self.trait_id.with(&self.constness, &self.self_ty, &self.trait_parameters) + self.trait_id.with(&self.effect, &self.self_ty, &self.trait_parameters) } } @@ -314,7 +314,7 @@ pub struct NegTraitImplBoundData { impl NegTraitImplBoundData { pub fn trait_ref(&self) -> TraitRef { - self.trait_id.with(&Constness::NotConst, &self.self_ty, &self.trait_parameters) + self.trait_id.with(&Effect::Runtime, &self.self_ty, &self.trait_parameters) } } @@ -352,7 +352,7 @@ impl WhereClause { match self.data() { WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => Some( trait_id - .with(&Constness::NotConst, self_ty, parameters) + .with(&Effect::Runtime, self_ty, parameters) .not_implemented() .upcast(), ), @@ -370,7 +370,7 @@ impl WhereClause { pub fn well_formed(&self) -> Wcs { match self.data() { WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => { - trait_id.with(&Constness::NotConst, self_ty, parameters).well_formed().upcast() + trait_id.with(&Effect::Runtime, self_ty, parameters).well_formed().upcast() } WhereClauseData::AliasEq(alias_ty, ty) => { let alias_param: Parameter = alias_ty.upcast(); diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index 3bb5ff6f..223b19db 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -7,7 +7,7 @@ use crate::grammar::{ use formality_core::{seq, Set, To, Upcast, Upcasted}; use formality_prove as prove; use formality_types::grammar::{ - AdtId, AliasTy, Binder, BoundVar, Constness, ParameterKind, Predicate, Relation, TraitId, Ty, Wc, Wcs, + AdtId, AliasTy, Binder, BoundVar, Effect, ParameterKind, Predicate, Relation, TraitId, Ty, Wc, Wcs, }; impl Program { @@ -80,7 +80,7 @@ impl Crate { self.items .iter() .flat_map(|item| match item { - CrateItem::Trait(Trait { id, binder, safety, constness}) => { + CrateItem::Trait(Trait { id, binder, safety, effect}) => { let ( vars, TraitBoundData { @@ -90,7 +90,7 @@ impl Crate { }, ) = binder.open(); Some(prove::TraitDecl { - constness: constness.clone(), + effect: effect.clone(), safety: safety.clone(), id: id.clone(), binder: Binder::new( @@ -117,7 +117,7 @@ impl Crate { let ( vars, TraitImplBoundData { - constness: _, + effect: _, trait_id, self_ty, trait_parameters, @@ -130,7 +130,7 @@ impl Crate { binder: Binder::new( vars, prove::ImplDeclBoundData { - trait_ref: trait_id.with(&Constness::NotConst, self_ty, trait_parameters), + trait_ref: trait_id.with(&Effect::Runtime, self_ty, trait_parameters), where_clause: where_clauses.to_wcs(), }, ), @@ -160,7 +160,7 @@ impl Crate { binder: Binder::new( vars, prove::NegImplDeclBoundData { - trait_ref: trait_id.with(&Constness::NotConst, self_ty, trait_parameters), + trait_ref: trait_id.with(&Effect::Runtime, self_ty, trait_parameters), where_clause: where_clauses.to_wcs(), }, ), @@ -179,7 +179,7 @@ impl Crate { let ( impl_vars, TraitImplBoundData { - constness: _, + effect: _, trait_id, self_ty, trait_parameters, @@ -416,7 +416,7 @@ impl ToWcs for WhereClause { fn to_wcs(&self) -> Wcs { match self.data() { WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => { - trait_id.with(&Constness::NotConst, self_ty, parameters).upcast() + trait_id.with(&Effect::Runtime, self_ty, parameters).upcast() } WhereClauseData::AliasEq(alias_ty, ty) => { Predicate::AliasEq(alias_ty.clone(), ty.clone()).upcast() @@ -442,7 +442,7 @@ impl WhereBound { match self.data() { WhereBoundData::IsImplemented(trait_id, parameters) => { - trait_id.with(&Constness::NotConst, self_ty, parameters).upcast() + trait_id.with(&Effect::Runtime, self_ty, parameters).upcast() } WhereBoundData::Outlives(lt) => Relation::outlives(self_ty, lt).upcast(), WhereBoundData::ForAll(binder) => { diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index 6f91b106..c3e22e89 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -11,6 +11,7 @@ use super::Parameters; use super::TraitId; use super::Ty; + pub type Fallible = anyhow::Result; /// Atomic predicates are the base goals we can try to prove; the rules for proving them @@ -110,7 +111,7 @@ impl Predicate { pub fn debone(&self) -> (Skeleton, Vec) { match self { Predicate::IsImplemented(TraitRef { - constness: _, + effect: _, trait_id, parameters, }) => ( @@ -118,7 +119,7 @@ impl Predicate { parameters.clone(), ), Predicate::NotImplemented(TraitRef { - constness: _, + effect: _, trait_id, parameters, }) => ( @@ -131,7 +132,7 @@ impl Predicate { (Skeleton::AliasEq(name.clone()), params) } Predicate::WellFormedTraitRef(TraitRef { - constness: _, + effect: _, trait_id, parameters, }) => ( @@ -139,7 +140,7 @@ impl Predicate { parameters.clone(), ), Predicate::IsLocal(TraitRef { - constness: _, + effect: _, trait_id, parameters, }) => (Skeleton::IsLocal(trait_id.clone()), parameters.clone()), @@ -195,20 +196,22 @@ impl Relation { } } + #[term] #[derive(Default)] -pub enum Constness { - #[default] - NotConst, - #[grammar(~const)] - MaybeConst, +pub enum Effect { Const, + #[default] + Runtime, + // TODO: associated effect from trait here + // For >::E, TraitRef can uniquely identify an impl, and an impl has only one effect. + Union(Vec), } -#[term($?constness $trait_id ( $,parameters ))] +#[term($?effect $trait_id ( $,parameters ))] pub struct TraitRef { - pub constness: Constness, + pub effect: Effect, pub trait_id: TraitId, pub parameters: Parameters, } @@ -216,13 +219,13 @@ pub struct TraitRef { impl TraitId { pub fn with( &self, - constness: &Constness, + effect: &Effect, self_ty: impl Upcast, parameters: impl Upcast>, ) -> TraitRef { let self_ty: Ty = self_ty.upcast(); let parameters: Vec = parameters.upcast(); - TraitRef::new(constness, self, (Some(self_ty), parameters)) + TraitRef::new(effect, self, (Some(self_ty), parameters)) } } From 2cb02fd35b77e98cbae4fa3480ab74ff8ebcc5cb Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 25 Feb 2025 01:21:54 +0800 Subject: [PATCH 19/65] Substitute ConstEffect with Effect --- crates/formality-rust/src/grammar.rs | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index c9fdd21e..96aa2e18 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -196,19 +196,11 @@ impl TraitBinder { } } -#[term] -pub enum ConstEffect { - Const, - Runtime, - // For >::E, TraitRef can uniquely identify an impl, and an impl has only one effect. - FullyQualified(TraitRef), -} - #[term($:where $,where_clauses { $*effect_items $*trait_items })] pub struct TraitBoundData { pub where_clauses: Vec, pub trait_items: Vec, - pub effect_items: Vec, + pub effect_items: Vec, } #[term] From 44b770e99315ced87f4d74abd27cf8b6e017c105 Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 25 Feb 2025 01:25:40 +0800 Subject: [PATCH 20/65] Remove const trait impl check --- tests/const_trait.rs | 25 ------------------------- 1 file changed, 25 deletions(-) diff --git a/tests/const_trait.rs b/tests/const_trait.rs index ac7e8f08..e3a35745 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -24,28 +24,3 @@ fn test_const_syntax() { test_program_ok(&gen_program("")).assert_ok(expect_test::expect!["()"]); } -// Check if the impl is const, then the trait should also be declared as const. -#[test] -fn test_const_trait_impl() { - let gen_program = |addl: &str| { - const BASE_PROGRAM: &str = "[ - crate core { - trait Default { - } - - impl const Default for () { - } - } - - ]"; - - BASE_PROGRAM.replace("ADDITIONAL", addl) - }; - - test_program_ok(&gen_program("")).assert_err(expect_test::expect![[r#" - check_trait_impl(impl const Default for () { }) - - Caused by: - implementing the trait `Default` is not const"#]]); -} - From ca7a72ccdfa87c24cd9b49f0864a1ec333a4a2ab Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 25 Feb 2025 01:26:33 +0800 Subject: [PATCH 21/65] Fix test output --- crates/formality-rust/src/test.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crates/formality-rust/src/test.rs b/crates/formality-rust/src/test.rs index 8bdfd91d..9a32c80c 100644 --- a/crates/formality-rust/src/test.rs +++ b/crates/formality-rust/src/test.rs @@ -33,7 +33,7 @@ fn test_parse_rust_like_trait_impl_syntax() { Ty, ], term: TraitImplBoundData { - constness: NotConst, + effect: Runtime, trait_id: PartialEq, self_ty: Ty { data: Variable( @@ -85,7 +85,7 @@ fn test_parse_rust_like_trait_syntax() { Trait( Trait { safety: Safe, - constness: NotConst, + effect: Runtime, id: Foo, binder: where ^ty0_1 : Bar <^ty0_0> { }, }, From 4ae18d228eedc9c2ff7f43debd73fa6ccc5ac305 Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 28 Feb 2025 00:54:32 +0800 Subject: [PATCH 22/65] Add more stuff to Effect enum --- crates/formality-prove/src/prove.rs | 1 + .../formality-prove/src/prove/prove_effect.rs | 25 +++++++++++++++++++ .../formality-types/src/grammar/formulas.rs | 8 ++++-- 3 files changed, 32 insertions(+), 2 deletions(-) create mode 100644 crates/formality-prove/src/prove/prove_effect.rs diff --git a/crates/formality-prove/src/prove.rs b/crates/formality-prove/src/prove.rs index 315d7e1e..526b3016 100644 --- a/crates/formality-prove/src/prove.rs +++ b/crates/formality-prove/src/prove.rs @@ -11,6 +11,7 @@ mod prove_via; mod prove_wc; mod prove_wc_list; mod prove_wf; +mod prove_effect; pub use constraints::Constraints; use formality_core::judgment::{FailedRule, TryIntoIter}; diff --git a/crates/formality-prove/src/prove/prove_effect.rs b/crates/formality-prove/src/prove/prove_effect.rs new file mode 100644 index 00000000..3ffb724f --- /dev/null +++ b/crates/formality-prove/src/prove/prove_effect.rs @@ -0,0 +1,25 @@ + +use formality_core::judgment_fn; +use formality_types::grammar::Effect; + +judgment_fn! { + pub fn subset_of(e1: Effect, e2: Effect) => () { + debug(e1, e2) + trivial(e1 == e2 => ()) + ( + // no premises + -------- ("runtime") + (subset_of(_e1, Effect::Runtime) => ()) + ) + ( + ((subset_of(&*e1, &*e2)) => ()) + -------- ("left-union") + (subset_of(_e1, Effect::Union(e1, e2)) => ()) + ) + ( + ((subset_of(&*e1, &*e2)) => ()) + -------- ("right-union") + (subset_of(_e1, Effect::Union(e1, e2)) => ()) + ) + } +} diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index c3e22e89..c0be700b 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -1,3 +1,5 @@ +use std::sync::Arc; + use formality_core::term; use formality_core::To; @@ -203,9 +205,11 @@ pub enum Effect { Const, #[default] Runtime, - // TODO: associated effect from trait here + #[grammar(AssociatedEffect($v0))] + AssociatedEffect(Arc), // For >::E, TraitRef can uniquely identify an impl, and an impl has only one effect. - Union(Vec), + #[grammar(EffectUnion($v0, $v1))] + Union(Arc, Arc), } From f8081a26d405968195fb640670aef3df8819bfff Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 28 Feb 2025 00:57:19 +0800 Subject: [PATCH 23/65] Shift comment --- crates/formality-types/src/grammar/formulas.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index c0be700b..34ed3626 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -205,9 +205,9 @@ pub enum Effect { Const, #[default] Runtime, + // For >::E, TraitRef can uniquely identify an impl, and an impl has only one effect. #[grammar(AssociatedEffect($v0))] AssociatedEffect(Arc), - // For >::E, TraitRef can uniquely identify an impl, and an impl has only one effect. #[grammar(EffectUnion($v0, $v1))] Union(Arc, Arc), } From 16a06172476bea6347acae65259a692f8abfd8a9 Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 28 Feb 2025 19:03:05 +0800 Subject: [PATCH 24/65] Move it as part of function --- crates/formality-types/src/grammar/formulas.rs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index 34ed3626..48e1e35f 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -212,6 +212,22 @@ pub enum Effect { Union(Arc, Arc), } +impl Effect { + fn subset_of(&self, e1: &Effect) -> bool { + if *self == *e1 { + return true; + } + if self.subset_of(e1) { + if let Effect::Union(e2, e3) = e1 { + if **e2 == *e1 || **e3 == *e1 { + return true; + } + } + } + false + } +} + #[term($?effect $trait_id ( $,parameters ))] pub struct TraitRef { From 683c3aafa3fd55d7cea4b736b2ddf0d3057191a0 Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 28 Feb 2025 19:08:08 +0800 Subject: [PATCH 25/65] Remove prove_effect --- .../formality-prove/src/prove/prove_effect.rs | 25 ------------------- 1 file changed, 25 deletions(-) delete mode 100644 crates/formality-prove/src/prove/prove_effect.rs diff --git a/crates/formality-prove/src/prove/prove_effect.rs b/crates/formality-prove/src/prove/prove_effect.rs deleted file mode 100644 index 3ffb724f..00000000 --- a/crates/formality-prove/src/prove/prove_effect.rs +++ /dev/null @@ -1,25 +0,0 @@ - -use formality_core::judgment_fn; -use formality_types::grammar::Effect; - -judgment_fn! { - pub fn subset_of(e1: Effect, e2: Effect) => () { - debug(e1, e2) - trivial(e1 == e2 => ()) - ( - // no premises - -------- ("runtime") - (subset_of(_e1, Effect::Runtime) => ()) - ) - ( - ((subset_of(&*e1, &*e2)) => ()) - -------- ("left-union") - (subset_of(_e1, Effect::Union(e1, e2)) => ()) - ) - ( - ((subset_of(&*e1, &*e2)) => ()) - -------- ("right-union") - (subset_of(_e1, Effect::Union(e1, e2)) => ()) - ) - } -} From 0699cfc15d7bb63465affdf4f19a79e7812b3073 Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 28 Feb 2025 19:31:45 +0800 Subject: [PATCH 26/65] Add EffectSubset predicate --- crates/formality-prove/src/prove.rs | 1 - crates/formality-prove/src/prove/prove_wc.rs | 5 +++++ crates/formality-types/src/grammar/formulas.rs | 11 ++++++++++- crates/formality-types/src/grammar/ty.rs | 3 +-- 4 files changed, 16 insertions(+), 4 deletions(-) diff --git a/crates/formality-prove/src/prove.rs b/crates/formality-prove/src/prove.rs index 526b3016..315d7e1e 100644 --- a/crates/formality-prove/src/prove.rs +++ b/crates/formality-prove/src/prove.rs @@ -11,7 +11,6 @@ mod prove_via; mod prove_wc; mod prove_wc_list; mod prove_wf; -mod prove_effect; pub use constraints::Constraints; use formality_core::judgment::{FailedRule, TryIntoIter}; diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index 1f4f8f25..cb1fe733 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -133,5 +133,10 @@ judgment_fn! { ----------------------------- ("const has ty") (prove_wc(decls, env, assumptions, Predicate::ConstHasType(ct, ty)) => c) ) + ( + (if e1.subset_of(&e2) == true) + ------------------------ ("effect subset") + (prove_wc(_decls, env, _assumptions, Predicate::EffectSubset(e1, e2)) => Constraints::none(env)) + ) } } diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index 48e1e35f..18e0ef94 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -46,6 +46,10 @@ pub enum Predicate { #[grammar(@ConstHasType($v0, $v1))] ConstHasType(Const, Ty), + + + #[grammar(@EffectSubset($v0, $v1))] + EffectSubset(Effect, Effect), } /// A coinductive predicate is one that can be proven via a cycle. @@ -100,6 +104,7 @@ pub enum Skeleton { WellFormedTraitRef(TraitId), IsLocal(TraitId), ConstHasType, + EffectSubset, Equals, Sub, @@ -150,6 +155,10 @@ impl Predicate { Skeleton::ConstHasType, vec![ct.clone().upcast(), ty.clone().upcast()], ), + Predicate::EffectSubset(_e1, _e2 ) => ( + Skeleton::EffectSubset, + vec![], // TODO: what is this for? + ) } } } @@ -213,7 +222,7 @@ pub enum Effect { } impl Effect { - fn subset_of(&self, e1: &Effect) -> bool { + pub fn subset_of(&self, e1: &Effect) -> bool { if *self == *e1 { return true; } diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs index 8284e10e..b51329d4 100644 --- a/crates/formality-types/src/grammar/ty.rs +++ b/crates/formality-types/src/grammar/ty.rs @@ -7,8 +7,7 @@ mod term_impls; use formality_core::{DowncastTo, To, Upcast, UpcastFrom}; use super::{ - consts::Const, AdtId, AssociatedItemId, Binder, BoundVar, ExistentialVar, FnId, TraitId, - UniversalVar, Variable, + consts::Const, AdtId, AssociatedItemId, Binder, BoundVar, ExistentialVar, FnId, TraitId, UniversalVar, Variable }; #[term] From 98f6ffc03801ee5a89adc0660da2bcc1c8b397ee Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 28 Feb 2025 19:59:36 +0800 Subject: [PATCH 27/65] Tweak the subset rule --- crates/formality-prove/src/prove/prove_wc.rs | 2 +- crates/formality-types/src/grammar/formulas.rs | 15 ++++++++------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index cb1fe733..78480d9f 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -134,7 +134,7 @@ judgment_fn! { (prove_wc(decls, env, assumptions, Predicate::ConstHasType(ct, ty)) => c) ) ( - (if e1.subset_of(&e2) == true) + (if e1.subset_of(&e2, None) == true) ------------------------ ("effect subset") (prove_wc(_decls, env, _assumptions, Predicate::EffectSubset(e1, e2)) => Constraints::none(env)) ) diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index 18e0ef94..e5a14b8e 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -222,17 +222,18 @@ pub enum Effect { } impl Effect { - pub fn subset_of(&self, e1: &Effect) -> bool { - if *self == *e1 { + pub fn subset_of(&self, e1: &Effect, e2: Option) -> bool { + if *e1 == Effect::Runtime || self == e1 { return true; } - if self.subset_of(e1) { - if let Effect::Union(e2, e3) = e1 { - if **e2 == *e1 || **e3 == *e1 { - return true; + // If self if subset of e1, self is subset of effect union that contains e1. + if let Some(effect) = e2 { + if self.subset_of(e1, None) { + if let Effect::Union(e2, e3) = effect { + return *e2 == *e1 || *e3 == *e1; } } - } + } false } } From b64aa4cdd3841d481c0dd989b59d6edefb9c5ada Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 28 Feb 2025 23:43:40 +0800 Subject: [PATCH 28/65] Everything from 28Feb office hour --- crates/formality-prove/src/prove.rs | 1 + .../src/prove/prove_effect_subset.rs | 128 ++++++++++++++++++ crates/formality-prove/src/prove/prove_eq.rs | 25 ++++ crates/formality-types/src/grammar/wc.rs | 5 +- 4 files changed, 158 insertions(+), 1 deletion(-) create mode 100644 crates/formality-prove/src/prove/prove_effect_subset.rs diff --git a/crates/formality-prove/src/prove.rs b/crates/formality-prove/src/prove.rs index 315d7e1e..48784626 100644 --- a/crates/formality-prove/src/prove.rs +++ b/crates/formality-prove/src/prove.rs @@ -11,6 +11,7 @@ mod prove_via; mod prove_wc; mod prove_wc_list; mod prove_wf; +mod prove_effect_subset; pub use constraints::Constraints; use formality_core::judgment::{FailedRule, TryIntoIter}; diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs new file mode 100644 index 00000000..e6a4c059 --- /dev/null +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -0,0 +1,128 @@ +use formality_core::visit::CoreVisit; +use formality_core::{judgment_fn, Downcast, ProvenSet, Upcast}; +use formality_core::{Deduplicate, Upcasted}; +use formality_types::grammar::{ + AliasTy, ExistentialVar, Parameter, Relation, RigidTy, Substitution, TyData, UniversalVar, + Variable, Wcs, +}; + +use crate::{ + decls::Decls, + prove::{ + constraints::occurs_in, prove, prove_after::prove_after, prove_normalize::prove_normalize, + }, +}; + +use super::{constraints::Constraints, env::Env}; + +/// Goal(s) to prove `a` and `b` are equal +pub fn eq(a: impl Upcast, b: impl Upcast) -> Relation { + Relation::equals(a, b) +} + +judgment_fn! { + pub fn prove_effect_subset( + _decls: Decls, + env: Env, + assumptions: Wcs, + f1: Effect + f2: Effect, + ) => Constraints { + debug(f1, f2, assumptions, env) + trivial(f1 == f2 => Constraints::empty()) + + // fn foo() { } + // () == () + // + // () == () => [?X => !T] + + ( + // forall E1 in Subset + // exists E2 in Superset + // E1 == E2 + + + --- ("union-subset-lhs") + (prove_effect_subset(decls, env, assumptions, f1, Effect::Union(f2_1, f2_2)) => constraints) + ) + } +} + + +judgment_fn! { + fn prove_atomic_effect_subset_effect( + _decls: Decls, + env: Env, + assumptions: Wcs, + atomic_subset: Effect + superset: Effect, + ) => Constraints { + debug(atomic, superset, assumptions, env) + + ( + // find some atomic effect in the superset... + (some_atomic_effect(superset) => atomic_superset) + + // ...and prove it is equal to the atomic from the subset + (prove_atomic_effect_eq(decls, env, assumptions, atomic_subset, atomic_superset) => constraints) + --- ("union-subset-lhs") + (prove_atomic_effect_subset_effect(decls, env, assumptions, f1, Effect::Union(f2_1, f2_2)) => constraints) + ) + } +} + + +judgment_fn! { + fn prove_atomic_effect_eq( + ) => Constraints { + debug(f1, f2, assumptions, env) + trivial(f1 == f2 => Constraints::empty()) + + ( + (prove_trait_ref_eq(decls, env, assumptions, tr1, tr2) => constraints) + --- ("associated-effect") + (prove_effect_subset(decls, env, assumptions, Effect::AssociatedEffect(tr1), Effect::AssociatedEffect(tr2)) => constraints) + ) + } +) + +/// Proves judgment for each of the given items. +pub fn collect(judgment: ProvenSet) -> ProvenSet> { + match judgment.into_set() { + Ok(s) => ProvenSet::proven(set![s]), + Err(e) => ProvenSet::from(*e), + } +} + +judgment_fn! { + fn some_atomic_effect( + f1: Effect + ) => Effect { + debug(f1) + + ( + --- ("union-lhs") + (atomic_effect(Effect::Union(f1, _f2)) => f1) + ) + + ( + --- ("union-rhs") + (atomic_effect(Effect::Union(_f1, f2)) => f2) + ) + + ( + --- ("assoc-effect") + (atomic_effect(Effect::AssociatedEffect(tr)) => Effect::AssociatedEffect(tr)) + ) + + ( + --- ("assoc-const") + (atomic_effect(Effect::Const) => Effect::Const) + ) + + ( + --- ("assoc-runtime") + (atomic_effect(Effect::Runtime) => Effect::Runtime) + ) + } +} \ No newline at end of file diff --git a/crates/formality-prove/src/prove/prove_eq.rs b/crates/formality-prove/src/prove/prove_eq.rs index 92dc3470..a48ce658 100644 --- a/crates/formality-prove/src/prove/prove_eq.rs +++ b/crates/formality-prove/src/prove/prove_eq.rs @@ -73,6 +73,31 @@ judgment_fn! { } } +judgement_fn! { + pub fn prove_traitref_eq( + _decls: Decls, + env: Env, + assumptions: Wcs, + a: TraitRef, + b: TraitRef, + ) => Constraints { + debug(a, b, assumptions, env) + + trivial(a == b => Constraints::none(env)) + + ( + (let TraitRef { effect: a_effect, trait_id: a_trait_id, parameters: a_parameters } = a) + (let TraitRef { effect: b_effect, trait_id: b_trait_id, parameters: b_parameters } = b) + (if a_trait_id == b_trait_id)! + (prove(decls, env, assumptions, Wcs::all_eq(a_parameters, b_parameters)) => constraints) + (prove_after(decls, constraints, assumptions, WcData::EffectSubset(a_effect, b_effect)) => constraints) + (prove_after(decls, constraints, assumptions, WcData::EffectSubset(b_effect, a_effect)) => constraints) + ----------------------------- ("traitref") + (prove_traitref_eq(decls, env, assumptions, a, b) => constraints) + ) + } +} + judgment_fn! { pub fn prove_existential_var_eq( _decls: Decls, diff --git a/crates/formality-types/src/grammar/wc.rs b/crates/formality-types/src/grammar/wc.rs index c85361ad..2e483a67 100644 --- a/crates/formality-types/src/grammar/wc.rs +++ b/crates/formality-types/src/grammar/wc.rs @@ -4,7 +4,7 @@ use formality_core::{ cast_impl, set, term, Cons, DowncastFrom, DowncastTo, Set, Upcast, UpcastFrom, Upcasted, }; -use super::{Binder, BoundVar, Parameter, Predicate, Relation, TraitRef}; +use super::{Binder, BoundVar, Effect, Parameter, Predicate, Relation, TraitRef}; #[term($set)] #[derive(Default)] @@ -136,6 +136,9 @@ pub enum WcData { #[grammar(if $v0 $v1)] Implies(Wcs, Wc), + + #[grammar(subset($v0, $v1))] + EffectSubset(Effect, Effect), } // --- From 3411c7c069a1329d4dce67cfd33cadeb12170f16 Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 6 Mar 2025 00:53:12 +0800 Subject: [PATCH 29/65] Make everything compile --- crates/formality-prove/src/decls.rs | 1 + .../src/prove/prove_effect_subset.rs | 117 ++++++++---------- crates/formality-prove/src/prove/prove_eq.rs | 17 +-- 3 files changed, 65 insertions(+), 70 deletions(-) diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 13ce23ff..4289b182 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -189,6 +189,7 @@ impl TraitDecl { is_supertrait(self_var, binder.peek()) } formality_types::grammar::WcData::Implies(_, c) => is_supertrait(self_var, c), + formality_types::grammar::WcData::EffectSubset(_, _) => todo!(), } } diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index e6a4c059..b7230256 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -1,52 +1,39 @@ -use formality_core::visit::CoreVisit; -use formality_core::{judgment_fn, Downcast, ProvenSet, Upcast}; -use formality_core::{Deduplicate, Upcasted}; -use formality_types::grammar::{ - AliasTy, ExistentialVar, Parameter, Relation, RigidTy, Substitution, TyData, UniversalVar, - Variable, Wcs, -}; - -use crate::{ - decls::Decls, - prove::{ - constraints::occurs_in, prove, prove_after::prove_after, prove_normalize::prove_normalize, - }, -}; - -use super::{constraints::Constraints, env::Env}; - -/// Goal(s) to prove `a` and `b` are equal -pub fn eq(a: impl Upcast, b: impl Upcast) -> Relation { - Relation::equals(a, b) -} - -judgment_fn! { - pub fn prove_effect_subset( - _decls: Decls, - env: Env, - assumptions: Wcs, - f1: Effect - f2: Effect, - ) => Constraints { - debug(f1, f2, assumptions, env) - trivial(f1 == f2 => Constraints::empty()) - - // fn foo() { } - // () == () - // - // () == () => [?X => !T] - - ( - // forall E1 in Subset - // exists E2 in Superset - // E1 == E2 - - - --- ("union-subset-lhs") - (prove_effect_subset(decls, env, assumptions, f1, Effect::Union(f2_1, f2_2)) => constraints) - ) - } -} +use formality_core::{judgment_fn, ProvenSet, Set, set}; +use formality_types::grammar::{Effect, Wcs}; +use std::fmt::Debug; + +use crate::{prove::prove_eq::prove_traitref_eq, Decls}; + +use super::{Constraints, Env}; + + +//judgment_fn! { +// pub fn prove_effect_subset( +// _decls: Decls, +// env: Env, +// assumptions: Wcs, +// f1: Effect, +// f2: Effect, +// ) => Constraints { +// debug(f1, f2, assumptions, env) +// trivial(f1 == f2 => Constraints::empty()) +// +// // fn foo() { } +// // () == () +// // +// // () == () => [?X => !T] +// +// ( +// // forall E1 in Subset +// // exists E2 in Superset +// // E1 == E2 +// +// +// --- ("union-subset-lhs") +// (prove_effect_subset(decls, env, assumptions, f1, Effect::Union(f2_1, f2_2)) => constraints) +// ) +// } +//} judgment_fn! { @@ -54,19 +41,18 @@ judgment_fn! { _decls: Decls, env: Env, assumptions: Wcs, - atomic_subset: Effect + atomic_subset: Effect, superset: Effect, ) => Constraints { - debug(atomic, superset, assumptions, env) + debug(atomic_subset, superset, assumptions, env) ( // find some atomic effect in the superset... (some_atomic_effect(superset) => atomic_superset) - // ...and prove it is equal to the atomic from the subset - (prove_atomic_effect_eq(decls, env, assumptions, atomic_subset, atomic_superset) => constraints) + (prove_atomic_effect_eq(&decls, &env, &assumptions, atomic_subset, atomic_superset) => constraints) --- ("union-subset-lhs") - (prove_atomic_effect_subset_effect(decls, env, assumptions, f1, Effect::Union(f2_1, f2_2)) => constraints) + (prove_atomic_effect_subset_effect(decls, env, assumptions, _f1, Effect::Union(_f2_1, _f2_2)) => constraints) ) } } @@ -74,17 +60,22 @@ judgment_fn! { judgment_fn! { fn prove_atomic_effect_eq( + _decls: Decls, + env: Env, + assumptions: Wcs, + f1: Effect, + f2: Effect, ) => Constraints { debug(f1, f2, assumptions, env) - trivial(f1 == f2 => Constraints::empty()) + trivial(f1 == f2 => Constraints::none(env)) ( - (prove_trait_ref_eq(decls, env, assumptions, tr1, tr2) => constraints) + (prove_traitref_eq(decls, env, assumptions, &*tr1, &*tr2) => constraints) --- ("associated-effect") - (prove_effect_subset(decls, env, assumptions, Effect::AssociatedEffect(tr1), Effect::AssociatedEffect(tr2)) => constraints) + (prove_atomic_effect_eq(decls, env, assumptions, Effect::AssociatedEffect(tr1), Effect::AssociatedEffect(tr2)) => constraints) ) } -) +} /// Proves judgment for each of the given items. pub fn collect(judgment: ProvenSet) -> ProvenSet> { @@ -102,27 +93,27 @@ judgment_fn! { ( --- ("union-lhs") - (atomic_effect(Effect::Union(f1, _f2)) => f1) + (some_atomic_effect(Effect::Union(f1, _f2)) => &*f1) ) ( --- ("union-rhs") - (atomic_effect(Effect::Union(_f1, f2)) => f2) + (some_atomic_effect(Effect::Union(_f1, f2)) => &*f2) ) ( --- ("assoc-effect") - (atomic_effect(Effect::AssociatedEffect(tr)) => Effect::AssociatedEffect(tr)) + (some_atomic_effect(Effect::AssociatedEffect(tr)) => Effect::AssociatedEffect(tr)) ) ( --- ("assoc-const") - (atomic_effect(Effect::Const) => Effect::Const) + (some_atomic_effect(Effect::Const) => Effect::Const) ) ( --- ("assoc-runtime") - (atomic_effect(Effect::Runtime) => Effect::Runtime) + (some_atomic_effect(Effect::Runtime) => Effect::Runtime) ) } } \ No newline at end of file diff --git a/crates/formality-prove/src/prove/prove_eq.rs b/crates/formality-prove/src/prove/prove_eq.rs index a48ce658..c5b19bee 100644 --- a/crates/formality-prove/src/prove/prove_eq.rs +++ b/crates/formality-prove/src/prove/prove_eq.rs @@ -1,10 +1,12 @@ use formality_core::visit::CoreVisit; -use formality_core::{judgment_fn, Downcast, ProvenSet, Upcast}; +use formality_core::{judgment_fn, Downcast, ProvenSet, Upcast, UpcastFrom}; use formality_core::{Deduplicate, Upcasted}; use formality_types::grammar::{ - AliasTy, ExistentialVar, Parameter, Relation, RigidTy, Substitution, TyData, UniversalVar, - Variable, Wcs, + AliasTy, ExistentialVar, Parameter, Relation, RigidTy, Substitution, TyData, UniversalVar, Variable, Wc, Wcs }; +use formality_types::grammar::TraitRef; +use formality_types::grammar::WcData; + use crate::{ decls::Decls, @@ -73,7 +75,7 @@ judgment_fn! { } } -judgement_fn! { +judgment_fn! { pub fn prove_traitref_eq( _decls: Decls, env: Env, @@ -85,13 +87,14 @@ judgement_fn! { trivial(a == b => Constraints::none(env)) + // Two trait_refs are equal if they have the same id, effect, and parameters. ( (let TraitRef { effect: a_effect, trait_id: a_trait_id, parameters: a_parameters } = a) (let TraitRef { effect: b_effect, trait_id: b_trait_id, parameters: b_parameters } = b) (if a_trait_id == b_trait_id)! - (prove(decls, env, assumptions, Wcs::all_eq(a_parameters, b_parameters)) => constraints) - (prove_after(decls, constraints, assumptions, WcData::EffectSubset(a_effect, b_effect)) => constraints) - (prove_after(decls, constraints, assumptions, WcData::EffectSubset(b_effect, a_effect)) => constraints) + (prove(&decls, env, assumptions.clone(), Wcs::all_eq(a_parameters, b_parameters)) => constraints) + (prove_after(&decls, constraints, assumptions.clone(), Wc::upcast_from(WcData::EffectSubset(a_effect.clone(), b_effect.clone()))) => constraints) + (prove_after(&decls, constraints, assumptions.clone(),Wc::upcast_from(WcData::EffectSubset(b_effect.clone(), a_effect.clone()))) => constraints) ----------------------------- ("traitref") (prove_traitref_eq(decls, env, assumptions, a, b) => constraints) ) From 04680a694c9055567476f4f4790fd6c7340db957 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 7 Mar 2025 14:35:26 +0000 Subject: [PATCH 30/65] comments + newtype for DebonedPredicate --- crates/formality-prove/src/prove/prove_via.rs | 26 +++-- .../formality-types/src/grammar/formulas.rs | 101 +++++++++++------- crates/formality-types/src/grammar/wc.rs | 7 ++ 3 files changed, 86 insertions(+), 48 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_via.rs b/crates/formality-prove/src/prove/prove_via.rs index 4ddbd463..94e0db1c 100644 --- a/crates/formality-prove/src/prove/prove_via.rs +++ b/crates/formality-prove/src/prove/prove_via.rs @@ -1,5 +1,5 @@ use formality_core::judgment_fn; -use formality_types::grammar::{WcData, Wcs}; +use formality_types::grammar::{DebonedPredicate, WcData, Wcs}; use crate::{ decls::Decls, @@ -23,30 +23,30 @@ judgment_fn! { debug(goal, via, assumptions, env) ( - // `c` = "clause", the name for something that we are assuming is true. - (let (skel_c, parameters_c) = pred_1.debone()) - // `g` = "goal, the name for something that we are trying to prove. - (let (skel_g, parameters_g) = pred_2.debone()) + (let DebonedPredicate { skeleton: skel_c, parameters: parameters_c } = pred_c.debone()) + (let DebonedPredicate { skeleton: skel_g, parameters: parameters_g } = pred_g.debone()) (if skel_c == skel_g)! (prove(decls, env, assumptions, Wcs::all_eq(parameters_c, parameters_g)) => c) ----------------------------- ("predicate-congruence-axiom") - (prove_via(decls, env, assumptions, WcData::Predicate(pred_1), WcData::Predicate(pred_2)) => c) + (prove_via(decls, env, assumptions, WcData::Predicate(pred_c), WcData::Predicate(pred_g)) => c) ) ( - (let (skel_c, parameters_c) = rel_1.debone()) - (let (skel_g, parameters_g) = rel_2.debone()) + (let DebonedPredicate { skeleton: skel_c, parameters: parameters_c } = rel_c.debone()) + (let DebonedPredicate { skeleton: skel_g, parameters: parameters_g } = rel_g.debone()) (if skel_c == skel_g) (if parameters_c == parameters_g)! // for relations, we require 100% match ----------------------------- ("relation-axiom") - (prove_via(_decls, env, _assumptions, WcData::Relation(rel_1), WcData::Relation(rel_2)) => Constraints::none(env)) + (prove_via(_decls, env, _assumptions, WcData::Relation(rel_c), WcData::Relation(rel_g)) => Constraints::none(env)) ) - // If you have `where for<'a> T: Trait<'a>` then you can prove `T: Trait<'b>` for any `'b`. + // If you have `where for<'a> T: Trait<'a>` then you can prove `T: Trait<'b>` for any `'b` ( + // replace `'a` with an existential variable `?a` (let (env, subst) = env.existential_substitution(&binder)) (let via1 = binder.instantiate_with(&subst).unwrap()) - // Try to prove `T: Trait == goal`. + + // try to prove `T: Trait == goal` (prove_via(decls, env, assumptions, via1, goal) => c) ----------------------------- ("forall") (prove_via(decls, env, assumptions, WcData::ForAll(binder), goal) => c.pop_subst(&subst)) @@ -56,6 +56,10 @@ judgment_fn! { ( // if the goal is `T: Foo`... (prove_via(&decls, env, &assumptions, wc_consequence, goal) => c) +<<<<<<< HEAD +======= + +>>>>>>> 1c31da9 (comments + newtype for DebonedPredicate) // ...and we can prove `T: Debug`... then it holds. (prove_after(&decls, c, &assumptions, &wc_condition) => c) ----------------------------- ("implies") diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index e5a14b8e..841c4569 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -13,7 +13,6 @@ use super::Parameters; use super::TraitId; use super::Ty; - pub type Fallible = anyhow::Result; /// Atomic predicates are the base goals we can try to prove; the rules for proving them @@ -47,7 +46,6 @@ pub enum Predicate { #[grammar(@ConstHasType($v0, $v1))] ConstHasType(Const, Ty), - #[grammar(@EffectSubset($v0, $v1))] EffectSubset(Effect, Effect), } @@ -111,54 +109,73 @@ pub enum Skeleton { Outlives, } +/// A "deboned predicate" is an alternate representation +/// of a [`Predicate`][] where the "constant" parts of the +/// predicate (e.g., which variant is it, the traid-id, etc) +/// are pulled into the "skeleton" and the unifiable parts +/// (types, lifetimes, effects) are pulled into a distinct list. +/// +/// This is useful for unifying predicates because you can +/// (1) compare the skeletons with `==` and then (2) unify the rest +/// and you don't have to write a bunch of tedious code to +/// match variants one by one. +#[term] +pub struct DebonedPredicate { + pub skeleton: Skeleton, + pub parameters: Vec, +} + impl Predicate { /// Separate an atomic predicate into the "skeleton" (which can be compared for equality using `==`) /// and the parameters (which must be related). #[tracing::instrument(level = "trace", ret)] - pub fn debone(&self) -> (Skeleton, Vec) { + pub fn debone(&self) -> DebonedPredicate { match self { Predicate::IsImplemented(TraitRef { effect: _, trait_id, parameters, - }) => ( - Skeleton::IsImplemented(trait_id.clone()), - parameters.clone(), - ), + }) => DebonedPredicate { + skeleton: Skeleton::IsImplemented(trait_id.clone()), + parameters: parameters.clone(), + }, Predicate::NotImplemented(TraitRef { effect: _, trait_id, parameters, - }) => ( - Skeleton::NotImplemented(trait_id.clone()), - parameters.clone(), - ), + }) => DebonedPredicate { + skeleton: Skeleton::NotImplemented(trait_id.clone()), + parameters: parameters.clone(), + }, Predicate::AliasEq(AliasTy { name, parameters }, ty) => { let mut params = parameters.clone(); params.push(ty.clone().upcast()); - (Skeleton::AliasEq(name.clone()), params) + DebonedPredicate { + skeleton: Skeleton::AliasEq(name.clone()), + parameters: params, + } } Predicate::WellFormedTraitRef(TraitRef { effect: _, trait_id, parameters, - }) => ( - Skeleton::WellFormedTraitRef(trait_id.clone()), - parameters.clone(), - ), + }) => DebonedPredicate { + skeleton: Skeleton::WellFormedTraitRef(trait_id.clone()), + parameters: parameters.clone(), + }, Predicate::IsLocal(TraitRef { effect: _, trait_id, parameters, - }) => (Skeleton::IsLocal(trait_id.clone()), parameters.clone()), - Predicate::ConstHasType(ct, ty) => ( - Skeleton::ConstHasType, - vec![ct.clone().upcast(), ty.clone().upcast()], - ), - Predicate::EffectSubset(_e1, _e2 ) => ( - Skeleton::EffectSubset, - vec![], // TODO: what is this for? - ) + }) => DebonedPredicate { + skeleton: Skeleton::IsLocal(trait_id.clone()), + parameters: parameters.clone(), + }, + Predicate::ConstHasType(ct, ty) => DebonedPredicate { + skeleton: Skeleton::ConstHasType, + parameters: vec![ct.clone().upcast(), ty.clone().upcast()], + }, + Predicate::EffectSubset(_e1, _e2) => todo!(), } } } @@ -197,24 +214,35 @@ pub enum Relation { impl Relation { #[tracing::instrument(level = "trace", ret)] - pub fn debone(&self) -> (Skeleton, Vec) { + pub fn debone(&self) -> DebonedPredicate { match self { - Relation::Equals(a, b) => (Skeleton::Equals, vec![a.clone(), b.clone()]), - Relation::Sub(a, b) => (Skeleton::Sub, vec![a.clone(), b.clone()]), - Relation::Outlives(a, b) => (Skeleton::Outlives, vec![a.clone(), b.clone()]), - Relation::WellFormed(p) => (Skeleton::WellFormed, vec![p.clone()]), + Relation::Equals(a, b) => DebonedPredicate { + skeleton: Skeleton::Equals, + parameters: vec![a.clone(), b.clone()], + }, + Relation::Sub(a, b) => DebonedPredicate { + skeleton: Skeleton::Sub, + parameters: vec![a.clone(), b.clone()], + }, + Relation::Outlives(a, b) => DebonedPredicate { + skeleton: Skeleton::Outlives, + parameters: vec![a.clone(), b.clone()], + }, + Relation::WellFormed(p) => DebonedPredicate { + skeleton: Skeleton::WellFormed, + parameters: vec![p.clone()], + }, } } } - #[term] #[derive(Default)] pub enum Effect { Const, #[default] Runtime, - // For >::E, TraitRef can uniquely identify an impl, and an impl has only one effect. + // For >::E, TraitRef can uniquely identify an impl, and an impl has only one effect. #[grammar(AssociatedEffect($v0))] AssociatedEffect(Arc), #[grammar(EffectUnion($v0, $v1))] @@ -233,12 +261,11 @@ impl Effect { return *e2 == *e1 || *e3 == *e1; } } - } - false + } + false } } - #[term($?effect $trait_id ( $,parameters ))] pub struct TraitRef { pub effect: Effect, @@ -260,13 +287,13 @@ impl TraitId { } pub trait Debone { - fn debone(&self) -> (Skeleton, Vec); + fn debone(&self) -> DebonedPredicate; } macro_rules! debone_impl { ($t:ty) => { impl Debone for $t { - fn debone(&self) -> (Skeleton, Vec) { + fn debone(&self) -> DebonedPredicate { self.debone() } } diff --git a/crates/formality-types/src/grammar/wc.rs b/crates/formality-types/src/grammar/wc.rs index 2e483a67..c5d8c28b 100644 --- a/crates/formality-types/src/grammar/wc.rs +++ b/crates/formality-types/src/grammar/wc.rs @@ -134,9 +134,16 @@ pub enum WcData { #[grammar(for $v0)] ForAll(Binder), + // An *implication* `if $v0 $v1` says "assuming v0 is true, v1 is true". + // These are useful to express hypothetical syntax like + // `for<'a: 'b, 'b>` or as part of an implied bounds scheme + // where you might make the Rust syntax `for<'a, 'b> T: Something<'a, 'b>` + // expand to `for<'a, 'b> if ('a: 'b) (T: Something<'a, 'b>)` + // (given `trait Something<'a, 'b> where 'a: 'b`). #[grammar(if $v0 $v1)] Implies(Wcs, Wc), + // Means that the effects `$v0` are a subset of `$v1`. #[grammar(subset($v0, $v1))] EffectSubset(Effect, Effect), } From 9793fba165a7289d62aed153adf8aa1739f98467 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 7 Mar 2025 14:47:02 +0000 Subject: [PATCH 31/65] add effects into DebonedPredicate (FIXME) --- crates/formality-prove/src/prove/prove_via.rs | 15 ++++++++++----- crates/formality-types/src/grammar/formulas.rs | 18 +++++++++++++++++- 2 files changed, 27 insertions(+), 6 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_via.rs b/crates/formality-prove/src/prove/prove_via.rs index 94e0db1c..e13c9c58 100644 --- a/crates/formality-prove/src/prove/prove_via.rs +++ b/crates/formality-prove/src/prove/prove_via.rs @@ -23,19 +23,24 @@ judgment_fn! { debug(goal, via, assumptions, env) ( - (let DebonedPredicate { skeleton: skel_c, parameters: parameters_c } = pred_c.debone()) - (let DebonedPredicate { skeleton: skel_g, parameters: parameters_g } = pred_g.debone()) + // `c` = "clause", the name for something that we are assuming is true + (let DebonedPredicate { skeleton: skel_c, parameters: parameters_c, effects: effects_c } = pred_c.debone()) + // `g` = "goal, the name for something that we are trying to prove + (let DebonedPredicate { skeleton: skel_g, parameters: parameters_g, effects: effects_g } = pred_g.debone()) (if skel_c == skel_g)! (prove(decls, env, assumptions, Wcs::all_eq(parameters_c, parameters_g)) => c) + (if effects_c == effects_g) // FIXME: this is not general enough but we will revisit it ----------------------------- ("predicate-congruence-axiom") (prove_via(decls, env, assumptions, WcData::Predicate(pred_c), WcData::Predicate(pred_g)) => c) ) ( - (let DebonedPredicate { skeleton: skel_c, parameters: parameters_c } = rel_c.debone()) - (let DebonedPredicate { skeleton: skel_g, parameters: parameters_g } = rel_g.debone()) + (let DebonedPredicate { skeleton: skel_c, parameters: parameters_c, effects: effects_c } = rel_c.debone()) + (let DebonedPredicate { skeleton: skel_g, parameters: parameters_g, effects: effects_g } = rel_g.debone()) (if skel_c == skel_g) - (if parameters_c == parameters_g)! // for relations, we require 100% match + // for relations, we require 100% match + (if parameters_c == parameters_g) + (if effects_c == effects_g)! ----------------------------- ("relation-axiom") (prove_via(_decls, env, _assumptions, WcData::Relation(rel_c), WcData::Relation(rel_g)) => Constraints::none(env)) ) diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index 841c4569..50af5406 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -46,6 +46,7 @@ pub enum Predicate { #[grammar(@ConstHasType($v0, $v1))] ConstHasType(Const, Ty), + // FIXME: should be in `Relation` #[grammar(@EffectSubset($v0, $v1))] EffectSubset(Effect, Effect), } @@ -123,6 +124,7 @@ pub enum Skeleton { pub struct DebonedPredicate { pub skeleton: Skeleton, pub parameters: Vec, + pub effects: Vec, } impl Predicate { @@ -138,6 +140,7 @@ impl Predicate { }) => DebonedPredicate { skeleton: Skeleton::IsImplemented(trait_id.clone()), parameters: parameters.clone(), + effects: Default::default(), }, Predicate::NotImplemented(TraitRef { effect: _, @@ -146,6 +149,7 @@ impl Predicate { }) => DebonedPredicate { skeleton: Skeleton::NotImplemented(trait_id.clone()), parameters: parameters.clone(), + effects: Default::default(), }, Predicate::AliasEq(AliasTy { name, parameters }, ty) => { let mut params = parameters.clone(); @@ -153,6 +157,7 @@ impl Predicate { DebonedPredicate { skeleton: Skeleton::AliasEq(name.clone()), parameters: params, + effects: Default::default(), } } Predicate::WellFormedTraitRef(TraitRef { @@ -162,6 +167,7 @@ impl Predicate { }) => DebonedPredicate { skeleton: Skeleton::WellFormedTraitRef(trait_id.clone()), parameters: parameters.clone(), + effects: Default::default(), }, Predicate::IsLocal(TraitRef { effect: _, @@ -170,12 +176,18 @@ impl Predicate { }) => DebonedPredicate { skeleton: Skeleton::IsLocal(trait_id.clone()), parameters: parameters.clone(), + effects: Default::default(), }, Predicate::ConstHasType(ct, ty) => DebonedPredicate { skeleton: Skeleton::ConstHasType, parameters: vec![ct.clone().upcast(), ty.clone().upcast()], + effects: Default::default(), + }, + Predicate::EffectSubset(e1, e2) => DebonedPredicate { + skeleton: Skeleton::EffectSubset, + parameters: Default::default(), + effects: vec![e1, e2].upcast(), }, - Predicate::EffectSubset(_e1, _e2) => todo!(), } } } @@ -219,18 +231,22 @@ impl Relation { Relation::Equals(a, b) => DebonedPredicate { skeleton: Skeleton::Equals, parameters: vec![a.clone(), b.clone()], + effects: Default::default(), }, Relation::Sub(a, b) => DebonedPredicate { skeleton: Skeleton::Sub, parameters: vec![a.clone(), b.clone()], + effects: Default::default(), }, Relation::Outlives(a, b) => DebonedPredicate { skeleton: Skeleton::Outlives, parameters: vec![a.clone(), b.clone()], + effects: Default::default(), }, Relation::WellFormed(p) => DebonedPredicate { skeleton: Skeleton::WellFormed, parameters: vec![p.clone()], + effects: Default::default(), }, } } From 76e25e1d7d7103aa59374c30ee0236ebd69fbb4a Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 7 Mar 2025 15:16:17 +0000 Subject: [PATCH 32/65] implement subset --- crates/formality-prove/src/decls.rs | 5 +- .../src/prove/prove_effect_subset.rs | 117 +++++++++++------- .../formality-types/src/grammar/formulas.rs | 36 +++--- 3 files changed, 87 insertions(+), 71 deletions(-) diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 4289b182..0500b0d6 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -1,8 +1,7 @@ use formality_core::{set, Set, Upcast}; use formality_macros::term; use formality_types::grammar::{ - AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, - Wcs, + AdtId, AliasName, AliasTy, AtomicEffect, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, Wcs }; use formality_types::grammar::Effect; @@ -200,7 +199,7 @@ impl TraitDecl { binder: Binder::new( &variables, TraitInvariantBoundData { - trait_ref: TraitRef::new(Effect::Runtime, &self.id, &variables), + trait_ref: TraitRef::new(AtomicEffect::Runtime, &self.id, &variables), where_clause, }, ), diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index b7230256..b8bdf8a0 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -7,52 +7,83 @@ use crate::{prove::prove_eq::prove_traitref_eq, Decls}; use super::{Constraints, Env}; -//judgment_fn! { -// pub fn prove_effect_subset( -// _decls: Decls, -// env: Env, -// assumptions: Wcs, -// f1: Effect, -// f2: Effect, -// ) => Constraints { -// debug(f1, f2, assumptions, env) -// trivial(f1 == f2 => Constraints::empty()) -// -// // fn foo() { } -// // () == () -// // -// // () == () => [?X => !T] -// -// ( -// // forall E1 in Subset -// // exists E2 in Superset -// // E1 == E2 -// -// -// --- ("union-subset-lhs") -// (prove_effect_subset(decls, env, assumptions, f1, Effect::Union(f2_1, f2_2)) => constraints) -// ) -// } -//} +judgment_fn! { + pub fn prove_effect_subset( + decls: Decls, + env: Env, + assumptions: Wcs, + subset: Effect, + superset: Effect, + ) => Constraints { + debug(subset, superset, assumptions, env) + trivial(subset == superset => Constraints::empty()) + + // (A union B) is a subset of C if + // * A is a subset of C and + // * B is a subset of C + ( + // example: imagine that `subset = union({::Effect}, {::Effect})`, and then + // + // * subset1 = `{::Effect}` and + // * superset = `{::Effect, ::Effect)` + // + // this is provable in two ways (and hence will yield two results) + // + // * first, with c1 = [?T = u32] + // * later, with c1 = [?T = i32] + (prove_effect_subset(decls, env, assumptions, subset1, superset) => c1) + + // replace any inference variables in `subset2` that got constrained + // with the value they were forced to equal + // + // continuing the example, imagine + // + // * subset2 = `{::Effect}` + // + // with the first value of `c1`, we will substitute and get + // + // * subset2 = `{u32 as Trait>::Effect}` + // + // and we will then try to prove it (which succeeds with no constraints). + // + // in second iteration, we will get `::Effect`, again provable. + (let subset2 = c1.substitution().apply(&subset2)) + + // prove that this refined version of `subset2` is true + (prove_effect_subset(decls, c1.env(), assumptions, subset2, superset) => c2) + --- ("union") + (prove_effect_subset(decls, env, assumptions, Effect::Union(subset1, subset2), superset) => c1.seq(c2)) + ) + + // If `subset` is an atomic effect, then use the `prove_atomic_effect_subset` rule + ( + (prove_atomic_effect_subset(decls, env, assumptions, subeffect, superset) => constraints) + --- ("atomic") + (prove_effect_subset(decls, env, assumptions, Effect::Atomic(subeffect), superset) => constraints) + ) + } +} judgment_fn! { - fn prove_atomic_effect_subset_effect( + /// Prove that an atomic effect appears in `superset`. + /// Search for any atomic element of superset and check that it is equal. + fn prove_atomic_effect_subset( _decls: Decls, env: Env, assumptions: Wcs, - atomic_subset: Effect, + subeffect: AtomicEffect, superset: Effect, ) => Constraints { debug(atomic_subset, superset, assumptions, env) ( // find some atomic effect in the superset... - (some_atomic_effect(superset) => atomic_superset) + (some_atomic_effect(superset) => supereffect) // ...and prove it is equal to the atomic from the subset - (prove_atomic_effect_eq(&decls, &env, &assumptions, atomic_subset, atomic_superset) => constraints) + (prove_atomic_effect_eq(&decls, &env, &assumptions, subeffect, supereffect) => constraints) --- ("union-subset-lhs") - (prove_atomic_effect_subset_effect(decls, env, assumptions, _f1, Effect::Union(_f2_1, _f2_2)) => constraints) + (prove_atomic_effect_subset_effect(decls, env, assumptions, subeffect, superset) => constraints) ) } } @@ -63,8 +94,8 @@ judgment_fn! { _decls: Decls, env: Env, assumptions: Wcs, - f1: Effect, - f2: Effect, + f1: AtomicEffect, + f2: AtomicEffect, ) => Constraints { debug(f1, f2, assumptions, env) trivial(f1 == f2 => Constraints::none(env)) @@ -72,7 +103,7 @@ judgment_fn! { ( (prove_traitref_eq(decls, env, assumptions, &*tr1, &*tr2) => constraints) --- ("associated-effect") - (prove_atomic_effect_eq(decls, env, assumptions, Effect::AssociatedEffect(tr1), Effect::AssociatedEffect(tr2)) => constraints) + (prove_atomic_effect_eq(decls, env, assumptions, AtomicEffect::AssociatedEffect(tr1), AtomicEffect::AssociatedEffect(tr2)) => constraints) ) } } @@ -88,7 +119,7 @@ pub fn collect(judgment: ProvenSet) -> ProvenSet> { judgment_fn! { fn some_atomic_effect( f1: Effect - ) => Effect { + ) => AtomicEffect { debug(f1) ( @@ -102,18 +133,8 @@ judgment_fn! { ) ( - --- ("assoc-effect") - (some_atomic_effect(Effect::AssociatedEffect(tr)) => Effect::AssociatedEffect(tr)) - ) - - ( - --- ("assoc-const") - (some_atomic_effect(Effect::Const) => Effect::Const) - ) - - ( - --- ("assoc-runtime") - (some_atomic_effect(Effect::Runtime) => Effect::Runtime) + --- ("atomic") + (some_atomic_effect(Effect::Atomic(e)) => e) ) } } \ No newline at end of file diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index 50af5406..d9659c9b 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -253,33 +253,29 @@ impl Relation { } #[term] -#[derive(Default)] pub enum Effect { + #[cast] + Atomic(AtomicEffect), + + #[grammar(EffectUnion($v0, $v1))] + Union(Arc, Arc), +} + +impl Default for Effect { + fn default() -> Self { + AtomicEffect::default().upcast() + } +} + +#[term] +#[derive(Default)] +pub enum AtomicEffect { Const, #[default] Runtime, // For >::E, TraitRef can uniquely identify an impl, and an impl has only one effect. #[grammar(AssociatedEffect($v0))] AssociatedEffect(Arc), - #[grammar(EffectUnion($v0, $v1))] - Union(Arc, Arc), -} - -impl Effect { - pub fn subset_of(&self, e1: &Effect, e2: Option) -> bool { - if *e1 == Effect::Runtime || self == e1 { - return true; - } - // If self if subset of e1, self is subset of effect union that contains e1. - if let Some(effect) = e2 { - if self.subset_of(e1, None) { - if let Effect::Union(e2, e3) = effect { - return *e2 == *e1 || *e3 == *e1; - } - } - } - false - } } #[term($?effect $trait_id ( $,parameters ))] From a02b25930fe93169e27f5e76d7525b51e4b624c0 Mon Sep 17 00:00:00 2001 From: tiif Date: Wed, 12 Mar 2025 23:27:31 +0800 Subject: [PATCH 33/65] Fix some low-hanging fruits --- .../src/prove/prove_effect_subset.rs | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index b8bdf8a0..0a4463e8 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -1,5 +1,5 @@ use formality_core::{judgment_fn, ProvenSet, Set, set}; -use formality_types::grammar::{Effect, Wcs}; +use formality_types::grammar::{AtomicEffect, Effect, Wcs}; use std::fmt::Debug; use crate::{prove::prove_eq::prove_traitref_eq, Decls}; @@ -9,14 +9,14 @@ use super::{Constraints, Env}; judgment_fn! { pub fn prove_effect_subset( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, subset: Effect, superset: Effect, ) => Constraints { debug(subset, superset, assumptions, env) - trivial(subset == superset => Constraints::empty()) + trivial(subset == superset => Constraints::none(env)) // (A union B) is a subset of C if // * A is a subset of C and @@ -31,7 +31,7 @@ judgment_fn! { // // * first, with c1 = [?T = u32] // * later, with c1 = [?T = i32] - (prove_effect_subset(decls, env, assumptions, subset1, superset) => c1) + (prove_effect_subset(decls, env, assumptions, &*subset1, superset) => c1) // replace any inference variables in `subset2` that got constrained // with the value they were forced to equal @@ -50,16 +50,16 @@ judgment_fn! { (let subset2 = c1.substitution().apply(&subset2)) // prove that this refined version of `subset2` is true - (prove_effect_subset(decls, c1.env(), assumptions, subset2, superset) => c2) + (prove_effect_subset(&decls, c1.env(), assumptions, &*subset2, superset) => c2) --- ("union") - (prove_effect_subset(decls, env, assumptions, Effect::Union(subset1, subset2), superset) => c1.seq(c2)) + (prove_effect_subset(&decls, env, assumptions, Effect::Union(subset1, subset2), superset) => c1.seq(c2)) ) // If `subset` is an atomic effect, then use the `prove_atomic_effect_subset` rule ( - (prove_atomic_effect_subset(decls, env, assumptions, subeffect, superset) => constraints) + (prove_atomic_effect_subset(&decls, env, assumptions, subeffect, superset) => constraints) --- ("atomic") - (prove_effect_subset(decls, env, assumptions, Effect::Atomic(subeffect), superset) => constraints) + (prove_effect_subset(&decls, env, assumptions, Effect::Atomic(subeffect), superset) => constraints) ) } } @@ -72,18 +72,18 @@ judgment_fn! { _decls: Decls, env: Env, assumptions: Wcs, - subeffect: AtomicEffect, + atomic_subeffect: AtomicEffect, superset: Effect, ) => Constraints { - debug(atomic_subset, superset, assumptions, env) + debug(atomic_subeffect, superset, assumptions, env) ( // find some atomic effect in the superset... (some_atomic_effect(superset) => supereffect) // ...and prove it is equal to the atomic from the subset - (prove_atomic_effect_eq(&decls, &env, &assumptions, subeffect, supereffect) => constraints) + (prove_atomic_effect_eq(&decls, &env, &assumptions, &atomic_subeffect, supereffect) => constraints) --- ("union-subset-lhs") - (prove_atomic_effect_subset_effect(decls, env, assumptions, subeffect, superset) => constraints) + (prove_atomic_effect_subset(decls, env, assumptions, &atomic_subeffect, superset) => constraints) ) } } @@ -124,7 +124,7 @@ judgment_fn! { ( --- ("union-lhs") - (some_atomic_effect(Effect::Union(f1, _f2)) => &*f1) + (some_atomic_effect(Effect::Union(f1, _f2)) => f1) ) ( From b4ce2d029d56b269d411cd3dda05e885b589bef8 Mon Sep 17 00:00:00 2001 From: tiif Date: Wed, 12 Mar 2025 23:41:28 +0800 Subject: [PATCH 34/65] Fix more errors --- .../src/prove/prove_effect_subset.rs | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index 0a4463e8..75bc6097 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -31,7 +31,7 @@ judgment_fn! { // // * first, with c1 = [?T = u32] // * later, with c1 = [?T = i32] - (prove_effect_subset(decls, env, assumptions, &*subset1, superset) => c1) + (prove_effect_subset(&decls, env, &assumptions, &*subset1, &superset) => c1) // replace any inference variables in `subset2` that got constrained // with the value they were forced to equal @@ -50,16 +50,16 @@ judgment_fn! { (let subset2 = c1.substitution().apply(&subset2)) // prove that this refined version of `subset2` is true - (prove_effect_subset(&decls, c1.env(), assumptions, &*subset2, superset) => c2) + (prove_effect_subset(&decls, c1.env(), &assumptions, &*subset2, &superset) => c2) --- ("union") - (prove_effect_subset(&decls, env, assumptions, Effect::Union(subset1, subset2), superset) => c1.seq(c2)) + (prove_effect_subset(decls, env, assumptions, Effect::Union(subset1, subset2), superset) => c1.seq(c2)) ) // If `subset` is an atomic effect, then use the `prove_atomic_effect_subset` rule ( (prove_atomic_effect_subset(&decls, env, assumptions, subeffect, superset) => constraints) --- ("atomic") - (prove_effect_subset(&decls, env, assumptions, Effect::Atomic(subeffect), superset) => constraints) + (prove_effect_subset(decls, env, assumptions, Effect::Atomic(subeffect), superset) => constraints) ) } } @@ -83,7 +83,7 @@ judgment_fn! { // ...and prove it is equal to the atomic from the subset (prove_atomic_effect_eq(&decls, &env, &assumptions, &atomic_subeffect, supereffect) => constraints) --- ("union-subset-lhs") - (prove_atomic_effect_subset(decls, env, assumptions, &atomic_subeffect, superset) => constraints) + (prove_atomic_effect_subset(decls, env, assumptions, atomic_subeffect, superset) => constraints) ) } } @@ -116,6 +116,7 @@ pub fn collect(judgment: ProvenSet) -> ProvenSet> { } } +// TODO: try to convert this to using collect? judgment_fn! { fn some_atomic_effect( f1: Effect @@ -124,7 +125,7 @@ judgment_fn! { ( --- ("union-lhs") - (some_atomic_effect(Effect::Union(f1, _f2)) => f1) + (some_atomic_effect(Effect::Union(f1, _f2)) => &*f1) ) ( From 4354ad4ee156065ca70b1b32aaeb8c29a9ffb16e Mon Sep 17 00:00:00 2001 From: tiif Date: Wed, 12 Mar 2025 23:54:21 +0800 Subject: [PATCH 35/65] Add some assumptions to make some_atomic_effect works --- crates/formality-prove/src/prove/prove_effect_subset.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index 75bc6097..b9242bfb 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -90,6 +90,7 @@ judgment_fn! { judgment_fn! { + /// Prove two atomic effects are equal. fn prove_atomic_effect_eq( _decls: Decls, env: Env, @@ -124,13 +125,15 @@ judgment_fn! { debug(f1) ( + (if let Effect::Atomic(e) = *f1)! --- ("union-lhs") - (some_atomic_effect(Effect::Union(f1, _f2)) => &*f1) + (some_atomic_effect(Effect::Union(f1, _f2)) => e) ) ( + (if let Effect::Atomic(e) = *f2)! --- ("union-rhs") - (some_atomic_effect(Effect::Union(_f1, f2)) => &*f2) + (some_atomic_effect(Effect::Union(_f1, f2)) => e) ) ( From f36ca3e56005bf2fb32a9325b744a069326ef484 Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 13 Mar 2025 00:00:18 +0800 Subject: [PATCH 36/65] Use prove_effect_subset in prove_wc --- .../src/prove/prove_effect_subset.rs | 3 ++- crates/formality-prove/src/prove/prove_wc.rs | 13 +++---------- 2 files changed, 5 insertions(+), 11 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index b9242bfb..3ca18788 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -8,6 +8,7 @@ use super::{Constraints, Env}; judgment_fn! { + /// Prove an effect is the subset of another effect. pub fn prove_effect_subset( _decls: Decls, env: Env, @@ -117,8 +118,8 @@ pub fn collect(judgment: ProvenSet) -> ProvenSet> { } } -// TODO: try to convert this to using collect? judgment_fn! { + /// Get any atomic effect from an Effect::Union. fn some_atomic_effect( f1: Effect ) => AtomicEffect { diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index 78480d9f..48d5ca5a 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -4,14 +4,7 @@ use formality_types::grammar::{Predicate, Relation, Wc, WcData, Wcs}; use crate::{ decls::Decls, prove::{ - combinators::for_all, - env::{Bias, 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, + env::{Bias, Env}, is_local::{is_local_trait_ref, may_be_remote}, prove, prove_after::prove_after, prove_effect_subset::prove_effect_subset, prove_eq::prove_eq, prove_via::prove_via, prove_wf::prove_wf }, }; @@ -134,9 +127,9 @@ judgment_fn! { (prove_wc(decls, env, assumptions, Predicate::ConstHasType(ct, ty)) => c) ) ( - (if e1.subset_of(&e2, None) == true) + (prove_effect_subset(decls, env, assumptions, e1, e2) => c) ------------------------ ("effect subset") - (prove_wc(_decls, env, _assumptions, Predicate::EffectSubset(e1, e2)) => Constraints::none(env)) + (prove_wc(decls, env, assumptions, Predicate::EffectSubset(e1, e2)) => c) ) } } From 862567bc93a255140f5ce4a0188e6d20f07037ca Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 13 Mar 2025 00:05:08 +0800 Subject: [PATCH 37/65] Make everything compiles --- crates/formality-check/src/impls.rs | 3 ++- crates/formality-rust/src/grammar.rs | 7 ++++--- crates/formality-rust/src/prove.rs | 9 +++++---- 3 files changed, 11 insertions(+), 8 deletions(-) diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index a534a053..dbd76dc0 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -15,6 +15,7 @@ use formality_types::{ grammar::{Binder, Effect, Fallible, Relation, Substitution, Wcs}, rust::Term, }; +use formality_types::grammar::AtomicEffect::Runtime; impl super::Check<'_> { #[context("check_trait_impl({trait_impl:?})")] @@ -69,7 +70,7 @@ impl super::Check<'_> { where_clauses, } = env.instantiate_universally(binder); - let trait_ref = trait_id.with(&Effect::Runtime, self_ty, trait_parameters); + let trait_ref = trait_id.with(&Effect::Atomic(Runtime), self_ty, trait_parameters); // Negative impls are always safe (rustc E0198) regardless of the trait's safety. if *safety == Safety::Unsafe { diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 96aa2e18..88f97675 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -10,6 +10,7 @@ use formality_types::{ }, rust::Term, }; +use formality_types::grammar::AtomicEffect::Runtime; use crate::grammar::mir::MirFnBody; @@ -306,7 +307,7 @@ pub struct NegTraitImplBoundData { impl NegTraitImplBoundData { pub fn trait_ref(&self) -> TraitRef { - self.trait_id.with(&Effect::Runtime, &self.self_ty, &self.trait_parameters) + self.trait_id.with(&Effect::Atomic(Runtime), &self.self_ty, &self.trait_parameters) } } @@ -344,7 +345,7 @@ impl WhereClause { match self.data() { WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => Some( trait_id - .with(&Effect::Runtime, self_ty, parameters) + .with(&Effect::Atomic(Runtime), self_ty, parameters) .not_implemented() .upcast(), ), @@ -362,7 +363,7 @@ impl WhereClause { pub fn well_formed(&self) -> Wcs { match self.data() { WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => { - trait_id.with(&Effect::Runtime, self_ty, parameters).well_formed().upcast() + trait_id.with(&Effect::Atomic(Runtime), self_ty, parameters).well_formed().upcast() } WhereClauseData::AliasEq(alias_ty, ty) => { let alias_param: Parameter = alias_ty.upcast(); diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index 223b19db..25365d3b 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -9,6 +9,7 @@ use formality_prove as prove; use formality_types::grammar::{ AdtId, AliasTy, Binder, BoundVar, Effect, ParameterKind, Predicate, Relation, TraitId, Ty, Wc, Wcs, }; +use formality_types::grammar::AtomicEffect::Runtime; impl Program { pub fn to_prove_decls(&self) -> prove::Decls { @@ -130,7 +131,7 @@ impl Crate { binder: Binder::new( vars, prove::ImplDeclBoundData { - trait_ref: trait_id.with(&Effect::Runtime, self_ty, trait_parameters), + trait_ref: trait_id.with(&Effect::Atomic(Runtime), self_ty, trait_parameters), where_clause: where_clauses.to_wcs(), }, ), @@ -160,7 +161,7 @@ impl Crate { binder: Binder::new( vars, prove::NegImplDeclBoundData { - trait_ref: trait_id.with(&Effect::Runtime, self_ty, trait_parameters), + trait_ref: trait_id.with(&Effect::Atomic(Runtime), self_ty, trait_parameters), where_clause: where_clauses.to_wcs(), }, ), @@ -416,7 +417,7 @@ impl ToWcs for WhereClause { fn to_wcs(&self) -> Wcs { match self.data() { WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => { - trait_id.with(&Effect::Runtime, self_ty, parameters).upcast() + trait_id.with(&Effect::Atomic(Runtime), self_ty, parameters).upcast() } WhereClauseData::AliasEq(alias_ty, ty) => { Predicate::AliasEq(alias_ty.clone(), ty.clone()).upcast() @@ -442,7 +443,7 @@ impl WhereBound { match self.data() { WhereBoundData::IsImplemented(trait_id, parameters) => { - trait_id.with(&Effect::Runtime, self_ty, parameters).upcast() + trait_id.with(&Effect::Atomic(Runtime), self_ty, parameters).upcast() } WhereBoundData::Outlives(lt) => Relation::outlives(self_ty, lt).upcast(), WhereBoundData::ForAll(binder) => { From a5b833ecd31426d33bb38b90b44e0d5445432a66 Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 13 Mar 2025 00:06:00 +0800 Subject: [PATCH 38/65] Run fmt --- crates/formality-check/src/impls.rs | 2 +- crates/formality-prove/src/decls.rs | 5 ++- crates/formality-prove/src/prove.rs | 2 +- .../src/prove/prove_effect_subset.rs | 13 +++--- crates/formality-prove/src/prove/prove_eq.rs | 10 ++--- crates/formality-prove/src/prove/prove_wc.rs | 9 ++++- crates/formality-rust/src/grammar.rs | 18 ++++++--- crates/formality-rust/src/prove.rs | 40 +++++++++++++------ crates/formality-types/src/grammar/ty.rs | 3 +- 9 files changed, 64 insertions(+), 38 deletions(-) diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index dbd76dc0..99c427d1 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -11,11 +11,11 @@ use formality_rust::{ }, prove::ToWcs, }; +use formality_types::grammar::AtomicEffect::Runtime; use formality_types::{ grammar::{Binder, Effect, Fallible, Relation, Substitution, Wcs}, rust::Term, }; -use formality_types::grammar::AtomicEffect::Runtime; impl super::Check<'_> { #[context("check_trait_impl({trait_impl:?})")] diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 0500b0d6..948e3112 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -1,9 +1,10 @@ use formality_core::{set, Set, Upcast}; use formality_macros::term; +use formality_types::grammar::Effect; use formality_types::grammar::{ - AdtId, AliasName, AliasTy, AtomicEffect, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, Wcs + AdtId, AliasName, AliasTy, AtomicEffect, Binder, Parameter, Predicate, Relation, TraitId, + TraitRef, Ty, Wc, Wcs, }; -use formality_types::grammar::Effect; #[term] pub struct Decls { diff --git a/crates/formality-prove/src/prove.rs b/crates/formality-prove/src/prove.rs index 48784626..dcb75367 100644 --- a/crates/formality-prove/src/prove.rs +++ b/crates/formality-prove/src/prove.rs @@ -5,13 +5,13 @@ mod is_local; mod minimize; mod negation; mod prove_after; +mod prove_effect_subset; mod prove_eq; mod prove_normalize; mod prove_via; mod prove_wc; mod prove_wc_list; mod prove_wf; -mod prove_effect_subset; pub use constraints::Constraints; use formality_core::judgment::{FailedRule, TryIntoIter}; diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index 3ca18788..123137d9 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -1,4 +1,4 @@ -use formality_core::{judgment_fn, ProvenSet, Set, set}; +use formality_core::{judgment_fn, set, ProvenSet, Set}; use formality_types::grammar::{AtomicEffect, Effect, Wcs}; use std::fmt::Debug; @@ -6,9 +6,8 @@ use crate::{prove::prove_eq::prove_traitref_eq, Decls}; use super::{Constraints, Env}; - judgment_fn! { - /// Prove an effect is the subset of another effect. + /// Prove an effect is the subset of another effect. pub fn prove_effect_subset( _decls: Decls, env: Env, @@ -65,7 +64,6 @@ judgment_fn! { } } - judgment_fn! { /// Prove that an atomic effect appears in `superset`. /// Search for any atomic element of superset and check that it is equal. @@ -89,9 +87,8 @@ judgment_fn! { } } - judgment_fn! { - /// Prove two atomic effects are equal. + /// Prove two atomic effects are equal. fn prove_atomic_effect_eq( _decls: Decls, env: Env, @@ -119,7 +116,7 @@ pub fn collect(judgment: ProvenSet) -> ProvenSet> { } judgment_fn! { - /// Get any atomic effect from an Effect::Union. + /// Get any atomic effect from an Effect::Union. fn some_atomic_effect( f1: Effect ) => AtomicEffect { @@ -142,4 +139,4 @@ judgment_fn! { (some_atomic_effect(Effect::Atomic(e)) => e) ) } -} \ No newline at end of file +} diff --git a/crates/formality-prove/src/prove/prove_eq.rs b/crates/formality-prove/src/prove/prove_eq.rs index c5b19bee..3c25d52f 100644 --- a/crates/formality-prove/src/prove/prove_eq.rs +++ b/crates/formality-prove/src/prove/prove_eq.rs @@ -1,12 +1,12 @@ use formality_core::visit::CoreVisit; use formality_core::{judgment_fn, Downcast, ProvenSet, Upcast, UpcastFrom}; use formality_core::{Deduplicate, Upcasted}; -use formality_types::grammar::{ - AliasTy, ExistentialVar, Parameter, Relation, RigidTy, Substitution, TyData, UniversalVar, Variable, Wc, Wcs -}; use formality_types::grammar::TraitRef; use formality_types::grammar::WcData; - +use formality_types::grammar::{ + AliasTy, ExistentialVar, Parameter, Relation, RigidTy, Substitution, TyData, UniversalVar, + Variable, Wc, Wcs, +}; use crate::{ decls::Decls, @@ -87,7 +87,7 @@ judgment_fn! { trivial(a == b => Constraints::none(env)) - // Two trait_refs are equal if they have the same id, effect, and parameters. + // Two trait_refs are equal if they have the same id, effect, and parameters. ( (let TraitRef { effect: a_effect, trait_id: a_trait_id, parameters: a_parameters } = a) (let TraitRef { effect: b_effect, trait_id: b_trait_id, parameters: b_parameters } = b) diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index 48d5ca5a..71147d9b 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -4,7 +4,14 @@ use formality_types::grammar::{Predicate, Relation, Wc, WcData, Wcs}; use crate::{ decls::Decls, prove::{ - env::{Bias, Env}, is_local::{is_local_trait_ref, may_be_remote}, prove, prove_after::prove_after, prove_effect_subset::prove_effect_subset, prove_eq::prove_eq, prove_via::prove_via, prove_wf::prove_wf + env::{Bias, Env}, + is_local::{is_local_trait_ref, may_be_remote}, + prove, + prove_after::prove_after, + prove_effect_subset::prove_effect_subset, + prove_eq::prove_eq, + prove_via::prove_via, + prove_wf::prove_wf, }, }; diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 88f97675..742f5e7b 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -2,6 +2,7 @@ use std::sync::Arc; use formality_core::{term, Upcast}; use formality_prove::Safety; +use formality_types::grammar::AtomicEffect::Runtime; use formality_types::grammar::Effect; use formality_types::{ grammar::{ @@ -10,7 +11,6 @@ use formality_types::{ }, rust::Term, }; -use formality_types::grammar::AtomicEffect::Runtime; use crate::grammar::mir::MirFnBody; @@ -287,7 +287,8 @@ pub struct TraitImplBoundData { impl TraitImplBoundData { pub fn trait_ref(&self) -> TraitRef { - self.trait_id.with(&self.effect, &self.self_ty, &self.trait_parameters) + self.trait_id + .with(&self.effect, &self.self_ty, &self.trait_parameters) } } @@ -307,7 +308,11 @@ pub struct NegTraitImplBoundData { impl NegTraitImplBoundData { pub fn trait_ref(&self) -> TraitRef { - self.trait_id.with(&Effect::Atomic(Runtime), &self.self_ty, &self.trait_parameters) + self.trait_id.with( + &Effect::Atomic(Runtime), + &self.self_ty, + &self.trait_parameters, + ) } } @@ -362,9 +367,10 @@ impl WhereClause { pub fn well_formed(&self) -> Wcs { match self.data() { - WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => { - trait_id.with(&Effect::Atomic(Runtime), self_ty, parameters).well_formed().upcast() - } + WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => trait_id + .with(&Effect::Atomic(Runtime), self_ty, parameters) + .well_formed() + .upcast(), WhereClauseData::AliasEq(alias_ty, ty) => { let alias_param: Parameter = alias_ty.upcast(); let ty_param: Parameter = ty.upcast(); diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index 25365d3b..b516fb74 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -6,10 +6,11 @@ use crate::grammar::{ }; use formality_core::{seq, Set, To, Upcast, Upcasted}; use formality_prove as prove; +use formality_types::grammar::AtomicEffect::Runtime; use formality_types::grammar::{ - AdtId, AliasTy, Binder, BoundVar, Effect, ParameterKind, Predicate, Relation, TraitId, Ty, Wc, Wcs, + AdtId, AliasTy, Binder, BoundVar, Effect, ParameterKind, Predicate, Relation, TraitId, Ty, Wc, + Wcs, }; -use formality_types::grammar::AtomicEffect::Runtime; impl Program { pub fn to_prove_decls(&self) -> prove::Decls { @@ -81,7 +82,12 @@ impl Crate { self.items .iter() .flat_map(|item| match item { - CrateItem::Trait(Trait { id, binder, safety, effect}) => { + CrateItem::Trait(Trait { + id, + binder, + safety, + effect, + }) => { let ( vars, TraitBoundData { @@ -131,12 +137,16 @@ impl Crate { binder: Binder::new( vars, prove::ImplDeclBoundData { - trait_ref: trait_id.with(&Effect::Atomic(Runtime), self_ty, trait_parameters), + trait_ref: trait_id.with( + &Effect::Atomic(Runtime), + self_ty, + trait_parameters, + ), where_clause: where_clauses.to_wcs(), }, ), }) - }, + } _ => None, }) .collect() @@ -161,7 +171,11 @@ impl Crate { binder: Binder::new( vars, prove::NegImplDeclBoundData { - trait_ref: trait_id.with(&Effect::Atomic(Runtime), self_ty, trait_parameters), + trait_ref: trait_id.with( + &Effect::Atomic(Runtime), + self_ty, + trait_parameters, + ), where_clause: where_clauses.to_wcs(), }, ), @@ -221,7 +235,7 @@ impl Crate { }, ), }) - }, + } })) } _ => vec![], @@ -416,9 +430,9 @@ impl ToWcs for [WhereClause] { impl ToWcs for WhereClause { fn to_wcs(&self) -> Wcs { match self.data() { - WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => { - trait_id.with(&Effect::Atomic(Runtime), self_ty, parameters).upcast() - } + WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => trait_id + .with(&Effect::Atomic(Runtime), self_ty, parameters) + .upcast(), WhereClauseData::AliasEq(alias_ty, ty) => { Predicate::AliasEq(alias_ty.clone(), ty.clone()).upcast() } @@ -442,9 +456,9 @@ impl WhereBound { let self_ty: Ty = self_ty.upcast(); match self.data() { - WhereBoundData::IsImplemented(trait_id, parameters) => { - trait_id.with(&Effect::Atomic(Runtime), self_ty, parameters).upcast() - } + WhereBoundData::IsImplemented(trait_id, parameters) => trait_id + .with(&Effect::Atomic(Runtime), self_ty, parameters) + .upcast(), WhereBoundData::Outlives(lt) => Relation::outlives(self_ty, lt).upcast(), WhereBoundData::ForAll(binder) => { let (vars, bound) = binder.open(); diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs index b51329d4..8284e10e 100644 --- a/crates/formality-types/src/grammar/ty.rs +++ b/crates/formality-types/src/grammar/ty.rs @@ -7,7 +7,8 @@ mod term_impls; use formality_core::{DowncastTo, To, Upcast, UpcastFrom}; use super::{ - consts::Const, AdtId, AssociatedItemId, Binder, BoundVar, ExistentialVar, FnId, TraitId, UniversalVar, Variable + consts::Const, AdtId, AssociatedItemId, Binder, BoundVar, ExistentialVar, FnId, TraitId, + UniversalVar, Variable, }; #[term] From cead2c315ce597b4e95fdc8be184f0694f17f8ce Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 13 Mar 2025 00:06:19 +0800 Subject: [PATCH 39/65] Run more fmt --- tests/const_trait.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/const_trait.rs b/tests/const_trait.rs index e3a35745..6f344678 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -23,4 +23,3 @@ fn test_const_syntax() { test_program_ok(&gen_program("")).assert_ok(expect_test::expect!["()"]); } - From c7f359a4e6f78bdefce0d346f1a2d96e2eee47e2 Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 13 Mar 2025 15:37:43 +0800 Subject: [PATCH 40/65] Move EffectSubset from Predicate to Relation --- crates/formality-prove/src/prove/prove_wc.rs | 2 +- crates/formality-types/src/grammar/formulas.rs | 18 +++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index 71147d9b..dd567432 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -136,7 +136,7 @@ judgment_fn! { ( (prove_effect_subset(decls, env, assumptions, e1, e2) => c) ------------------------ ("effect subset") - (prove_wc(decls, env, assumptions, Predicate::EffectSubset(e1, e2)) => c) + (prove_wc(decls, env, assumptions, Relation::EffectSubset(e1, e2)) => c) ) } } diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index d9659c9b..c08c11e3 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -45,10 +45,6 @@ pub enum Predicate { #[grammar(@ConstHasType($v0, $v1))] ConstHasType(Const, Ty), - - // FIXME: should be in `Relation` - #[grammar(@EffectSubset($v0, $v1))] - EffectSubset(Effect, Effect), } /// A coinductive predicate is one that can be proven via a cycle. @@ -183,11 +179,6 @@ impl Predicate { parameters: vec![ct.clone().upcast(), ty.clone().upcast()], effects: Default::default(), }, - Predicate::EffectSubset(e1, e2) => DebonedPredicate { - skeleton: Skeleton::EffectSubset, - parameters: Default::default(), - effects: vec![e1, e2].upcast(), - }, } } } @@ -222,6 +213,10 @@ pub enum Relation { #[grammar(@wf($v0))] WellFormed(Parameter), + + // Means that the effects `$v0` are a subset of `$v1`. + #[grammar(subset($v0, $v1))] + EffectSubset(Effect, Effect), } impl Relation { @@ -248,6 +243,11 @@ impl Relation { parameters: vec![p.clone()], effects: Default::default(), }, + Relation::EffectSubset(e1, e2) => DebonedPredicate { + skeleton: Skeleton::EffectSubset, + parameters: Default::default(), + effects: vec![e1, e2].upcast(), + }, } } } From 6192d81a3072853be3172ad0427c0df94797fef0 Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 14 Mar 2025 21:49:04 +0800 Subject: [PATCH 41/65] Change the premises in some_atomic_effect --- crates/formality-prove/src/prove/prove_effect_subset.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index 123137d9..5d99397e 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -123,13 +123,13 @@ judgment_fn! { debug(f1) ( - (if let Effect::Atomic(e) = *f1)! + (some_atomic_effect(&*f1) => e) --- ("union-lhs") (some_atomic_effect(Effect::Union(f1, _f2)) => e) ) ( - (if let Effect::Atomic(e) = *f2)! + (some_atomic_effect(&*f2) => e) --- ("union-rhs") (some_atomic_effect(Effect::Union(_f1, f2)) => e) ) From 21350781142bc87ef1be137817b74c48aca85227 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 14 Mar 2025 14:26:28 +0000 Subject: [PATCH 42/65] add comments to prove_eq --- crates/formality-prove/src/prove/prove_eq.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/crates/formality-prove/src/prove/prove_eq.rs b/crates/formality-prove/src/prove/prove_eq.rs index 3c25d52f..73eb0ca0 100644 --- a/crates/formality-prove/src/prove/prove_eq.rs +++ b/crates/formality-prove/src/prove/prove_eq.rs @@ -66,8 +66,21 @@ judgment_fn! { (prove_eq(decls, env, assumptions, Variable::ExistentialVar(v), r) => c) ) + // Example: we are trying to prove `x` (which equals ` as Iterator>::Item`) + // is equal to some type `z`. ( + // Normalize `x` will find alternative "spellings" that it is equivalent to. + // For example, if there is an impl like + // `impl Iterator for SomeX { type Item = u32; ... }` + // then `prove_normalize` would yield `(c, u32)` where `c` are any constraints + // needed to show that it normalized (in this case, `c` would include the + // substitution `?V = i32`). (prove_normalize(&decls, env, &assumptions, &x) => (c, y)) + + // Now that we know that `x` is equivalent to `y`, we try to prove + // that `y` is equivalent to `z` (our original goal). + // We do that with `prove_after` so that the constraints `c` are considered + // (e.g., if `z` includes `?V`, it will be replaced with `i32`). (prove_after(&decls, c, &assumptions, eq(y, &z)) => c) ----------------------------- ("normalize-l") (prove_eq(decls, env, assumptions, x, z) => c) From fc6fe5fe32d40821bd58f237280fdf14b21646d8 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 14 Mar 2025 14:26:41 +0000 Subject: [PATCH 43/65] use prove_after (horray!) --- .../src/prove/prove_effect_subset.rs | 38 ++++--------------- 1 file changed, 7 insertions(+), 31 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index 5d99397e..56d26a59 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -1,8 +1,8 @@ use formality_core::{judgment_fn, set, ProvenSet, Set}; -use formality_types::grammar::{AtomicEffect, Effect, Wcs}; +use formality_types::grammar::{AtomicEffect, Effect, Relation, Wcs}; use std::fmt::Debug; -use crate::{prove::prove_eq::prove_traitref_eq, Decls}; +use crate::{prove::{prove_after::prove_after, prove_eq::prove_traitref_eq}, Decls}; use super::{Constraints, Env}; @@ -22,37 +22,13 @@ judgment_fn! { // * A is a subset of C and // * B is a subset of C ( - // example: imagine that `subset = union({::Effect}, {::Effect})`, and then - // - // * subset1 = `{::Effect}` and - // * superset = `{::Effect, ::Effect)` - // - // this is provable in two ways (and hence will yield two results) - // - // * first, with c1 = [?T = u32] - // * later, with c1 = [?T = i32] - (prove_effect_subset(&decls, env, &assumptions, &*subset1, &superset) => c1) + // first prove that `A -subset- C` + (prove_effect_subset(&decls, env, &assumptions, &*subset1, &superset) => c) - // replace any inference variables in `subset2` that got constrained - // with the value they were forced to equal - // - // continuing the example, imagine - // - // * subset2 = `{::Effect}` - // - // with the first value of `c1`, we will substitute and get - // - // * subset2 = `{u32 as Trait>::Effect}` - // - // and we will then try to prove it (which succeeds with no constraints). - // - // in second iteration, we will get `::Effect`, again provable. - (let subset2 = c1.substitution().apply(&subset2)) - - // prove that this refined version of `subset2` is true - (prove_effect_subset(&decls, c1.env(), &assumptions, &*subset2, &superset) => c2) + // now prove that `B -subset- C` + (prove_after(&decls, c, &assumptions, Relation::effect_subset(&*subset2, &superset)) => c) --- ("union") - (prove_effect_subset(decls, env, assumptions, Effect::Union(subset1, subset2), superset) => c1.seq(c2)) + (prove_effect_subset(decls, env, assumptions, Effect::Union(subset1, subset2), superset) => c) ) // If `subset` is an atomic effect, then use the `prove_atomic_effect_subset` rule From d5378b76afd01fe2da0798dd2baad3b8b02071c8 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 14 Mar 2025 14:33:59 +0000 Subject: [PATCH 44/65] WIP add supereffects --- .../src/prove/prove_effect_subset.rs | 32 +++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index 56d26a59..7d9285c7 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -60,9 +60,41 @@ judgment_fn! { --- ("union-subset-lhs") (prove_atomic_effect_subset(decls, env, assumptions, atomic_subeffect, superset) => constraints) ) + + // Example: we are trying to prove `X <= S` + ( + // If we can find some other effect `B` such that `X <= B`... + (prove_effect_upper_bound(&decls, env, &assumptions, &atomic_subeffect) => (c, bounding_effect)) + + // ...and we can prove `B <= S`, then we know `X <= S` (transitivity). + (prove_after(&decls, c, &assumptions, Relation::effect_subset(&*bounding_effect, &superset)) => c) + ----------------------------- ("transitive") + (prove_atomic_effect_subset(decls, env, assumptions, atomic_subeffect, superset) => c) + ) + } } + +judgment_fn! { + /// `prove_effect_bound(..., a) => b` means that `a <= b` + fn prove_effect_upper_bound( + _decls: Decls, + env: Env, + assumptions: Wcs, + f1: AtomicEffect, + ) => (Constraints, AtomicEffect) { + debug(f1, assumptions, env) + + + ( + --- ("runtime bounded by const") + (prove_effect_upper_bound(decls, env, assumptions, AtomicEffect::Const) => (Constraints::none(env), AtomicEffect::Runtime)) + ) + } +} + + judgment_fn! { /// Prove two atomic effects are equal. fn prove_atomic_effect_eq( From c5cb3c9874808b42024be7489d9853c0ba8c9713 Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 18 Mar 2025 22:29:58 +0800 Subject: [PATCH 45/65] Make it compile --- crates/formality-prove/src/prove/prove_effect_subset.rs | 4 ++-- crates/formality-prove/src/test/test_effect_subset.rs | 5 +++++ 2 files changed, 7 insertions(+), 2 deletions(-) create mode 100644 crates/formality-prove/src/test/test_effect_subset.rs diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index 7d9285c7..5b3cbce2 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -67,7 +67,7 @@ judgment_fn! { (prove_effect_upper_bound(&decls, env, &assumptions, &atomic_subeffect) => (c, bounding_effect)) // ...and we can prove `B <= S`, then we know `X <= S` (transitivity). - (prove_after(&decls, c, &assumptions, Relation::effect_subset(&*bounding_effect, &superset)) => c) + (prove_after(&decls, c, &assumptions, Relation::effect_subset(bounding_effect, &superset)) => c) ----------------------------- ("transitive") (prove_atomic_effect_subset(decls, env, assumptions, atomic_subeffect, superset) => c) ) @@ -89,7 +89,7 @@ judgment_fn! { ( --- ("runtime bounded by const") - (prove_effect_upper_bound(decls, env, assumptions, AtomicEffect::Const) => (Constraints::none(env), AtomicEffect::Runtime)) + (prove_effect_upper_bound(_decls, env, _assumptions, AtomicEffect::Const) => (Constraints::none(env), AtomicEffect::Runtime)) ) } } diff --git a/crates/formality-prove/src/test/test_effect_subset.rs b/crates/formality-prove/src/test/test_effect_subset.rs new file mode 100644 index 00000000..6c2b94b9 --- /dev/null +++ b/crates/formality-prove/src/test/test_effect_subset.rs @@ -0,0 +1,5 @@ +#[test] +fn test_some_atomic_effect() { + let goal: Wc = term("Debug(Vec)"); + prove(decls(), (), (), goal).assert_ok(expect![[]]); +} \ No newline at end of file From 38b6143dd3f00e2e2d0807c0efd24024a3336f9c Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 18 Mar 2025 23:03:36 +0800 Subject: [PATCH 46/65] Fix rebase error --- crates/formality-prove/src/prove/prove_via.rs | 4 ---- crates/formality-prove/src/prove/prove_wc.rs | 1 + 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_via.rs b/crates/formality-prove/src/prove/prove_via.rs index e13c9c58..0d89ff56 100644 --- a/crates/formality-prove/src/prove/prove_via.rs +++ b/crates/formality-prove/src/prove/prove_via.rs @@ -61,10 +61,6 @@ judgment_fn! { ( // if the goal is `T: Foo`... (prove_via(&decls, env, &assumptions, wc_consequence, goal) => c) -<<<<<<< HEAD -======= - ->>>>>>> 1c31da9 (comments + newtype for DebonedPredicate) // ...and we can prove `T: Debug`... then it holds. (prove_after(&decls, c, &assumptions, &wc_condition) => c) ----------------------------- ("implies") diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index dd567432..caa49ed1 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -4,6 +4,7 @@ use formality_types::grammar::{Predicate, Relation, Wc, WcData, Wcs}; use crate::{ decls::Decls, prove::{ + combinators::for_all, env::{Bias, Env}, is_local::{is_local_trait_ref, may_be_remote}, prove, From 459384237d078fc18ef889afece0a082085331e1 Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 20 Mar 2025 01:46:23 +0800 Subject: [PATCH 47/65] Add test for effect subset --- crates/formality-prove/src/test.rs | 1 + .../src/test/test_effect_subset.rs | 222 +++++++++++++++++- 2 files changed, 220 insertions(+), 3 deletions(-) diff --git a/crates/formality-prove/src/test.rs b/crates/formality-prove/src/test.rs index f04b7e12..f3feb4e3 100644 --- a/crates/formality-prove/src/test.rs +++ b/crates/formality-prove/src/test.rs @@ -8,3 +8,4 @@ mod magic_copy; mod occurs_check; mod simple_impl; mod universes; +mod test_effect_subset; diff --git a/crates/formality-prove/src/test/test_effect_subset.rs b/crates/formality-prove/src/test/test_effect_subset.rs index 6c2b94b9..9149c686 100644 --- a/crates/formality-prove/src/test/test_effect_subset.rs +++ b/crates/formality-prove/src/test/test_effect_subset.rs @@ -1,5 +1,221 @@ + +use std::sync::Arc; + +use expect_test::expect; +use formality_macros::test; +use formality_types::grammar::{AtomicEffect, Effect, Relation, Wcs}; + +use crate::{decls::Decls, prove::prove, Env}; + #[test] -fn test_some_atomic_effect() { - let goal: Wc = term("Debug(Vec)"); - prove(decls(), (), (), goal).assert_ok(expect![[]]); +fn test_effect_subset_success() { + let runtime_eff = Effect::Atomic(AtomicEffect::Runtime); + let const_eff = Effect::Atomic(AtomicEffect::Const); + let runtime_const_union = Effect::Union(Arc::new(runtime_eff.clone()), Arc::new(const_eff.clone())); + // Test (runtime) <: (runtime, const) + let constraint_0 = prove(Decls::empty(), Env::default(), Wcs::t(), Relation::EffectSubset(runtime_eff.clone(), runtime_const_union.clone())); + expect![[r#" + { + Constraints { + env: Env { + variables: [], + bias: Soundness, + }, + known_true: true, + substitution: {}, + }, + } + "#]] + .assert_debug_eq(&constraint_0); + // Test (const) <: (runtime, const) + let constraint_1 = prove(Decls::empty(), Env::default(), Wcs::t(), Relation::EffectSubset(const_eff.clone(), runtime_const_union.clone())); + expect![[r#" + { + Constraints { + env: Env { + variables: [], + bias: Soundness, + }, + known_true: true, + substitution: {}, + }, + } + "#]] + .assert_debug_eq(&constraint_1); + // Test (const) <: (runtime) + let constraint_2 = prove(Decls::empty(), Env::default(), Wcs::t(), Relation::EffectSubset(const_eff.clone(), runtime_eff.clone())); + expect![[r#" + { + Constraints { + env: Env { + variables: [], + bias: Soundness, + }, + known_true: true, + substitution: {}, + }, + } + "#]] + .assert_debug_eq(&constraint_2); + // Test (const, runtime) <: (runtime) + let constraint_3 = prove(Decls::empty(), Env::default(), Wcs::t(), Relation::EffectSubset(runtime_const_union.clone(), runtime_eff.clone())); + expect![[r#" + { + Constraints { + env: Env { + variables: [], + bias: Soundness, + }, + known_true: true, + substitution: {}, + }, + } + "#]] + .assert_debug_eq(&constraint_3); + +} + +#[test] +fn test_effect_subset_failure() { + let runtime_eff = Effect::Atomic(AtomicEffect::Runtime); + let const_eff = Effect::Atomic(AtomicEffect::Const); + + // Runtime is not subset of const. + // FIXME: the test output can be better? + let constraint = prove(Decls::empty(), Env::default(), Wcs::t(), Relation::EffectSubset(runtime_eff.clone(), const_eff.clone())); + expect![[r#" + FailedJudgment { + judgment: "prove { goal: {subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }", + failed_rules: { + FailedRule { + rule_name_index: None, + file: "crates/formality-prove/src/prove.rs", + line: 70, + column: 59, + cause: FailedJudgment( + FailedJudgment { + judgment: "prove_wc_list { goal: {subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }", + failed_rules: { + FailedRule { + rule_name_index: Some( + ( + "some", + 0, + ), + ), + file: "crates/formality-prove/src/prove/prove_wc_list.rs", + line: 28, + column: 14, + cause: FailedJudgment( + FailedJudgment { + judgment: "prove_wc { goal: subset(runtime , const), assumptions: {}, env: Env { variables: [], bias: Soundness } }", + failed_rules: { + FailedRule { + rule_name_index: Some( + ( + "effect subset", + 0, + ), + ), + file: "crates/formality-prove/src/prove/prove_wc.rs", + line: 138, + column: 14, + cause: FailedJudgment( + FailedJudgment { + judgment: "prove_effect_subset { subset: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }", + failed_rules: { + FailedRule { + rule_name_index: Some( + ( + "atomic", + 0, + ), + ), + file: "crates/formality-prove/src/prove/prove_effect_subset.rs", + line: 36, + column: 14, + cause: FailedJudgment( + FailedJudgment { + judgment: "prove_atomic_effect_subset { atomic_subeffect: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }", + failed_rules: { + FailedRule { + rule_name_index: Some( + ( + "transitive", + 0, + ), + ), + file: "crates/formality-prove/src/prove/prove_effect_subset.rs", + line: 67, + column: 14, + cause: FailedJudgment( + FailedJudgment { + judgment: "prove_effect_upper_bound { f1: runtime, assumptions: {}, env: Env { variables: [], bias: Soundness } }", + failed_rules: {}, + }, + ), + }, + FailedRule { + rule_name_index: Some( + ( + "union-subset-lhs", + 1, + ), + ), + file: "crates/formality-prove/src/prove/prove_effect_subset.rs", + line: 59, + column: 14, + cause: FailedJudgment( + FailedJudgment { + judgment: "prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }", + failed_rules: {}, + }, + ), + }, + }, + }, + ), + }, + }, + }, + ), + }, + }, + }, + ), + }, + }, + }, + ), + }, + }, + } + "#]] + .assert_debug_eq(&constraint); +} + + +#[test] +fn three_atomic_test() { + // runtime <: Union(Union(const, const), runtime) + let runtime_eff = Effect::Atomic(AtomicEffect::Runtime); + let const_eff = Effect::Atomic(AtomicEffect::Const); + let union0 = Effect::Union(Arc::new(const_eff.clone()), Arc::new(const_eff.clone())); + let union1 = Effect::Union(Arc::new(union0), Arc::new(runtime_eff.clone())); + // Test (runtime) <: (runtime, const) + let constraint_0 = prove(Decls::empty(), Env::default(), Wcs::t(), Relation::EffectSubset(runtime_eff, union1)); + expect![[r#" + { + Constraints { + env: Env { + variables: [], + bias: Soundness, + }, + known_true: true, + substitution: {}, + }, + } + "#]] + .assert_debug_eq(&constraint_0); + } \ No newline at end of file From 8627b040052e09d089226b7282ecd4251b250f10 Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 20 Mar 2025 01:50:01 +0800 Subject: [PATCH 48/65] Run update expect --- crates/formality-prove/src/test/test_effect_subset.rs | 1 - crates/formality-rust/src/test.rs | 8 ++++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/crates/formality-prove/src/test/test_effect_subset.rs b/crates/formality-prove/src/test/test_effect_subset.rs index 9149c686..48f4bd59 100644 --- a/crates/formality-prove/src/test/test_effect_subset.rs +++ b/crates/formality-prove/src/test/test_effect_subset.rs @@ -202,7 +202,6 @@ fn three_atomic_test() { let const_eff = Effect::Atomic(AtomicEffect::Const); let union0 = Effect::Union(Arc::new(const_eff.clone()), Arc::new(const_eff.clone())); let union1 = Effect::Union(Arc::new(union0), Arc::new(runtime_eff.clone())); - // Test (runtime) <: (runtime, const) let constraint_0 = prove(Decls::empty(), Env::default(), Wcs::t(), Relation::EffectSubset(runtime_eff, union1)); expect![[r#" { diff --git a/crates/formality-rust/src/test.rs b/crates/formality-rust/src/test.rs index 9a32c80c..59b40be9 100644 --- a/crates/formality-rust/src/test.rs +++ b/crates/formality-rust/src/test.rs @@ -33,7 +33,9 @@ fn test_parse_rust_like_trait_impl_syntax() { Ty, ], term: TraitImplBoundData { - effect: Runtime, + effect: Atomic( + Runtime, + ), trait_id: PartialEq, self_ty: Ty { data: Variable( @@ -85,7 +87,9 @@ fn test_parse_rust_like_trait_syntax() { Trait( Trait { safety: Safe, - effect: Runtime, + effect: Atomic( + Runtime, + ), id: Foo, binder: where ^ty0_1 : Bar <^ty0_0> { }, }, From 84d8fb9640a61fc34dc5f5f854ca3b369b6a2eca Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 21 Mar 2025 00:33:38 +0800 Subject: [PATCH 49/65] Add test for const trait --- tests/const_trait.rs | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/tests/const_trait.rs b/tests/const_trait.rs index 6f344678..0469e76f 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -1,8 +1,11 @@ #![allow(non_snake_case)] // we embed type names into the names for our test functions -use a_mir_formality::test_program_ok; +use a_mir_formality::{test_program_ok, test_where_clause}; +use expect_test::expect; use formality_core::test_util::ResultTestExt; use formality_macros::test; +use formality_prove::{test_util::test_prove, Decls}; +use formality_types::rust::term; #[test] fn test_const_syntax() { @@ -23,3 +26,19 @@ fn test_const_syntax() { test_program_ok(&gen_program("")).assert_ok(expect_test::expect!["()"]); } + +// FIXME: this test is incorrect? +#[test] +fn test_const_trait_unprovable() { + let base: &str = "[ + crate test { + const trait Foo {} + } + ]"; + + test_where_clause( + base, + "forall { const Foo(T) } => { Foo(T) }", + ) + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness }, known_true: true, substitution: {} }}"]); +} From fb7050e606163d91a4ec89938e19b3a4fdf35f77 Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 21 Mar 2025 00:33:56 +0800 Subject: [PATCH 50/65] fmt --- .../src/prove/prove_effect_subset.rs | 7 +-- crates/formality-prove/src/test.rs | 2 +- .../src/test/test_effect_subset.rs | 51 ++++++++++++++----- 3 files changed, 44 insertions(+), 16 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index 5b3cbce2..6da1e18f 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -2,7 +2,10 @@ use formality_core::{judgment_fn, set, ProvenSet, Set}; use formality_types::grammar::{AtomicEffect, Effect, Relation, Wcs}; use std::fmt::Debug; -use crate::{prove::{prove_after::prove_after, prove_eq::prove_traitref_eq}, Decls}; +use crate::{ + prove::{prove_after::prove_after, prove_eq::prove_traitref_eq}, + Decls, +}; use super::{Constraints, Env}; @@ -75,7 +78,6 @@ judgment_fn! { } } - judgment_fn! { /// `prove_effect_bound(..., a) => b` means that `a <= b` fn prove_effect_upper_bound( @@ -94,7 +96,6 @@ judgment_fn! { } } - judgment_fn! { /// Prove two atomic effects are equal. fn prove_atomic_effect_eq( diff --git a/crates/formality-prove/src/test.rs b/crates/formality-prove/src/test.rs index f3feb4e3..bb72eba4 100644 --- a/crates/formality-prove/src/test.rs +++ b/crates/formality-prove/src/test.rs @@ -7,5 +7,5 @@ mod is_local; mod magic_copy; mod occurs_check; mod simple_impl; -mod universes; mod test_effect_subset; +mod universes; diff --git a/crates/formality-prove/src/test/test_effect_subset.rs b/crates/formality-prove/src/test/test_effect_subset.rs index 48f4bd59..d0a8ff0c 100644 --- a/crates/formality-prove/src/test/test_effect_subset.rs +++ b/crates/formality-prove/src/test/test_effect_subset.rs @@ -1,4 +1,3 @@ - use std::sync::Arc; use expect_test::expect; @@ -11,9 +10,15 @@ use crate::{decls::Decls, prove::prove, Env}; fn test_effect_subset_success() { let runtime_eff = Effect::Atomic(AtomicEffect::Runtime); let const_eff = Effect::Atomic(AtomicEffect::Const); - let runtime_const_union = Effect::Union(Arc::new(runtime_eff.clone()), Arc::new(const_eff.clone())); + let runtime_const_union = + Effect::Union(Arc::new(runtime_eff.clone()), Arc::new(const_eff.clone())); // Test (runtime) <: (runtime, const) - let constraint_0 = prove(Decls::empty(), Env::default(), Wcs::t(), Relation::EffectSubset(runtime_eff.clone(), runtime_const_union.clone())); + let constraint_0 = prove( + Decls::empty(), + Env::default(), + Wcs::t(), + Relation::EffectSubset(runtime_eff.clone(), runtime_const_union.clone()), + ); expect![[r#" { Constraints { @@ -28,7 +33,12 @@ fn test_effect_subset_success() { "#]] .assert_debug_eq(&constraint_0); // Test (const) <: (runtime, const) - let constraint_1 = prove(Decls::empty(), Env::default(), Wcs::t(), Relation::EffectSubset(const_eff.clone(), runtime_const_union.clone())); + let constraint_1 = prove( + Decls::empty(), + Env::default(), + Wcs::t(), + Relation::EffectSubset(const_eff.clone(), runtime_const_union.clone()), + ); expect![[r#" { Constraints { @@ -43,7 +53,12 @@ fn test_effect_subset_success() { "#]] .assert_debug_eq(&constraint_1); // Test (const) <: (runtime) - let constraint_2 = prove(Decls::empty(), Env::default(), Wcs::t(), Relation::EffectSubset(const_eff.clone(), runtime_eff.clone())); + let constraint_2 = prove( + Decls::empty(), + Env::default(), + Wcs::t(), + Relation::EffectSubset(const_eff.clone(), runtime_eff.clone()), + ); expect![[r#" { Constraints { @@ -58,7 +73,12 @@ fn test_effect_subset_success() { "#]] .assert_debug_eq(&constraint_2); // Test (const, runtime) <: (runtime) - let constraint_3 = prove(Decls::empty(), Env::default(), Wcs::t(), Relation::EffectSubset(runtime_const_union.clone(), runtime_eff.clone())); + let constraint_3 = prove( + Decls::empty(), + Env::default(), + Wcs::t(), + Relation::EffectSubset(runtime_const_union.clone(), runtime_eff.clone()), + ); expect![[r#" { Constraints { @@ -72,7 +92,6 @@ fn test_effect_subset_success() { } "#]] .assert_debug_eq(&constraint_3); - } #[test] @@ -82,7 +101,12 @@ fn test_effect_subset_failure() { // Runtime is not subset of const. // FIXME: the test output can be better? - let constraint = prove(Decls::empty(), Env::default(), Wcs::t(), Relation::EffectSubset(runtime_eff.clone(), const_eff.clone())); + let constraint = prove( + Decls::empty(), + Env::default(), + Wcs::t(), + Relation::EffectSubset(runtime_eff.clone(), const_eff.clone()), + ); expect![[r#" FailedJudgment { judgment: "prove { goal: {subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }", @@ -194,7 +218,6 @@ fn test_effect_subset_failure() { .assert_debug_eq(&constraint); } - #[test] fn three_atomic_test() { // runtime <: Union(Union(const, const), runtime) @@ -202,7 +225,12 @@ fn three_atomic_test() { let const_eff = Effect::Atomic(AtomicEffect::Const); let union0 = Effect::Union(Arc::new(const_eff.clone()), Arc::new(const_eff.clone())); let union1 = Effect::Union(Arc::new(union0), Arc::new(runtime_eff.clone())); - let constraint_0 = prove(Decls::empty(), Env::default(), Wcs::t(), Relation::EffectSubset(runtime_eff, union1)); + let constraint_0 = prove( + Decls::empty(), + Env::default(), + Wcs::t(), + Relation::EffectSubset(runtime_eff, union1), + ); expect![[r#" { Constraints { @@ -216,5 +244,4 @@ fn three_atomic_test() { } "#]] .assert_debug_eq(&constraint_0); - -} \ No newline at end of file +} From 19b33673745b3d28fdfd8abeadfbf1cec942ade1 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 21 Mar 2025 13:42:53 +0000 Subject: [PATCH 51/65] move to externalized test --- .../formality-types/src/grammar/formulas.rs | 4 +-- tests/effects.rs | 35 +++++++++++++++++++ 2 files changed, 37 insertions(+), 2 deletions(-) create mode 100644 tests/effects.rs diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index c08c11e3..a5cc818e 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -215,7 +215,7 @@ pub enum Relation { WellFormed(Parameter), // Means that the effects `$v0` are a subset of `$v1`. - #[grammar(subset($v0, $v1))] + #[grammar(@subset($v0, $v1))] EffectSubset(Effect, Effect), } @@ -257,7 +257,7 @@ pub enum Effect { #[cast] Atomic(AtomicEffect), - #[grammar(EffectUnion($v0, $v1))] + #[grammar(union($v0, $v1))] Union(Arc, Arc), } diff --git a/tests/effects.rs b/tests/effects.rs new file mode 100644 index 00000000..7ec7b82f --- /dev/null +++ b/tests/effects.rs @@ -0,0 +1,35 @@ +use a_mir_formality::test_where_clause; +use formality_core::test_util::ResultTestExt; + +const EFFECT_PREFIX: &str = "[ + crate test { + trait Trait { + } + } +]"; + +#[test] +fn test_runtime_subset_const() { + test_where_clause(EFFECT_PREFIX, "{} => {@subset(runtime, const)}") + .assert_err(expect_test::expect![[r#" + judgment `prove { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Trait ], [], [], [], [], [], {Trait}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ subset(runtime , const), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "effect subset" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_effect_subset { subset: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "atomic" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_atomic_effect_subset { atomic_subeffect: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "transitive" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_effect_upper_bound { f1: runtime, assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]); +} + + +#[test] +fn test_const_subset_runtime() { + test_where_clause(EFFECT_PREFIX, "{} => {@subset(const, runtime)}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); +} From f26d08090b80c494dbf2566a3c9b9d2370c5a839 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 21 Mar 2025 13:45:14 +0000 Subject: [PATCH 52/65] fix test --- .../formality-prove/src/test/test_effect_subset.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/crates/formality-prove/src/test/test_effect_subset.rs b/crates/formality-prove/src/test/test_effect_subset.rs index d0a8ff0c..88049eda 100644 --- a/crates/formality-prove/src/test/test_effect_subset.rs +++ b/crates/formality-prove/src/test/test_effect_subset.rs @@ -109,7 +109,7 @@ fn test_effect_subset_failure() { ); expect![[r#" FailedJudgment { - judgment: "prove { goal: {subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }", + judgment: "prove { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }", failed_rules: { FailedRule { rule_name_index: None, @@ -118,7 +118,7 @@ fn test_effect_subset_failure() { column: 59, cause: FailedJudgment( FailedJudgment { - judgment: "prove_wc_list { goal: {subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }", + judgment: "prove_wc_list { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }", failed_rules: { FailedRule { rule_name_index: Some( @@ -132,7 +132,7 @@ fn test_effect_subset_failure() { column: 14, cause: FailedJudgment( FailedJudgment { - judgment: "prove_wc { goal: subset(runtime , const), assumptions: {}, env: Env { variables: [], bias: Soundness } }", + judgment: "prove_wc { goal: @ subset(runtime , const), assumptions: {}, env: Env { variables: [], bias: Soundness } }", failed_rules: { FailedRule { rule_name_index: Some( @@ -156,7 +156,7 @@ fn test_effect_subset_failure() { ), ), file: "crates/formality-prove/src/prove/prove_effect_subset.rs", - line: 36, + line: 39, column: 14, cause: FailedJudgment( FailedJudgment { @@ -170,7 +170,7 @@ fn test_effect_subset_failure() { ), ), file: "crates/formality-prove/src/prove/prove_effect_subset.rs", - line: 67, + line: 70, column: 14, cause: FailedJudgment( FailedJudgment { @@ -187,7 +187,7 @@ fn test_effect_subset_failure() { ), ), file: "crates/formality-prove/src/prove/prove_effect_subset.rs", - line: 59, + line: 62, column: 14, cause: FailedJudgment( FailedJudgment { From 3d35cce68b0aec73ed3b4e0bd32a5e968c5f715f Mon Sep 17 00:00:00 2001 From: tiif Date: Wed, 26 Mar 2025 17:38:17 +0800 Subject: [PATCH 53/65] Use better syntax for the effect subset tests --- crates/formality-prove/src/test.rs | 1 - .../src/test/test_effect_subset.rs | 247 ------------------ tests/const_trait.rs | 3 - tests/effects.rs | 28 +- 4 files changed, 25 insertions(+), 254 deletions(-) delete mode 100644 crates/formality-prove/src/test/test_effect_subset.rs diff --git a/crates/formality-prove/src/test.rs b/crates/formality-prove/src/test.rs index bb72eba4..f04b7e12 100644 --- a/crates/formality-prove/src/test.rs +++ b/crates/formality-prove/src/test.rs @@ -7,5 +7,4 @@ mod is_local; mod magic_copy; mod occurs_check; mod simple_impl; -mod test_effect_subset; mod universes; diff --git a/crates/formality-prove/src/test/test_effect_subset.rs b/crates/formality-prove/src/test/test_effect_subset.rs deleted file mode 100644 index 88049eda..00000000 --- a/crates/formality-prove/src/test/test_effect_subset.rs +++ /dev/null @@ -1,247 +0,0 @@ -use std::sync::Arc; - -use expect_test::expect; -use formality_macros::test; -use formality_types::grammar::{AtomicEffect, Effect, Relation, Wcs}; - -use crate::{decls::Decls, prove::prove, Env}; - -#[test] -fn test_effect_subset_success() { - let runtime_eff = Effect::Atomic(AtomicEffect::Runtime); - let const_eff = Effect::Atomic(AtomicEffect::Const); - let runtime_const_union = - Effect::Union(Arc::new(runtime_eff.clone()), Arc::new(const_eff.clone())); - // Test (runtime) <: (runtime, const) - let constraint_0 = prove( - Decls::empty(), - Env::default(), - Wcs::t(), - Relation::EffectSubset(runtime_eff.clone(), runtime_const_union.clone()), - ); - expect![[r#" - { - Constraints { - env: Env { - variables: [], - bias: Soundness, - }, - known_true: true, - substitution: {}, - }, - } - "#]] - .assert_debug_eq(&constraint_0); - // Test (const) <: (runtime, const) - let constraint_1 = prove( - Decls::empty(), - Env::default(), - Wcs::t(), - Relation::EffectSubset(const_eff.clone(), runtime_const_union.clone()), - ); - expect![[r#" - { - Constraints { - env: Env { - variables: [], - bias: Soundness, - }, - known_true: true, - substitution: {}, - }, - } - "#]] - .assert_debug_eq(&constraint_1); - // Test (const) <: (runtime) - let constraint_2 = prove( - Decls::empty(), - Env::default(), - Wcs::t(), - Relation::EffectSubset(const_eff.clone(), runtime_eff.clone()), - ); - expect![[r#" - { - Constraints { - env: Env { - variables: [], - bias: Soundness, - }, - known_true: true, - substitution: {}, - }, - } - "#]] - .assert_debug_eq(&constraint_2); - // Test (const, runtime) <: (runtime) - let constraint_3 = prove( - Decls::empty(), - Env::default(), - Wcs::t(), - Relation::EffectSubset(runtime_const_union.clone(), runtime_eff.clone()), - ); - expect![[r#" - { - Constraints { - env: Env { - variables: [], - bias: Soundness, - }, - known_true: true, - substitution: {}, - }, - } - "#]] - .assert_debug_eq(&constraint_3); -} - -#[test] -fn test_effect_subset_failure() { - let runtime_eff = Effect::Atomic(AtomicEffect::Runtime); - let const_eff = Effect::Atomic(AtomicEffect::Const); - - // Runtime is not subset of const. - // FIXME: the test output can be better? - let constraint = prove( - Decls::empty(), - Env::default(), - Wcs::t(), - Relation::EffectSubset(runtime_eff.clone(), const_eff.clone()), - ); - expect![[r#" - FailedJudgment { - judgment: "prove { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }", - failed_rules: { - FailedRule { - rule_name_index: None, - file: "crates/formality-prove/src/prove.rs", - line: 70, - column: 59, - cause: FailedJudgment( - FailedJudgment { - judgment: "prove_wc_list { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }", - failed_rules: { - FailedRule { - rule_name_index: Some( - ( - "some", - 0, - ), - ), - file: "crates/formality-prove/src/prove/prove_wc_list.rs", - line: 28, - column: 14, - cause: FailedJudgment( - FailedJudgment { - judgment: "prove_wc { goal: @ subset(runtime , const), assumptions: {}, env: Env { variables: [], bias: Soundness } }", - failed_rules: { - FailedRule { - rule_name_index: Some( - ( - "effect subset", - 0, - ), - ), - file: "crates/formality-prove/src/prove/prove_wc.rs", - line: 138, - column: 14, - cause: FailedJudgment( - FailedJudgment { - judgment: "prove_effect_subset { subset: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }", - failed_rules: { - FailedRule { - rule_name_index: Some( - ( - "atomic", - 0, - ), - ), - file: "crates/formality-prove/src/prove/prove_effect_subset.rs", - line: 39, - column: 14, - cause: FailedJudgment( - FailedJudgment { - judgment: "prove_atomic_effect_subset { atomic_subeffect: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }", - failed_rules: { - FailedRule { - rule_name_index: Some( - ( - "transitive", - 0, - ), - ), - file: "crates/formality-prove/src/prove/prove_effect_subset.rs", - line: 70, - column: 14, - cause: FailedJudgment( - FailedJudgment { - judgment: "prove_effect_upper_bound { f1: runtime, assumptions: {}, env: Env { variables: [], bias: Soundness } }", - failed_rules: {}, - }, - ), - }, - FailedRule { - rule_name_index: Some( - ( - "union-subset-lhs", - 1, - ), - ), - file: "crates/formality-prove/src/prove/prove_effect_subset.rs", - line: 62, - column: 14, - cause: FailedJudgment( - FailedJudgment { - judgment: "prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }", - failed_rules: {}, - }, - ), - }, - }, - }, - ), - }, - }, - }, - ), - }, - }, - }, - ), - }, - }, - }, - ), - }, - }, - } - "#]] - .assert_debug_eq(&constraint); -} - -#[test] -fn three_atomic_test() { - // runtime <: Union(Union(const, const), runtime) - let runtime_eff = Effect::Atomic(AtomicEffect::Runtime); - let const_eff = Effect::Atomic(AtomicEffect::Const); - let union0 = Effect::Union(Arc::new(const_eff.clone()), Arc::new(const_eff.clone())); - let union1 = Effect::Union(Arc::new(union0), Arc::new(runtime_eff.clone())); - let constraint_0 = prove( - Decls::empty(), - Env::default(), - Wcs::t(), - Relation::EffectSubset(runtime_eff, union1), - ); - expect![[r#" - { - Constraints { - env: Env { - variables: [], - bias: Soundness, - }, - known_true: true, - substitution: {}, - }, - } - "#]] - .assert_debug_eq(&constraint_0); -} diff --git a/tests/const_trait.rs b/tests/const_trait.rs index 0469e76f..e26905bc 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -1,11 +1,8 @@ #![allow(non_snake_case)] // we embed type names into the names for our test functions use a_mir_formality::{test_program_ok, test_where_clause}; -use expect_test::expect; use formality_core::test_util::ResultTestExt; use formality_macros::test; -use formality_prove::{test_util::test_prove, Decls}; -use formality_types::rust::term; #[test] fn test_const_syntax() { diff --git a/tests/effects.rs b/tests/effects.rs index 7ec7b82f..fa06f1d6 100644 --- a/tests/effects.rs +++ b/tests/effects.rs @@ -8,6 +8,27 @@ const EFFECT_PREFIX: &str = "[ } ]"; +// Basic tests for const-runtime relation that should pass. +#[test] +fn test_const_runtime_basic() { + // (const) <: (runtime) + test_where_clause(EFFECT_PREFIX, "{} => {@subset(const, runtime)}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + + // (runtime) <: (runtime, const) + test_where_clause(EFFECT_PREFIX, "{} => {@subset(runtime, union(runtime, const))}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + + // (const) <: (runtime, const) + test_where_clause(EFFECT_PREFIX, "{} => {@subset(const, union(runtime, const))}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + + // (const, runtime) <: (runtime) + test_where_clause(EFFECT_PREFIX, "{} => {@subset(union(const, runtime), runtime)}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); +} + +// Runtime is not subset of const, so this test should fail. #[test] fn test_runtime_subset_const() { test_where_clause(EFFECT_PREFIX, "{} => {@subset(runtime, const)}") @@ -27,9 +48,10 @@ fn test_runtime_subset_const() { judgment had no applicable rules: `prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]); } - +// Test if the rule is still correct when there is more than two atomic effects. #[test] -fn test_const_subset_runtime() { - test_where_clause(EFFECT_PREFIX, "{} => {@subset(const, runtime)}") +fn test_three_atomic_effect() { + //union(union(const, const), runtime) <: runtime + test_where_clause(EFFECT_PREFIX, "{} => {@subset(union(union(const, const), runtime), runtime)}") .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); } From 2ef0c7d2e747f5e8bf5443c9ead017cb654f3d3a Mon Sep 17 00:00:00 2001 From: tiif Date: Wed, 26 Mar 2025 17:45:45 +0800 Subject: [PATCH 54/65] Clean up --- .../src/prove/prove_effect_subset.rs | 13 ++----------- tests/effects.rs | 1 + 2 files changed, 3 insertions(+), 11 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index 6da1e18f..49d578f2 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -1,6 +1,5 @@ -use formality_core::{judgment_fn, set, ProvenSet, Set}; +use formality_core::judgment_fn; use formality_types::grammar::{AtomicEffect, Effect, Relation, Wcs}; -use std::fmt::Debug; use crate::{ prove::{prove_after::prove_after, prove_eq::prove_traitref_eq}, @@ -90,7 +89,7 @@ judgment_fn! { ( - --- ("runtime bounded by const") + --- ("const bounded by runtime") (prove_effect_upper_bound(_decls, env, _assumptions, AtomicEffect::Const) => (Constraints::none(env), AtomicEffect::Runtime)) ) } @@ -116,14 +115,6 @@ judgment_fn! { } } -/// Proves judgment for each of the given items. -pub fn collect(judgment: ProvenSet) -> ProvenSet> { - match judgment.into_set() { - Ok(s) => ProvenSet::proven(set![s]), - Err(e) => ProvenSet::from(*e), - } -} - judgment_fn! { /// Get any atomic effect from an Effect::Union. fn some_atomic_effect( diff --git a/tests/effects.rs b/tests/effects.rs index fa06f1d6..cacc047b 100644 --- a/tests/effects.rs +++ b/tests/effects.rs @@ -1,6 +1,7 @@ use a_mir_formality::test_where_clause; use formality_core::test_util::ResultTestExt; +// FIXME: we don't need this for the current set of test to pass, but we might eventually need this, so keep this here. const EFFECT_PREFIX: &str = "[ crate test { trait Trait { From aaca632659949186ac23a144d1bda574d6c0bfac Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 27 Mar 2025 06:54:21 +0800 Subject: [PATCH 55/65] Add effect to where-clause data --- crates/formality-rust/src/grammar.rs | 6 ++++++ crates/formality-rust/src/prove.rs | 5 +++++ 2 files changed, 11 insertions(+) diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 742f5e7b..cc347a51 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -346,6 +346,7 @@ impl WhereClause { &self.data } + // (tiif): what is this invert for? pub fn invert(&self) -> Option { match self.data() { WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => Some( @@ -362,6 +363,7 @@ impl WhereClause { Some(Wc::for_all(&vars, wc)) } WhereClauseData::TypeOfConst(_, _) => None, + WhereClauseData::FnEffect(_) => None, } } @@ -413,6 +415,7 @@ impl WhereClause { wcs.push(ty_param.well_formed()); wcs.into_iter().map(|r| r.upcast()).collect() } + WhereClauseData::FnEffect(_) => Wcs::default(), } } } @@ -433,6 +436,9 @@ pub enum WhereClauseData { #[grammar(type_of_const $v0 is $v1)] TypeOfConst(Const, Ty), + + #[grammar(effect is $v0)] + FnEffect(Effect), } #[term($data)] diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index b516fb74..066507c9 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -447,6 +447,11 @@ impl ToWcs for WhereClause { WhereClauseData::TypeOfConst(ct, ty) => { Predicate::ConstHasType(ct.clone(), ty.clone()).upcast() } + // FIXME (tiif): we need to check if the function body's effect is subset of fn's. But we don't have the function body effect + // information for now. + WhereClauseData::FnEffect(e) => { + Relation::EffectSubset(e.clone(), e.clone()).upcast() + } } } } From 7790d3beaa8f884cd87286253287013baa696ad3 Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 27 Mar 2025 07:09:38 +0800 Subject: [PATCH 56/65] Add test with effect that did nothing yet --- tests/const_trait.rs | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/tests/const_trait.rs b/tests/const_trait.rs index e26905bc..a0aa24f5 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -24,7 +24,21 @@ fn test_const_syntax() { test_program_ok(&gen_program("")).assert_ok(expect_test::expect!["()"]); } -// FIXME: this test is incorrect? +#[test] +fn test_effect_fn() { + let BASE_PROGRAM: &str = "[ + crate test { + fn foo() -> () where effect is runtime {trusted} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); +} + +// FIXME: this test is incorrect, remove this later #[test] fn test_const_trait_unprovable() { let base: &str = "[ From d503eb3c61832c22d46e21535d05867efbbd1ef5 Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 27 Mar 2025 07:10:02 +0800 Subject: [PATCH 57/65] Clean up --- tests/const_trait.rs | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/tests/const_trait.rs b/tests/const_trait.rs index a0aa24f5..20676da2 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -37,19 +37,3 @@ fn test_effect_fn() { ) .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); } - -// FIXME: this test is incorrect, remove this later -#[test] -fn test_const_trait_unprovable() { - let base: &str = "[ - crate test { - const trait Foo {} - } - ]"; - - test_where_clause( - base, - "forall { const Foo(T) } => { Foo(T) }", - ) - .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness }, known_true: true, substitution: {} }}"]); -} From 7aac3e1da435a0552543b8bee79c8eb045456056 Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 27 Mar 2025 07:30:34 +0800 Subject: [PATCH 58/65] Add FnBodyWithEffect --- crates/formality-rust/src/grammar.rs | 3 +++ tests/const_trait.rs | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index cc347a51..1a74002e 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -243,6 +243,9 @@ pub enum FnBody { #[cast] #[grammar(= $v0 ;)] MirFnBody(MirFnBody), + + #[grammar({($v0)})] + FnBodyWithEffect(Effect), } #[term(type $id $binder ;)] diff --git a/tests/const_trait.rs b/tests/const_trait.rs index 20676da2..2e7792ff 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -28,7 +28,7 @@ fn test_const_syntax() { fn test_effect_fn() { let BASE_PROGRAM: &str = "[ crate test { - fn foo() -> () where effect is runtime {trusted} + fn foo() -> () where effect is runtime {(runtime)} } ]"; test_where_clause( From e6b125d46ee57e550c83ae12b9b85a235fd4f519 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Sat, 29 Mar 2025 16:06:44 +0000 Subject: [PATCH 59/65] changes --- crates/formality-check/src/fns.rs | 37 +++++++++++++++-- crates/formality-check/src/impls.rs | 62 ++++++++++++++++++++++++++++ crates/formality-rust/src/grammar.rs | 9 +--- crates/formality-rust/src/prove.rs | 5 --- tests/const_trait.rs | 18 +++++++- 5 files changed, 114 insertions(+), 17 deletions(-) diff --git a/crates/formality-check/src/fns.rs b/crates/formality-check/src/fns.rs index 15f2357a..fd769ea4 100644 --- a/crates/formality-check/src/fns.rs +++ b/crates/formality-check/src/fns.rs @@ -1,9 +1,9 @@ use formality_prove::Env; use formality_rust::{ - grammar::{Fn, FnBoundData}, + grammar::{Fn, FnBody, FnBoundData, MaybeFnBody}, prove::ToWcs, }; -use formality_types::grammar::{Fallible, Wcs}; +use formality_types::grammar::{Fallible, Relation, Wcs}; use crate::Check; @@ -29,7 +29,8 @@ impl Check<'_> { input_tys, output_ty, where_clauses, - body: _, + effect: declared_effect, + body, } = env.instantiate_universally(binder); let fn_assumptions: Wcs = (in_assumptions, &where_clauses).to_wcs(); @@ -42,6 +43,36 @@ impl Check<'_> { self.prove_goal(&env, &fn_assumptions, output_ty.well_formed())?; + // prove that the body type checks (if present) + eprintln!("check_fn: {body:?}"); + match body { + MaybeFnBody::NoFnBody => { + // No fn body: this occurs e.g. for the fn `bar` + // in `trait Foo { fn bar(); }`. No check required. + } + MaybeFnBody::FnBody(fn_body) => match fn_body { + FnBody::TrustedFnBody => { + // Trusted: just assume it's ok, useful for tests + // to indicate things we don't want to think about. + } + FnBody::MirFnBody(_mir_fn_body) => { + // TODO: this nikomatsakis is theoretically working on removing + // though he has not made much time for it. + unimplemented!() + } + FnBody::FnBodyWithEffect(body_effect) => { + // Useful for tests: declares "some body" with the + // given effect. So we need to check that the effect + // is in bounds of the declaration. + self.prove_goal( + &env, + &fn_assumptions, + Relation::EffectSubset(body_effect, declared_effect) + )?; + } + } + } + Ok(()) } } diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index 99c427d1..98a525ee 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -118,6 +118,44 @@ impl super::Check<'_> { } } + /// Check that function `ii_fn` that appears in an impl is valid. + /// This includes the core check from [`Self::check_fn`][], + /// but also additional checks to ensure that the signature in the impl + /// matches what is declared in the trait. + /// + /// # Example + /// + /// Suppose we are checking ` as Potable>::drink` in this example... + /// + /// ```rust,ignore + /// trait Potable { + /// fn drink(&self); // `trait_items` includes these fns + /// fn smell(&self); // + /// } + /// + /// struct Water; + /// impl Potable for Water { + /// fn drink(&self) {} + /// fn smell(&self) {} + /// } + /// + /// struct Cup; + /// impl Potable for Cup // <-- env has `L` in scope + /// where + /// L: Potable, // <-- `impl_assumptions` + /// { + /// fn drink(&self) {} // <-- `ii_fn` + /// fn smell(&self) {} // not currently being checked + /// } + /// ``` + /// + /// # Parameters + /// + /// * `env`, the environment from the impl header + /// * `impl_assumptions`, where-clauses declared on the impl + /// * `trait_items`, items declared in the trait that is being implemented + /// (we search this to find the corresponding declaration of the method) + /// * `ii_fn`, the fn as declared in the impl fn check_fn_in_impl( &self, env: &Env, @@ -146,16 +184,21 @@ impl super::Check<'_> { let mut env = env.clone(); let ( + // ii_: the signature of the function as found in the impl item (ii) FnBoundData { input_tys: ii_input_tys, output_ty: ii_output_ty, where_clauses: ii_where_clauses, + effect: ii_effect, body: _, }, + + // ti_: the signature of the function as found in the trait item (ti) FnBoundData { input_tys: ti_input_tys, output_ty: ti_output_ty, where_clauses: ti_where_clauses, + effect: ti_effect, body: _, }, ) = env.instantiate_universally(&self.merge_binders(&ii_fn.binder, &ti_fn.binder)?); @@ -166,6 +209,7 @@ impl super::Check<'_> { &ii_where_clauses, )?; + // Must have same number of arguments as declared in the trait if ii_input_tys.len() != ti_input_tys.len() { bail!( "impl has {} function arguments but trait has {} function arguments", @@ -174,6 +218,16 @@ impl super::Check<'_> { ) } + // The type `ii_input_ty` of argument `i` in the impl + // must be a supertype of the correspond type `ti_input_ty` from the trait. + // + // e.g. if you have `fn foo(arg: for<'a> fn(&u8))` in the trait + // you can have `fn foo(arg: fn(&'static u8))` in the impl. + // + // Why? Trait guarantees you are receiving a fn that can take + // an `&u8` in any lifetime. Impl is saying "I only need a fn that can + // take `&u8` in static lifetime", which is more narrow, and that's ok, + // because a functon that can handle any lifetime can also handle static. for (ii_input_ty, ti_input_ty) in ii_input_tys.iter().zip(&ti_input_tys) { self.prove_goal( &env, @@ -182,12 +236,20 @@ impl super::Check<'_> { )?; } + // Impl must return a subtype of the return type from the trait. self.prove_goal( &env, (&impl_assumptions, &ii_where_clauses), Relation::sub(ii_output_ty, ti_output_ty), )?; + // Impl must not have more effects than what are declared in the trait. + self.prove_goal( + &env, + (&impl_assumptions, &ii_where_clauses), + Relation::EffectSubset(ii_effect, ti_effect), + )?; + Ok(()) } diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 1a74002e..e834b4ce 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -218,10 +218,11 @@ pub struct Fn { pub binder: Binder, } -#[term($(input_tys) -> $output_ty $:where $,where_clauses $body)] +#[term($(input_tys) -> $output_ty $:where $,where_clauses $:do $effect $body)] pub struct FnBoundData { pub input_tys: Vec, pub output_ty: Ty, + pub effect: Effect, pub where_clauses: Vec, pub body: MaybeFnBody, } @@ -349,7 +350,6 @@ impl WhereClause { &self.data } - // (tiif): what is this invert for? pub fn invert(&self) -> Option { match self.data() { WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => Some( @@ -366,7 +366,6 @@ impl WhereClause { Some(Wc::for_all(&vars, wc)) } WhereClauseData::TypeOfConst(_, _) => None, - WhereClauseData::FnEffect(_) => None, } } @@ -418,7 +417,6 @@ impl WhereClause { wcs.push(ty_param.well_formed()); wcs.into_iter().map(|r| r.upcast()).collect() } - WhereClauseData::FnEffect(_) => Wcs::default(), } } } @@ -439,9 +437,6 @@ pub enum WhereClauseData { #[grammar(type_of_const $v0 is $v1)] TypeOfConst(Const, Ty), - - #[grammar(effect is $v0)] - FnEffect(Effect), } #[term($data)] diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index 066507c9..b516fb74 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -447,11 +447,6 @@ impl ToWcs for WhereClause { WhereClauseData::TypeOfConst(ct, ty) => { Predicate::ConstHasType(ct.clone(), ty.clone()).upcast() } - // FIXME (tiif): we need to check if the function body's effect is subset of fn's. But we don't have the function body effect - // information for now. - WhereClauseData::FnEffect(e) => { - Relation::EffectSubset(e.clone(), e.clone()).upcast() - } } } } diff --git a/tests/const_trait.rs b/tests/const_trait.rs index 2e7792ff..f0a28c30 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -25,10 +25,10 @@ fn test_const_syntax() { } #[test] -fn test_effect_fn() { +fn test_runtime_fn_with_runtime_effect() { let BASE_PROGRAM: &str = "[ crate test { - fn foo() -> () where effect is runtime {(runtime)} + fn foo() -> () do runtime {(runtime)} } ]"; test_where_clause( @@ -37,3 +37,17 @@ fn test_effect_fn() { ) .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); } + +#[test] +fn test_const_fn_with_runtime_effect() { + let BASE_PROGRAM: &str = "[ + crate test { + fn foo() -> () do const {(runtime)} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_err(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); +} From 70a6bdbc805af869034f77a976cebe7cab49008c Mon Sep 17 00:00:00 2001 From: tiif Date: Mon, 31 Mar 2025 19:52:17 +0800 Subject: [PATCH 60/65] unfortunate version that works --- crates/formality-check/src/fns.rs | 2 +- crates/formality-rust/src/grammar.rs | 2 +- tests/const_trait.rs | 109 ++++++++++++++++++++++++++- 3 files changed, 109 insertions(+), 4 deletions(-) diff --git a/crates/formality-check/src/fns.rs b/crates/formality-check/src/fns.rs index fd769ea4..2080d018 100644 --- a/crates/formality-check/src/fns.rs +++ b/crates/formality-check/src/fns.rs @@ -43,8 +43,8 @@ impl Check<'_> { self.prove_goal(&env, &fn_assumptions, output_ty.well_formed())?; + // prove that the body type checks (if present) - eprintln!("check_fn: {body:?}"); match body { MaybeFnBody::NoFnBody => { // No fn body: this occurs e.g. for the fn `bar` diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index e834b4ce..806b8da8 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -218,7 +218,7 @@ pub struct Fn { pub binder: Binder, } -#[term($(input_tys) -> $output_ty $:where $,where_clauses $:do $effect $body)] +#[term($(input_tys) -> $output_ty $:where $,where_clauses $effect $body)] pub struct FnBoundData { pub input_tys: Vec, pub output_ty: Ty, diff --git a/tests/const_trait.rs b/tests/const_trait.rs index f0a28c30..c2b83874 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -42,12 +42,117 @@ fn test_runtime_fn_with_runtime_effect() { fn test_const_fn_with_runtime_effect() { let BASE_PROGRAM: &str = "[ crate test { - fn foo() -> () do const {(runtime)} + fn foo() -> () some_random_keyword const {(runtime)} } ]"; test_where_clause( BASE_PROGRAM, "{} => {}", ) - .assert_err(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + .assert_err(expect_test::expect![[r#" + judgment `prove { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ subset(runtime , const), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "effect subset" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_effect_subset { subset: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "atomic" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_atomic_effect_subset { atomic_subeffect: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "transitive" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_effect_upper_bound { f1: runtime, assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` + + Stack backtrace: + 0: anyhow::error:: for anyhow::Error>::from + at /home/tiif/.cargo/registry/src/index.crates.io-6f17d22bba15001f/anyhow-1.0.75/src/backtrace.rs:27:14 + 1: as core::ops::try_trait::FromResidual>>::from_residual + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/core/src/result.rs:1989:27 + 2: formality_check::Check::prove_goal + at ./crates/formality-check/src/lib.rs:141:18 + 3: formality_check::fns::::check_fn + at ./crates/formality-check/src/fns.rs:69:21 + 4: formality_check::fns::::check_free_fn + at ./crates/formality-check/src/fns.rs:12:9 + 5: formality_check::Check::check_crate_item + at ./crates/formality-check/src/lib.rs:116:33 + 6: formality_check::Check::check_current_crate + at ./crates/formality-check/src/lib.rs:66:13 + 7: formality_check::Check::check + at ./crates/formality-check/src/lib.rs:55:13 + 8: formality_check::check_current_crate + at ./crates/formality-check/src/lib.rs:32:5 + 9: formality_check::check_all_crates + at ./crates/formality-check/src/lib.rs:23:9 + 10: a_mir_formality::test_where_clause::{{closure}} + at ./src/lib.rs:80:9 + 11: tracing_core::dispatcher::with_default + at /home/tiif/.cargo/registry/src/index.crates.io-6f17d22bba15001f/tracing-core-0.1.32/src/dispatcher.rs:265:5 + 12: tracing::subscriber::with_default + at /home/tiif/.cargo/registry/src/index.crates.io-6f17d22bba15001f/tracing-0.1.40/src/subscriber.rs:24:5 + 13: formality_core::with_tracing_logs + at ./crates/formality-core/src/lib.rs:59:5 + 14: a_mir_formality::test_where_clause + at ./src/lib.rs:78:5 + 15: const_trait::test_const_fn_with_runtime_effect::{{closure}} + at ./tests/const_trait.rs:48:5 + 16: tracing_core::dispatcher::with_default + at /home/tiif/.cargo/registry/src/index.crates.io-6f17d22bba15001f/tracing-core-0.1.32/src/dispatcher.rs:265:5 + 17: tracing::subscriber::with_default + at /home/tiif/.cargo/registry/src/index.crates.io-6f17d22bba15001f/tracing-0.1.40/src/subscriber.rs:24:5 + 18: formality_core::with_tracing_logs + at ./crates/formality-core/src/lib.rs:59:5 + 19: const_trait::test_const_fn_with_runtime_effect + at ./tests/const_trait.rs:41:1 + 20: const_trait::test_const_fn_with_runtime_effect::{{closure}} + at ./tests/const_trait.rs:42:39 + 21: core::ops::function::FnOnce::call_once + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/core/src/ops/function.rs:250:5 + 22: core::ops::function::FnOnce::call_once + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/core/src/ops/function.rs:250:5 + 23: test::__rust_begin_short_backtrace + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/test/src/lib.rs:625:18 + 24: test::run_test_in_process::{{closure}} + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/test/src/lib.rs:648:60 + 25: as core::ops::function::FnOnce<()>>::call_once + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/core/src/panic/unwind_safe.rs:272:9 + 26: std::panicking::try::do_call + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/panicking.rs:553:40 + 27: std::panicking::try + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/panicking.rs:517:19 + 28: std::panic::catch_unwind + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/panic.rs:350:14 + 29: test::run_test_in_process + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/test/src/lib.rs:648:27 + 30: test::run_test::{{closure}} + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/test/src/lib.rs:569:43 + 31: test::run_test::{{closure}} + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/test/src/lib.rs:599:41 + 32: std::sys_common::backtrace::__rust_begin_short_backtrace + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/sys_common/backtrace.rs:155:18 + 33: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}} + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/thread/mod.rs:542:17 + 34: as core::ops::function::FnOnce<()>>::call_once + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/core/src/panic/unwind_safe.rs:272:9 + 35: std::panicking::try::do_call + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/panicking.rs:553:40 + 36: std::panicking::try + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/panicking.rs:517:19 + 37: std::panic::catch_unwind + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/panic.rs:350:14 + 38: std::thread::Builder::spawn_unchecked_::{{closure}} + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/thread/mod.rs:541:30 + 39: core::ops::function::FnOnce::call_once{{vtable.shim}} + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/core/src/ops/function.rs:250:5 + 40: as core::ops::function::FnOnce>::call_once + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/alloc/src/boxed.rs:2062:9 + 41: as core::ops::function::FnOnce>::call_once + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/alloc/src/boxed.rs:2062:9 + 42: std::sys::pal::unix::thread::Thread::new::thread_start + at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/sys/pal/unix/thread.rs:108:17 + 43: start_thread + at ./nptl/pthread_create.c:442:8 + 44: __GI___clone3 + at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81"#]]); } From c152fe976976238e15215f727c1dc031c71e1324 Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 1 Apr 2025 18:27:24 +0800 Subject: [PATCH 61/65] Added more test and make the grammar slighly better --- crates/formality-check/src/fns.rs | 1 - crates/formality-rust/src/grammar.rs | 2 +- tests/const_trait.rs | 128 +++++++-------------------- 3 files changed, 33 insertions(+), 98 deletions(-) diff --git a/crates/formality-check/src/fns.rs b/crates/formality-check/src/fns.rs index 2080d018..a2130f4c 100644 --- a/crates/formality-check/src/fns.rs +++ b/crates/formality-check/src/fns.rs @@ -43,7 +43,6 @@ impl Check<'_> { self.prove_goal(&env, &fn_assumptions, output_ty.well_formed())?; - // prove that the body type checks (if present) match body { MaybeFnBody::NoFnBody => { diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 806b8da8..e834b4ce 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -218,7 +218,7 @@ pub struct Fn { pub binder: Binder, } -#[term($(input_tys) -> $output_ty $:where $,where_clauses $effect $body)] +#[term($(input_tys) -> $output_ty $:where $,where_clauses $:do $effect $body)] pub struct FnBoundData { pub input_tys: Vec, pub output_ty: Ty, diff --git a/tests/const_trait.rs b/tests/const_trait.rs index c2b83874..a78addcc 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -28,7 +28,35 @@ fn test_const_syntax() { fn test_runtime_fn_with_runtime_effect() { let BASE_PROGRAM: &str = "[ crate test { - fn foo() -> () do runtime {(runtime)} + fn foo() -> () random_keyword do runtime {(runtime)} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); +} + +#[test] +fn test_const_fn_with_const_effect() { + let BASE_PROGRAM: &str = "[ + crate test { + fn foo() -> () random_keyword do const {(const)} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); +} + +#[test] +fn test_runtime_fn_with_const_effect() { + let BASE_PROGRAM: &str = "[ + crate test { + fn foo() -> () random_keyword do runtime {(const)} } ]"; test_where_clause( @@ -42,7 +70,7 @@ fn test_runtime_fn_with_runtime_effect() { fn test_const_fn_with_runtime_effect() { let BASE_PROGRAM: &str = "[ crate test { - fn foo() -> () some_random_keyword const {(runtime)} + fn foo() -> () keyword do const {(runtime)} } ]"; test_where_clause( @@ -62,97 +90,5 @@ fn test_const_fn_with_runtime_effect() { the rule "transitive" failed at step #0 (src/file.rs:LL:CC) because judgment had no applicable rules: `prove_effect_upper_bound { f1: runtime, assumptions: {}, env: Env { variables: [], bias: Soundness } }` the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` - - Stack backtrace: - 0: anyhow::error:: for anyhow::Error>::from - at /home/tiif/.cargo/registry/src/index.crates.io-6f17d22bba15001f/anyhow-1.0.75/src/backtrace.rs:27:14 - 1: as core::ops::try_trait::FromResidual>>::from_residual - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/core/src/result.rs:1989:27 - 2: formality_check::Check::prove_goal - at ./crates/formality-check/src/lib.rs:141:18 - 3: formality_check::fns::::check_fn - at ./crates/formality-check/src/fns.rs:69:21 - 4: formality_check::fns::::check_free_fn - at ./crates/formality-check/src/fns.rs:12:9 - 5: formality_check::Check::check_crate_item - at ./crates/formality-check/src/lib.rs:116:33 - 6: formality_check::Check::check_current_crate - at ./crates/formality-check/src/lib.rs:66:13 - 7: formality_check::Check::check - at ./crates/formality-check/src/lib.rs:55:13 - 8: formality_check::check_current_crate - at ./crates/formality-check/src/lib.rs:32:5 - 9: formality_check::check_all_crates - at ./crates/formality-check/src/lib.rs:23:9 - 10: a_mir_formality::test_where_clause::{{closure}} - at ./src/lib.rs:80:9 - 11: tracing_core::dispatcher::with_default - at /home/tiif/.cargo/registry/src/index.crates.io-6f17d22bba15001f/tracing-core-0.1.32/src/dispatcher.rs:265:5 - 12: tracing::subscriber::with_default - at /home/tiif/.cargo/registry/src/index.crates.io-6f17d22bba15001f/tracing-0.1.40/src/subscriber.rs:24:5 - 13: formality_core::with_tracing_logs - at ./crates/formality-core/src/lib.rs:59:5 - 14: a_mir_formality::test_where_clause - at ./src/lib.rs:78:5 - 15: const_trait::test_const_fn_with_runtime_effect::{{closure}} - at ./tests/const_trait.rs:48:5 - 16: tracing_core::dispatcher::with_default - at /home/tiif/.cargo/registry/src/index.crates.io-6f17d22bba15001f/tracing-core-0.1.32/src/dispatcher.rs:265:5 - 17: tracing::subscriber::with_default - at /home/tiif/.cargo/registry/src/index.crates.io-6f17d22bba15001f/tracing-0.1.40/src/subscriber.rs:24:5 - 18: formality_core::with_tracing_logs - at ./crates/formality-core/src/lib.rs:59:5 - 19: const_trait::test_const_fn_with_runtime_effect - at ./tests/const_trait.rs:41:1 - 20: const_trait::test_const_fn_with_runtime_effect::{{closure}} - at ./tests/const_trait.rs:42:39 - 21: core::ops::function::FnOnce::call_once - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/core/src/ops/function.rs:250:5 - 22: core::ops::function::FnOnce::call_once - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/core/src/ops/function.rs:250:5 - 23: test::__rust_begin_short_backtrace - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/test/src/lib.rs:625:18 - 24: test::run_test_in_process::{{closure}} - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/test/src/lib.rs:648:60 - 25: as core::ops::function::FnOnce<()>>::call_once - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/core/src/panic/unwind_safe.rs:272:9 - 26: std::panicking::try::do_call - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/panicking.rs:553:40 - 27: std::panicking::try - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/panicking.rs:517:19 - 28: std::panic::catch_unwind - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/panic.rs:350:14 - 29: test::run_test_in_process - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/test/src/lib.rs:648:27 - 30: test::run_test::{{closure}} - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/test/src/lib.rs:569:43 - 31: test::run_test::{{closure}} - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/test/src/lib.rs:599:41 - 32: std::sys_common::backtrace::__rust_begin_short_backtrace - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/sys_common/backtrace.rs:155:18 - 33: std::thread::Builder::spawn_unchecked_::{{closure}}::{{closure}} - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/thread/mod.rs:542:17 - 34: as core::ops::function::FnOnce<()>>::call_once - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/core/src/panic/unwind_safe.rs:272:9 - 35: std::panicking::try::do_call - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/panicking.rs:553:40 - 36: std::panicking::try - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/panicking.rs:517:19 - 37: std::panic::catch_unwind - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/panic.rs:350:14 - 38: std::thread::Builder::spawn_unchecked_::{{closure}} - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/thread/mod.rs:541:30 - 39: core::ops::function::FnOnce::call_once{{vtable.shim}} - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/core/src/ops/function.rs:250:5 - 40: as core::ops::function::FnOnce>::call_once - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/alloc/src/boxed.rs:2062:9 - 41: as core::ops::function::FnOnce>::call_once - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/alloc/src/boxed.rs:2062:9 - 42: std::sys::pal::unix::thread::Thread::new::thread_start - at /rustc/3cf924b934322fd7b514600a7dc84fc517515346/library/std/src/sys/pal/unix/thread.rs:108:17 - 43: start_thread - at ./nptl/pthread_create.c:442:8 - 44: __GI___clone3 - at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81"#]]); -} + judgment had no applicable rules: `prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]); + } From c1644aee7f1e414fdaf7d154c5d5c6badc381527 Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 1 Apr 2025 18:29:08 +0800 Subject: [PATCH 62/65] use the same keyword --- tests/const_trait.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/const_trait.rs b/tests/const_trait.rs index a78addcc..1f3f79e9 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -70,7 +70,7 @@ fn test_runtime_fn_with_const_effect() { fn test_const_fn_with_runtime_effect() { let BASE_PROGRAM: &str = "[ crate test { - fn foo() -> () keyword do const {(runtime)} + fn foo() -> () random_keyword do const {(runtime)} } ]"; test_where_clause( From 4db5c86335daad0ccccb47d130508f1e5af1d7aa Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 4 Apr 2025 21:13:50 +0800 Subject: [PATCH 63/65] Add rules for associated effect --- .../formality-prove/src/prove/prove_effect_subset.rs | 10 ++++++++++ crates/formality-types/src/grammar/formulas.rs | 4 ++++ 2 files changed, 14 insertions(+) diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index 49d578f2..a0ed1a10 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -39,6 +39,16 @@ judgment_fn! { --- ("atomic") (prove_effect_subset(decls, env, assumptions, Effect::Atomic(subeffect), superset) => constraints) ) + + // If it is associated effect, get the effect from the trait_ref, then proceed with normal prove_effect_subset. + ( + (let subeffect = trait_ref.get_effect()) + (prove_effect_subset(decls, env, assumptions, subeffect, superset) => constraints) + --- ("associated effect") + (prove_effect_subset(decls, env, assumptions, Effect::Atomic(AtomicEffect::AssociatedEffect(trait_ref)), superset) => constraints) + + ) + } } diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index a5cc818e..58245e1f 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -68,6 +68,10 @@ impl TraitRef { pub fn not_implemented(&self) -> Predicate { Predicate::NotImplemented(self.clone()) } + + pub fn get_effect(&self) -> Effect { + return self.effect.clone(); + } } impl Ty { From 8fb16ad9fb595ba39758a79ffcf8ac8920369e96 Mon Sep 17 00:00:00 2001 From: tiif Date: Mon, 7 Apr 2025 21:48:28 +0800 Subject: [PATCH 64/65] Add tests for associated effect --- .../src/prove/prove_effect_subset.rs | 2 +- tests/const_trait.rs | 54 +++++++++++++++++++ tests/effects.rs | 46 +++++++++++++++- 3 files changed, 99 insertions(+), 3 deletions(-) diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs index a0ed1a10..5d560fb7 100644 --- a/crates/formality-prove/src/prove/prove_effect_subset.rs +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -40,7 +40,7 @@ judgment_fn! { (prove_effect_subset(decls, env, assumptions, Effect::Atomic(subeffect), superset) => constraints) ) - // If it is associated effect, get the effect from the trait_ref, then proceed with normal prove_effect_subset. + // For associated effect, we get the actual effect from the trait_ref, then proceed with normal prove_effect_subset. ( (let subeffect = trait_ref.get_effect()) (prove_effect_subset(decls, env, assumptions, subeffect, superset) => constraints) diff --git a/tests/const_trait.rs b/tests/const_trait.rs index 1f3f79e9..18bd82eb 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -92,3 +92,57 @@ fn test_const_fn_with_runtime_effect() { the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because judgment had no applicable rules: `prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]); } + + +#[test] +fn test_associated_effect_reflexive() { + let BASE_PROGRAM: &str = "[ + crate test { + trait Foo {} + + fn foo() -> () random_keyword do AssociatedEffect(Foo()) {(AssociatedEffect(Foo()))} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + } + + + // TODO: fix the rule to make this work. +#[test] +fn test_const_associated_effect_in_const_fn() { + let BASE_PROGRAM: &str = "[ + crate test { + const trait Foo {} + + fn foo() -> () random_keyword do const {(AssociatedEffect(Foo()))} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + } + + +#[test] +fn test_const_associated_effect_in_runtime_fn() { + let BASE_PROGRAM: &str = "[ + crate test { + const trait Foo {} + + fn foo() -> () random_keyword do runtime {(AssociatedEffect(Foo()))} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + } + + //TODO: add test where associated effect is in the do bound? diff --git a/tests/effects.rs b/tests/effects.rs index cacc047b..f68c6e6a 100644 --- a/tests/effects.rs +++ b/tests/effects.rs @@ -1,10 +1,11 @@ use a_mir_formality::test_where_clause; use formality_core::test_util::ResultTestExt; +use formality_types::grammar::{TraitId, TraitRef}; // FIXME: we don't need this for the current set of test to pass, but we might eventually need this, so keep this here. const EFFECT_PREFIX: &str = "[ crate test { - trait Trait { + trait Foo { } } ]"; @@ -34,7 +35,7 @@ fn test_const_runtime_basic() { fn test_runtime_subset_const() { test_where_clause(EFFECT_PREFIX, "{} => {@subset(runtime, const)}") .assert_err(expect_test::expect![[r#" - judgment `prove { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Trait ], [], [], [], [], [], {Trait}, {}) }` failed at the following rule(s): + judgment `prove { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because judgment `prove_wc_list { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because @@ -56,3 +57,44 @@ fn test_three_atomic_effect() { test_where_clause(EFFECT_PREFIX, "{} => {@subset(union(union(const, const), runtime), runtime)}") .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); } + +#[test] +fn test_associated_effect() { + // A runtime associated effect is subset of runtime. + test_where_clause(EFFECT_PREFIX, "{} => {@ subset(AssociatedEffect(Foo()) , runtime)}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + + + // An associated effect is subset of itself. + test_where_clause(EFFECT_PREFIX, "{} => {@ subset(AssociatedEffect(Foo()) , AssociatedEffect(Foo()))}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + +} + +#[test] +fn test_assoc_runtime_not_subset_of_const() { + // A runtime associated effect is NOT subset of const. + test_where_clause(EFFECT_PREFIX, "{} => {@ subset(AssociatedEffect(Foo()) , const)}") + .assert_err(expect_test::expect![[r#" + judgment `prove { goal: {@ subset(AssociatedEffect(Foo()) , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ subset(AssociatedEffect(Foo()) , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ subset(AssociatedEffect(Foo()) , const), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "effect subset" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_effect_subset { subset: AssociatedEffect(Foo()), superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "associated effect" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove_effect_subset { subset: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "atomic" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_atomic_effect_subset { atomic_subeffect: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "transitive" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_effect_upper_bound { f1: runtime, assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "atomic" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_atomic_effect_subset { atomic_subeffect: AssociatedEffect(Foo()), superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "transitive" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_effect_upper_bound { f1: AssociatedEffect(Foo()), assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_atomic_effect_eq { f1: AssociatedEffect(Foo()), f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]); +} From 49d11e3c90feb7ef8ad7ce5086ed590c199a42ba Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 8 Apr 2025 23:51:33 +0800 Subject: [PATCH 65/65] Fix the tests --- tests/const_trait.rs | 100 ++++++++++++++++++++++++++++++++++++++----- 1 file changed, 89 insertions(+), 11 deletions(-) diff --git a/tests/const_trait.rs b/tests/const_trait.rs index 18bd82eb..9c9a6f1f 100644 --- a/tests/const_trait.rs +++ b/tests/const_trait.rs @@ -94,13 +94,29 @@ fn test_const_fn_with_runtime_effect() { } +// FIXME(tiif): The trait ref syntax is a little bit confusing for now, +// `const Foo()` is the syntax for a trait ref named Foo with const effect +// `Foo()` is the syntax for a trait ref named Foo with runtime effect. + + +/// Somewhat equivalent to +/// ``` +/// fn foo() +/// where +/// T: Default, +/// do +/// +/// { +/// ::default() +/// } +/// ```` #[test] fn test_associated_effect_reflexive() { + // FIXME (tiif): we should find a way to define the trait, and only using the TraitId instead of creating + // Default trait ref twice.... let BASE_PROGRAM: &str = "[ crate test { - trait Foo {} - - fn foo() -> () random_keyword do AssociatedEffect(Foo()) {(AssociatedEffect(Foo()))} + fn foo() -> () random_keyword do AssociatedEffect(Default()) {(AssociatedEffect(Default()))} } ]"; test_where_clause( @@ -111,14 +127,22 @@ fn test_associated_effect_reflexive() { } - // TODO: fix the rule to make this work. +/// Somewhat equivalent to +/// ``` +/// fn foo() +/// where +/// T: Default, +/// do +/// const +/// { +/// ::default() +/// } +/// ```` #[test] fn test_const_associated_effect_in_const_fn() { let BASE_PROGRAM: &str = "[ crate test { - const trait Foo {} - - fn foo() -> () random_keyword do const {(AssociatedEffect(Foo()))} + fn foo() -> () random_keyword do const {(AssociatedEffect(const Default()))} } ]"; test_where_clause( @@ -129,13 +153,22 @@ fn test_const_associated_effect_in_const_fn() { } +/// Somewhat equivalent to +/// ``` +/// fn foo() +/// where +/// T: Default, +/// do +/// runtime +/// { +/// ::default() +/// } +/// ```` #[test] fn test_const_associated_effect_in_runtime_fn() { let BASE_PROGRAM: &str = "[ crate test { - const trait Foo {} - - fn foo() -> () random_keyword do runtime {(AssociatedEffect(Foo()))} + fn foo() -> () random_keyword do runtime {(AssociatedEffect(const Default()))} } ]"; test_where_clause( @@ -145,4 +178,49 @@ fn test_const_associated_effect_in_runtime_fn() { .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); } - //TODO: add test where associated effect is in the do bound? +/// Somewhat equivalent to +/// ``` +/// fn foo() +/// where +/// T: Default, +/// do +/// const +/// { +/// ::default() +/// } +/// ```` +#[test] +fn test_runtime_associated_effect_in_const_fn() { + let BASE_PROGRAM: &str = "[ + crate test { + fn foo() -> () random_keyword do const {(AssociatedEffect(Default()))} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_err(expect_test::expect![[r#" + judgment `prove { goal: {@ subset(AssociatedEffect(Default()) , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ subset(AssociatedEffect(Default()) , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ subset(AssociatedEffect(Default()) , const), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "effect subset" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_effect_subset { subset: AssociatedEffect(Default()), superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "associated effect" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove_effect_subset { subset: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "atomic" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_atomic_effect_subset { atomic_subeffect: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "transitive" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_effect_upper_bound { f1: runtime, assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "atomic" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_atomic_effect_subset { atomic_subeffect: AssociatedEffect(Default()), superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "transitive" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_effect_upper_bound { f1: AssociatedEffect(Default()), assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_atomic_effect_eq { f1: AssociatedEffect(Default()), f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]); + } +