Merge pull request #161 from nikomatsakis/upcast-arc-and-more

More usability improvements
rust-lang · Jan 4, 2024 · 0de138c · 0de138c
2 parents a2d8b3d + f913710
commit 0de138c
Show file tree

Hide file tree

Showing 26 changed files with 269 additions and 83 deletions.
diff --git a/crates/formality-core/src/collections.rs b/crates/formality-core/src/collections.rs
@@ -70,13 +70,37 @@ impl<T: Ord + Clone> VecExt<T> for Vec<T> {
 }
 
 pub trait SetExt<T>: Sized {
-    fn split_first(self) -> Option<(T, Self)>;
+    fn split_first(self) -> Option<(T, Set<T>)>;
 
-    fn union_with(self, other: Self) -> Self;
+    fn union_with(self, other: impl Upcast<Set<T>>) -> Set<T>;
 
-    fn plus(self, other: T) -> Self;
+    fn with_element(self, other: impl Upcast<T>) -> Set<T>;
 
-    fn split_nth(&self, i: usize) -> Option<(T, Self)>;
+    fn without_element(self, other: impl Upcast<T>) -> Set<T>;
+
+    fn split_nth(&self, i: usize) -> Option<(T, Set<T>)>;
+}
+
+impl<T: Ord + Clone> SetExt<T> for &Set<T> {
+    fn split_first(self) -> Option<(T, Set<T>)> {
+        self.clone().split_first()
+    }
+
+    fn union_with(self, other: impl Upcast<Set<T>>) -> Set<T> {
+        self.clone().union_with(other)
+    }
+
+    fn with_element(self, other: impl Upcast<T>) -> Set<T> {
+        self.clone().with_element(other)
+    }
+
+    fn without_element(self, other: impl Upcast<T>) -> Set<T> {
+        self.clone().without_element(other)
+    }
+
+    fn split_nth(&self, i: usize) -> Option<(T, Set<T>)> {
+        <Set<T>>::split_nth(self, i)
+    }
 }
 
 impl<T: Ord + Clone> SetExt<T> for Set<T> {
@@ -87,22 +111,28 @@ impl<T: Ord + Clone> SetExt<T> for Set<T> {
         Some((e, c))
     }
 
-    fn split_nth(&self, i: usize) -> Option<(T, Self)> {
+    fn split_nth(&self, i: usize) -> Option<(T, Set<T>)> {
         let mut s = self.clone();
         let item = self.iter().skip(i).next()?;
         let item = s.take(item).unwrap();
         Some((item, s))
     }
 
-    fn union_with(mut self, other: Self) -> Self {
+    fn union_with(mut self, other: impl Upcast<Set<T>>) -> Set<T> {
+        let other: Set<T> = other.upcast();
         for item in other {
             self.insert(item);
         }
         self
     }
 
-    fn plus(mut self, other: T) -> Self {
-        self.insert(other);
+    fn with_element(mut self, other: impl Upcast<T>) -> Set<T> {
+        self.insert(other.upcast());
+        self
+    }
+
+    fn without_element(mut self, other: impl Upcast<T>) -> Set<T> {
+        self.remove(&other.upcast());
         self
     }
 }

diff --git a/crates/formality-core/src/judgment.rs b/crates/formality-core/src/judgment.rs
@@ -178,15 +178,20 @@ macro_rules! push_rules {
     ) => {
         // Found the conclusion.
         {
-            // give the user a type error if the name they gave
-            // in the conclusion is not the same as the name of the
-            // function
-            #[allow(dead_code)]
-            struct WrongJudgmentNameInConclusion;
-            const _: WrongJudgmentNameInConclusion = {
-                let $judgment_name = WrongJudgmentNameInConclusion;
+            $crate::respan!(
                 $conclusion_name
-            };
+                (
+                    // give the user a type error if the name they gave
+                    // in the conclusion is not the same as the name of the
+                    // function
+                    #[allow(dead_code)]
+                    struct WrongJudgmentNameInConclusion;
+                    const _: WrongJudgmentNameInConclusion = {
+                        let $judgment_name = WrongJudgmentNameInConclusion;
+                        $conclusion_name
+                    };
+                )
+            );
 
             if let Some(__JudgmentStruct($($input_names),*)) = Some($input_value) {
                 $crate::push_rules!(@match
@@ -283,33 +288,104 @@ macro_rules! push_rules {
     // expression `v` is carried in from the conclusion and forms the final
     // output of this rule, once all the conditions are evaluated.
 
-    (@body $args:tt; $inputs:tt; $step_index:expr; (if $c:expr) $($m:tt)*) => {
-        if $c {
+    (@body $args:tt; $inputs:tt; $step_index:expr; (if let $p:pat = $e:expr) $($m:tt)*) => {
+        let value = &$e;
+        if let $p = Clone::clone(value) {
             $crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
         } else {
-            $crate::push_rules!(@record_failure $inputs; $step_index, $c; $crate::judgment::RuleFailureCause::IfFalse {
-                expr: stringify!($c).to_string(),
+            $crate::push_rules!(@record_failure $inputs; $step_index, $e; $crate::judgment::RuleFailureCause::IfLetDidNotMatch {
+                pattern: stringify!($p).to_string(),
+                value: format!("{:?}", value),
             });
         }
     };
 
-    (@body $args:tt; $inputs:tt; $step_index:expr; (assert $c:expr) $($m:tt)*) => {
-        assert!($c);
-        $crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
+    // For `(if ...)`, we have special treatment to try and extract the arguments so we can give better information
+    // about why the expression evaluated to false.
+    (@body $args:tt; $inputs:tt; $step_index:expr; (if $($c:tt)*) $($m:tt)*) => {
+        $crate::push_rules!(@body_if $args; $inputs; $step_index; $($c)*; $($c)*; $($m)*)
     };
 
-    (@body $args:tt; $inputs:tt; $step_index:expr; (if let $p:pat = $e:expr) $($m:tt)*) => {
-        let value = &$e;
-        if let $p = Clone::clone(value) {
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident . $method:ident ( ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0); arg0.$method(); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; ! $arg0:ident . $method:ident ( ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0); !arg0.$method(); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident . $method:ident ( $arg1:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); arg0.$method(arg1); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; ! $arg0:ident . $method:ident ( $arg1:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); !arg0.$method(arg1); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident . $method:ident ( $arg1:expr, $arg2:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1, arg2 = $arg2); arg0.$method(arg1, arg2); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; ! $arg0:ident . $method:ident ( $arg1:expr, $arg2:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1, arg2 = $arg2); !arg0.$method(arg1, arg2); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $func:ident ( $arg0:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0); $func(arg0); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; ! $func:ident ( $arg0:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0); !$func(arg0); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $func:ident ( $arg0:expr, $arg1:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); $func(arg0, arg1); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; ! $func:ident ( $arg0:expr, $arg1:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); ! $func(arg0, arg1); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident == $arg1:ident; $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); arg0 == arg1; $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident != $arg1:ident; $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); arg0 != arg1; $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $e:expr; $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (); $e; $origcond; $($m)*)
+    };
+
+    (@structured_if $args:tt; $inputs:tt; $step_index:expr; ($($argn:ident = $arge:expr),*); $cond:expr; $origcond:expr; $($m:tt)*) => {
+        $(
+            let $argn = &$arge;
+        )*
+        if {
+            $(
+                let $argn = Clone::clone($argn);
+            )*
+            $cond
+        } {
             $crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
         } else {
-            $crate::push_rules!(@record_failure $inputs; $step_index, $e; $crate::judgment::RuleFailureCause::IfLetDidNotMatch {
-                pattern: stringify!($p).to_string(),
-                value: format!("{:?}", value),
+            $crate::push_rules!(@record_failure $inputs; $step_index, $origcond; $crate::judgment::RuleFailureCause::IfFalse {
+                expr: stringify!($origcond).to_string(),
+                args: vec![
+                    $(
+                        (stringify!($arge).to_string(), format!("{:?}", $argn)),
+                    )*
+                ],
             });
         }
     };
 
+    (@body $args:tt; $inputs:tt; $step_index:expr; (assert $c:expr) $($m:tt)*) => {
+        assert!($c);
+        $crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
+    };
+
     (@body $args:tt; $inputs:tt; $step_index:expr; ($i:expr => $p:pat) $($m:tt)*) => {
         // Explicitly calling `into_iter` silences some annoying lints
         // in the case where `$i` is an `Option` or a `Result`

diff --git a/crates/formality-core/src/judgment/proven_set.rs b/crates/formality-core/src/judgment/proven_set.rs
@@ -1,4 +1,4 @@
-use crate::{set, Set, SetExt};
+use crate::{set, Set};
 use std::{
     fmt::Debug,
     hash::{Hash, Hasher},
@@ -316,11 +316,12 @@ impl FailedJudgment {
                     // This will return a boolean indicating if all the failed rules
                     // ultimately failed because of a cycle.
 
+                    let mut stack1 = stack.clone();
+                    stack1.insert(&judgment.judgment);
+
                     let judgment_has_non_cycle;
-                    (judgment.failed_rules, judgment_has_non_cycle) = Self::strip_cycles(
-                        stack.clone().plus(&judgment.judgment),
-                        judgment.failed_rules,
-                    );
+                    (judgment.failed_rules, judgment_has_non_cycle) =
+                        Self::strip_cycles(stack1, judgment.failed_rules);
                     failed_rule.cause = RuleFailureCause::FailedJudgment(judgment);
 
                     if judgment_has_non_cycle.0 {
@@ -384,7 +385,14 @@ impl FailedRule {
 #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Debug)]
 pub enum RuleFailureCause {
     /// The rule did not succeed because an `(if X)` condition evaluated to false.
-    IfFalse { expr: String },
+    IfFalse {
+        /// The stringified form of the expression.
+        expr: String,
+
+        /// A set of pairs with the stringified form of arguments within the expression plus the debug representation of its value.
+        /// This is a best effort extraction via the macro.
+        args: Vec<(String, String)>,
+    },
 
     /// The rule did not succeed because an `(if let)` pattern failed to match.
     IfLetDidNotMatch { pattern: String, value: String },
@@ -426,8 +434,8 @@ impl std::fmt::Display for FailedJudgment {
         if failed_rules.is_empty() {
             write!(f, "judgment had no applicable rules: `{judgment}` ",)
         } else {
-            let rules: String = failed_rules.iter().map(|r| r.to_string()).collect();
-            let rules = indent(rules);
+            let rules: Vec<String> = failed_rules.iter().map(|r| r.to_string()).collect();
+            let rules = indent(rules.join("\n"));
             write!(
                 f,
                 "judgment `{judgment}` failed at the following rule(s):\n{rules}"
@@ -465,8 +473,12 @@ impl std::fmt::Display for FailedRule {
 impl std::fmt::Display for RuleFailureCause {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self {
-            RuleFailureCause::IfFalse { expr } => {
-                write!(f, "condition evaluted to false: `{expr}`")
+            RuleFailureCause::IfFalse { expr, args } => {
+                write!(f, "condition evaluted to false: `{expr}`")?;
+                for (arg_expr, arg_value) in args {
+                    write!(f, "\n  {arg_expr} = {arg_value}")?;
+                }
+                Ok(())
             }
             RuleFailureCause::IfLetDidNotMatch { pattern, value } => {
                 write!(f, "pattern `{pattern}` did not match value `{value}`")
@@ -492,7 +504,7 @@ impl<T: Debug> std::fmt::Display for ProvenSet<T> {
             Data::Success(set) => {
                 write!(f, "{{\n")?;
                 for item in set {
-                    write!(f, "{}", indent(format!("{item:?},\n")))?;
+                    write!(f, "{},\n", indent(format!("{item:?}")))?;
                 }
                 write!(f, "}}\n")?;
                 Ok(())
@@ -503,14 +515,12 @@ impl<T: Debug> std::fmt::Display for ProvenSet<T> {
 
 fn indent(s: impl std::fmt::Display) -> String {
     let s = s.to_string();
-    s.lines()
+    let lines: Vec<String> = s
+        .lines()
         .map(|l| format!("  {l}"))
         .map(|l| l.trim_end().to_string())
-        .map(|mut l| {
-            l.push_str("\n");
-            l
-        })
-        .collect()
+        .collect();
+    lines.join("\n")
 }
 
 /// This trait is used for the `(foo => bar)` patterns.

diff --git a/crates/formality-core/src/judgment/test_filtered.rs b/crates/formality-core/src/judgment/test_filtered.rs
@@ -51,8 +51,7 @@ fn judgment() {
     transitive_reachable(&graph, 0).assert_err(expect_test::expect![[r#"
         judgment `transitive_reachable { node: 0, g: Graph { edges: [(0, 1), (1, 2), (2, 4), (2, 3), (3, 6), (4, 8), (8, 10)] } }` failed at the following rule(s):
           the rule "base" failed at step #1 (src/file.rs:LL:CC) because
-            condition evaluted to false: `b % 2 == 0`
-    "#]]);
+            condition evaluted to false: `b % 2 == 0`"#]]);
 
     transitive_reachable(&graph, 2).assert_ok(expect_test::expect![[r#"
         {

diff --git a/crates/formality-core/src/test_util.rs b/crates/formality-core/src/test_util.rs
@@ -60,6 +60,7 @@ where
     T: Debug,
     E: Debug,
 {
+    #[track_caller]
     fn assert_ok(self, expect: expect_test::Expect) {
         match self {
             Ok(v) => {
@@ -71,11 +72,12 @@ where
         }
     }
 
+    #[track_caller]
     fn assert_err(self, expect: expect_test::Expect) {
         match self {
             Ok(v) => panic!("expected `Err`, got `Ok`: {v:?}"),
             Err(e) => {
-                expect.assert_eq(&format!("{e:?}"));
+                expect.assert_eq(&normalize_paths(format!("{e:?}")));
             }
         }
     }

diff --git a/crates/formality-prove/src/test/adt_wf.rs b/crates/formality-prove/src/test/adt_wf.rs
@@ -63,6 +63,5 @@ fn not_well_formed_adt() {
                           the rule "some" failed at step #0 (src/file.rs:LL:CC) because
                             judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
                               the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
-                                expression evaluated to an empty collection: `decls.trait_invariants()`
-    "#]]);
+                                expression evaluated to an empty collection: `decls.trait_invariants()`"#]]);
 }
diff --git a/crates/formality-prove/src/test/eq_assumptions.rs b/crates/formality-prove/src/test/eq_assumptions.rs
@@ -192,8 +192,7 @@ fn test_normalize_assoc_ty_existential0() {
                                                                           the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because
                                                                             condition evaluted to false: `env.universe(p) < env.universe(v)`
                                                       the rule "normalize-via-impl" failed at step #0 (src/file.rs:LL:CC) because
-                                                        expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`
-    "#]]);
+                                                        expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`"#]]);
 }
 
 #[test]

diff --git a/crates/formality-prove/src/test/eq_partial_eq.rs b/crates/formality-prove/src/test/eq_partial_eq.rs
@@ -54,8 +54,7 @@ fn not_partial_eq_implies_eq() {
                       the rule "assumption" 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], coherence_mode: false }, 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], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
-    "#]]);
+                        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], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`"#]]);
 }
 
 #[test]
@@ -102,6 +101,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], coherence_mode: false }, 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: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
-    "#]]);
+                                    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], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`"#]]);
 }
diff --git a/crates/formality-prove/src/test/is_local.rs b/crates/formality-prove/src/test/is_local.rs
@@ -22,7 +22,8 @@ fn test_forall_not_local() {
                     judgment `is_local_trait_ref { goal: Debug(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], coherence_mode: true }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                       the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because
                         condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)`
-    "#]]);
+                          decls = decls(222, [], [], [], [], [], [], {}, {})
+                          &goal.trait_id = Debug"#]]);
 }
 
 #[test]