From 9846bae087a7ef8483347d72145085fd41261a0f Mon Sep 17 00:00:00 2001 From: Pablo Lanza Date: Wed, 11 Nov 2026 18:16:37 +0000 Subject: [PATCH 1/6] fix(ir): resolve identifier! paths through $crate - `identifier!` named `Id` unqualified and `Identifier` through the private `arena` module, so it only expanded inside kirin-ir modules that imported `Id`. - Refer to both through their `$crate` re-exports, so other crates can declare arena ids with it. - Drop the `Id` imports that existed only for the macro. --- crates/kirin-ir/src/arena/id.rs | 10 +++++----- crates/kirin-ir/src/node/block.rs | 2 +- crates/kirin-ir/src/node/cfg.rs | 2 +- crates/kirin-ir/src/node/digraph.rs | 2 +- crates/kirin-ir/src/node/function/generic.rs | 1 - crates/kirin-ir/src/node/function/staged.rs | 2 +- crates/kirin-ir/src/node/port.rs | 1 - crates/kirin-ir/src/node/ungraph.rs | 2 +- 8 files changed, 10 insertions(+), 12 deletions(-) diff --git a/crates/kirin-ir/src/arena/id.rs b/crates/kirin-ir/src/arena/id.rs index 133bc8fc1..ec2372b10 100644 --- a/crates/kirin-ir/src/arena/id.rs +++ b/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 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 {} }; } diff --git a/crates/kirin-ir/src/node/block.rs b/crates/kirin-ir/src/node/block.rs index 9bc379a16..c8a65a8e5 100644 --- a/crates/kirin-ir/src/node/block.rs +++ b/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, }; diff --git a/crates/kirin-ir/src/node/cfg.rs b/crates/kirin-ir/src/node/cfg.rs index e711e8907..e8e70e69f 100644 --- a/crates/kirin-ir/src/node/cfg.rs +++ b/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; diff --git a/crates/kirin-ir/src/node/digraph.rs b/crates/kirin-ir/src/node/digraph.rs index 937c3f74b..453299663 100644 --- a/crates/kirin-ir/src/node/digraph.rs +++ b/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}; diff --git a/crates/kirin-ir/src/node/function/generic.rs b/crates/kirin-ir/src/node/function/generic.rs index aedd791e8..b33c38530 100644 --- a/crates/kirin-ir/src/node/function/generic.rs +++ b/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; diff --git a/crates/kirin-ir/src/node/function/staged.rs b/crates/kirin-ir/src/node/function/staged.rs index 53ce0a6dc..b01bd4f7b 100644 --- a/crates/kirin-ir/src/node/function/staged.rs +++ b/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}; diff --git a/crates/kirin-ir/src/node/port.rs b/crates/kirin-ir/src/node/port.rs index 3a332467d..791e1530e 100644 --- a/crates/kirin-ir/src/node/port.rs +++ b/crates/kirin-ir/src/node/port.rs @@ -1,4 +1,3 @@ -use crate::arena::Id; use crate::identifier; use super::digraph::DiGraph; diff --git a/crates/kirin-ir/src/node/ungraph.rs b/crates/kirin-ir/src/node/ungraph.rs index ba8c1bd8c..882ef183f 100644 --- a/crates/kirin-ir/src/node/ungraph.rs +++ b/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}; From 4a05744aa2221bf9a055a07be464390c10168ca7 Mon Sep 17 00:00:00 2001 From: Pablo Lanza Date: Wed, 11 Nov 2026 18:28:22 +0000 Subject: [PATCH 2/6] feat(types): add kirin-types with sorted static terms - New crate `kirin-types`: the implementation of an ATS-style type system. - Sorts (`type`, `bool`, and dialect index sorts via `IndexSort`), literal values (`SortValue`), and static constructor sets via `StaticSig` (signature plus evaluation on literals). - `StaticTerm` in locally nameless form, arena-allocated in `Statics`: de Bruijn `Bound` indices, named `Free` variables with a sort and a name hint, literals, constructors, type formers and quantifiers. - `Statics::check_sort`, `term_eq`, `mentions`, and `display` for diagnostics; `SortError`. - The tests build terms from the `int` and `bool` constructor sets, so they compile from the next commit. --- Cargo.lock | 9 + Cargo.toml | 2 + crates/kirin-types/Cargo.toml | 13 + crates/kirin-types/src/display.rs | 144 ++++++++++ crates/kirin-types/src/error.rs | 37 +++ crates/kirin-types/src/lib.rs | 9 + crates/kirin-types/src/statics/check.rs | 103 ++++++++ crates/kirin-types/src/statics/mod.rs | 9 + crates/kirin-types/src/statics/term.rs | 233 ++++++++++++++++ crates/kirin-types/tests/common/mod.rs | 121 +++++++++ crates/kirin-types/tests/sort_check.rs | 338 ++++++++++++++++++++++++ 11 files changed, 1018 insertions(+) create mode 100644 crates/kirin-types/Cargo.toml create mode 100644 crates/kirin-types/src/display.rs create mode 100644 crates/kirin-types/src/error.rs create mode 100644 crates/kirin-types/src/lib.rs create mode 100644 crates/kirin-types/src/statics/check.rs create mode 100644 crates/kirin-types/src/statics/mod.rs create mode 100644 crates/kirin-types/src/statics/term.rs create mode 100644 crates/kirin-types/tests/common/mod.rs create mode 100644 crates/kirin-types/tests/sort_check.rs diff --git a/Cargo.lock b/Cargo.lock index 12df4b235..a6afa809a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1067,6 +1067,15 @@ dependencies = [ "thiserror 2.0.18", ] +[[package]] +name = "kirin-types" +version = "0.1.0" +dependencies = [ + "kirin-ir", + "serde", + "thiserror 2.0.18", +] + [[package]] name = "kirin-wildcard" version = "0.1.0" diff --git a/Cargo.toml b/Cargo.toml index 8d291b1cb..fb9bf2936 100644 --- a/Cargo.toml +++ b/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" diff --git a/crates/kirin-types/Cargo.toml b/crates/kirin-types/Cargo.toml new file mode 100644 index 000000000..de208f5d4 --- /dev/null +++ b/crates/kirin-types/Cargo.toml @@ -0,0 +1,13 @@ +[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 } + +[features] +serde = ["dep:serde", "kirin-ir/serde"] diff --git a/crates/kirin-types/src/display.rs b/crates/kirin-types/src/display.rs new file mode 100644 index 000000000..23fff5bca --- /dev/null +++ b/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 Display for Sort { + 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 Display for SortValue { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Bool(value) => value.fmt(f), + Self::Index(value) => value.fmt(f), + } + } +} + +impl Statics { + /// 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, + term: StaticTermId, + depth: usize, + /// Parenthesize forms that would otherwise be ambiguous inside another term. + nested: bool, +} + +impl 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 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(()) + } +} diff --git a/crates/kirin-types/src/error.rs b/crates/kirin-types/src/error.rs new file mode 100644 index 000000000..aabb314f1 --- /dev/null +++ b/crates/kirin-types/src/error.rs @@ -0,0 +1,37 @@ +//! Errors from checking terms. + +use thiserror::Error; + +use crate::{Sort, StaticTermId}; + +/// A static term that has no sort. `term` is where the error was found; +/// `shown` renders it for the message. +#[derive(Clone, Debug, Error, PartialEq, Eq)] +pub enum SortError { + #[error("bound variable {index} has no binder: it is under only {depth} binders")] + UnboundVar { + term: StaticTermId, + index: usize, + depth: usize, + }, + #[error("`{shown}` expects {expected} arguments, but got {found}")] + ArityMismatch { + term: StaticTermId, + shown: String, + expected: usize, + found: usize, + }, + #[error("a product needs at least 2 components, but `{shown}` has {found}")] + ShortProduct { + term: StaticTermId, + shown: String, + found: usize, + }, + #[error("`{shown}` has sort `{found}`, but `{expected}` was expected")] + SortMismatch { + term: StaticTermId, + shown: String, + expected: Sort, + found: Sort, + }, +} diff --git a/crates/kirin-types/src/lib.rs b/crates/kirin-types/src/lib.rs new file mode 100644 index 000000000..a9079ee2b --- /dev/null +++ b/crates/kirin-types/src/lib.rs @@ -0,0 +1,9 @@ +mod display; +mod error; +mod statics; + +pub use error::SortError; +pub use statics::{ + IndexSort, Project, Sort, SortValue, StaticCon, StaticSig, StaticTerm, StaticTermId, StaticVar, + StaticVarId, Statics, +}; diff --git a/crates/kirin-types/src/statics/check.rs b/crates/kirin-types/src/statics/check.rs new file mode 100644 index 000000000..e14c5ae53 --- /dev/null +++ b/crates/kirin-types/src/statics/check.rs @@ -0,0 +1,103 @@ +use crate::SortError; + +use super::{IndexSort, Sort, StaticSig, StaticTerm, StaticTermId, Statics}; + +impl> Statics { + /// The sort of the locally closed `term`. + /// Locally closed means that there are no `Bound(i)` variables without a + /// corresponding enclosing binder. + pub fn check_sort(&self, term: StaticTermId) -> Result, SortError> { + self.sort_under(term, &mut Vec::new()) + } + + /// The sort of `term` under `context` of bound variables. + /// The last entry is `Bound(0)`. + fn sort_under( + &self, + term: StaticTermId, + context: &mut Vec>, + ) -> Result, SortError> { + match &*self.terms[term] { + StaticTerm::Bound(i) => { + let Some(index) = context.len().checked_sub(i + 1) else { + return Err(SortError::UnboundVar { + term, + index: *i, + depth: context.len(), + }); + }; + + Ok(context[index]) + } + StaticTerm::Free(var) => Ok(self.vars[*var].sort), + StaticTerm::Lit(v) => Ok(v.sort()), + StaticTerm::Constructor(constructor, args) => { + let sig = constructor.signature(); + + // Check that the arguments have the expected sorts + if args.len() != sig.args.len() { + return Err(SortError::ArityMismatch { + term, + shown: self.display(term, context.len()).to_string(), + expected: sig.args.len(), + found: args.len(), + }); + } + for (arg, expected) in args.iter().zip(sig.args.iter()) { + self.expect(*arg, *expected, context)?; + } + Ok(sig.result) + } + StaticTerm::Product(components) => { + if components.len() < 2 { + return Err(SortError::ShortProduct { + term, + shown: self.display(term, context.len()).to_string(), + found: components.len(), + }); + } + for component in components { + self.expect(*component, Sort::Type, context)?; + } + Ok(Sort::Type) + } + StaticTerm::Function(args, result) => { + for arg in args.iter().chain([result]) { + self.expect(*arg, Sort::Type, context)?; + } + Ok(Sort::Type) + } + StaticTerm::Guard(prop, ty) | StaticTerm::Assert(prop, ty) => { + self.expect(*prop, Sort::Bool, context)?; + self.expect(*ty, Sort::Type, context)?; + Ok(Sort::Type) + } + StaticTerm::Forall(sort, body) | StaticTerm::Exists(sort, body) => { + context.push(*sort); + let checked = self.expect(*body, Sort::Type, context); + context.pop(); + checked?; + Ok(Sort::Type) + } + } + } + + /// Checks that `arg`, under all of `context`'s binders, has sort `expected`. + fn expect( + &self, + arg: StaticTermId, + expected: Sort, + context: &mut Vec>, + ) -> Result<(), SortError> { + let found = self.sort_under(arg, context)?; + if found != expected { + return Err(SortError::SortMismatch { + term: arg, + shown: self.display(arg, context.len()).to_string(), + expected, + found, + }); + } + Ok(()) + } +} diff --git a/crates/kirin-types/src/statics/mod.rs b/crates/kirin-types/src/statics/mod.rs new file mode 100644 index 000000000..8ed743616 --- /dev/null +++ b/crates/kirin-types/src/statics/mod.rs @@ -0,0 +1,9 @@ +//! Statics: sorts, static constructors, and static terms. + +mod check; +mod term; + +pub use term::{ + IndexSort, Project, Sort, SortValue, StaticCon, StaticSig, StaticTerm, StaticTermId, StaticVar, + StaticVarId, Statics, +}; diff --git a/crates/kirin-types/src/statics/term.rs b/crates/kirin-types/src/statics/term.rs new file mode 100644 index 000000000..39fb5ed93 --- /dev/null +++ b/crates/kirin-types/src/statics/term.rs @@ -0,0 +1,233 @@ +use std::{ + fmt::{Debug, Display}, + hash::Hash, +}; + +use kirin_ir::{Arena, identifier}; + +/// What a dialect's sort must implement. +/// Often implemented for enums that compose multiple [`IndexSort`] variants. +pub trait IndexSort: Copy + Eq + Hash + Debug { + /// The underlying data type that an index sort evaluates to + /// e.g. `IntSortValue(i64)` for the `int` sort. + type T: Clone + Eq + Hash + Debug; + + /// If we only have the `value`, retrieve the sort that it belongs to. + fn sort_of(value: &Self::T) -> Self; + + /// How the sort is written, e.g. `int`. + fn name(&self) -> &'static str; +} + +/// The statics are first-order: every sort is a base sort. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub enum Sort { + /// `type`: the sort of types of dynamic terms. + Type, + /// `bool`: the sort of static propositions, e.g. guards. + /// Separate variant from `Index` since some [`StaticTerm`] variants rely + /// on it. + Bool, + /// An index sort contributed by a dialect, e.g. `int`. + Index(S), +} + +/// Automtically convert an [`IndexSort`] to a [`Sort`] +impl From for Sort { + fn from(base: S) -> Self { + Sort::Index(base) + } +} + +/// A dialect may compose many sorts, e.g. IntSort, FloatSort, etc. +/// When constraints combine multiple such sorts we need a way of extracting +/// the underlying values. This is provided by this trait. +pub trait Project { + fn project(&self) -> Option<&T>; +} + +impl Project for T { + fn project(&self) -> Option<&T> { + Some(self) + } +} + +/// The underlying value of a [`Sort`]: +/// - a `bool` for [`Sort::Bool`], +/// - a value `V` for [`Sort::Index`] +/// +/// +/// [`Sort::Type`] has no underlying value +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub enum SortValue { + Bool(bool), + Index(V), +} + +impl SortValue { + /// The `T` this value holds, if it is a value of `T`'s sort. + pub fn project(&self) -> Option<&T> + where + V: Project, + { + match self { + SortValue::Index(value) => value.project(), + SortValue::Bool(_) => None, + } + } + + /// The boolean this value is, if it is a `bool`. + pub fn as_bool(&self) -> Option { + match self { + SortValue::Bool(b) => Some(*b), + SortValue::Index(_) => None, + } + } + + /// The sort this value belongs to. + pub fn sort>(&self) -> Sort { + match self { + SortValue::Bool(_) => Sort::Bool, + SortValue::Index(value) => Sort::Index(S::sort_of(value)), + } + } +} + +/// The constructor for a static term defined in the dialect. +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct StaticCon { + pub args: Vec>, + pub result: Sort, +} + +pub trait StaticSig: Clone + PartialEq + Display { + // API to define the static constructors in a dialect. + fn signature(&self) -> StaticCon; + /// Evaluate a constructor when applied to `args`. + /// Returns `None` if this constructor does not evaluate to a value + /// (e.g. [`crate::IntStaticCon::IntOf`]). + fn eval(&self, args: &[SortValue]) -> Option>; +} + +identifier! { + /// A static term allocated in [`Statics::terms`]. + struct StaticTermId +} + +identifier! { + /// A free static variable allocated in [`Statics::vars`]. + struct StaticVarId +} + +/// A free static variable. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct StaticVar { + /// The sort of the variable. + pub sort: Sort, + /// A name for diagnostics, e.g. from an annotation or the SSA value the + /// variable was introduced for. + pub name: Option, +} + +/// Terms are kept in an `Arena` in `Statics` so they can be shared. +/// The derived `PartialEq` is shallow: it compares child ids, not the terms +/// they point to. Use [`Statics::term_eq`] to compare terms. +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub enum StaticTerm { + /// A variable is either + /// - `Bound(i)`, a de Bruijn index: references the `i`-th innermost + /// binder around the variable, e.g. `Bound(0)` is the innermost. + /// Binders are [`StaticTerm::Forall`]/[`StaticTerm::Exists`] and the + /// quantifiers of a [`crate::dynamics::DynSig`]. + Bound(usize), + /// - `Free(x)`, a variable whose sort is recorded in [`Statics::vars`], + /// introduced by the dynamics' static binders or by whoever builds the term. + Free(StaticVarId), + /// A literal value: a `bool`, or a value of a dialect's base sort. + Lit(SortValue), + /// A dialect's signature applied to its arguments. + Constructor(C, Vec), + /// `T_1 * … * T_n` with `n ≥ 2`, of sort `type`. + Product(Vec), + /// `(T_1, …, T_n) → T`, of sort `type`. + Function(Vec, StaticTermId), + /// `B ⊃ T`: a guarded type, usable only where `B` holds. + Guard(StaticTermId, StaticTermId), + /// `B ∧ T`: an asserting type, whose values establish `B`. + Assert(StaticTermId, StaticTermId), + /// `∀a:σ. T`, binding `a` as `Bound(0)` in `T`. + Forall(Sort, StaticTermId), + /// `∃a:σ. T`, binding `a` as `Bound(0)` in `T`. + Exists(Sort, StaticTermId), +} + +/// The static terms of one program, and their free variables. +pub struct Statics { + pub terms: Arena>, + pub vars: Arena>, +} + +impl Default for Statics { + fn default() -> Self { + Self { + terms: Arena::default(), + vars: Arena::default(), + } + } +} + +impl Statics { + pub fn alloc(&mut self, term: StaticTerm) -> StaticTermId { + self.terms.alloc(term) + } + + /// A new free variable of sort `sort`, with an optional name for + /// diagnostics. + pub fn fresh_var(&mut self, sort: Sort, name: Option) -> StaticVarId { + self.vars.alloc(StaticVar { sort, name }) + } + + /// Whether the free variable `var` occurs in `term`. + pub fn mentions(&self, term: StaticTermId, var: StaticVarId) -> bool { + use StaticTerm::*; + match &*self.terms[term] { + Free(x) => *x == var, + Bound(_) | Lit(_) => false, + Constructor(_, args) | Product(args) => args.iter().any(|a| self.mentions(*a, var)), + Function(args, result) => args.iter().chain([result]).any(|a| self.mentions(*a, var)), + Guard(p, t) | Assert(p, t) => self.mentions(*p, var) || self.mentions(*t, var), + Forall(_, body) | Exists(_, body) => self.mentions(*body, var), + } + } +} + +impl Statics { + /// Whether `a` and `b` are the same term, possibly stored at different ids. + /// Bound variables are de Bruijn indices, so terms that differ only in the + /// names of bound variables are identical: this is a plain structural + /// comparison. + pub fn term_eq(&self, a: StaticTermId, b: StaticTermId) -> bool { + use StaticTerm::*; + let all_eq = |xs: &[StaticTermId], ys: &[StaticTermId]| { + xs.len() == ys.len() && xs.iter().zip(ys).all(|(x, y)| self.term_eq(*x, *y)) + }; + if a == b { + return true; + } + match (&*self.terms[a], &*self.terms[b]) { + (Bound(i), Bound(j)) => i == j, + (Free(x), Free(y)) => x == y, + (Lit(x), Lit(y)) => x == y, + (Constructor(c, xs), Constructor(d, ys)) => c == d && all_eq(xs, ys), + (Product(xs), Product(ys)) => all_eq(xs, ys), + (Function(xs, r), Function(ys, s)) => all_eq(xs, ys) && self.term_eq(*r, *s), + (Guard(p, t), Guard(q, u)) | (Assert(p, t), Assert(q, u)) => { + self.term_eq(*p, *q) && self.term_eq(*t, *u) + } + (Forall(s, x), Forall(t, y)) | (Exists(s, x), Exists(t, y)) => { + s == t && self.term_eq(*x, *y) + } + _ => false, + } + } +} diff --git a/crates/kirin-types/tests/common/mod.rs b/crates/kirin-types/tests/common/mod.rs new file mode 100644 index 000000000..7192edfe6 --- /dev/null +++ b/crates/kirin-types/tests/common/mod.rs @@ -0,0 +1,121 @@ +//! Constructors, sorts, and a statics fixture shared by the integration tests. +#![allow(dead_code)] + +use std::fmt; + +use kirin_types::{ + BoolStaticCon, IntSort, IntSortT, IntStaticCon, Sort, SortError, SortValue, StaticCon, + StaticSig, StaticTerm, StaticTermId, Statics, +}; + +/// The `bool` and `int` constructors plus `token : () ⇒ type`, a type with +/// no structure to stand in wherever a test needs some type. +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub enum TestCon { + Bool(BoolStaticCon), + Int(IntStaticCon), + Token, +} + +impl StaticSig for TestCon { + fn signature(&self) -> StaticCon { + match self { + Self::Bool(con) => con.signature(), + Self::Int(con) => con.signature(), + Self::Token => StaticCon { + args: vec![], + result: Sort::Type, + }, + } + } + + fn eval(&self, args: &[SortValue]) -> Option> { + match self { + Self::Bool(con) => con.eval(args), + Self::Int(con) => StaticSig::::eval(con, args), + Self::Token => None, + } + } +} + +impl fmt::Display for TestCon { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Bool(con) => con.fmt(f), + Self::Int(con) => con.fmt(f), + Self::Token => f.write_str("token"), + } + } +} + +pub type TestSort = Sort; +pub type TestTerm = StaticTerm; + +pub fn int() -> TestSort { + Sort::Index(IntSort) +} + +pub fn boolean() -> TestSort { + Sort::Bool +} + +pub fn ty() -> TestSort { + Sort::Type +} + +/// Statics plus shorthands for building terms. +pub struct Fixture { + pub statics: Statics, +} + +impl Fixture { + pub fn new() -> Self { + Self { + statics: Statics::default(), + } + } + + pub fn term(&mut self, term: TestTerm) -> StaticTermId { + self.statics.alloc(term) + } + + pub fn bound(&mut self, i: usize) -> StaticTermId { + self.term(StaticTerm::Bound(i)) + } + + /// A fresh free variable of sort `sort`, as a term. + pub fn free(&mut self, sort: TestSort) -> StaticTermId { + let var = self.statics.fresh_var(sort, None); + self.term(StaticTerm::Free(var)) + } + + pub fn int_con(&mut self, con: IntStaticCon, args: Vec) -> StaticTermId { + self.term(StaticTerm::Constructor(TestCon::Int(con), args)) + } + + pub fn bool_con( + &mut self, + con: BoolStaticCon, + args: Vec, + ) -> StaticTermId { + self.term(StaticTerm::Constructor(TestCon::Bool(con), args)) + } + + /// The `int` literal `n`. + pub fn lit(&mut self, n: i64) -> StaticTermId { + self.term(StaticTerm::Lit(SortValue::Index(IntSortT(n)))) + } + + /// The `bool` literal `b`. + pub fn bool_lit(&mut self, b: bool) -> StaticTermId { + self.term(StaticTerm::Lit(SortValue::Bool(b))) + } + + pub fn token(&mut self) -> StaticTermId { + self.term(StaticTerm::Constructor(TestCon::Token, vec![])) + } + + pub fn check(&self, term: StaticTermId) -> Result> { + self.statics.check_sort(term) + } +} diff --git a/crates/kirin-types/tests/sort_check.rs b/crates/kirin-types/tests/sort_check.rs new file mode 100644 index 000000000..da0a43b26 --- /dev/null +++ b/crates/kirin-types/tests/sort_check.rs @@ -0,0 +1,338 @@ +mod common; + +use common::{Fixture, boolean, int, ty}; +use kirin_types::{IntStaticCon, SortError, StaticTerm}; + +#[test] +fn free_variables_have_their_recorded_sort() { + let mut f = Fixture::new(); + let (n, b) = (f.free(int()), f.free(boolean())); + assert_eq!(f.check(n), Ok(int())); + assert_eq!(f.check(b), Ok(boolean())); +} + +#[test] +fn dangling_bound_variable_is_unbound() { + let mut f = Fixture::new(); + let var = f.bound(0); + assert_eq!( + f.check(var), + Err(SortError::UnboundVar { + term: var, + index: 0, + depth: 0 + }) + ); +} + +#[test] +fn nested_quantifiers_number_binders_innermost_first() { + let mut f = Fixture::new(); + // ∀(n: int). ∃(b: bool). b ⊃ ((n ≥ 0) ∧ token) — b is Var(0), n is Var(1) + let (b, n, zero, token) = (f.bound(0), f.bound(1), f.lit(0), f.token()); + let nonneg = f.int_con(IntStaticCon::Geq, vec![n, zero]); + let asserted = f.term(StaticTerm::Assert(nonneg, token)); + let guarded = f.term(StaticTerm::Guard(b, asserted)); + let exists = f.term(StaticTerm::Exists(boolean(), guarded)); + let forall = f.term(StaticTerm::Forall(int(), exists)); + assert_eq!(f.check(forall), Ok(ty())); +} + +#[test] +fn swapped_binders_are_rejected() { + let mut f = Fixture::new(); + // ∀(n: int). ∃(b: bool). n ⊃ token — Var(1) is the int, not the bool + let (n, token) = (f.bound(1), f.token()); + let guarded = f.term(StaticTerm::Guard(n, token)); + let exists = f.term(StaticTerm::Exists(boolean(), guarded)); + let forall = f.term(StaticTerm::Forall(int(), exists)); + assert_eq!( + f.check(forall), + Err(SortError::SortMismatch { + term: n, + shown: "a0".into(), + expected: boolean(), + found: int() + }) + ); +} + +#[test] +fn quantifier_body_sees_free_variables() { + let mut f = Fixture::new(); + // ∃(n: int). p ⊃ token, with p a free bool + let (p, token) = (f.free(boolean()), f.token()); + let guarded = f.term(StaticTerm::Guard(p, token)); + let exists = f.term(StaticTerm::Exists(int(), guarded)); + assert_eq!(f.check(exists), Ok(ty())); +} + +#[test] +fn var_beyond_a_quantifier_is_unbound() { + let mut f = Fixture::new(); + let escaped = f.bound(1); + let forall = f.term(StaticTerm::Forall(int(), escaped)); + assert_eq!( + f.check(forall), + Err(SortError::UnboundVar { + term: escaped, + index: 1, + depth: 1 + }) + ); +} + +#[test] +fn constructor_result_comes_from_its_signature() { + let mut f = Fixture::new(); + let one = f.lit(1); + assert_eq!(f.check(one), Ok(int())); + let two = f.lit(2); + let sum = f.int_con(IntStaticCon::Add, vec![one, two]); + assert_eq!(f.check(sum), Ok(int())); + let geq = f.int_con(IntStaticCon::Geq, vec![sum, one]); + assert_eq!(f.check(geq), Ok(boolean())); +} + +#[test] +fn constructor_with_wrong_arity_is_rejected() { + let mut f = Fixture::new(); + let one = f.lit(1); + let add = f.int_con(IntStaticCon::Add, vec![one]); + assert_eq!( + f.check(add), + Err(SortError::ArityMismatch { + term: add, + shown: "+(Index(IntSortT(1)))".into(), + expected: 2, + found: 1 + }) + ); +} + +#[test] +fn constructor_with_wrong_argument_sort_is_rejected() { + let mut f = Fixture::new(); + let yes = f.bool_lit(true); + let one = f.lit(1); + let geq = f.int_con(IntStaticCon::Geq, vec![yes, one]); + assert_eq!( + f.check(geq), + Err(SortError::SortMismatch { + term: yes, + shown: "Bool(true)".into(), + expected: int(), + found: boolean() + }) + ); +} + +#[test] +fn bool_literals_have_sort_bool() { + let mut f = Fixture::new(); + let no = f.bool_lit(false); + assert_eq!(f.check(no), Ok(boolean())); +} + +#[test] +fn forall_binds_var_zero_in_its_body() { + let mut f = Fixture::new(); + // ∀(n: int). (n ≥ 0) ⊃ token + let (n, zero) = (f.bound(0), f.lit(0)); + let guard = f.int_con(IntStaticCon::Geq, vec![n, zero]); + let token = f.token(); + let guarded = f.term(StaticTerm::Guard(guard, token)); + let forall = f.term(StaticTerm::Forall(int(), guarded)); + assert_eq!(f.check(forall), Ok(ty())); +} + +#[test] +fn quantifier_body_must_be_a_type() { + let mut f = Fixture::new(); + // ∃(n: int). n ≥ 0 — the body is a bool, not a type + let (n, zero) = (f.bound(0), f.lit(0)); + let geq = f.int_con(IntStaticCon::Geq, vec![n, zero]); + let exists = f.term(StaticTerm::Exists(int(), geq)); + assert_eq!( + f.check(exists), + Err(SortError::SortMismatch { + term: geq, + shown: "≥(a0, Index(IntSortT(0)))".into(), + expected: ty(), + found: boolean() + }) + ); +} + +#[test] +fn guard_and_assert_need_a_bool_then_a_type() { + let mut f = Fixture::new(); + let (yes, token) = (f.bool_lit(true), f.token()); + let assert = f.term(StaticTerm::Assert(yes, token)); + assert_eq!(f.check(assert), Ok(ty())); + + let swapped = f.term(StaticTerm::Guard(token, yes)); + assert_eq!( + f.check(swapped), + Err(SortError::SortMismatch { + term: token, + shown: "token".into(), + expected: boolean(), + found: ty() + }) + ); +} + +#[test] +fn product_and_function_types_take_types() { + let mut f = Fixture::new(); + let token = f.token(); + let triple = f.term(StaticTerm::Product(vec![token, token, token])); + assert_eq!(f.check(triple), Ok(ty())); + let fun_ty = f.term(StaticTerm::Function(vec![token, triple], token)); + assert_eq!(f.check(fun_ty), Ok(ty())); +} + +#[test] +fn function_type_result_must_be_a_type() { + let mut f = Fixture::new(); + let (token, one) = (f.token(), f.lit(1)); + // (token, token) → 1: the result is argument 2, after the two parameters + let fun_ty = f.term(StaticTerm::Function(vec![token, token], one)); + assert_eq!( + f.check(fun_ty), + Err(SortError::SortMismatch { + term: one, + shown: "Index(IntSortT(1))".into(), + expected: ty(), + found: int() + }) + ); +} + +#[test] +fn terms_render_with_variables_named_by_level() { + let mut f = Fixture::new(); + // ∀a0: int. ∃a1: bool. a1 ⊃ ((≥(a0, 0) ∧ token) * (token) → token) + let (b, n, zero, token) = (f.bound(0), f.bound(1), f.lit(0), f.token()); + let nonneg = f.int_con(IntStaticCon::Geq, vec![n, zero]); + let asserted = f.term(StaticTerm::Assert(nonneg, token)); + let thunk = f.term(StaticTerm::Function(vec![token], token)); + let pair = f.term(StaticTerm::Product(vec![asserted, thunk])); + let guarded = f.term(StaticTerm::Guard(b, pair)); + let exists = f.term(StaticTerm::Exists(boolean(), guarded)); + let forall = f.term(StaticTerm::Forall(int(), exists)); + assert_eq!( + f.statics.display(forall, 0).to_string(), + "∀a0: int. (∃a1: bool. (a1 ⊃ ((≥(a0, Index(IntSortT(0))) ∧ token) * ((token) → token))))" + ); + // the same body under a context of one variable, and an unbound variable + assert_eq!( + f.statics.display(nonneg, 2).to_string(), + "≥(a0, Index(IntSortT(0)))" + ); + let dangling = f.bound(3); + assert_eq!(f.statics.display(dangling, 1).to_string(), "?3"); + let free = f.free(int()); + assert_eq!(f.statics.display(free, 0).to_string(), "x0"); +} + +#[test] +fn free_variables_render_by_their_name_hint() { + let mut f = Fixture::new(); + let named = f.statics.fresh_var(int(), Some("n".into())); + let n = f.term(StaticTerm::Free(named)); + let unnamed = f.free(int()); + let geq = f.int_con(IntStaticCon::Geq, vec![n, unnamed]); + // a variable without a hint falls back to its id + assert_eq!(f.statics.display(geq, 0).to_string(), "≥(n, x1)"); +} + +#[test] +fn errors_display_the_offending_term() { + let mut f = Fixture::new(); + let (token, yes) = (f.token(), f.bool_lit(true)); + let swapped = f.term(StaticTerm::Guard(token, yes)); + assert_eq!( + f.check(swapped).unwrap_err().to_string(), + "`token` has sort `type`, but `bool` was expected" + ); + let one = f.lit(1); + let add = f.int_con(IntStaticCon::Add, vec![one]); + assert_eq!( + f.check(add).unwrap_err().to_string(), + "`+(Index(IntSortT(1)))` expects 2 arguments, but got 1" + ); +} + +#[test] +fn products_need_at_least_two_components() { + let mut f = Fixture::new(); + let token = f.token(); + assert_eq!(f.check(token), Ok(ty())); + let pair = f.term(StaticTerm::Product(vec![token, token])); + assert_eq!(f.check(pair), Ok(ty())); + + let empty = f.term(StaticTerm::Product(vec![])); + assert_eq!( + f.check(empty), + Err(SortError::ShortProduct { + term: empty, + shown: "()".into(), + found: 0 + }) + ); + let single = f.term(StaticTerm::Product(vec![token])); + assert_eq!( + f.check(single).unwrap_err().to_string(), + "a product needs at least 2 components, but `(token)` has 1" + ); +} + +#[test] +fn term_eq_compares_structure_not_ids() { + let mut f = Fixture::new(); + // two separately allocated copies of ∀(n: int). (n ≥ 0) ⊃ (token * token) + let build = |f: &mut Fixture| { + let (n, zero, token) = (f.bound(0), f.lit(0), f.token()); + let guard = f.int_con(IntStaticCon::Geq, vec![n, zero]); + let pair = f.term(StaticTerm::Product(vec![token, token])); + let guarded = f.term(StaticTerm::Guard(guard, pair)); + f.term(StaticTerm::Forall(int(), guarded)) + }; + let (a, b) = (build(&mut f), build(&mut f)); + assert_ne!(a, b); + assert!(f.statics.term_eq(a, b)); +} + +#[test] +fn term_eq_distinguishes_different_terms() { + let mut f = Fixture::new(); + let (token, zero, one) = (f.token(), f.lit(0), f.lit(1)); + let (x, y) = (f.bound(0), f.bound(1)); + let pair = f.term(StaticTerm::Product(vec![token, token])); + let triple = f.term(StaticTerm::Product(vec![token, token, token])); + let forall_int = f.term(StaticTerm::Forall(int(), token)); + let forall_bool = f.term(StaticTerm::Forall(boolean(), token)); + let exists_int = f.term(StaticTerm::Exists(int(), token)); + assert!(!f.statics.term_eq(zero, one)); // different constructors + assert!(!f.statics.term_eq(x, y)); // different bound variables + let (n, m) = (f.free(int()), f.free(int())); + assert!(!f.statics.term_eq(n, m)); // different free variables + assert!(!f.statics.term_eq(pair, triple)); // different arity + assert!(!f.statics.term_eq(forall_int, forall_bool)); // different binder sort + assert!(!f.statics.term_eq(forall_int, exists_int)); // different quantifier + assert!(!f.statics.term_eq(token, pair)); // different shape +} + +#[test] +fn mentions_finds_free_variables_under_binders() { + let mut f = Fixture::new(); + let var = f.statics.fresh_var(boolean(), None); + let (p, other, token) = (f.term(StaticTerm::Free(var)), f.free(boolean()), f.token()); + let guarded = f.term(StaticTerm::Guard(p, token)); + let forall = f.term(StaticTerm::Forall(int(), guarded)); + assert!(f.statics.mentions(forall, var)); + let unrelated = f.term(StaticTerm::Guard(other, token)); + assert!(!f.statics.mentions(unrelated, var)); +} From 160d0fc45e2071fe24667b41f863349c8d02bde3 Mon Sep 17 00:00:00 2001 From: Pablo Lanza Date: Wed, 11 Nov 2026 18:29:58 +0000 Subject: [PATCH 3/6] feat(types): add int and bool static constructor sets MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - `IntSort` with `IntStaticCon`: linear arithmetic, `≥`, and the singleton type `int(n)`; evaluation uses checked arithmetic. - `BoolStaticCon`: connectives, equality at each sort, and the singleton type `bool(B)`. - `kirin-test-utils` gains a `types` feature with `assert_eval_matches_signature`, used to test both sets. --- Cargo.lock | 2 + crates/kirin-test-utils/Cargo.toml | 2 + crates/kirin-test-utils/src/lib.rs | 3 + crates/kirin-test-utils/src/types.rs | 35 ++++++ crates/kirin-types/Cargo.toml | 3 + crates/kirin-types/src/lib.rs | 2 + crates/kirin-types/src/sorts/boolean.rs | 65 +++++++++++ crates/kirin-types/src/sorts/int.rs | 99 +++++++++++++++++ crates/kirin-types/src/sorts/mod.rs | 8 ++ crates/kirin-types/tests/sorts.rs | 142 ++++++++++++++++++++++++ 10 files changed, 361 insertions(+) create mode 100644 crates/kirin-test-utils/src/types.rs create mode 100644 crates/kirin-types/src/sorts/boolean.rs create mode 100644 crates/kirin-types/src/sorts/int.rs create mode 100644 crates/kirin-types/src/sorts/mod.rs create mode 100644 crates/kirin-types/tests/sorts.rs diff --git a/Cargo.lock b/Cargo.lock index a6afa809a..85725d424 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1051,6 +1051,7 @@ dependencies = [ "kirin-lexer", "kirin-prettyless", "kirin-test-types", + "kirin-types", "serde", "serde_json", ] @@ -1072,6 +1073,7 @@ name = "kirin-types" version = "0.1.0" dependencies = [ "kirin-ir", + "kirin-test-utils", "serde", "thiserror 2.0.18", ] diff --git a/crates/kirin-test-utils/Cargo.toml b/crates/kirin-test-utils/Cargo.toml index 146ad06be..280ec8133 100644 --- a/crates/kirin-test-utils/Cargo.toml +++ b/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"] diff --git a/crates/kirin-test-utils/src/lib.rs b/crates/kirin-test-utils/src/lib.rs index d9b1c8d1d..6ef09a997 100644 --- a/crates/kirin-test-utils/src/lib.rs +++ b/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; diff --git a/crates/kirin-test-utils/src/types.rs b/crates/kirin-test-utils/src/types.rs new file mode 100644 index 000000000..cc47d1a7b --- /dev/null +++ b/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(con: &C, args: &[SortValue]) +where + S: IndexSort, + C: StaticSig, +{ + 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::(), + *expected, + "the sample argument {arg:?} of `{con}` has the wrong sort" + ); + } + if let Some(value) = con.eval(args) { + assert_eq!( + value.sort::(), + sig.result, + "`{con}` evaluates {args:?} to {value:?}, which isn't of its result sort" + ); + } +} diff --git a/crates/kirin-types/Cargo.toml b/crates/kirin-types/Cargo.toml index de208f5d4..72f2f89d4 100644 --- a/crates/kirin-types/Cargo.toml +++ b/crates/kirin-types/Cargo.toml @@ -9,5 +9,8 @@ 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"] diff --git a/crates/kirin-types/src/lib.rs b/crates/kirin-types/src/lib.rs index a9079ee2b..31456c612 100644 --- a/crates/kirin-types/src/lib.rs +++ b/crates/kirin-types/src/lib.rs @@ -1,8 +1,10 @@ mod display; mod error; +mod sorts; mod statics; pub use error::SortError; +pub use sorts::{BoolStaticCon, IntSort, IntSortT, IntStaticCon}; pub use statics::{ IndexSort, Project, Sort, SortValue, StaticCon, StaticSig, StaticTerm, StaticTermId, StaticVar, StaticVarId, Statics, diff --git a/crates/kirin-types/src/sorts/boolean.rs b/crates/kirin-types/src/sorts/boolean.rs new file mode 100644 index 000000000..969f01d5e --- /dev/null +++ b/crates/kirin-types/src/sorts/boolean.rs @@ -0,0 +1,65 @@ +//! Booleans: literals, propositional connectives, equality, and the singleton +//! type of a proposition, over the built-in sort `bool`. + +use std::fmt; + +use crate::{IndexSort, Sort, SortValue, StaticCon, StaticSig}; + +/// Boolean static terms. `bool` is a built-in sort, so unlike `int` there is +/// no base sort to contribute, only constructors. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub enum BoolStaticCon { + /// `¬ : (bool) ⇒ bool` + Not, + /// `∧ : (bool, bool) ⇒ bool` + And, + /// `∨ : (bool, bool) ⇒ bool` + Or, + /// `⇒ : (bool, bool) ⇒ bool` + Implies, + /// `= : (σ, σ) ⇒ bool`, equality at the sort `σ`: one constructor per sort. + Equal(Sort), + /// `bool : (bool) ⇒ type`, the singleton type of the boolean `B`: branching + /// on its value establishes `B` in one arm and `¬B` in the other. + BoolOf, +} + +impl StaticSig for BoolStaticCon { + fn signature(&self) -> StaticCon { + let (args, result) = match *self { + Self::Not => (vec![Sort::Bool], Sort::Bool), + Self::And | Self::Or | Self::Implies => (vec![Sort::Bool, Sort::Bool], Sort::Bool), + Self::Equal(sort) => (vec![sort, sort], Sort::Bool), + Self::BoolOf => (vec![Sort::Bool], Sort::Type), + }; + StaticCon { args, result } + } + + fn eval(&self, args: &[SortValue]) -> Option> { + let value = match (self, args) { + (Self::Not, [p]) => !p.as_bool()?, + (Self::And, [p, q]) => p.as_bool()? && q.as_bool()?, + (Self::Or, [p, q]) => p.as_bool()? || q.as_bool()?, + (Self::Implies, [p, q]) => !p.as_bool()? || q.as_bool()?, + // Both arguments have sort `σ`, so their values compare directly + (Self::Equal(_), [a, b]) => a == b, + // `bool(B)` is a type, not a value + (Self::BoolOf, _) => return None, + _ => unreachable!("`eval` takes one value per argument of `signature`"), + }; + Some(SortValue::Bool(value)) + } +} + +impl fmt::Display for BoolStaticCon { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.write_str(match self { + Self::Not => "¬", + Self::And => "∧", + Self::Or => "∨", + Self::Implies => "⇒", + Self::Equal(_) => "=", + Self::BoolOf => "bool", + }) + } +} diff --git a/crates/kirin-types/src/sorts/int.rs b/crates/kirin-types/src/sorts/int.rs new file mode 100644 index 000000000..3ce00f0ff --- /dev/null +++ b/crates/kirin-types/src/sorts/int.rs @@ -0,0 +1,99 @@ +//! Integers: an index sort with literals, linear arithmetic, comparison, and +//! the singleton type of an integer. + +use std::fmt; + +use crate::{IndexSort, Project, Sort, SortValue, StaticCon, StaticSig}; + +/// `int`: an index sort, introduced like any user-defined base sort. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub struct IntSort; + +/// The type that values of sort `int` evaluate to. +/// Wraps around `i64` so other dialect sorts can also use `i64` as their `T`. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub struct IntSortT(pub i64); + +impl IndexSort for IntSort { + type T = IntSortT; + + fn sort_of(_: &IntSortT) -> Self { + IntSort + } + + fn name(&self) -> &'static str { + "int" + } +} + +/// Integer index terms: literals, linear arithmetic, comparison, and the +/// singleton type of an integer. Equality +/// is [`BoolStaticCon::Equal`](crate::BoolStaticCon::Equal). +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub enum IntStaticCon { + /// `+ : (int, int) ⇒ int` + Add, + /// `- : (int, int) ⇒ int` + Sub, + /// `k · _ : (int) ⇒ int`, + /// multiplication by a literal only, so arithmetic stays linear. + Mul(i64), + /// `≥ : (int, int) ⇒ bool` + Geq, + /// `int : (int) ⇒ type`, the type of runtime int parameterized their value + IntOf, +} + +impl StaticSig for IntStaticCon +where + S: IndexSort + From, + S::T: From + Project, +{ + fn signature(&self) -> StaticCon { + let int = Sort::Index(S::from(IntSort)); + match self { + Self::Add | Self::Sub => StaticCon { + args: vec![int, int], + result: int, + }, + Self::Mul(_) => StaticCon { + args: vec![int], + result: int, + }, + Self::Geq => StaticCon { + args: vec![int, int], + result: Sort::Bool, + }, + Self::IntOf => StaticCon { + args: vec![int], + result: Sort::Type, + }, + } + } + + fn eval(&self, args: &[SortValue]) -> Option> { + let int = |value: &SortValue| value.project::().map(|n| n.0); + let ext = |n: i64| SortValue::Index(IntSortT(n).into()); + match (self, args) { + (Self::Add, [a, b]) => int(a)?.checked_add(int(b)?).map(ext), + (Self::Sub, [a, b]) => int(a)?.checked_sub(int(b)?).map(ext), + (Self::Mul(k), [a]) => k.checked_mul(int(a)?).map(ext), + (Self::Geq, [a, b]) => Some(SortValue::Bool(int(a)? >= int(b)?)), + // `int(n)` is a type, not a value + (Self::IntOf, _) => None, + _ => unreachable!("`eval` takes one value per argument of `signature`"), + } + } +} + +impl fmt::Display for IntStaticCon { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Add => f.write_str("+"), + Self::Sub => f.write_str("-"), + Self::Mul(k) => write!(f, "{k}·"), + Self::Geq => f.write_str("≥"), + Self::IntOf => f.write_str("int"), + } + } +} diff --git a/crates/kirin-types/src/sorts/mod.rs b/crates/kirin-types/src/sorts/mod.rs new file mode 100644 index 000000000..4e0da342d --- /dev/null +++ b/crates/kirin-types/src/sorts/mod.rs @@ -0,0 +1,8 @@ +//! Library sorts and static constructor sets, for dialects to compose into +//! their own. + +mod boolean; +mod int; + +pub use boolean::BoolStaticCon; +pub use int::{IntSort, IntSortT, IntStaticCon}; diff --git a/crates/kirin-types/tests/sorts.rs b/crates/kirin-types/tests/sorts.rs new file mode 100644 index 000000000..1bd217164 --- /dev/null +++ b/crates/kirin-types/tests/sorts.rs @@ -0,0 +1,142 @@ +mod common; + +use common::{Fixture, boolean, int, ty}; +use kirin_test_utils::types::assert_eval_matches_signature; +use kirin_types::{ + BoolStaticCon, IntSort, IntSortT, IntStaticCon, SortError, SortValue, StaticSig, +}; + +#[test] +fn connectives_and_equality_have_sort_bool() { + use BoolStaticCon::*; + let mut f = Fixture::new(); + let (p, q, n) = (f.free(boolean()), f.free(boolean()), f.free(int())); + let zero = f.lit(0); + let not = f.bool_con(Not, vec![p]); + let and = f.bool_con(And, vec![not, q]); + let eq = f.bool_con(Equal(int()), vec![n, zero]); + let implies = f.bool_con(Implies, vec![and, eq]); + let or = f.bool_con(Or, vec![implies, p]); + assert_eq!(f.check(or), Ok(boolean())); + assert_eq!( + f.statics.display(or, 0).to_string(), + "∨(⇒(∧(¬(x0), x1), =(x2, Index(IntSortT(0)))), x0)" + ); +} + +#[test] +fn equality_compares_terms_of_its_sort() { + let mut f = Fixture::new(); + let (p, zero) = (f.free(boolean()), f.lit(0)); + let eq = f.bool_con(BoolStaticCon::Equal(int()), vec![p, zero]); + assert_eq!( + f.check(eq), + Err(SortError::SortMismatch { + term: p, + shown: "x0".into(), + expected: int(), + found: boolean() + }) + ); +} + +#[test] +fn bool_of_is_the_singleton_type_of_a_proposition() { + let mut f = Fixture::new(); + let (n, zero) = (f.free(int()), f.lit(0)); + let geq = f.int_con(IntStaticCon::Geq, vec![n, zero]); + let bool_of = f.bool_con(BoolStaticCon::BoolOf, vec![geq]); + assert_eq!(f.check(bool_of), Ok(ty())); + assert_eq!( + f.statics.display(bool_of, 0).to_string(), + "bool(≥(x0, Index(IntSortT(0))))" + ); +} + +#[test] +fn equality_is_distinguished_by_its_sort() { + let mut f = Fixture::new(); + let n = f.free(int()); + let eq_int = f.bool_con(BoolStaticCon::Equal(int()), vec![n, n]); + let eq_bool = f.bool_con(BoolStaticCon::Equal(boolean()), vec![n, n]); + assert!(!f.statics.term_eq(eq_int, eq_bool)); +} + +#[test] +fn int_of_is_the_singleton_type_of_an_integer() { + let mut f = Fixture::new(); + let n = f.free(int()); + let int_of = f.int_con(IntStaticCon::IntOf, vec![n]); + assert_eq!(f.check(int_of), Ok(ty())); + assert_eq!(f.statics.display(int_of, 0).to_string(), "int(x0)"); + + // its argument is an integer, not a type + let token = f.token(); + let wrong = f.int_con(IntStaticCon::IntOf, vec![token]); + assert_eq!( + f.check(wrong), + Err(SortError::SortMismatch { + term: token, + shown: "token".into(), + expected: int(), + found: ty() + }) + ); +} + +#[test] +fn constructors_evaluate_across_sorts() { + let (two, three) = (SortValue::Index(IntSortT(2)), SortValue::Index(IntSortT(3))); + let int_eval = + |con: IntStaticCon, args: &[SortValue]| StaticSig::::eval(&con, args); + let bool_eval = |con: BoolStaticCon, args: &[SortValue]| con.eval(args); + + // int ⇒ int, and int ⇒ bool + assert_eq!( + int_eval(IntStaticCon::Add, &[two, three]), + Some(SortValue::Index(IntSortT(5))) + ); + assert_eq!( + int_eval(IntStaticCon::Geq, &[two, three]), + Some(SortValue::Bool(false)) + ); + // equality at `int` compares integers + assert_eq!( + bool_eval(BoolStaticCon::Equal(int()), &[three, three]), + Some(SortValue::Bool(true)) + ); + // bool ⇒ bool + assert_eq!( + bool_eval( + BoolStaticCon::Implies, + &[SortValue::Bool(true), SortValue::Bool(false)] + ), + Some(SortValue::Bool(false)) + ); + // overflow, and types, don't fold + let max = SortValue::Index(IntSortT(i64::MAX)); + assert_eq!(int_eval(IntStaticCon::Add, &[max, two]), None); + assert_eq!(int_eval(IntStaticCon::IntOf, &[two]), None); +} + +#[test] +fn eval_matches_signatures() { + let (two, three) = (SortValue::Index(IntSortT(2)), SortValue::Index(IntSortT(3))); + let (yes, no) = (SortValue::Bool(true), SortValue::Bool(false)); + for con in [IntStaticCon::Add, IntStaticCon::Sub, IntStaticCon::Geq] { + assert_eval_matches_signature::(&con, &[two, three]); + } + assert_eval_matches_signature::(&IntStaticCon::Mul(4), &[three]); + assert_eval_matches_signature::(&IntStaticCon::IntOf, &[three]); + for con in [ + BoolStaticCon::And, + BoolStaticCon::Or, + BoolStaticCon::Implies, + ] { + assert_eval_matches_signature::(&con, &[yes, no]); + } + assert_eval_matches_signature::(&BoolStaticCon::Not, &[yes]); + assert_eval_matches_signature::(&BoolStaticCon::BoolOf, &[no]); + assert_eval_matches_signature::(&BoolStaticCon::Equal(int()), &[two, three]); + assert_eval_matches_signature::(&BoolStaticCon::Equal(boolean()), &[yes, no]); +} From d39dfc9b46e861d78e79fd72c982aae4ec70efcd Mon Sep 17 00:00:00 2001 From: Pablo Lanza Date: Wed, 11 Nov 2026 18:31:38 +0000 Subject: [PATCH 4/6] feat(types): substitute static arguments into static terms - `map_term`: a shared bottom-up rebuild of a static term that keeps unchanged subterms shared. - `Statics::instantiate` replaces a binder's bound variables with arguments (outermost first) and lowers the remaining indices. - `Statics::close` turns a free variable into a bound one, for wrapping in a new binder. --- crates/kirin-types/src/statics/mod.rs | 1 + crates/kirin-types/src/statics/subst.rs | 58 ++++++++++++++++++++ crates/kirin-types/src/statics/term.rs | 68 ++++++++++++++++++++++++ crates/kirin-types/tests/subst.rs | 70 +++++++++++++++++++++++++ 4 files changed, 197 insertions(+) create mode 100644 crates/kirin-types/src/statics/subst.rs create mode 100644 crates/kirin-types/tests/subst.rs diff --git a/crates/kirin-types/src/statics/mod.rs b/crates/kirin-types/src/statics/mod.rs index 8ed743616..d67811fd7 100644 --- a/crates/kirin-types/src/statics/mod.rs +++ b/crates/kirin-types/src/statics/mod.rs @@ -1,6 +1,7 @@ //! Statics: sorts, static constructors, and static terms. mod check; +mod subst; mod term; pub use term::{ diff --git a/crates/kirin-types/src/statics/subst.rs b/crates/kirin-types/src/statics/subst.rs new file mode 100644 index 000000000..b0c6afb7b --- /dev/null +++ b/crates/kirin-types/src/statics/subst.rs @@ -0,0 +1,58 @@ +use std::convert::Infallible; + +use super::{IndexSort, StaticTerm, StaticTermId, StaticVarId, Statics}; + +impl Statics { + /// Apply static arguments to a binder term's body. For example, + /// - `∀x:σ. T': Static argument `a` substitutes for `x` in `T` + /// - `∃x:σ. T': Static argument `a` substitutes for `x` in `T` + /// - [`DynSig`](crate::DynSig): Static arguments from + /// [`DynTerm::Constructor`](crate::DynTerm::Constructor) substitute + /// for the quantifiers in the signature's guards, arguments, and results. + /// + /// + /// The caller is expected to remove the binder term itself(e.g. + /// [`StaticTerm::Forall`] or [`StaticTerm::Exists`]). + /// + /// This function + /// 1. Replaces `term`'s bound variables with the corresponding argument + /// supplied in `args`: `Bound(i)` is replaced by ith arg from the + /// back in `args`, + /// 2. Shifts all other bound variables by the number of arguments + /// i.e. 1 in the case of Forall/Exists, and args.len() in the case of + /// a `DynSig`'s quantifiers. + pub fn instantiate(&mut self, term: StaticTermId, args: &[StaticTermId]) -> StaticTermId { + let k = args.len(); + + // Applies the corresponding argument to `term`'s bound variables + // and shifts all other bound variables. + let instantiate_bound_with_arg = + |statics: &mut Statics, node: &StaticTerm, depth| { + let StaticTerm::Bound(i) = *node else { + return None; + }; + match i.checked_sub(depth) { + None => None, + Some(level) if level < k => Some(args[k - 1 - level]), + Some(_) => Some(statics.alloc(StaticTerm::Bound(i - k))), + } + }; + + let Ok(instantiated) = self.map_term::(term, 0, &|statics, _, node, depth| { + Ok(instantiate_bound_with_arg(statics, node, depth)) + }); + instantiated + } + + /// Replace `Free(var)` with `Bound(d)`, where `d` is its depth in `term`. + /// The caller should then wrap the resulting `term` in a binder. + pub fn close(&mut self, term: StaticTermId, var: StaticVarId) -> StaticTermId { + let Ok(closed) = self.map_term::(term, 0, &|statics, _, node, depth| { + Ok(match *node { + StaticTerm::Free(x) if x == var => Some(statics.alloc(StaticTerm::Bound(depth))), + _ => None, + }) + }); + closed + } +} diff --git a/crates/kirin-types/src/statics/term.rs b/crates/kirin-types/src/statics/term.rs index 39fb5ed93..334e16d12 100644 --- a/crates/kirin-types/src/statics/term.rs +++ b/crates/kirin-types/src/statics/term.rs @@ -231,3 +231,71 @@ impl Statics { } } } + +impl Statics { + /// Maps `term` and its children nodes with function `f`. Traversal of + /// the nodes is done bottom-up, such that a node's children are mapped + /// before the node itself. + /// The function `f` is called with the following arguments: + /// * `self`: the `Statics` object to allocate any new terms. + /// * `term`: the original version of the current node being visited. + /// This is the same `term` as is `map_term`'s arguments + /// * `&rebuilt`: the version of the current node but with the children + /// already mapped by `f`. + /// * `depth`: The current depth from the starting node. + pub(super) fn map_term( + &mut self, + term: StaticTermId, + depth: usize, + f: &impl Fn( + &mut Self, + StaticTermId, + &StaticTerm, + usize, + ) -> Result, E>, + ) -> Result { + use StaticTerm::*; + let mut changed = false; + let mut map = |statics: &mut Self, child: StaticTermId, depth: usize| { + let mapped = statics.map_term(child, depth, f)?; + changed |= mapped != child; + Ok(mapped) + }; + // Recursively apply `map_term` to the `term`'s children. + // We take a copy of the node, so the recursive `&mut self` calls don't + // overlap its borrow. + let rebuilt = match (*self.terms[term]).clone() { + leaf @ (Bound(_) | Free(_) | Lit(_)) => leaf, + Constructor(c, args) => Constructor( + c, + args.into_iter() + .map(|arg| map(self, arg, depth)) + .collect::>()?, + ), + Product(args) => Product( + args.into_iter() + .map(|arg| map(self, arg, depth)) + .collect::>()?, + ), + Function(args, result) => { + let args = args + .into_iter() + .map(|arg| map(self, arg, depth)) + .collect::>()?; + Function(args, map(self, result, depth)?) + } + Guard(p, t) => Guard(map(self, p, depth)?, map(self, t, depth)?), + Assert(p, t) => Assert(map(self, p, depth)?, map(self, t, depth)?), + Forall(sort, body) => Forall(sort, map(self, body, depth + 1)?), + Exists(sort, body) => Exists(sort, map(self, body, depth + 1)?), + }; + + // Apply `f` to the node and return any changes made to the current node + if let Some(replacement) = f(self, term, &rebuilt, depth)? { + return Ok(replacement); + } + + // If any changes were made to the children, return the rebuilt node + Ok(if changed { self.alloc(rebuilt) } else { term }) + } +} diff --git a/crates/kirin-types/tests/subst.rs b/crates/kirin-types/tests/subst.rs new file mode 100644 index 000000000..2ddf7790a --- /dev/null +++ b/crates/kirin-types/tests/subst.rs @@ -0,0 +1,70 @@ +mod common; + +use common::{Fixture, int, ty}; +use kirin_types::{BoolStaticCon, IntStaticCon, StaticTerm}; + +#[test] +fn instantiate_takes_arguments_outermost_first() { + let mut f = Fixture::new(); + // ≥(Bound(1), Bound(0)) under the quantifiers (a, b), instantiated with (5, 3) + let (a, b, five, three) = (f.bound(1), f.bound(0), f.lit(5), f.lit(3)); + let geq = f.int_con(IntStaticCon::Geq, vec![a, b]); + let instantiated = f.statics.instantiate(geq, &[five, three]); + assert_eq!( + f.statics.display(instantiated, 0).to_string(), + "≥(Index(IntSortT(5)), Index(IntSortT(3)))" + ); +} + +#[test] +fn instantiate_skips_inner_binders_and_lowers_outer_indices() { + let mut f = Fixture::new(); + // ∀(m: int). (m = Bound(1)) ⊃ token, with Bound(1) the eliminated + // binder, and Bound(2) beyond it, which drops to Bound(1) + let (m, a, beyond, n) = (f.bound(0), f.bound(1), f.bound(2), f.free(int())); + let eq = f.bool_con(BoolStaticCon::Equal(int()), vec![m, a]); + let token = f.token(); + let guarded = f.term(StaticTerm::Guard(eq, token)); + let forall = f.term(StaticTerm::Forall(int(), guarded)); + let instantiated = f.statics.instantiate(forall, &[n]); + assert_eq!( + f.statics.display(instantiated, 0).to_string(), + "∀a0: int. (=(a0, x0) ⊃ token)" + ); + + let lowered = f.statics.instantiate(beyond, &[n]); + let expected = f.bound(1); + assert!(f.statics.term_eq(lowered, expected)); +} + +#[test] +fn instantiate_shares_terms_without_variables() { + let mut f = Fixture::new(); + let (token, one) = (f.token(), f.lit(1)); + let pair = f.term(StaticTerm::Product(vec![token, token])); + assert_eq!(f.statics.instantiate(pair, &[one]), pair); +} + +#[test] +fn close_then_instantiate_gives_back_the_term() { + let mut f = Fixture::new(); + // ∀(m: int). ≥(m, n) with n free + let var = f.statics.fresh_var(int(), None); + let (m, n) = (f.bound(0), f.term(StaticTerm::Free(var))); + let geq = f.int_con(IntStaticCon::Geq, vec![m, n]); + let token = f.token(); + let guarded = f.term(StaticTerm::Guard(geq, token)); + let forall = f.term(StaticTerm::Forall(int(), guarded)); + + let closed = f.statics.close(forall, var); + assert!(!f.statics.mentions(closed, var)); + let rebound = f.term(StaticTerm::Exists(int(), closed)); + assert_eq!( + f.statics.display(rebound, 0).to_string(), + "∃a0: int. (∀a1: int. (≥(a1, a0) ⊃ token))" + ); + assert_eq!(f.check(rebound), Ok(ty())); + + let reopened = f.statics.instantiate(closed, &[n]); + assert!(f.statics.term_eq(reopened, forall)); +} From c30764c8255cb314e285ab3d119d3fb56b32bf00 Mon Sep 17 00:00:00 2001 From: Pablo Lanza Date: Wed, 11 Nov 2026 18:33:08 +0000 Subject: [PATCH 5/6] feat(types): fold constant static terms - `Statics::reduce` folds constructor applications whose arguments are all literals, through `StaticSig::eval`, sharing what it can't fold. - Checks the argument count before evaluating, and rejects a result of the wrong sort with `SortError::EvalSort`. --- crates/kirin-types/src/error.rs | 9 ++ crates/kirin-types/src/statics/mod.rs | 1 + crates/kirin-types/src/statics/reduce.rs | 72 +++++++++++++++ crates/kirin-types/tests/reduce.rs | 113 +++++++++++++++++++++++ 4 files changed, 195 insertions(+) create mode 100644 crates/kirin-types/src/statics/reduce.rs create mode 100644 crates/kirin-types/tests/reduce.rs diff --git a/crates/kirin-types/src/error.rs b/crates/kirin-types/src/error.rs index aabb314f1..f02c4b781 100644 --- a/crates/kirin-types/src/error.rs +++ b/crates/kirin-types/src/error.rs @@ -34,4 +34,13 @@ pub enum SortError { expected: Sort, found: Sort, }, + #[error( + "`{shown}` evaluates to a value of sort `{found}`, but its signature's result is `{expected}`" + )] + EvalSort { + term: StaticTermId, + shown: String, + expected: Sort, + found: Sort, + }, } diff --git a/crates/kirin-types/src/statics/mod.rs b/crates/kirin-types/src/statics/mod.rs index d67811fd7..7db5962de 100644 --- a/crates/kirin-types/src/statics/mod.rs +++ b/crates/kirin-types/src/statics/mod.rs @@ -1,6 +1,7 @@ //! Statics: sorts, static constructors, and static terms. mod check; +mod reduce; mod subst; mod term; diff --git a/crates/kirin-types/src/statics/reduce.rs b/crates/kirin-types/src/statics/reduce.rs new file mode 100644 index 000000000..66168147c --- /dev/null +++ b/crates/kirin-types/src/statics/reduce.rs @@ -0,0 +1,72 @@ +use crate::SortError; + +use super::{IndexSort, StaticSig, StaticTerm, StaticTermId, Statics}; + +impl> Statics { + /// Folds constants in `term`: traverses `term` bottom-up, every + /// constructor application whose arguments are all literals is replaced + /// by the literal it evaluates to, if its [`StaticSig::eval`] gives one. + /// + /// Fails if a constructor applied to literals has the wrong number of + /// arguments, or evaluates to a value of another sort than its + /// signature's result. + pub fn reduce(&mut self, term: StaticTermId) -> Result> { + self.map_term(term, 0, &|statics, original, node, _| { + statics.reduce_constructor(original, node) + }) + } + + /// Reduces any [`StaticTerm::Constructor`] to the value it evaluates to + /// if all its args are [`StaticTerm::Lit`]. + fn reduce_constructor( + &mut self, + term: StaticTermId, + node: &StaticTerm, + ) -> Result, SortError> { + let StaticTerm::Constructor(con, args) = node else { + return Ok(None); + }; + + // Get the values of the literal args + let Some(values) = args + .iter() + .map(|arg| match &*self.terms[*arg] { + StaticTerm::Lit(value) => Some(value.clone()), + _ => None, + }) + .collect::>>() + else { + // return early if one of the args was not a `Lit` + return Ok(None); + }; + + // Number of arguments must match the signature's + let sig = con.signature(); + if values.len() != sig.args.len() { + return Err(SortError::ArityMismatch { + term, + shown: self.display(term, 0).to_string(), + expected: sig.args.len(), + found: values.len(), + }); + } + + let Some(value) = con.eval(&values) else { + // Some constructors do not evaluate + return Ok(None); + }; + + // The result value's sort must match the signature's + let found = value.sort(); + if found != sig.result { + return Err(SortError::EvalSort { + term, + shown: self.display(term, 0).to_string(), + expected: sig.result, + found, + }); + } + + Ok(Some(self.alloc(StaticTerm::Lit(value)))) + } +} diff --git a/crates/kirin-types/tests/reduce.rs b/crates/kirin-types/tests/reduce.rs new file mode 100644 index 000000000..7be45e67d --- /dev/null +++ b/crates/kirin-types/tests/reduce.rs @@ -0,0 +1,113 @@ +mod common; + +use std::fmt; + +use common::{Fixture, int}; +use kirin_types::{ + IntSort, IntSortT, IntStaticCon, Sort, SortError, SortValue, StaticCon, StaticSig, StaticTerm, + Statics, +}; + +#[test] +fn reduce_folds_constructors_applied_to_literals() { + let mut f = Fixture::new(); + // ≥(+(2, 3), 3) folds to `true`, through `5` + let (two, three) = (f.lit(2), f.lit(3)); + let sum = f.int_con(IntStaticCon::Add, vec![two, three]); + let geq = f.int_con(IntStaticCon::Geq, vec![sum, three]); + + let folded_sum = f.statics.reduce(sum).unwrap(); + let five = f.lit(5); + assert!(f.statics.term_eq(folded_sum, five)); + + let folded = f.statics.reduce(geq).unwrap(); + let yes = f.bool_lit(true); + assert!(f.statics.term_eq(folded, yes)); +} + +#[test] +fn reduce_stops_at_variables_and_folds_around_them() { + let mut f = Fixture::new(); + // ∀n: int. ≥(n, +(1, 1)) folds to ∀n: int. ≥(n, 2) + let (n, one) = (f.bound(0), f.lit(1)); + let sum = f.int_con(IntStaticCon::Add, vec![one, one]); + let geq = f.int_con(IntStaticCon::Geq, vec![n, sum]); + let token = f.token(); + let guarded = f.term(StaticTerm::Guard(geq, token)); + let forall = f.term(StaticTerm::Forall(int(), guarded)); + + let folded = f.statics.reduce(forall).unwrap(); + let two = f.lit(2); + let expected_geq = f.int_con(IntStaticCon::Geq, vec![n, two]); + let expected_guard = f.term(StaticTerm::Guard(expected_geq, token)); + let expected = f.term(StaticTerm::Forall(int(), expected_guard)); + assert!(f.statics.term_eq(folded, expected)); +} + +#[test] +fn reduce_shares_terms_it_cannot_fold() { + let mut f = Fixture::new(); + // overflow leaves `+(max, 1)` as it is, and a free variable blocks folding + let (max, one, x) = (f.lit(i64::MAX), f.lit(1), f.free(int())); + let overflow = f.int_con(IntStaticCon::Add, vec![max, one]); + assert_eq!(f.statics.reduce(overflow), Ok(overflow)); + let symbolic = f.int_con(IntStaticCon::Add, vec![x, one]); + assert_eq!(f.statics.reduce(symbolic), Ok(symbolic)); +} + +#[test] +fn reduce_checks_the_arity_before_evaluating() { + let mut f = Fixture::new(); + let one = f.lit(1); + let add = f.int_con(IntStaticCon::Add, vec![one]); + assert!(matches!( + f.statics.reduce(add), + Err(SortError::ArityMismatch { + expected: 2, + found: 1, + .. + }) + )); +} + +/// `liar : () ⇒ int`, whose `eval` wrongly gives a `bool`. +#[derive(Clone, PartialEq)] +struct Liar; + +impl StaticSig for Liar { + fn signature(&self) -> StaticCon { + StaticCon { + args: vec![], + result: int(), + } + } + + fn eval(&self, _: &[SortValue]) -> Option> { + Some(SortValue::Bool(true)) + } +} + +impl fmt::Display for Liar { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.write_str("liar") + } +} + +#[test] +fn reduce_rejects_a_value_of_the_wrong_sort() { + let mut statics = Statics::::default(); + let liar = statics.alloc(StaticTerm::Constructor(Liar, vec![])); + assert_eq!( + statics.reduce(liar), + Err(SortError::EvalSort { + term: liar, + shown: "liar".into(), + expected: int(), + found: Sort::Bool + }) + ); + assert_eq!( + statics.reduce(liar).unwrap_err().to_string(), + "`liar` evaluates to a value of sort `bool`, but its signature's result is `int`" + ); +} From 10b01a9d26c353e8293a7cc30cf32b98e6f71ca1 Mon Sep 17 00:00:00 2001 From: Pablo Lanza Date: Wed, 11 Nov 2026 18:35:52 +0000 Subject: [PATCH 6/6] feat(types): add dynamic terms and their type checker - `DynTerm`: the dynamic level, with named variables and constructors applied through signatures (`DynSig`) stored in `Dynamics`. - `Dynamics::check_type` synthesizes a term's type in a `Scope` of variable types and assumed propositions, instantiating signatures and quantifiers and comparing types after folding constants. - `slam` and `unpack` reject a static variable that the scope's types or assumptions already mention (`StaticRebound`), so a binder can't capture it. - Guard and assertion entailment are left as TODOs for a solver. - `TypeError` for dynamic terms. --- crates/kirin-types/src/dynamics/check.rs | 377 ++++++++++++++++ crates/kirin-types/src/dynamics/mod.rs | 7 + crates/kirin-types/src/dynamics/term.rs | 139 ++++++ crates/kirin-types/src/error.rs | 64 ++- crates/kirin-types/src/lib.rs | 4 +- crates/kirin-types/tests/check_type.rs | 537 +++++++++++++++++++++++ 6 files changed, 1126 insertions(+), 2 deletions(-) create mode 100644 crates/kirin-types/src/dynamics/check.rs create mode 100644 crates/kirin-types/src/dynamics/mod.rs create mode 100644 crates/kirin-types/src/dynamics/term.rs create mode 100644 crates/kirin-types/tests/check_type.rs diff --git a/crates/kirin-types/src/dynamics/check.rs b/crates/kirin-types/src/dynamics/check.rs new file mode 100644 index 000000000..1f7a37f30 --- /dev/null +++ b/crates/kirin-types/src/dynamics/check.rs @@ -0,0 +1,377 @@ +use std::collections::HashMap; + +use kirin_ir::Id; + +use crate::{ + IndexSort, Sort, SortError, StaticSig, StaticTerm, StaticTermId, StaticVarId, TypeError, +}; + +use super::{DynTerm, DynTermId, DynVarId, Dynamics}; + +/// The context at the point of a term being checked. +#[derive(Clone, Debug, Default)] +pub struct Scope { + /// The types (of sort `type`) of the dynamic variables in scope. + pub vars: HashMap, + /// The propositions (of sort `bool`) assumed to hold. + pub props: Vec, +} + +impl> Dynamics { + /// The type of `term` in `scope`. `scope` is left as it was given, unless + /// an error is returned. + pub fn check_type( + &mut self, + term: DynTermId, + scope: &mut Scope, + ) -> Result> { + // A copy of the node, so the recursive `&mut self` calls don't overlap its borrow. + match (*self.terms[term]).clone() { + DynTerm::Var(var) => { + scope + .vars + .get(&var) + .copied() + .ok_or_else(|| TypeError::UnboundVar { + term, + var, + shown: self.show_var(var), + }) + } + DynTerm::Constructor(sig, s_args, d_args, results, body) => { + // A copy of the signature, so `self.statics` can be mutated while it's read. + let sig = (*self.sigs[sig]).clone(); + + // Check that the static arguments match the signature's quantifiers + Self::expect_arity( + term, + "static arguments", + sig.quantifiers.len(), + s_args.len(), + )?; + for (s_arg, expected_sort) in s_args.iter().zip(&sig.quantifiers) { + self.expect_sort(*s_arg, *expected_sort)?; + } + + for guard in &sig.guards { + let _guard = self.instantiate(*guard, &s_args)?; + // TODO: check that `_guard` is entailed by `props` + } + + // Check that the dynamic arguments match the signature's argument types + Self::expect_arity(term, "arguments", sig.args.len(), d_args.len())?; + for (d_arg, expected_type) in d_args.iter().zip(&sig.args) { + let actual_type = self.check_type(*d_arg, scope)?; + let expected_type = self.instantiate(*expected_type, &s_args)?; + self.expect_type(*d_arg, expected_type, actual_type)?; + } + + // Bind the signature's results in `body`... + Self::expect_arity(term, "results", sig.results.len(), results.len())?; + let bindings = results + .iter() + .zip(&sig.results) + .map(|(var, ty)| Ok((*var, self.instantiate(*ty, &s_args)?))) + .collect::, TypeError>>()?; + + // ... and check the body's type with them in scope + self.check_under(term, &bindings, body, scope) + } + DynTerm::Tuple(sub_terms) => { + if sub_terms.len() < 2 { + return Err(TypeError::ShortTuple { + term, + found: sub_terms.len(), + }); + } + let component_types = sub_terms + .iter() + .map(|t| self.check_type(*t, scope)) + .collect::, _>>()?; + Ok(self.statics.alloc(StaticTerm::Product(component_types))) + } + DynTerm::Proj(index, tuple_term) => { + // Check that `tuple_term` has a product type + let tuple_type = self.check_type(tuple_term, scope)?; + let StaticTerm::Product(sub_types) = &*self.statics.terms[tuple_type] else { + return Err(self.shape_mismatch(term, "a product type", tuple_type)); + }; + + // Return the type of the `index`-th element + sub_types + .get(index) + .copied() + .ok_or(TypeError::ProjOutOfBounds { + term, + index, + len: sub_types.len(), + }) + } + DynTerm::Lam(params, body) => { + // Check all the parameter types are of sort `type` + for (_, ty) in ¶ms { + self.expect_sort(*ty, Sort::Type)?; + } + + // Check the body with the parameters in scope + let body_type = self.check_under(term, ¶ms, body, scope)?; + let param_types = params.into_iter().map(|(_, ty)| ty).collect(); + Ok(self + .statics + .alloc(StaticTerm::Function(param_types, body_type))) + } + DynTerm::App(fun, args) => { + // `fun` should have a function type + let fun_type = self.check_type(fun, scope)?; + let (expected_arg_tys, result_ty) = match &*self.statics.terms[fun_type] { + StaticTerm::Function(arg_tys, result_ty) => (arg_tys.clone(), *result_ty), + _ => return Err(self.shape_mismatch(fun, "a function type", fun_type)), + }; + + // `args`'s types should match the function's argument types + Self::expect_arity(term, "arguments", expected_arg_tys.len(), args.len())?; + for (arg, expected_ty) in args.iter().zip(&expected_arg_tys) { + let arg_ty = self.check_type(*arg, scope)?; + self.expect_type(*arg, *expected_ty, arg_ty)?; + } + Ok(result_ty) + } + DynTerm::GuardIntro(guard, body) => { + // Check that `guard` is of sort `bool` + self.expect_sort(guard, Sort::Bool)?; + + // Check the body with the guard added to the propositions + scope.props.push(guard); + let body_type = self.check_type(body, scope); + scope.props.pop(); + + Ok(self.statics.alloc(StaticTerm::Guard(guard, body_type?))) + } + DynTerm::GuardElim(guarded) => { + let guard_type = self.check_type(guarded, scope)?; + let StaticTerm::Guard(_guard_term, body_type) = *self.statics.terms[guard_type] + else { + return Err(self.shape_mismatch(guarded, "a guarded type", guard_type)); + }; + // TODO: check that `_guard_term` is entailed by `scope.props` + Ok(body_type) + } + DynTerm::StaticLam(var, body) => { + // `var` is generalized, so nothing in scope may depend on it + self.expect_fresh(term, var, scope)?; + let body_type = self.check_type(body, scope)?; + let sort = self.statics.vars[var].sort; + let closed = self.statics.close(body_type, var); + Ok(self.statics.alloc(StaticTerm::Forall(sort, closed))) + } + DynTerm::StaticApp(forall, s_arg) => { + let forall_ty = self.check_type(forall, scope)?; + let StaticTerm::Forall(expected_sort, body_type) = *self.statics.terms[forall_ty] + else { + return Err(self.shape_mismatch(forall, "a universal type", forall_ty)); + }; + self.expect_sort(s_arg, expected_sort)?; + self.instantiate(body_type, &[s_arg]) + } + DynTerm::Assert(prop, body) => { + self.expect_sort(prop, Sort::Bool)?; + // TODO: check that `prop` is entailed by `scope.props` + let body_type = self.check_type(body, scope)?; + Ok(self.statics.alloc(StaticTerm::Assert(prop, body_type))) + } + DynTerm::LetAssert(var, bound, body) => { + let bound_type = self.check_type(bound, scope)?; + let StaticTerm::Assert(prop, value_type) = *self.statics.terms[bound_type] else { + return Err(self.shape_mismatch(bound, "an asserting type", bound_type)); + }; + + scope.props.push(prop); + let body_type = self.check_under(term, &[(var, value_type)], body, scope); + scope.props.pop(); + + body_type + } + DynTerm::Pack(witness, inner, body) => { + let sort = self.statics.check_sort(witness)?; + // Checking the existential checks `inner` under its binder. + let exists = self.statics.alloc(StaticTerm::Exists(sort, inner)); + self.expect_sort(exists, Sort::Type)?; + + let body_type = self.check_type(body, scope)?; + let expected = self.instantiate(inner, &[witness])?; + self.expect_type(body, expected, body_type)?; + + Ok(exists) + } + DynTerm::Unpack(var, value, packed, body) => { + let packed_type = self.check_type(packed, scope)?; + let StaticTerm::Exists(sort, inner) = *self.statics.terms[packed_type] else { + return Err(self.shape_mismatch(packed, "an existential type", packed_type)); + }; + let var_sort = self.statics.vars[var].sort; + if var_sort != sort { + return Err(TypeError::BinderSort { + term, + shown: self.statics.display(packed_type, 0).to_string(), + expected: sort, + found: var_sort, + }); + } + // `var` stands for the hidden witness, so nothing in scope may + // already mention it + self.expect_fresh(term, var, scope)?; + + let free = self.statics.alloc(StaticTerm::Free(var)); + let opened = self.statics.instantiate(inner, &[free]); + let body_type = self.check_under(term, &[(value, opened)], body, scope)?; + + if self.statics.mentions(body_type, var) { + return Err(TypeError::Escape { + term, + shown: self.statics.display(body_type, 0).to_string(), + }); + } + Ok(body_type) + } + } + } + + /// Checks `body` with `bindings` added to the scope, removing them + /// afterwards. `term` is the binder, for errors. + fn check_under( + &mut self, + term: DynTermId, + bindings: &[(DynVarId, StaticTermId)], + body: DynTermId, + scope: &mut Scope, + ) -> Result> { + // insert the bindings into the scope, checking for rebinding errors + for (var, ty) in bindings { + if scope.vars.insert(*var, *ty).is_some() { + return Err(TypeError::Rebound { + term, + var: *var, + shown: self.show_var(*var), + }); + } + } + // check the body's type + let body_type = self.check_type(body, scope); + // remove the bindings from the scope, leaving it as it was + for (var, _) in bindings { + scope.vars.remove(var); + } + + body_type + } + + /// Checks that the static variable `var`, which the binder `term` is about + /// to bind, is not mentioned by `scope`: neither by the types of its + /// variables nor by its propositions. Otherwise the binder would capture + /// a variable that something outside it depends on. + fn expect_fresh( + &mut self, + term: DynTermId, + var: StaticVarId, + scope: &Scope, + ) -> Result<(), TypeError> { + let mentioned = scope + .vars + .values() + .chain(&scope.props) + .any(|t| self.statics.mentions(*t, var)); + if mentioned { + let free = self.statics.alloc(StaticTerm::Free(var)); + return Err(TypeError::StaticRebound { + term, + var, + shown: self.statics.display(free, 0).to_string(), + }); + } + Ok(()) + } + + /// The name of `var`, or `v` followed by its id. + fn show_var(&self, var: DynVarId) -> String { + match &self.vars[var].name { + Some(name) => name.clone(), + None => format!("v{}", Id::from(var).raw()), + } + } + + /// Checks that the locally closed static term `term` has sort `expected`. + fn expect_sort(&self, term: StaticTermId, expected: Sort) -> Result<(), TypeError> { + let found = self.statics.check_sort(term)?; + if found != expected { + return Err(SortError::SortMismatch { + term, + shown: self.statics.display(term, 0).to_string(), + expected, + found, + } + .into()); + } + Ok(()) + } + + /// `term` with `args` substituted for its outermost binders, then + /// reduced, so that literal arithmetic in it is folded. + fn instantiate( + &mut self, + term: StaticTermId, + args: &[StaticTermId], + ) -> Result> { + let instantiated = self.statics.instantiate(term, args); + Ok(self.statics.reduce(instantiated)?) + } + + /// Checks that `term`, of type `found`, has type `expected`. Both are + /// reduced first, so e.g. `int(add(1, 2))` and `int(3)` are equal. + fn expect_type( + &mut self, + term: DynTermId, + expected: StaticTermId, + found: StaticTermId, + ) -> Result<(), TypeError> { + let expected = self.statics.reduce(expected)?; + let found = self.statics.reduce(found)?; + if !self.statics.term_eq(expected, found) { + return Err(TypeError::TypeMismatch { + term, + expected: self.statics.display(expected, 0).to_string(), + found: self.statics.display(found, 0).to_string(), + }); + } + Ok(()) + } + + fn expect_arity( + term: DynTermId, + what: &'static str, + expected: usize, + found: usize, + ) -> Result<(), TypeError> { + if found != expected { + return Err(TypeError::ArityMismatch { + term, + what, + expected, + found, + }); + } + Ok(()) + } + + fn shape_mismatch( + &self, + term: DynTermId, + expected: &'static str, + found: StaticTermId, + ) -> TypeError { + TypeError::ShapeMismatch { + term, + expected, + found: self.statics.display(found, 0).to_string(), + } + } +} diff --git a/crates/kirin-types/src/dynamics/mod.rs b/crates/kirin-types/src/dynamics/mod.rs new file mode 100644 index 000000000..ef564a75a --- /dev/null +++ b/crates/kirin-types/src/dynamics/mod.rs @@ -0,0 +1,7 @@ +//! Dynamics: program terms, classified by static terms of sort `type`. + +mod check; +mod term; + +pub use check::Scope; +pub use term::{DynSig, DynSigId, DynTerm, DynTermId, DynVar, DynVarId, Dynamics}; diff --git a/crates/kirin-types/src/dynamics/term.rs b/crates/kirin-types/src/dynamics/term.rs new file mode 100644 index 000000000..817257a7a --- /dev/null +++ b/crates/kirin-types/src/dynamics/term.rs @@ -0,0 +1,139 @@ +use kirin_ir::{Arena, identifier}; + +use crate::{IndexSort, Sort, StaticTermId, StaticVarId, Statics}; + +/// The signature for a dynamic constructor: +/// `∀ā:σ̄. B̄ ⊃ (T_1, …, T_n) ⇒ (U_1, …, U_m)` +/// May have any number of results, like a kirin-ir Statement. +/// +/// The quantifiers `ā` bind `guards`, `args`, and `results` as `Bound` +/// indices: the last quantifier is `Bound(0)` and the first is `Bound(k - 1)`. +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct DynSig { + /// The sorts `σ̄` of the quantified static variables `ā`. + pub quantifiers: Vec>, + /// The guards `B̄`, each of sort `bool`. + pub guards: Vec, + /// The argument types `T_1, …, T_n`, each of sort `type`. + pub args: Vec, + /// The result types `U_1, …, U_m`, each of sort `type`. + pub results: Vec, +} + +identifier! { + /// A signature allocated in [`Dynamics::sigs`]. + struct DynSigId +} + +identifier! { + /// A dynamic term allocated in [`Dynamics::terms`]. + struct DynTermId +} + +identifier! { + /// A dynamic variable allocated in [`Dynamics::vars`]. + struct DynVarId +} + +/// A dynamic variable. Each binder introduces its own variables, so a +/// variable is bound exactly once. +#[derive(Clone, Debug, Default, PartialEq, Eq)] +pub struct DynVar { + /// A name for diagnostics, e.g. the SSA value the variable stands for. + pub name: Option, +} + +/// A dynamic term. +/// +/// The terms `GuardIntro`, `GuardElim`, `StaticLam`, `StaticApp`, `Assert`, +/// `LetAssert`, `Pack`, and `Unpack` are not expected to be used directly +/// by the user. They will be inserted by the type checker when it elaborates +/// a term that requires them. +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub enum DynTerm { + /// A dynamic variable, bound by `Constructor`, `Lam`, `LetAssert`, or + /// `Unpack`. + Var(DynVarId), + /// `let (x_1, …, x_m) = dcx{s̄}(e_1, …, e_n) in e`: a constructor, given + /// by its signature, applied to static then dynamic arguments, binding its + /// `m` results to the variables `x_1, …, x_m` in `e`. + Constructor( + DynSigId, // The signature of the constructor `dcx` + Vec, // The static arguments `s̄` + Vec, // The dynamic arguments `e_1, …, e_n` + Vec, // The bound variables `x_1, …, x_m` + DynTermId, // The successor term `e` + ), + /// `⟨e_1, …, e_n⟩` with `n ≥ 2`: introduces a `Product` type. + Tuple(Vec), + /// `proj_i(e)`: eliminates a `Product`, selecting component `i` (0-based). + Proj(usize, DynTermId), + /// `lam (x_1: T_1, …, x_n: T_n). e`: introduces a `Function`, binding the + /// variables `x_1, …, x_n` in `e`. Each `T_i` has sort `type`. + Lam(Vec<(DynVarId, StaticTermId)>, DynTermId), + /// `app(e, (e_1, …, e_n))`: eliminates a `Function`. + App(DynTermId, Vec), + /// `⊃⁺[B](e)`: introduces a guarded type `B ⊃ T`, checking `e` under the + /// assumption `B` (of sort `bool`). + GuardIntro(StaticTermId, DynTermId), + /// `⊃⁻(e)`: eliminates a guarded type once its guard is entailed. + GuardElim(DynTermId), + /// `slam (a: σ). e`: introduces `∀a:σ. T`, where `σ` is the sort of `a` in + /// [`Statics::vars`] and the static terms within `e` (type annotations, + /// static arguments, propositions) refer to `a` as + /// [`StaticTerm::Free(a)`](`crate::StaticTerm::Free`). + StaticLam(StaticVarId, DynTermId), + /// `sapp(e, s)` eliminates a ∀ type, applying a static argument `s`. + StaticApp(DynTermId, StaticTermId), + /// `∧[B](e)`: introduces an asserting type `B ∧ T`, once `B` (of sort + /// `bool`) is entailed. + Assert(StaticTermId, DynTermId), + /// `let ∧(x) = e_1 in e_2`, binding the variable `x` in `e_2`. + LetAssert(DynVarId, DynTermId, DynTermId), + /// `⟨s, e⟩ as ∃a. T`: introduces `∃a:σ. T`, where `σ` is the sort of the + /// witness `s` and `T` binds `a` as `Bound(0)`; `e` must have type `T[a ↦ s]`. + Pack(StaticTermId, StaticTermId, DynTermId), + /// `let ⟨a, x⟩ = e_1 in e_2`: eliminates `∃a:σ. T`, where `e_1` has that + /// type and `σ` must be the sort of `a` in [`Statics::vars`]. In `e_2`, the + /// static terms (type annotations, static arguments, propositions) refer to + /// `a` as [`StaticTerm::Free(a)`](`crate::StaticTerm::Free`), and `x` is a + /// dynamic variable of type `T` with `a` for its bound variable. + Unpack(StaticVarId, DynVarId, DynTermId, DynTermId), +} + +/// The dynamic terms of one program, their variables, the signatures of the +/// constructors they apply, and the static terms they mention. +pub struct Dynamics { + pub terms: Arena, + pub vars: Arena, + pub sigs: Arena>, + pub statics: Statics, +} + +impl Default for Dynamics { + fn default() -> Self { + Self { + terms: Arena::default(), + vars: Arena::default(), + sigs: Arena::default(), + statics: Statics::default(), + } + } +} + +impl Dynamics { + pub fn alloc(&mut self, term: DynTerm) -> DynTermId { + self.terms.alloc(term) + } + + /// Stores `sig`, whose static terms are in [`Dynamics::statics`], so that + /// `Constructor`s can refer to it. + pub fn alloc_sig(&mut self, sig: DynSig) -> DynSigId { + self.sigs.alloc(sig) + } + + /// A new dynamic variable, with an optional name for diagnostics. + pub fn fresh_var(&mut self, name: Option) -> DynVarId { + self.vars.alloc(DynVar { name }) + } +} diff --git a/crates/kirin-types/src/error.rs b/crates/kirin-types/src/error.rs index f02c4b781..dea8472c9 100644 --- a/crates/kirin-types/src/error.rs +++ b/crates/kirin-types/src/error.rs @@ -2,7 +2,7 @@ use thiserror::Error; -use crate::{Sort, StaticTermId}; +use crate::{DynTermId, DynVarId, Sort, StaticTermId, StaticVarId}; /// A static term that has no sort. `term` is where the error was found; /// `shown` renders it for the message. @@ -44,3 +44,65 @@ pub enum SortError { found: Sort, }, } + +/// A dynamic term that has no type. `term` is where the error was found; +/// static terms are rendered into the message where they appear. +#[derive(Clone, Debug, Error, PartialEq, Eq)] +pub enum TypeError { + #[error(transparent)] + Sort(#[from] SortError), + #[error("dynamic variable `{shown}` is not in scope")] + UnboundVar { + term: DynTermId, + var: DynVarId, + shown: String, + }, + #[error("dynamic variable `{shown}` is bound while already in scope")] + Rebound { + term: DynTermId, + var: DynVarId, + shown: String, + }, + #[error("static variable `{shown}` is bound while the scope mentions it")] + StaticRebound { + term: DynTermId, + var: StaticVarId, + shown: String, + }, + #[error("expected type `{expected}`, but found `{found}`")] + TypeMismatch { + term: DynTermId, + expected: String, + found: String, + }, + #[error("expected {expected}, but found `{found}`")] + ShapeMismatch { + term: DynTermId, + expected: &'static str, + found: String, + }, + #[error("expected {expected} {what}, but got {found}")] + ArityMismatch { + term: DynTermId, + what: &'static str, + expected: usize, + found: usize, + }, + #[error("the binder has sort `{found}`, but the unpacked `{shown}` binds a `{expected}`")] + BinderSort { + term: DynTermId, + shown: String, + expected: Sort, + found: Sort, + }, + #[error("the type `{shown}` of an unpack's body mentions its bound variable")] + Escape { term: DynTermId, shown: String }, + #[error("a tuple needs at least 2 components, but got {found}")] + ShortTuple { term: DynTermId, found: usize }, + #[error("projection {index} is out of bounds for a product of {len} components")] + ProjOutOfBounds { + term: DynTermId, + index: usize, + len: usize, + }, +} diff --git a/crates/kirin-types/src/lib.rs b/crates/kirin-types/src/lib.rs index 31456c612..863b9eb4a 100644 --- a/crates/kirin-types/src/lib.rs +++ b/crates/kirin-types/src/lib.rs @@ -1,9 +1,11 @@ mod display; +mod dynamics; mod error; mod sorts; mod statics; -pub use error::SortError; +pub use dynamics::{DynSig, DynSigId, DynTerm, DynTermId, DynVar, DynVarId, Dynamics, Scope}; +pub use error::{SortError, TypeError}; pub use sorts::{BoolStaticCon, IntSort, IntSortT, IntStaticCon}; pub use statics::{ IndexSort, Project, Sort, SortValue, StaticCon, StaticSig, StaticTerm, StaticTermId, StaticVar, diff --git a/crates/kirin-types/tests/check_type.rs b/crates/kirin-types/tests/check_type.rs new file mode 100644 index 000000000..dabdd0c99 --- /dev/null +++ b/crates/kirin-types/tests/check_type.rs @@ -0,0 +1,537 @@ +mod common; + +use common::{TestCon, TestSort, TestTerm, boolean, int, ty}; +use kirin_types::{ + DynSig, DynSigId, DynTerm, DynTermId, DynVarId, Dynamics, IntSort, IntSortT, IntStaticCon, + Scope, SortValue, StaticTerm, StaticTermId, StaticVarId, TypeError, +}; + +/// Dynamics with the signatures of `mk` and `id`, plus shorthands for +/// building and checking terms. +struct Fixture { + dynamics: Dynamics, + mk: DynSigId, + id: DynSigId, +} + +impl Fixture { + fn new() -> Self { + let mut dynamics = Dynamics::::default(); + + // mk : () ⇒ (token) + let token = dynamics + .statics + .alloc(StaticTerm::Constructor(TestCon::Token, vec![])); + let mk = dynamics.alloc_sig(DynSig { + quantifiers: vec![], + guards: vec![], + args: vec![], + results: vec![token], + }); + + // id : ∀a:type. (a) ⇒ (a) + let a = dynamics.statics.alloc(StaticTerm::Bound(0)); + let id = dynamics.alloc_sig(DynSig { + quantifiers: vec![ty()], + guards: vec![], + args: vec![a], + results: vec![a], + }); + + Self { dynamics, mk, id } + } + + fn st(&mut self, term: TestTerm) -> StaticTermId { + self.dynamics.statics.alloc(term) + } + + fn dt(&mut self, term: DynTerm) -> DynTermId { + self.dynamics.alloc(term) + } + + fn token(&mut self) -> StaticTermId { + self.st(StaticTerm::Constructor(TestCon::Token, vec![])) + } + + /// A new static variable of sort `sort` named `name`. + fn static_var(&mut self, sort: TestSort, name: &str) -> StaticVarId { + self.dynamics.statics.fresh_var(sort, Some(name.into())) + } + + /// A new dynamic variable named `name`. + fn var(&mut self, name: &str) -> DynVarId { + self.dynamics.fresh_var(Some(name.into())) + } + + /// A use of `var`. + fn use_var(&mut self, var: DynVarId) -> DynTermId { + self.dt(DynTerm::Var(var)) + } + + /// `let (x) = mk() in body` + fn let_mk(&mut self, x: DynVarId, body: DynTermId) -> DynTermId { + self.dt(DynTerm::Constructor(self.mk, vec![], vec![], vec![x], body)) + } + + fn check(&mut self, term: DynTermId) -> Result> { + let mut scope = Scope::default(); + let checked = self.dynamics.check_type(term, &mut scope); + if checked.is_ok() { + assert!(scope.vars.is_empty() && scope.props.is_empty()); + } + checked + } + + /// The type of `term`, rendered. + fn type_of(&mut self, term: DynTermId) -> String { + let ty = self.check(term).unwrap(); + self.dynamics.statics.display(ty, 0).to_string() + } +} + +#[test] +fn constructor_binds_its_results() { + let mut f = Fixture::new(); + // let (x) = mk() in x + let x = f.var("x"); + let use_x = f.use_var(x); + let term = f.let_mk(x, use_x); + assert_eq!(f.type_of(term), "token"); +} + +#[test] +fn constructor_needs_a_variable_per_result() { + let mut f = Fixture::new(); + // `mk` has one result, but no variable is given for it + let x = f.var("x"); + let use_x = f.use_var(x); + let term = f.dt(DynTerm::Constructor(f.mk, vec![], vec![], vec![], use_x)); + assert_eq!( + f.check(term), + Err(TypeError::ArityMismatch { + term, + what: "results", + expected: 1, + found: 0 + }) + ); +} + +#[test] +fn constructor_instantiates_its_signature() { + let mut f = Fixture::new(); + // let (t) = mk() in let (r) = id{token}(t) in r + let (t, r) = (f.var("t"), f.var("r")); + let (use_t, use_r, token) = (f.use_var(t), f.use_var(r), f.token()); + let id = f.dt(DynTerm::Constructor( + f.id, + vec![token], + vec![use_t], + vec![r], + use_r, + )); + let term = f.let_mk(t, id); + assert_eq!(f.type_of(term), "token"); +} + +#[test] +fn constructor_checks_arguments_against_the_instantiated_types() { + let mut f = Fixture::new(); + // let (t) = mk() in let (r) = id{token * token}(t) in r + let (t, r) = (f.var("t"), f.var("r")); + let (use_t, use_r, token) = (f.use_var(t), f.use_var(r), f.token()); + let pair = f.st(StaticTerm::Product(vec![token, token])); + let id = f.dt(DynTerm::Constructor( + f.id, + vec![pair], + vec![use_t], + vec![r], + use_r, + )); + let term = f.let_mk(t, id); + assert_eq!( + f.check(term), + Err(TypeError::TypeMismatch { + term: use_t, + expected: "(token * token)".into(), + found: "token".into() + }) + ); +} + +#[test] +fn variable_out_of_scope_is_unbound() { + let mut f = Fixture::new(); + // ⟨let (x) = mk() in x, x⟩: the second `x` is outside its binder + let x = f.var("x"); + let (inner_x, outer_x) = (f.use_var(x), f.use_var(x)); + let bound = f.let_mk(x, inner_x); + let tuple = f.dt(DynTerm::Tuple(vec![bound, outer_x])); + assert_eq!( + f.check(tuple), + Err(TypeError::UnboundVar { + term: outer_x, + var: x, + shown: "x".into() + }) + ); +} + +#[test] +fn unnamed_variables_are_shown_by_id() { + let mut f = Fixture::new(); + let x = f.dynamics.fresh_var(None); + let use_x = f.use_var(x); + let TypeError::UnboundVar { shown, .. } = f.check(use_x).unwrap_err() else { + panic!("expected an unbound variable error"); + }; + assert_eq!(shown, "v0"); +} + +#[test] +fn binding_a_variable_already_in_scope_is_rejected() { + let mut f = Fixture::new(); + // let (x) = mk() in let (x) = mk() in x + let x = f.var("x"); + let use_x = f.use_var(x); + let inner = f.let_mk(x, use_x); + let outer = f.let_mk(x, inner); + assert_eq!( + f.check(outer), + Err(TypeError::Rebound { + term: inner, + var: x, + shown: "x".into() + }) + ); +} + +#[test] +fn projection_selects_a_component() { + let mut f = Fixture::new(); + // let (t) = mk() in proj_1(⟨t, ⟨t, t⟩⟩) + let t = f.var("t"); + let (first, second, third) = (f.use_var(t), f.use_var(t), f.use_var(t)); + let pair = f.dt(DynTerm::Tuple(vec![second, third])); + let tuple = f.dt(DynTerm::Tuple(vec![first, pair])); + let proj = f.dt(DynTerm::Proj(1, tuple)); + let term = f.let_mk(t, proj); + assert_eq!(f.type_of(term), "(token * token)"); +} + +#[test] +fn projection_out_of_bounds_is_rejected() { + let mut f = Fixture::new(); + // let (t) = mk() in proj_2(⟨t, t⟩) + let t = f.var("t"); + let (first, second) = (f.use_var(t), f.use_var(t)); + let pair = f.dt(DynTerm::Tuple(vec![first, second])); + let proj = f.dt(DynTerm::Proj(2, pair)); + let term = f.let_mk(t, proj); + assert_eq!( + f.check(term), + Err(TypeError::ProjOutOfBounds { + term: proj, + index: 2, + len: 2 + }) + ); +} + +#[test] +fn projection_needs_a_product_type() { + let mut f = Fixture::new(); + // let (t) = mk() in proj_0(t) + let t = f.var("t"); + let use_t = f.use_var(t); + let proj = f.dt(DynTerm::Proj(0, use_t)); + let term = f.let_mk(t, proj); + assert_eq!( + f.check(term), + Err(TypeError::ShapeMismatch { + term: proj, + expected: "a product type", + found: "token".into() + }) + ); +} + +#[test] +fn tuple_needs_at_least_two_components() { + let mut f = Fixture::new(); + // let (t) = mk() in ⟨t⟩ + let t = f.var("t"); + let use_t = f.use_var(t); + let tuple = f.dt(DynTerm::Tuple(vec![use_t])); + let term = f.let_mk(t, tuple); + assert_eq!( + f.check(term), + Err(TypeError::ShortTuple { + term: tuple, + found: 1 + }) + ); +} + +#[test] +fn guard_intro_then_elim_gives_back_the_type() { + let mut f = Fixture::new(); + // ⊃⁺[p](let (t) = mk() in t), with `p` a free proposition + let p = f.static_var(boolean(), "p"); + let prop = f.st(StaticTerm::Free(p)); + let t = f.var("t"); + let use_t = f.use_var(t); + let body = f.let_mk(t, use_t); + let guarded = f.dt(DynTerm::GuardIntro(prop, body)); + assert_eq!(f.type_of(guarded), "p ⊃ token"); + + // ⊃⁻(…) + let elim = f.dt(DynTerm::GuardElim(guarded)); + assert_eq!(f.type_of(elim), "token"); +} + +#[test] +fn assert_then_let_assert_gives_back_the_type() { + let mut f = Fixture::new(); + // ∧[p](let (t) = mk() in t), with `p` a free proposition + let p = f.static_var(boolean(), "p"); + let prop = f.st(StaticTerm::Free(p)); + let t = f.var("t"); + let use_t = f.use_var(t); + let body = f.let_mk(t, use_t); + let asserted = f.dt(DynTerm::Assert(prop, body)); + assert_eq!(f.type_of(asserted), "p ∧ token"); + + // let ∧(x) = … in x + let x = f.var("x"); + let use_x = f.use_var(x); + let let_assert = f.dt(DynTerm::LetAssert(x, asserted, use_x)); + assert_eq!(f.type_of(let_assert), "token"); +} + +#[test] +fn let_assert_needs_an_asserting_type() { + let mut f = Fixture::new(); + // let (t) = mk() in let ∧(x) = t in x + let (t, x) = (f.var("t"), f.var("x")); + let (use_t, use_x) = (f.use_var(t), f.use_var(x)); + let let_assert = f.dt(DynTerm::LetAssert(x, use_t, use_x)); + let term = f.let_mk(t, let_assert); + assert_eq!( + f.check(term), + Err(TypeError::ShapeMismatch { + term: use_t, + expected: "an asserting type", + found: "token".into() + }) + ); +} + +#[test] +fn static_lam_closes_its_variable_and_static_app_instantiates_it() { + let mut f = Fixture::new(); + // slam (a: type). lam (y: a). y + let a = f.static_var(ty(), "a"); + let free_a = f.st(StaticTerm::Free(a)); + let y = f.var("y"); + let use_y = f.use_var(y); + let lam = f.dt(DynTerm::Lam(vec![(y, free_a)], use_y)); + let slam = f.dt(DynTerm::StaticLam(a, lam)); + assert_eq!(f.type_of(slam), "∀a0: type. ((a0) → a0)"); + + let token = f.token(); + let sapp = f.dt(DynTerm::StaticApp(slam, token)); + assert_eq!(f.type_of(sapp), "(token) → token"); +} + +#[test] +fn static_lam_rejects_a_variable_the_scope_mentions() { + let mut f = Fixture::new(); + // lam (y: a). slam (a: type). y: generalizing `a` would claim that `y` + // has every type + let a = f.static_var(ty(), "a"); + let free_a = f.st(StaticTerm::Free(a)); + let y = f.var("y"); + let use_y = f.use_var(y); + let slam = f.dt(DynTerm::StaticLam(a, use_y)); + let lam = f.dt(DynTerm::Lam(vec![(y, free_a)], slam)); + assert_eq!( + f.check(lam), + Err(TypeError::StaticRebound { + term: slam, + var: a, + shown: "a".into() + }) + ); +} + +#[test] +fn static_lam_rejects_a_variable_an_assumption_mentions() { + let mut f = Fixture::new(); + // ⊃⁺[p](slam (p: bool). let (t) = mk() in t): generalizing `p` would + // claim the assumption `p` for every `p` + let p = f.static_var(boolean(), "p"); + let prop = f.st(StaticTerm::Free(p)); + let t = f.var("t"); + let use_t = f.use_var(t); + let body = f.let_mk(t, use_t); + let slam = f.dt(DynTerm::StaticLam(p, body)); + let guarded = f.dt(DynTerm::GuardIntro(prop, slam)); + assert_eq!( + f.check(guarded), + Err(TypeError::StaticRebound { + term: slam, + var: p, + shown: "p".into() + }) + ); +} + +#[test] +fn pack_checks_its_body_against_the_witnessed_type() { + let mut f = Fixture::new(); + // let (t) = mk() in ⟨token, t⟩ as ∃a. a + let t = f.var("t"); + let (use_t, token, a) = (f.use_var(t), f.token(), f.st(StaticTerm::Bound(0))); + let pack = f.dt(DynTerm::Pack(token, a, use_t)); + let term = f.let_mk(t, pack); + assert_eq!(f.type_of(term), "∃a0: type. a0"); + + // let (u) = mk() in ⟨token * token, u⟩ as ∃a. a + let u = f.var("u"); + let use_u = f.use_var(u); + let pair = f.st(StaticTerm::Product(vec![token, token])); + let wrong = f.dt(DynTerm::Pack(pair, a, use_u)); + let term = f.let_mk(u, wrong); + assert_eq!( + f.check(term), + Err(TypeError::TypeMismatch { + term: use_u, + expected: "(token * token)".into(), + found: "token".into() + }) + ); +} + +/// `let (t) = mk() in let ⟨a, y⟩ = (⟨token, t⟩ as ∃a. a) in body`, with `a` +/// of sort `sort`. Returns the term and the variables `t` and `y`, which +/// `body` may use; `body` is built from them by `make_body`. +fn unpack( + f: &mut Fixture, + sort: TestSort, + make_body: impl FnOnce(&mut Fixture, DynVarId, DynVarId) -> DynTermId, +) -> DynTermId { + let (t, y) = (f.var("t"), f.var("y")); + let (use_t, token, bound) = (f.use_var(t), f.token(), f.st(StaticTerm::Bound(0))); + let pack = f.dt(DynTerm::Pack(token, bound, use_t)); + let a = f.static_var(sort, "a"); + let body = make_body(f, t, y); + let unpack = f.dt(DynTerm::Unpack(a, y, pack, body)); + f.let_mk(t, unpack) +} + +#[test] +fn unpack_opens_the_existential_with_its_variable() { + let mut f = Fixture::new(); + // the body returns `t`, whose type does not mention `a` + let term = unpack(&mut f, ty(), |f, t, _| f.use_var(t)); + assert_eq!(f.type_of(term), "token"); +} + +#[test] +fn unpack_rejects_a_body_type_mentioning_its_variable() { + let mut f = Fixture::new(); + // the body returns `y : a`, so `a` would escape its scope + let term = unpack(&mut f, ty(), |f, _, y| f.use_var(y)); + let TypeError::Escape { shown, .. } = f.check(term).unwrap_err() else { + panic!("expected an escape error"); + }; + // the variable is shown by its name + assert_eq!(shown, "a"); +} + +#[test] +fn unpack_binder_must_have_the_existential_sort() { + let mut f = Fixture::new(); + let term = unpack(&mut f, int(), |f, t, _| f.use_var(t)); + let TypeError::BinderSort { + expected, found, .. + } = f.check(term).unwrap_err() + else { + panic!("expected a binder sort error"); + }; + assert_eq!((expected, found), (ty(), int())); +} + +#[test] +fn unpack_rejects_a_variable_the_scope_mentions() { + let mut f = Fixture::new(); + // lam (k: (a) → token). let (t) = mk() in + // let ⟨a, x⟩ = (⟨token, t⟩ as ∃a. a) in app(k, [x]) + // `x` has the hidden witness type, not the `a` that `k` takes + let a = f.static_var(ty(), "a"); + let (free_a, token, bound) = ( + f.st(StaticTerm::Free(a)), + f.token(), + f.st(StaticTerm::Bound(0)), + ); + let k_type = f.st(StaticTerm::Function(vec![free_a], token)); + let (k, t, x) = (f.var("k"), f.var("t"), f.var("x")); + let (use_k, use_t, use_x) = (f.use_var(k), f.use_var(t), f.use_var(x)); + let pack = f.dt(DynTerm::Pack(token, bound, use_t)); + let app = f.dt(DynTerm::App(use_k, vec![use_x])); + let unpack = f.dt(DynTerm::Unpack(a, x, pack, app)); + let body = f.let_mk(t, unpack); + let lam = f.dt(DynTerm::Lam(vec![(k, k_type)], body)); + assert_eq!( + f.check(lam), + Err(TypeError::StaticRebound { + term: unpack, + var: a, + shown: "a".into() + }) + ); +} + +/// `int(n)`, the singleton type of the integer term `n`. +fn int_of(f: &mut Fixture, n: StaticTermId) -> StaticTermId { + f.st(StaticTerm::Constructor( + TestCon::Int(IntStaticCon::IntOf), + vec![n], + )) +} + +/// `lam (y: int(given)). app(lam (x: int(expected)). x, [y])`: passes a +/// value of type `int(given)` where `int(expected)` is expected. +fn pass_int(f: &mut Fixture, given: StaticTermId, expected: StaticTermId) -> DynTermId { + let (given_ty, expected_ty) = (int_of(f, given), int_of(f, expected)); + let (x, y) = (f.var("x"), f.var("y")); + let use_x = f.use_var(x); + let identity = f.dt(DynTerm::Lam(vec![(x, expected_ty)], use_x)); + let use_y = f.use_var(y); + let app = f.dt(DynTerm::App(identity, vec![use_y])); + f.dt(DynTerm::Lam(vec![(y, given_ty)], app)) +} + +#[test] +fn types_are_compared_after_folding_constants() { + let mut f = Fixture::new(); + let lit = |f: &mut Fixture, n| f.st(StaticTerm::Lit(SortValue::Index(IntSortT(n)))); + let (one, two, three) = (lit(&mut f, 1), lit(&mut f, 2), lit(&mut f, 3)); + let sum = f.st(StaticTerm::Constructor( + TestCon::Int(IntStaticCon::Add), + vec![one, two], + )); + + // int(3) where int(+(1, 2)) is expected + let term = pass_int(&mut f, three, sum); + assert!(f.check(term).is_ok()); + + // int(3) where int(+(1, 1)) is expected + let small = f.st(StaticTerm::Constructor( + TestCon::Int(IntStaticCon::Add), + vec![one, one], + )); + let term = pass_int(&mut f, three, small); + assert!(matches!(f.check(term), Err(TypeError::TypeMismatch { .. }))); +}