Type system framework for Kirin

Cargo.toml

@@ -34,6 +34,7 @@ members = [
   "crates/kirin-test-types",
   "crates/kirin-test-utils",
   "crates/kirin-tuple",
+  "crates/kirin-types",
   "crates/kirin-wildcard",
   "example/toy-lang",
   "example/toy-qc"
@@ -98,6 +99,7 @@ kirin-test-languages = { path = "crates/kirin-test-languages", version = "0.1.0"
 kirin-test-types = { path = "crates/kirin-test-types", version = "0.1.0" }
 kirin-test-utils = { path = "crates/kirin-test-utils", version = "0.1.0" }
 kirin-tuple = { path = "crates/kirin-tuple", version = "0.1.0" }
+kirin-types = { path = "crates/kirin-types", version = "0.1.0" }
 kirin-wildcard = { path = "crates/kirin-wildcard", version = "0.1.0" }
 petgraph = "0.7"
 predicates = "3"

crates/kirin-ir/src/arena/id.rs

@@ -56,7 +56,7 @@ macro_rules! identifier {
         $(#[$attr])*
         #[derive(Clone, Copy, Hash, PartialEq, Eq)]
         #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
-        pub struct $name(pub(crate) Id);
+        pub struct $name(pub(crate) $crate::Id);
 
         // Name(id) instead of the default Name(Id(id))
         impl std::fmt::Debug for $name {
@@ -65,18 +65,18 @@ macro_rules! identifier {
             }
         }
 
-        impl From<Id> for $name {
-            fn from(value: Id) -> Self {
+        impl From<$crate::Id> for $name {
+            fn from(value: $crate::Id) -> Self {
                 Self(value)
             }
         }
 
-        impl From<$name> for Id {
+        impl From<$name> for $crate::Id {
             fn from(value: $name) -> Self {
                 value.0
             }
         }
 
-        impl $crate::arena::Identifier for $name {}
+        impl $crate::Identifier for $name {}
     };
 }

crates/kirin-ir/src/node/block.rs

@@ -2,7 +2,7 @@ use smallvec::SmallVec;
 
 use crate::{
     Dialect, Symbol,
-    arena::{GetInfo, GetInfoMut, Id, Item},
+    arena::{GetInfo, GetInfoMut, Item},
     identifier,
 };
 

crates/kirin-ir/src/node/cfg.rs

@@ -1,4 +1,4 @@
-use crate::arena::{GetInfo, GetInfoMut, Id, Item};
+use crate::arena::{GetInfo, GetInfoMut, Item};
 use crate::{Dialect, identifier};
 
 use super::block::Block;

crates/kirin-ir/src/node/digraph.rs

@@ -1,5 +1,5 @@
 use crate::Dialect;
-use crate::arena::{GetInfo, GetInfoMut, Id};
+use crate::arena::{GetInfo, GetInfoMut};
 use crate::identifier;
 
 use super::graph::{DiGraphExtra, GraphInfo};

crates/kirin-ir/src/node/function/generic.rs

@@ -1,6 +1,5 @@
 use indexmap::IndexMap;
 
-use crate::arena::Id;
 use crate::identifier;
 
 use super::compile_stage::CompileStage;

crates/kirin-ir/src/node/function/staged.rs

@@ -1,4 +1,4 @@
-use crate::arena::{GetInfo, GetInfoMut, Id, Item};
+use crate::arena::{GetInfo, GetInfoMut, Item};
 use crate::identifier;
 use crate::language::Dialect;
 use crate::signature::{Signature, SignatureCmp, SignatureSemantics};

crates/kirin-ir/src/node/port.rs

@@ -1,4 +1,3 @@
-use crate::arena::Id;
 use crate::identifier;
 
 use super::digraph::DiGraph;

crates/kirin-ir/src/node/ungraph.rs

@@ -1,5 +1,5 @@
 use crate::Dialect;
-use crate::arena::{GetInfo, GetInfoMut, Id};
+use crate::arena::{GetInfo, GetInfoMut};
 use crate::identifier;
 
 use super::graph::{GraphInfo, UnGraphExtra};

crates/kirin-test-utils/Cargo.toml

@@ -12,10 +12,12 @@ kirin-test-types = { workspace = true }
 kirin-chumsky = { workspace = true, optional = true }
 kirin-lexer = { workspace = true, optional = true }
 kirin-prettyless = { workspace = true, optional = true }
+kirin-types = { workspace = true, optional = true }
 
 [features]
 default = []
 parser = ["kirin-chumsky", "kirin-lexer"]
 pretty = ["kirin-prettyless"]
 roundtrip = ["parser", "pretty"]
+types = ["kirin-types"]
 serde = ["dep:serde", "dep:serde_json", "kirin-ir/serde"]

crates/kirin-test-utils/src/lib.rs

@@ -8,6 +8,9 @@ pub mod parser;
 #[cfg(feature = "roundtrip")]
 pub mod roundtrip;
 
+#[cfg(feature = "types")]
+pub mod types;
+
 pub use kirin_test_types::UnitType;
 pub use rustfmt::{rustfmt, rustfmt_display};
 pub use ssa::new_test_ssa;

crates/kirin-test-utils/src/types.rs

@@ -0,0 +1,35 @@
+//! Checks for the static constructors of `kirin-types`.
+
+use kirin_types::{IndexSort, SortValue, StaticSig};
+
+/// Asserts that `con`, applied to the sample `args`, evaluates consistently
+/// with its signature: `args` must match the signature's argument sorts, and
+/// a value `eval` returns must have the signature's result sort.
+pub fn assert_eval_matches_signature<S, C>(con: &C, args: &[SortValue<S::T>])
+where
+    S: IndexSort,
+    C: StaticSig<S>,
+{
+    let sig = con.signature();
+    assert_eq!(
+        args.len(),
+        sig.args.len(),
+        "`{con}` takes {} arguments, but the sample has {}",
+        sig.args.len(),
+        args.len()
+    );
+    for (arg, expected) in args.iter().zip(&sig.args) {
+        assert_eq!(
+            arg.sort::<S>(),
+            *expected,
+            "the sample argument {arg:?} of `{con}` has the wrong sort"
+        );
+    }
+    if let Some(value) = con.eval(args) {
+        assert_eq!(
+            value.sort::<S>(),
+            sig.result,
+            "`{con}` evaluates {args:?} to {value:?}, which isn't of its result sort"
+        );
+    }
+}

crates/kirin-types/Cargo.toml

@@ -0,0 +1,16 @@
+[package]
+rust-version.workspace = true
+name = "kirin-types"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]
+kirin-ir = { workspace = true }
+serde = { workspace = true, optional = true }
+thiserror = { workspace = true }
+
+[dev-dependencies]
+kirin-test-utils = { workspace = true, features = ["types"] }
+
+[features]
+serde = ["dep:serde", "kirin-ir/serde"]

crates/kirin-types/src/display.rs

@@ -0,0 +1,144 @@
+//! Rendering sorts and static terms for diagnostics.
+
+use std::fmt::{self, Display};
+
+use kirin_ir::Id;
+
+use crate::{IndexSort, Sort, SortValue, StaticTerm, StaticTermId, Statics};
+
+impl<B: IndexSort> Display for Sort<B> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.write_str(match self {
+            Self::Type => "type",
+            Self::Bool => "bool",
+            Self::Index(base) => base.name(),
+        })
+    }
+}
+
+impl<V: Display> Display for SortValue<V> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Self::Bool(value) => value.fmt(f),
+            Self::Index(value) => value.fmt(f),
+        }
+    }
+}
+
+impl<B: IndexSort, C: Display> Statics<B, C> {
+    /// Renders `term`, which sits under `depth` binders. Bound variables are
+    /// named by de Bruijn level, so `a0` is the outermost binder; a free
+    /// variable by its name hint, or else `x` followed by its id.
+    pub fn display(&self, term: StaticTermId, depth: usize) -> impl Display + '_ {
+        TermDisplay {
+            statics: self,
+            term,
+            depth,
+            nested: false,
+        }
+    }
+}
+
+struct TermDisplay<'a, B: IndexSort, C> {
+    statics: &'a Statics<B, C>,
+    term: StaticTermId,
+    depth: usize,
+    /// Parenthesize forms that would otherwise be ambiguous inside another term.
+    nested: bool,
+}
+
+impl<B: IndexSort, C: Display> TermDisplay<'_, B, C> {
+    fn child(&self, term: StaticTermId, depth: usize) -> Self {
+        Self {
+            statics: self.statics,
+            term,
+            depth,
+            nested: true,
+        }
+    }
+
+    fn list(&self, f: &mut fmt::Formatter<'_>, terms: &[StaticTermId], sep: &str) -> fmt::Result {
+        for (i, term) in terms.iter().enumerate() {
+            if i > 0 {
+                f.write_str(sep)?;
+            }
+            self.child(*term, self.depth).fmt(f)?;
+        }
+        Ok(())
+    }
+}
+
+impl<B: IndexSort, C: Display> Display for TermDisplay<'_, B, C> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let term = &*self.statics.terms[self.term];
+        let compound = matches!(
+            term,
+            StaticTerm::Function(..)
+                | StaticTerm::Guard(..)
+                | StaticTerm::Assert(..)
+                | StaticTerm::Forall(..)
+                | StaticTerm::Exists(..)
+        );
+        if self.nested && compound {
+            f.write_str("(")?;
+        }
+        match term {
+            StaticTerm::Bound(i) => match self.depth.checked_sub(i + 1) {
+                Some(level) => write!(f, "a{level}")?,
+                None => write!(f, "?{i}")?,
+            },
+            StaticTerm::Free(var) => match &self.statics.vars[*var].name {
+                Some(name) => f.write_str(name)?,
+                None => write!(f, "x{}", Id::from(*var).raw())?,
+            },
+            StaticTerm::Lit(value) => write!(f, "{value:?}")?,
+            StaticTerm::Constructor(constructor, args) if args.is_empty() => {
+                write!(f, "{constructor}")?
+            }
+            StaticTerm::Constructor(constructor, args) => {
+                write!(f, "{constructor}(")?;
+                self.list(f, args, ", ")?;
+                f.write_str(")")?;
+            }
+            StaticTerm::Product(components) => {
+                f.write_str("(")?;
+                self.list(f, components, " * ")?;
+                f.write_str(")")?;
+            }
+            StaticTerm::Function(args, result) => {
+                f.write_str("(")?;
+                self.list(f, args, ", ")?;
+                write!(f, ") → {}", self.child(*result, self.depth))?;
+            }
+            StaticTerm::Guard(prop, ty) => write!(
+                f,
+                "{} ⊃ {}",
+                self.child(*prop, self.depth),
+                self.child(*ty, self.depth)
+            )?,
+            StaticTerm::Assert(prop, ty) => write!(
+                f,
+                "{} ∧ {}",
+                self.child(*prop, self.depth),
+                self.child(*ty, self.depth)
+            )?,
+            StaticTerm::Forall(sort, body) | StaticTerm::Exists(sort, body) => {
+                let quantifier = if matches!(term, StaticTerm::Forall(..)) {
+                    '∀'
+                } else {
+                    '∃'
+                };
+                write!(
+                    f,
+                    "{quantifier}a{}: {sort}. {}",
+                    self.depth,
+                    self.child(*body, self.depth + 1)
+                )?;
+            }
+        }
+        if self.nested && compound {
+            f.write_str(")")?;
+        }
+        Ok(())
+    }
+}