logicaffeine_kernel/lib.rs
1#![cfg_attr(docsrs, feature(doc_cfg))]
2
3//! The Kernel: Calculus of Constructions
4//!
5//! A unified type system where terms and types are the same syntactic category,
6//! based on the Calculus of Inductive Constructions (CIC).
7//!
8//! # Core Insight
9//!
10//! Everything is a [`Term`]:
11//! - Types are Terms: `Nat : Type 0`
12//! - Values are Terms: `zero : Nat`
13//! - Functions are Terms: `λx:Nat. x`
14//! - Proofs are Terms: `refl : a = a`
15//!
16//! # Architecture
17//!
18//! ```text
19//! ┌─────────────────────────────────────────────────────────────┐
20//! │ Interface │
21//! │ (term_parser, literate_parser, command) │
22//! └─────────────────────────────────────────────────────────────┘
23//! │
24//! ▼
25//! ┌─────────────────────────────────────────────────────────────┐
26//! │ Type Checker │
27//! │ infer_type, is_subtype, substitute │
28//! └─────────────────────────────────────────────────────────────┘
29//! │
30//! ┌──────────────┴──────────────┐
31//! ▼ ▼
32//! ┌─────────────────────────┐ ┌─────────────────────────────┐
33//! │ Reduction │ │ Prelude │
34//! │ normalize, reduce │ │ standard library types │
35//! └─────────────────────────┘ └─────────────────────────────┘
36//! │
37//! ┌─────────────┬───────────────┼───────────────┐
38//! ▼ ▼ ▼ ▼
39//! ┌───────────────┐ ┌───────────────┐ ┌───────────────┐ ┌───────────┐
40//! │ ring │ │ lia │ │ cc │ │ omega │
41//! │ polynomial │ │ linear │ │ congruence │ │ integer │
42//! │ equality │ │ arithmetic │ │ closure │ │ arithmetic│
43//! └───────────────┘ └───────────────┘ └───────────────┘ └───────────┘
44//! ```
45//!
46//! # Public API
47//!
48//! ## Core Types
49//! - [`Term`] - The unified representation of terms, types, and proofs
50//! - [`Context`] - Typing context with local and global bindings
51//! - [`KernelError`] - Error types for type checking failures
52//!
53//! ## Type Checking
54//! - [`infer_type`] - Infer the type of a term
55//! - [`is_subtype`] - Check subtyping with cumulativity
56//! - [`normalize`] - Reduce a term to normal form
57//!
58//! ## Decision Procedures
59//! - [`ring`] - Polynomial equality by normalization
60//! - [`lia`] - Linear arithmetic by Fourier-Motzkin
61//! - [`cc`] - Congruence closure for uninterpreted functions
62//! - [`omega`] - Integer arithmetic with exact semantics
63//! - [`simp`] - General simplification with rewriting
64//!
65//! # Milner Invariant
66//!
67//! This crate has NO path to the lexicon. Adding words to the English
68//! vocabulary never triggers a recompile of the type checker. The kernel
69//! is purely logical and language-agnostic.
70
71mod context;
72mod error;
73pub mod interface;
74pub mod positivity;
75pub mod prelude;
76mod reduction;
77pub mod ring;
78pub mod lia;
79pub mod cc;
80pub mod simp;
81pub mod omega;
82pub mod termination;
83mod term;
84mod type_checker;
85
86pub use context::Context;
87pub use error::{KernelError, KernelResult};
88pub use reduction::normalize;
89pub use term::{Literal, Term, Universe};
90pub use type_checker::{infer_type, is_subtype};