Merge pull request #186 from FullyNonlinear/main

Use unique names for rules in prove_wc
rust-lang · Jul 11, 2024 · 8cc6aba · 8cc6aba
2 parents 8260367 + 0f0f782
commit 8cc6aba
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 10 deletions.
diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs
@@ -42,13 +42,13 @@ judgment_fn! {
         (
             (&assumptions => a)!
             (prove_via(&decls, &env, &assumptions, a, &goal) => c)
-            ----------------------------- ("assumption")
+            ----------------------------- ("assumption - predicate")
             (prove_wc(decls, env, assumptions, WcData::Predicate(goal)) => c)
         )
         (
             (&assumptions => a)!
             (prove_via(&decls, &env, &assumptions, a, &goal) => c)
-            ----------------------------- ("assumption")
+            ----------------------------- ("assumption - relation")
             (prove_wc(decls, env, assumptions, WcData::Relation(goal)) => c)
         )
 

diff --git a/crates/formality-prove/src/test/eq_partial_eq.rs b/crates/formality-prove/src/test/eq_partial_eq.rs
@@ -51,7 +51,7 @@ fn not_partial_eq_implies_eq() {
                 judgment `prove_wc { goal: if {PartialEq(!ty_1)} Eq(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                   the rule "implies" failed at step #0 (src/file.rs:LL:CC) because
                     judgment `prove_wc { goal: Eq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                      the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
+                      the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because
                         judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
                       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: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`"#]]);
@@ -70,21 +70,21 @@ fn universals_not_eq() {
                 judgment `prove_wc { goal: if {Eq(!ty_1)} PartialEq(!ty_2), assumptions: {}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                   the rule "implies" failed at step #0 (src/file.rs:LL:CC) because
                     judgment `prove_wc { goal: PartialEq(!ty_2), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                      the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
+                      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 }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
                       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)}, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                           the rule "prove_after" failed at step #1 (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 }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }` 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 }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                  the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
+                                  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 }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                                       the rule "predicate-congruence-axiom" failed at step #3 (src/file.rs:LL:CC) because
                                         judgment `prove_wc_list { goal: {!ty_0 = !ty_1}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                                           the rule "some" failed at step #0 (src/file.rs:LL:CC) because
                                             judgment `prove_wc { goal: !ty_0 = !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                              the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
+                                              the rule "assumption - relation" failed at step #1 (src/file.rs:LL:CC) because
                                                 judgment had no applicable rules: `prove_via { goal: !ty_0 = !ty_1, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
                                               the rule "eq" failed at step #0 (src/file.rs:LL:CC) because
                                                 judgment `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }` failed at the following rule(s):

diff --git a/crates/formality-prove/src/test/magic_copy.rs b/crates/formality-prove/src/test/magic_copy.rs
@@ -40,7 +40,7 @@ fn all_t_not_magic() {
                                 judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s):
                                   the rule "some" failed at step #0 (src/file.rs:LL:CC) because
                                     judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                      the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
+                                      the rule "assumption - relation" failed at step #1 (src/file.rs:LL:CC) because
                                         judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`
                                       the rule "eq" failed at step #0 (src/file.rs:LL:CC) because
                                         judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s):
@@ -85,7 +85,7 @@ fn all_t_not_copy() {
                     judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s):
                       the rule "some" failed at step #0 (src/file.rs:LL:CC) because
                         judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                          the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
+                          the rule "assumption - relation" failed at step #1 (src/file.rs:LL:CC) because
                             judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`
                           the rule "eq" failed at step #0 (src/file.rs:LL:CC) because
                             judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s):
@@ -117,7 +117,7 @@ fn all_t_not_copy() {
                                             judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s):
                                               the rule "some" failed at step #0 (src/file.rs:LL:CC) because
                                                 judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                                  the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
+                                                  the rule "assumption - relation" failed at step #1 (src/file.rs:LL:CC) because
                                                     judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`
                                                   the rule "eq" failed at step #0 (src/file.rs:LL:CC) because
                                                     judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s):

diff --git a/src/test/consts.rs b/src/test/consts.rs
@@ -21,7 +21,7 @@ fn nonsense_rigid_const_bound() {
                 1: judgment `prove_wc_list { goal: {u32 = bool, @ wf(u32), @ wf(const value(0, bool))}, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s):
                      the rule "some" failed at step #0 (src/file.rs:LL:CC) because
                        judgment `prove_wc { goal: u32 = bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s):
-                         the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
+                         the rule "assumption - relation" failed at step #1 (src/file.rs:LL:CC) because
                            judgment had no applicable rules: `prove_via { goal: u32 = bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }`
                          the rule "eq" failed at step #0 (src/file.rs:LL:CC) because
                            judgment `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s):