oxilean_kernel/env_index/mod.rs
1//! Indexed environment for fast declaration lookup.
2//!
3//! Maintains bidirectional Name ↔ compact u32 id mapping ([`NameIndex`]) and
4//! multi-dimensional secondary indices over declaration attributes
5//! ([`TypeIndex`] for sort level / Pi arity; [`ModuleIndex`] for namespace
6//! prefix). The composite [`EnvIndex`] provides a single entry-point for all
7//! indexed operations.
8//!
9//! # Design
10//!
11//! - **O(1) name→id and id→name** via dual `HashMap`/`Vec` in [`NameIndex`].
12//! - **Namespace grouping** via [`ModuleIndex`] using the dot-prefix of each
13//! qualified name (`"Nat.add"` → namespace `"Nat"`).
14//! - **Type attribute indexing** via [`TypeIndex`] keyed by sort level (`u8`)
15//! or Pi arity (`u32`).
16//! - **Append-only**: ids are assigned monotonically and never recycled; the
17//! index never shrinks.
18//!
19//! # Example
20//!
21//! ```
22//! use oxilean_kernel::env_index::{EnvIndex, is_in_namespace};
23//!
24//! let mut idx = EnvIndex::new();
25//! let id = idx.insert("Nat.add");
26//! let result = idx.lookup("Nat.add").unwrap();
27//! assert_eq!(result.id, id);
28//! assert_eq!(result.name, "Nat.add");
29//!
30//! assert!(is_in_namespace("Nat.add", "Nat"));
31//! assert!(!is_in_namespace("List.map", "Nat"));
32//! ```
33
34pub mod functions;
35pub mod types;
36
37pub use functions::{is_in_namespace, namespace_of};
38pub use types::{EnvIndex, IndexStats, LookupResult, ModuleIndex, NameIndex, TypeIndex};