Refactor ty_is_int

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,16 +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, ty_is_int, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression,
-    ValueExpression,
+    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};
@@ -229,9 +228,7 @@ impl Check<'_> {
                 // Check if the value is well-formed.
                 let value_ty = self.check_value(typeck_env, switch_value).unwrap();
 
-                if !ty_is_int(value_ty) {
-                    bail!("The value used for switch must be an 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 {
@@ -374,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

@@ -6,7 +6,7 @@ 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/minimize/test.rs

@@ -17,12 +17,14 @@ fn minimize_a() {
     let (env, subst) = env.existential_substitution(&term);
     let term = term.instantiate_with(&subst).unwrap();
 
-    expect!["(Env { variables: [?ty_1, ?ty_2, ?ty_3], bias: Soundness }, [?ty_1, ?ty_3])"]
-        .assert_eq(&format!("{:?}", (&env, &term)));
+    expect![
+        "(Env { variables: [?ty_1, ?ty_2, ?ty_3], bias: Soundness, pending: [] }, [?ty_1, ?ty_3])"
+    ]
+    .assert_eq(&format!("{:?}", (&env, &term)));
 
     let (mut env_min, term_min, m) = minimize(env, term);
 
-    expect!["(Env { variables: [?ty_0, ?ty_1], bias: Soundness }, [?ty_0, ?ty_1])"]
+    expect!["(Env { variables: [?ty_0, ?ty_1], bias: Soundness, pending: [] }, [?ty_0, ?ty_1])"]
         .assert_eq(&format!("{:?}", (&env_min, &term_min)));
 
     let ty0 = term_min[0].as_variable().unwrap();
@@ -51,6 +53,7 @@ fn minimize_a() {
                     ?ty_3,
                 ],
                 bias: Soundness,
+                pending: [],
             },
             known_true: true,
             substitution: {

crates/formality-prove/src/prove/prove_normalize.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/test/adt_wf.rs

@@ -32,6 +32,7 @@ fn well_formed_adt() {
                 env: Env {
                     variables: [],
                     bias: Soundness,
+                    pending: [],
                 },
                 known_true: true,
                 substitution: {},
@@ -51,21 +52,21 @@ fn not_well_formed_adt() {
         assumptions,
         Relation::WellFormed(goal),
     ).assert_err(expect![[r#"
-        judgment `prove { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
+        judgment `prove { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
           failed at (src/file.rs:LL:CC) because
-            judgment `prove_wc_list { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+            judgment `prove_wc_list { goal: {@ wf(X<u64>)}, 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: @ wf(X<u64>), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                judgment `prove_wc { goal: @ wf(X<u64>), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                   the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because
-                    judgment `prove_wf { goal: X<u64>, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                    judgment `prove_wf { goal: X<u64>, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                       the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because
-                        judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {} }` failed at the following rule(s):
+                        judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {} }` failed at the following rule(s):
                           the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
-                            judgment `prove { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
+                            judgment `prove { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
                               failed at (src/file.rs:LL:CC) because
-                                judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                                judgment `prove_wc_list { goal: {Foo(u64)}, 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: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                                    judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` 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()`"#]]);
 }