Write down the rules

Author: tiif

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

@@ -316,6 +316,25 @@ judgment_fn! {
     }
 }
 
+judgment_fn! {
+    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))
+        )
+
+    }
+
+}
+
 fn is_fundamental(_decls: &Decls, name: &RigidName) -> bool {
     // From https://rust-lang.github.io/rfcs/2451-re-rebalancing-coherence.html:
     //

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

@@ -16,7 +16,9 @@ use crate::{
 };
 
 use super::constraints::Constraints;
-use formality_types::grammar::Parameter::Ty;
+use formality_types::grammar::Parameter::{self, Ty};
+use formality_types::grammar::RigidName;
+use formality_types::grammar::RigidTy;
 
 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.
@@ -145,5 +147,30 @@ judgment_fn! {
             ----------------------------- ("const has ty")
             (prove_wc(decls, env, assumptions, Predicate::ConstHasType(ct, ty)) => c)
         )
+
+        (
+            (is_int(decl, env, assumptions, ty) => c)
+            ----------------------------- ("ty is int")
+            (prove_wc(decl, env, assumptions, Relation::IsInt(ty)) => c)
+        )
     }
 }
+
+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))
+        )
+
+    }
+
+}

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

@@ -72,6 +72,10 @@ impl Ty {
     pub fn well_formed(&self) -> Relation {
         Relation::WellFormed(self.upcast())
     }
+
+    pub fn is_int(&self) -> Relation {
+        Relation::IsInt(self.clone())
+    }
 }
 
 impl Parameter {
@@ -101,6 +105,7 @@ pub enum Skeleton {
     Equals,
     Sub,
     Outlives,
+    IsInt,
 }
 
 impl Predicate {
@@ -177,6 +182,9 @@ pub enum Relation {
 
     #[grammar(@wf($v0))]
     WellFormed(Parameter),
+
+    #[grammar(@is_int($v0))]
+    IsInt(Ty),
 }
 
 impl Relation {
@@ -187,6 +195,7 @@ 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/ty.rs

@@ -189,6 +189,24 @@ pub enum ScalarId {
     Isize,
 }
 
+impl ScalarId {
+    pub fn is_int(&self) -> bool {
+        match self {
+            ScalarId::U8
+            | ScalarId::U16
+            | ScalarId::U32
+            | ScalarId::U64
+            | ScalarId::I8
+            | ScalarId::I16
+            | ScalarId::I32
+            | ScalarId::I64
+            | ScalarId::Usize
+            | ScalarId::Isize => true,
+            ScalarId::Bool => false,
+        }
+    }
+}
+
 #[term((alias $name $*parameters))]
 #[customize(parse, debug)]
 pub struct AliasTy {