Refactor ty_is_int

Author: tiif

crates/formality-prove/src/prove.rs

@@ -1,6 +1,7 @@
 mod combinators;
 mod constraints;
 mod env;
+mod is_int;
 mod is_local;
 mod minimize;
 mod negation;

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

@@ -0,0 +1,38 @@
+use crate::prove::prove_normalize::prove_normalize;
+use crate::Constraints;
+use crate::Decls;
+use crate::Env;
+use formality_core::judgment_fn;
+use formality_types::grammar::Parameter::{self};
+use formality_types::grammar::RigidName;
+use formality_types::grammar::RigidTy;
+use formality_types::grammar::Wcs;
+
+judgment_fn! {
+    pub 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))
+        )
+
+    }
+}

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

@@ -6,20 +6,18 @@ 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,
         prove_eq::prove_eq,
-        prove_normalize::prove_normalize,
         prove_via::prove_via,
         prove_wf::prove_wf,
     },
 };
 
 use super::constraints::Constraints;
-use formality_types::grammar::Parameter::{self, Ty};
-use formality_types::grammar::RigidName;
-use formality_types::grammar::RigidTy;
+use formality_types::grammar::Parameter::Ty;
 
 judgment_fn! {
     /// The "heart" of the trait system -- prove that a where-clause holds given a set of declarations, variable environment, and set of assumptions.
@@ -150,37 +148,9 @@ judgment_fn! {
         )
 
         (
-            (is_int(&decl, &env, assumptions, ty) => c)
+            (ty_is_int(&decl, env, assumptions, ty) => c)
             ----------------------------- ("ty is int")
             (prove_wc(decl, env, assumptions, Relation::IsInt(ty)) => c)
         )
-
-        (
-            (if ty.is_alias())!
-            (prove_normalize(&decl, &env, &assumptions, ty) => (c1, p))
-            (let assumptions = c1.substitution().apply(&assumptions))
-            (is_int(&decl, &env, assumptions, p) => c2)
-            ----------------------------- ("aliasty is int")
-            (prove_wc(decl, env, assumptions, Relation::IsInt(ty)) => c2)
-        )
     }
 }
-
-judgment_fn! {
-    pub fn is_int(
-        _decls: Decls,
-        env: Env,
-        assumptions: Wcs,
-        goal: Parameter,
-    ) => Constraints {
-        debug(goal, assumptions, env)
-
-        (
-            (if id.is_int())
-            ------- ("is int")
-            (is_int(_decls, env, _assumptions, RigidTy {name: RigidName::ScalarId(id), parameters: _}) => Constraints::none(env))
-        )
-
-    }
-
-}

src/test/mir_fn_bodies.rs

@@ -664,8 +664,8 @@ fn test_invalid_value_in_switch_terminator() {
                   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 `is_int { goal: bool, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
-                          the rule "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"#]]
     )