logicaffeine_kernel/dag/
mod.rs

1//! The kernel core: a type theory over a hash-consed expression DAG, in two modes
2//! ([`tc::Theory`]): Lean 4's theory exactly, and LOGOS's Calculus of Inductive Constructions.
3//!
4//! This is the representation the kernel needs to be as fast as the fastest Lean kernels:
5//! de Bruijn indices, one id per structurally distinct term, loose-bound-variable ranges and
6//! free-variable flags cached per node, and every cache keyed on ids. In Lean's theory it checks
7//! `lean4export` streams directly ([`export::check_export`]). In LOGOS's it checks the declarations
8//! of a [`Context`](crate::Context) ([`logos_env::replay`], [`logos_env::admit`]) with LOGOS's own
9//! rules ([`logos_tc`]); LOGOS's proof surfaces are still decided by the [`Term`](crate::Term)
10//! kernel and [`recheck`](mod@crate::recheck), against which the core's verdicts are locked.
11//!
12//! Layout: [`name`], [`level`] and [`expr`] are the interned stores; [`env`](mod@env) the admitted
13//! declarations; [`tc`] inference, reduction and definitional equality by substitution, and
14//! [`sem`] the same judgment by evaluation into closures (Lean's theory); [`check`], [`inductive`]
15//! and [`primitive`] the admission rules; [`json`] and [`export`] the streaming reader; [`logos`]
16//! the lowering of LOGOS terms into the store, [`logos_tc`] LOGOS's rules and [`logos_env`] its
17//! declarations; [`mirror`] keeps a core in step with a context through the context's admission
18//! log.
19
20pub mod check;
21pub mod env;
22pub mod error;
23pub mod export;
24pub mod expr;
25pub mod inductive;
26pub mod json;
27pub mod level;
28pub mod logos;
29pub mod logos_env;
30pub(crate) mod logos_obs;
31pub mod logos_tc;
32pub mod mirror;
33pub mod name;
34pub mod nat;
35/// The closure-based conversion engine, compiled only with the `nbe` feature while it is built.
36#[cfg(feature = "nbe")]
37pub mod nbe;
38pub mod pretty;
39pub mod primitive;
40pub mod primitive_wf;
41pub mod relevance;
42pub mod sem;
43pub mod tc;
44pub mod wellknown;
45
46pub use error::{FailKind, KResult, KernelFailure};
47pub use export::{
48    check_export, check_export_in, check_export_observed, check_export_sized, check_export_with,
49    Verdict,
50};
51pub use tc::Kernel;
logicaffeine_kernel/dag/mod.rs

logicaffeine_kernel/dag/
mod.rs
