extend assertions so they can be results

Author: nikomatsakis

crates/formality-core/src/judgment.rs

@@ -2,6 +2,9 @@ use std::cell::RefCell;
 
 use crate::{fixed_point::FixedPointStack, Fallible, Set};
 
+mod assertion;
+pub use assertion::JudgmentAssertion;
+
 mod proven_set;
 pub use proven_set::{FailedJudgment, FailedRule, ProvenSet, RuleFailureCause, TryIntoIter};
 
@@ -77,8 +80,18 @@ macro_rules! judgment_fn {
             $(let $input_name: $input_ty = $crate::Upcast::upcast($input_name);)*
 
             $(
-                // Assertions are preconditions
-                assert!($assert_expr);
+                // Assertions are preconditions.
+                //
+                // NB: we can't use `$crate` in this expression because of the `respan!` call,
+                // which messes up `$crate` resolution. But we need the respan call for track_caller to properly
+                // assign the span of the panic to the assertion expression and not the invocation of the judgment_fn
+                // macro. Annoying! But our proc macros already reference `formality_core` so that seems ok.
+                $crate::respan!(
+                    $assert_expr
+                    (
+                        formality_core::judgment::JudgmentAssertion::assert($assert_expr, stringify!($assert_expr));
+                    )
+                );
             )*
 
             $(

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

@@ -0,0 +1,25 @@
+use std::fmt::Debug;
+
+/// Helper trait for assertions in judgments.
+/// For each `assert(x)`, we will invoke `JudgmentAssertion::assert`.
+/// This allows us to support both booleans and results.
+pub trait JudgmentAssertion {
+    fn assert(self, expr: &str);
+}
+
+impl<E: Debug> JudgmentAssertion for Result<(), E> {
+    #[track_caller]
+    fn assert(self, expr: &str) {
+        match self {
+            Ok(()) => (),
+            Err(e) => panic!("judgment assertion failed: `{expr}` got {e:?}"),
+        }
+    }
+}
+
+impl JudgmentAssertion for bool {
+    #[track_caller]
+    fn assert(self, expr: &str) {
+        assert!(self, "judgment assertion failed: `{expr}` is false");
+    }
+}

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

@@ -28,6 +28,8 @@ impl Check {
 judgment_fn!(
     fn jfn(c: Check, x: u32) => u32 {
         debug(c, x)
+        assert(x < 100)
+        assert(check_x(x))
 
         (
             (let y = c.is(x)?)
@@ -44,15 +46,20 @@ judgment_fn!(
     }
 );
 
+fn check_x(x: u32) -> Fallible<()> {
+    if x > 75 {
+        bail!("invalid x: {x}")
+    }
+    Ok(())
+}
+
 #[test]
 fn is_equal_22() {
-    jfn(Check { x: 22 }, 22).assert_ok(expect_test::expect![
-        [r#"
+    jfn(Check { x: 22 }, 22).assert_ok(expect_test::expect![[r#"
         {
           22,
         }
-    "#]
-    ]);
+    "#]]);
 }
 
 #[test]
@@ -74,3 +81,15 @@ fn is_not_equal() {
           the rule "rule" failed at step #0 (src/file.rs:LL:CC) because
             expected 22 got 23"#]]);
 }
+
+#[test]
+#[should_panic(expected = "judgment assertion failed: `x < 100` is false")]
+fn bool_assertion_fails() {
+    let _ = jfn(Check { x: 22 }, 110);
+}
+
+#[test]
+#[should_panic(expected = "judgment assertion failed: `check_x(x)` got invalid x")]
+fn result_assertion_fails() {
+    let _ = jfn(Check { x: 22 }, 76);
+}