support ? in let/if-let judgment fn clauses

Author: nikomatsakis

crates/formality-core/src/judgment.rs

@@ -1,10 +1,11 @@
 use std::cell::RefCell;
 
-use crate::{fixed_point::FixedPointStack, Set};
+use crate::{fixed_point::FixedPointStack, Fallible, Set};
 
 mod proven_set;
 pub use proven_set::{FailedJudgment, FailedRule, ProvenSet, RuleFailureCause, TryIntoIter};
 
+mod test_fallible;
 mod test_filtered;
 mod test_reachable;
 
@@ -290,14 +291,21 @@ macro_rules! push_rules {
     // output of this rule, once all the conditions are evaluated.
 
     (@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, $e; $crate::judgment::RuleFailureCause::IfLetDidNotMatch {
-                pattern: stringify!($p).to_string(),
-                value: format!("{:?}", value),
-            });
+        match $crate::judgment::try_catch(|| Ok($e)) {
+            Ok(value) => {
+                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, $e; $crate::judgment::RuleFailureCause::IfLetDidNotMatch {
+                        pattern: stringify!($p).to_string(),
+                        value: format!("{:?}", value),
+                    });
+                }
+            }
+
+            Err(e) => {
+                $crate::push_rules!(@record_failure $inputs; $step_index, $e; e);
+            }
         }
     };
 
@@ -405,16 +413,28 @@ macro_rules! push_rules {
     (@body $args:tt; $inputs:tt; $step_index:expr; (let $p:ident /*[1]*/: $t:ty = $i:expr) $($m:tt)*) => {
         // [1] I'd prefer to have `$p:pat` but the follow-set rules don't allow for it.
         // That's dumb.
-        {
-            let $p : $t = $i;
-            $crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
+        match $crate::judgment::try_catch::<$t>(|| Ok($i)) {
+            Ok(p) => {
+                let $p = p;
+                $crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
+            }
+
+            Err(e) => {
+                $crate::push_rules!(@record_failure $inputs; $step_index, $i; e);
+            }
         }
     };
 
     (@body $args:tt; $inputs:tt; $step_index:expr; (let $p:pat = $i:expr) $($m:tt)*) => {
-        {
-            let $p = $i;
-            $crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
+        match $crate::judgment::try_catch(|| Ok($i)) {
+            Ok(p) => {
+                let $p = p; // this enforces that `$p` is infalliblr
+                $crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
+            }
+
+            Err(e) => {
+                $crate::push_rules!(@record_failure $inputs; $step_index, $i; e);
+            }
         }
     };
 
@@ -464,3 +484,17 @@ macro_rules! push_rules {
         }
     }
 }
+
+/// Helper function that just calls `f` and returns the value.
+/// Used for implementing `judgement_fn` macro to allow expressions to include `?`.
+pub fn try_catch<R>(f: impl FnOnce() -> Fallible<R>) -> Result<R, RuleFailureCause> {
+    match f() {
+        Ok(v) => Ok(v),
+
+        // Kind of dumb that `Inapplicable` only includes a `String` and not an `anyhow::Error`
+        // but it's super annoying to package one of those up in the way we want.
+        Err(e) => Err(RuleFailureCause::Inapplicable {
+            reason: e.to_string(),
+        }),
+    }
+}

crates/formality-core/src/judgment/proven_set.rs

@@ -404,7 +404,7 @@ pub enum RuleFailureCause {
     /// (for the given reason).
     FailedJudgment(Box<FailedJudgment>),
 
-    /// The rule did not succeed for some custom reason; this is not generated by the macro.
+    /// The rule did not succeed for some custom reason. This occurs when a `?` fails in the judgment function macro.
     Inapplicable { reason: String },
 
     /// The rule attempted to prove something that was already in the process of being proven

crates/formality-core/src/judgment/test_fallible.rs

@@ -0,0 +1,76 @@
+#![cfg(test)]
+
+//! Test that we permit the use of `?` in `let` and `if let`
+
+use anyhow::bail;
+
+use crate::cast_impl;
+use crate::judgment_fn;
+use crate::Fallible;
+
+#[derive(Ord, PartialOrd, Eq, PartialEq, Clone, Debug, Hash)]
+struct Check {
+    x: u32,
+}
+
+cast_impl!(Check);
+
+impl Check {
+    fn is(&self, x: u32) -> Fallible<u32> {
+        if self.x == x {
+            Ok(x)
+        } else {
+            bail!("expected {} got {}", self.x, x)
+        }
+    }
+}
+
+judgment_fn!(
+    fn jfn(c: Check, x: u32) => u32 {
+        debug(c, x)
+
+        (
+            (let y = c.is(x)?)
+            --------------------------------------- ("rule")
+            (jfn(c, x) => y)
+        )
+
+
+        (
+            (if let 44 = c.is(x)?)
+            --------------------------------------- ("other-rule")
+            (jfn(c, x) => 45)
+        )
+    }
+);
+
+#[test]
+fn is_equal_22() {
+    jfn(Check { x: 22 }, 22).assert_ok(expect_test::expect![
+        [r#"
+        {
+          22,
+        }
+    "#]
+    ]);
+}
+
+#[test]
+fn is_equal_44() {
+    jfn(Check { x: 44 }, 44).assert_ok(expect_test::expect![[r#"
+        {
+          44,
+          45,
+        }
+    "#]]);
+}
+
+#[test]
+fn is_not_equal() {
+    jfn(Check { x: 22 }, 23).assert_err(expect_test::expect![[r#"
+        judgment `jfn { c: Check { x: 22 }, x: 23 }` failed at the following rule(s):
+          the rule "other-rule" failed at step #0 (src/file.rs:LL:CC) because
+            expected 22 got 23
+          the rule "rule" failed at step #0 (src/file.rs:LL:CC) because
+            expected 22 got 23"#]]);
+}