support one-off judgments in type check

The idea is that judgment functions correspond
to "Random Rust Code" in the compiler
and Predicates/Relations are limited to
things that can appear in where-clauses
(explicitly or implicitly).

The `formality_prove` module then roughly
corresponds to the trait system + type
inference logic in rustc.

Author: nikomatsakis

crates/formality-check/src/lib.rs

@@ -3,13 +3,16 @@
 use std::{collections::VecDeque, fmt::Debug};
 
 use anyhow::bail;
-use formality_core::Set;
-use formality_prove::{is_definitely_not_proveable, Decls, Env};
+use formality_core::{ProvenSet, Set};
+use formality_prove::{is_definitely_not_proveable, Constraints, Decls, Env};
 use formality_rust::{
     grammar::{Crate, CrateItem, Program, Test, TestBoundData},
     prove::ToWcs,
 };
-use formality_types::grammar::{CrateId, Fallible, Wcs};
+use formality_types::{
+    grammar::{CrateId, Fallible, Wcs},
+    rust::Visit,
+};
 
 mod mini_rust_check;
 
@@ -134,18 +137,36 @@ impl Check<'_> {
         goal: impl ToWcs + Debug,
     ) -> Fallible<()> {
         let goal: Wcs = goal.to_wcs();
+        self.prove_judgment(env, assumptions, goal.to_wcs(), formality_prove::prove)
+    }
+
+    fn prove_judgment<G>(
+        &self,
+        env: &Env,
+        assumptions: impl ToWcs,
+        goal: G,
+        judgment_fn: impl FnOnce(Decls, Env, Wcs, G) -> ProvenSet<Constraints>,
+    ) -> Fallible<()>
+    where
+        G: Debug + Visit + Clone,
+    {
         let assumptions: Wcs = assumptions.to_wcs();
 
         assert!(env.only_universal_variables());
         assert!(env.encloses((&assumptions, &goal)));
 
-        let cs = formality_prove::prove(self.decls, env, &assumptions, &goal);
+        let cs = judgment_fn(
+            self.decls.clone(),
+            env.clone(),
+            assumptions.clone(),
+            goal.clone(),
+        );
         let cs = cs.into_set()?;
         if cs.iter().any(|c| c.unconditionally_true()) {
             return Ok(());
         }
 
-        bail!("failed to prove {goal:?} given {assumptions:?}, got {cs:?}")
+        bail!("failed to prove `{goal:?}` given `{assumptions:?}`: got {cs:?}")
     }
 
     #[tracing::instrument(level = "Debug", skip(self, assumptions, goal))]

crates/formality-check/src/mini_rust_check.rs

@@ -1,15 +1,15 @@
 use std::iter::zip;
 
-use formality_core::{Fallible, Map, Upcast};
-use formality_prove::Env;
+use formality_core::{judgment_fn, Fallible, Map, Upcast};
+use formality_prove::{prove_normalize, Constraints, Decls, Env};
 use formality_rust::grammar::minirust::ArgumentExpression::{ByValue, InPlace};
 use formality_rust::grammar::minirust::PlaceExpression::Local;
 use formality_rust::grammar::minirust::ValueExpression::{Constant, Fn, Load};
 use formality_rust::grammar::minirust::{
     self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression,
 };
 use formality_rust::grammar::FnBoundData;
-use formality_types::grammar::{CrateId, FnId};
+use formality_types::grammar::{CrateId, FnId, Parameter, RigidName, RigidTy};
 use formality_types::grammar::{Relation, Ty, Wcs};
 
 use crate::{Check, CrateItem};
@@ -228,7 +228,7 @@ impl Check<'_> {
                 // Check if the value is well-formed.
                 let value_ty = self.check_value(typeck_env, switch_value).unwrap();
 
-                self.prove_goal(&typeck_env.env, Wcs::default(), value_ty.is_int())?;
+                self.prove_judgment(&typeck_env.env, &fn_assumptions, value_ty, ty_is_int)?;
 
                 // Ensure all bbid are valid.
                 for switch_target in switch_targets {
@@ -371,3 +371,34 @@ struct TypeckEnv {
     /// declared in the current crate.
     crate_id: CrateId,
 }
+
+judgment_fn! {
+    fn ty_is_int(
+        _decls: Decls,
+        env: Env,
+        assumptions: Wcs,
+        ty: Parameter,
+    ) => Constraints {
+        debug(assumptions, ty, env)
+        // If the type that we are currently checking is rigid, check if it is an int.
+        // If the type can be normalized, normalize until rigid then check if it is an int.
+        // For the rest of the case, it should fail.
+
+        (
+            (prove_normalize(&decl, &env, &assumptions, ty) => (c1, p))
+            (let assumptions = c1.substitution().apply(&assumptions))
+            (ty_is_int(&decl, &env, assumptions, p) => c2)
+            ----------------------------- ("alias_ty is int")
+            (ty_is_int(decl, env, assumptions, ty) => c2)
+        )
+
+        (
+            (if id.is_int())
+            ----------------------------- ("rigid_ty is int")
+            (ty_is_int(_decls, _env, _assumptions, RigidTy {name: RigidName::ScalarId(id), parameters: _}) => Constraints::none(env))
+        )
+
+    }
+}
+
+mod test;

crates/formality-check/src/mini_rust_check/test.rs

@@ -0,0 +1,29 @@
+// Decide how to do this test -- should it be a unit test?
+// Can it be an integration test?
+
+// const TEST_TY_IS_INT: &str = "[
+//     crate test {
+//         trait Id {
+//             type This: [];
+//         }
+
+//         impl<ty T> Id for T {
+//             type This = T;
+//         }
+//     }
+// ]";
+
+// #[test]
+// fn test_ty_is_int() {
+//     test_where_clause(
+//         TEST_TY_IS_INT,
+//         "{} => { <u16 as Id>::This = u16 }",
+//     )
+//     .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }}"]);
+
+//     test_where_clause(
+//         TEST_TY_IS_INT,
+//         "{} => { @is_int(<u16 as Id>::This) }",
+//     )
+//     .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }}"]);
+// }

crates/formality-prove/src/lib.rs

@@ -1,3 +1,12 @@
+//! This crate contains the trait proving + type inference logic.
+//! It correpsonds loosely to the `InferenceContext` and trait solving (fulfillment context, etc)
+//! in the Rust compiler.
+//!
+//! The base operations we export are:
+//!
+//! * [`prove`][] -- prove a set of where-clauses to be true
+//! * [`prove_normalize`][] -- normalize a type one step (typically used in a recursive setup)
+
 // Defines the language used by derive(term) and friends.
 use formality_types::rust::FormalityLang;
 
@@ -7,6 +16,7 @@ mod prove;
 
 pub use decls::*;
 pub use prove::prove;
+pub use prove::prove_normalize::prove_normalize;
 pub use prove::Constraints;
 pub use prove::{is_definitely_not_proveable, may_not_be_provable, negation_via_failure};
 pub use prove::{Bias, Env};

crates/formality-prove/src/prove.rs

@@ -1,13 +1,12 @@
 mod combinators;
 mod constraints;
 mod env;
-mod is_int;
 mod is_local;
 mod minimize;
 mod negation;
 mod prove_after;
 mod prove_eq;
-mod prove_normalize;
+pub mod prove_normalize;
 mod prove_via;
 mod prove_wc;
 mod prove_wc_list;

crates/formality-prove/src/prove/is_int.rs

@@ -14,6 +14,9 @@ use crate::{
 use super::constraints::Constraints;
 
 judgment_fn! {
+    /// Normalize `p` one step, returning a set of constraints and a new parameter `q` that is
+    /// semantically equivalent to `p`. e.g., if p is `<Vec<T> as IntoIterator>::Item`, this would
+    /// return `T`.
     pub fn prove_normalize(
         _decls: Decls,
         env: Env,

crates/formality-prove/src/prove/prove_normalize.rs

@@ -6,7 +6,6 @@ use crate::{
     prove::{
         combinators::for_all,
         env::{Bias, Env},
-        is_int::ty_is_int,
         is_local::{is_local_trait_ref, may_be_remote},
         prove,
         prove_after::prove_after,
@@ -146,11 +145,5 @@ judgment_fn! {
             ----------------------------- ("const has ty")
             (prove_wc(decls, env, assumptions, Predicate::ConstHasType(ct, ty)) => c)
         )
-
-        (
-            (ty_is_int(&decl, env, assumptions, ty) => c)
-            ----------------------------- ("ty is int")
-            (prove_wc(decl, env, assumptions, Relation::IsInt(ty)) => c)
-        )
     }
 }

crates/formality-prove/src/prove/prove_wc.rs

@@ -72,10 +72,6 @@ impl Ty {
     pub fn well_formed(&self) -> Relation {
         Relation::WellFormed(self.upcast())
     }
-
-    pub fn is_int(&self) -> Relation {
-        Relation::IsInt(self.clone())
-    }
 }
 
 impl Parameter {
@@ -182,9 +178,6 @@ pub enum Relation {
 
     #[grammar(@wf($v0))]
     WellFormed(Parameter),
-
-    #[grammar(@is_int($v0))]
-    IsInt(Ty),
 }
 
 impl Relation {
@@ -195,7 +188,6 @@ impl Relation {
             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::IsInt(ty) => (Skeleton::IsInt, vec![ty.to_parameter()]),
         }
     }
 }

crates/formality-types/src/grammar/formulas.rs

@@ -658,15 +658,9 @@ fn test_invalid_value_in_switch_terminator() {
         ]
         []
         expect_test::expect![[r#"
-            judgment `prove { goal: {@ is_int(bool)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-              failed at (src/file.rs:LL:CC) because
-                judgment `prove_wc_list { goal: {@ is_int(bool)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
-                  the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-                    judgment `prove_wc { goal: @ is_int(bool), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
-                      the rule "ty is int" failed at step #0 (src/file.rs:LL:CC) because
-                        judgment `ty_is_int { assumptions: {}, ty: bool, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
-                          the rule "rigid_ty is int" failed at step #0 (src/file.rs:LL:CC) because
-                            condition evaluted to false: `id.is_int()`
-                              id = bool"#]]
+            judgment `ty_is_int { assumptions: {}, ty: bool, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
+              the rule "rigid_ty is int" failed at step #0 (src/file.rs:LL:CC) because
+                condition evaluted to false: `id.is_int()`
+                  id = bool"#]]
     )
 }