oxilean_kernel/env_index/
types.rs

1//! Types for the indexed environment layer.
2//!
3//! Provides bidirectional Name ↔ compact u32 id mapping and multi-dimensional
4//! indices over declaration attributes (sort level, Pi arity, namespace prefix)
5//! for sub-linear declaration lookup in large kernel environments.
6
7use std::collections::HashMap;
8
9// ---------------------------------------------------------------------------
10// NameIndex
11// ---------------------------------------------------------------------------
12
13/// Bidirectional mapping between declaration names and compact `u32` identifiers.
14///
15/// Assigning a dense integer id to each name enables O(1) lookup by id and
16/// compact storage in downstream indices.
17#[derive(Clone, Debug)]
18pub struct NameIndex {
19    /// Maps the string form of a name to its assigned id.
20    pub(super) name_to_id: HashMap<String, u32>,
21    /// Maps an id back to the string form of the name.
22    pub(super) id_to_name: Vec<String>,
23}
24
25// ---------------------------------------------------------------------------
26// TypeIndex
27// ---------------------------------------------------------------------------
28
29/// Index over declaration type attributes: sort level and Pi-type arity.
30///
31/// Enables efficient retrieval of all declarations with a given sort level or
32/// a given number of explicit arguments.
33#[derive(Clone, Debug)]
34pub struct TypeIndex {
35    /// Maps a sort level (universe level byte) to the ids of declarations
36    /// whose outermost type lives at that sort.
37    pub(super) by_sort: HashMap<u8, Vec<u32>>,
38    /// Maps a Pi arity (number of binders before the return type) to the ids
39    /// of declarations with that arity.
40    pub(super) by_arity: HashMap<u32, Vec<u32>>,
41}
42
43// ---------------------------------------------------------------------------
44// ModuleIndex
45// ---------------------------------------------------------------------------
46
47/// Groups declarations by their namespace prefix.
48///
49/// The namespace is the dot-separated prefix of a name: the namespace of
50/// `"Nat.add"` is `"Nat"`, and top-level names (no dot) live in the `""`
51/// (empty) namespace.
52#[derive(Clone, Debug)]
53pub struct ModuleIndex {
54    /// Maps a namespace prefix to the ids of all declarations in that namespace.
55    pub(super) modules: HashMap<String, Vec<u32>>,
56}
57
58// ---------------------------------------------------------------------------
59// EnvIndex
60// ---------------------------------------------------------------------------
61
62/// Composite index combining name, type, and module indices.
63///
64/// Provides a single entry point for all indexed lookups over a kernel
65/// `Environment`.  The index is append-only: names are inserted as
66/// declarations are added, and ids are never recycled.
67#[derive(Clone, Debug)]
68pub struct EnvIndex {
69    /// Bidirectional name ↔ id mapping.
70    pub name_idx: NameIndex,
71    /// Index over sort level and Pi arity.
72    pub type_idx: TypeIndex,
73    /// Index grouping declarations by namespace.
74    pub module_idx: ModuleIndex,
75    /// Total number of indexed declarations (equals `name_idx.len()`).
76    pub size: usize,
77}
78
79// ---------------------------------------------------------------------------
80// IndexStats
81// ---------------------------------------------------------------------------
82
83/// A snapshot of index statistics.
84#[derive(Clone, Debug)]
85pub struct IndexStats {
86    /// Total number of indexed declarations.
87    pub total: usize,
88    /// Declaration counts grouped by a logical kind tag (currently unused by
89    /// the index itself; callers populate this from external data).
90    pub by_kind: HashMap<String, usize>,
91    /// Number of distinct namespace prefixes.
92    pub namespaces: usize,
93}
94
95impl std::fmt::Display for IndexStats {
96    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
97        write!(
98            f,
99            "IndexStats {{ total: {}, namespaces: {} }}",
100            self.total, self.namespaces
101        )
102    }
103}
104
105// ---------------------------------------------------------------------------
106// LookupResult
107// ---------------------------------------------------------------------------
108
109/// The result of a successful indexed lookup.
110///
111/// Borrows the name string from the owning `NameIndex` to avoid allocation.
112#[derive(Clone, Copy, Debug, PartialEq, Eq)]
113pub struct LookupResult<'a> {
114    /// The compact identifier assigned at insertion time.
115    pub id: u32,
116    /// The string form of the matched name.
117    pub name: &'a str,
118}
oxilean_kernel/env_index/types.rs

oxilean_kernel/env_index/
types.rs
