oxilean_kernel/infer/

types.rs

//! Auto-generated module
//!
//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)

use super::proj_target::{proj_target, proj_type_params};
use crate::declaration::{ConstructorVal, InductiveVal};
use crate::def_eq::DefEqChecker;
use crate::error::KernelError;
use crate::expr_util::{get_app_args, get_app_fn, has_any_fvar, has_loose_bvars, mk_app};
use crate::instantiate::instantiate_type_lparams;
use crate::reduce::{Reducer, TransparencyMode};
use crate::subst::{abstract_expr, instantiate};
use crate::Node;
use crate::{BinderInfo, Environment, Expr, FVarId, Level, Literal, Name};
use std::rc::Rc;

use std::collections::HashMap;

/// A simple directed acyclic graph.
#[allow(dead_code)]
pub struct SimpleDag {
    /// `edges[i]` is the list of direct successors of node `i`.
    edges: Vec<Vec<usize>>,
}
#[allow(dead_code)]
impl SimpleDag {
    /// Creates a DAG with `n` nodes and no edges.
    pub fn new(n: usize) -> Self {
        Self {
            edges: vec![Vec::new(); n],
        }
    }
    /// Adds an edge from `from` to `to`.
    pub fn add_edge(&mut self, from: usize, to: usize) {
        if from < self.edges.len() {
            self.edges[from].push(to);
        }
    }
    /// Returns the successors of `node`.
    pub fn successors(&self, node: usize) -> &[usize] {
        self.edges.get(node).map(|v| v.as_slice()).unwrap_or(&[])
    }
    /// Returns `true` if `from` can reach `to` via DFS.
    pub fn can_reach(&self, from: usize, to: usize) -> bool {
        let mut visited = vec![false; self.edges.len()];
        self.dfs(from, to, &mut visited)
    }
    fn dfs(&self, cur: usize, target: usize, visited: &mut Vec<bool>) -> bool {
        if cur == target {
            return true;
        }
        if cur >= visited.len() || visited[cur] {
            return false;
        }
        visited[cur] = true;
        for &next in self.successors(cur) {
            if self.dfs(next, target, visited) {
                return true;
            }
        }
        false
    }
    /// Returns the topological order of nodes, or `None` if a cycle is detected.
    pub fn topological_sort(&self) -> Option<Vec<usize>> {
        let n = self.edges.len();
        let mut in_degree = vec![0usize; n];
        for succs in &self.edges {
            for &s in succs {
                if s < n {
                    in_degree[s] += 1;
                }
            }
        }
        let mut queue: std::collections::VecDeque<usize> =
            (0..n).filter(|&i| in_degree[i] == 0).collect();
        let mut order = Vec::new();
        while let Some(node) = queue.pop_front() {
            order.push(node);
            for &s in self.successors(node) {
                if s < n {
                    in_degree[s] -= 1;
                    if in_degree[s] == 0 {
                        queue.push_back(s);
                    }
                }
            }
        }
        if order.len() == n {
            Some(order)
        } else {
            None
        }
    }
    /// Returns the number of nodes.
    pub fn num_nodes(&self) -> usize {
        self.edges.len()
    }
}
/// A dependency closure builder (transitive closure via BFS).
#[allow(dead_code)]
pub struct TransitiveClosure {
    adj: Vec<Vec<usize>>,
    n: usize,
}
#[allow(dead_code)]
impl TransitiveClosure {
    /// Creates a transitive closure builder for `n` nodes.
    pub fn new(n: usize) -> Self {
        Self {
            adj: vec![Vec::new(); n],
            n,
        }
    }
    /// Adds a direct edge.
    pub fn add_edge(&mut self, from: usize, to: usize) {
        if from < self.n {
            self.adj[from].push(to);
        }
    }
    /// Computes all nodes reachable from `start` (including `start`).
    pub fn reachable_from(&self, start: usize) -> Vec<usize> {
        let mut visited = vec![false; self.n];
        let mut queue = std::collections::VecDeque::new();
        queue.push_back(start);
        while let Some(node) = queue.pop_front() {
            if node >= self.n || visited[node] {
                continue;
            }
            visited[node] = true;
            for &next in &self.adj[node] {
                queue.push_back(next);
            }
        }
        (0..self.n).filter(|&i| visited[i]).collect()
    }
    /// Returns `true` if `from` can transitively reach `to`.
    pub fn can_reach(&self, from: usize, to: usize) -> bool {
        self.reachable_from(from).contains(&to)
    }
}
/// A hierarchical configuration tree.
#[allow(dead_code)]
pub struct ConfigNode {
    key: String,
    value: Option<String>,
    children: Vec<ConfigNode>,
}
#[allow(dead_code)]
impl ConfigNode {
    /// Creates a leaf config node with a value.
    pub fn leaf(key: impl Into<String>, value: impl Into<String>) -> Self {
        Self {
            key: key.into(),
            value: Some(value.into()),
            children: Vec::new(),
        }
    }
    /// Creates a section node with children.
    pub fn section(key: impl Into<String>) -> Self {
        Self {
            key: key.into(),
            value: None,
            children: Vec::new(),
        }
    }
    /// Adds a child node.
    pub fn add_child(&mut self, child: ConfigNode) {
        self.children.push(child);
    }
    /// Returns the key.
    pub fn key(&self) -> &str {
        &self.key
    }
    /// Returns the value, or `None` for section nodes.
    pub fn value(&self) -> Option<&str> {
        self.value.as_deref()
    }
    /// Returns the number of children.
    pub fn num_children(&self) -> usize {
        self.children.len()
    }
    /// Looks up a dot-separated path.
    pub fn lookup(&self, path: &str) -> Option<&str> {
        let mut parts = path.splitn(2, '.');
        let head = parts.next()?;
        let tail = parts.next();
        if head != self.key {
            return None;
        }
        match tail {
            None => self.value.as_deref(),
            Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
        }
    }
    fn lookup_relative(&self, path: &str) -> Option<&str> {
        let mut parts = path.splitn(2, '.');
        let head = parts.next()?;
        let tail = parts.next();
        if head != self.key {
            return None;
        }
        match tail {
            None => self.value.as_deref(),
            Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
        }
    }
}
/// A typing judgment: an expression with its inferred type.
#[allow(dead_code)]
#[derive(Debug, Clone)]
pub struct TypingJudgment {
    /// The expression.
    pub expr: Expr,
    /// The inferred type.
    pub ty: Expr,
    /// Whether the inference was successful.
    pub success: bool,
}
impl TypingJudgment {
    /// Create a successful typing judgment.
    #[allow(dead_code)]
    pub fn ok(expr: Expr, ty: Expr) -> Self {
        Self {
            expr,
            ty,
            success: true,
        }
    }
    /// Create a failed typing judgment (no type available).
    #[allow(dead_code)]
    pub fn fail(expr: Expr) -> Self {
        Self {
            ty: Expr::Sort(Level::zero()),
            expr,
            success: false,
        }
    }
    /// Check if the judgment was successful.
    #[allow(dead_code)]
    pub fn is_ok(&self) -> bool {
        self.success
    }
}
/// A sparse vector: stores only non-default elements.
#[allow(dead_code)]
pub struct SparseVec<T: Default + Clone + PartialEq> {
    entries: std::collections::HashMap<usize, T>,
    default_: T,
    logical_len: usize,
}
#[allow(dead_code)]
impl<T: Default + Clone + PartialEq> SparseVec<T> {
    /// Creates a new sparse vector with logical length `len`.
    pub fn new(len: usize) -> Self {
        Self {
            entries: std::collections::HashMap::new(),
            default_: T::default(),
            logical_len: len,
        }
    }
    /// Sets element at `idx`.
    pub fn set(&mut self, idx: usize, val: T) {
        if val == self.default_ {
            self.entries.remove(&idx);
        } else {
            self.entries.insert(idx, val);
        }
    }
    /// Gets element at `idx`.
    pub fn get(&self, idx: usize) -> &T {
        self.entries.get(&idx).unwrap_or(&self.default_)
    }
    /// Returns the logical length.
    pub fn len(&self) -> usize {
        self.logical_len
    }
    /// Returns whether the collection is empty.
    pub fn is_empty(&self) -> bool {
        self.len() == 0
    }
    /// Returns the number of non-default elements.
    pub fn nnz(&self) -> usize {
        self.entries.len()
    }
}
/// A simple stack-based calculator for arithmetic expressions.
#[allow(dead_code)]
pub struct StackCalc {
    stack: Vec<i64>,
}
#[allow(dead_code)]
impl StackCalc {
    /// Creates a new empty calculator.
    pub fn new() -> Self {
        Self { stack: Vec::new() }
    }
    /// Pushes an integer literal.
    pub fn push(&mut self, n: i64) {
        self.stack.push(n);
    }
    /// Replaces the top two values, `b` on top of `a`, with `op(a, b)` and
    /// returns it.  Returns `None`, leaving the stack unchanged, if it holds
    /// fewer than two values.
    fn apply_binary(&mut self, op: impl FnOnce(i64, i64) -> i64) -> Option<i64> {
        let (rest_len, a, b) = match self.stack[..] {
            [ref rest @ .., a, b] => (rest.len(), a, b),
            _ => return None,
        };
        let value = op(a, b);
        self.stack.truncate(rest_len);
        self.stack.push(value);
        Some(value)
    }
    /// Adds the top two values and returns the sum, which replaces them.
    /// Returns `None`, leaving the stack unchanged, if it holds fewer than
    /// two values.
    pub fn add(&mut self) -> Option<i64> {
        self.apply_binary(|a, b| a + b)
    }
    /// Subtracts top from second and returns the difference, which replaces
    /// them.  Returns `None`, leaving the stack unchanged, if it holds fewer
    /// than two values.
    pub fn sub(&mut self) -> Option<i64> {
        self.apply_binary(|a, b| a - b)
    }
    /// Multiplies the top two values and returns the product, which replaces
    /// them.  Returns `None`, leaving the stack unchanged, if it holds fewer
    /// than two values.
    pub fn mul(&mut self) -> Option<i64> {
        self.apply_binary(|a, b| a * b)
    }
    /// Peeks the top value.
    pub fn peek(&self) -> Option<i64> {
        self.stack.last().copied()
    }
    /// Returns the stack depth.
    pub fn depth(&self) -> usize {
        self.stack.len()
    }
}
/// A window iterator that yields overlapping windows of size `n`.
#[allow(dead_code)]
pub struct WindowIterator<'a, T> {
    pub(super) data: &'a [T],
    pub(super) pos: usize,
    pub(super) window: usize,
}
#[allow(dead_code)]
impl<'a, T> WindowIterator<'a, T> {
    /// Creates a new window iterator.
    pub fn new(data: &'a [T], window: usize) -> Self {
        Self {
            data,
            pos: 0,
            window,
        }
    }
}
/// A cache entry for type inference results.
#[allow(dead_code)]
#[derive(Debug, Clone)]
pub struct InferCacheEntry {
    /// The expression whose type was inferred.
    pub expr: Expr,
    /// The inferred type.
    pub ty: Expr,
}
/// Represents a rewrite rule `lhs → rhs`.
#[allow(dead_code)]
#[allow(missing_docs)]
pub struct RewriteRule {
    /// The name of the rule.
    pub name: String,
    /// A string representation of the LHS pattern.
    pub lhs: String,
    /// A string representation of the RHS.
    pub rhs: String,
    /// Whether this is a conditional rule (has side conditions).
    pub conditional: bool,
}
#[allow(dead_code)]
impl RewriteRule {
    /// Creates an unconditional rewrite rule.
    pub fn unconditional(
        name: impl Into<String>,
        lhs: impl Into<String>,
        rhs: impl Into<String>,
    ) -> Self {
        Self {
            name: name.into(),
            lhs: lhs.into(),
            rhs: rhs.into(),
            conditional: false,
        }
    }
    /// Creates a conditional rewrite rule.
    pub fn conditional(
        name: impl Into<String>,
        lhs: impl Into<String>,
        rhs: impl Into<String>,
    ) -> Self {
        Self {
            name: name.into(),
            lhs: lhs.into(),
            rhs: rhs.into(),
            conditional: true,
        }
    }
    /// Returns a textual representation.
    pub fn display(&self) -> String {
        format!("{}: {} → {}", self.name, self.lhs, self.rhs)
    }
}
/// A set of rewrite rules.
#[allow(dead_code)]
pub struct RewriteRuleSet {
    rules: Vec<RewriteRule>,
}
#[allow(dead_code)]
impl RewriteRuleSet {
    /// Creates an empty rule set.
    pub fn new() -> Self {
        Self { rules: Vec::new() }
    }
    /// Adds a rule.
    pub fn add(&mut self, rule: RewriteRule) {
        self.rules.push(rule);
    }
    /// Returns the number of rules.
    pub fn len(&self) -> usize {
        self.rules.len()
    }
    /// Returns `true` if the set is empty.
    pub fn is_empty(&self) -> bool {
        self.rules.is_empty()
    }
    /// Returns all conditional rules.
    pub fn conditional_rules(&self) -> Vec<&RewriteRule> {
        self.rules.iter().filter(|r| r.conditional).collect()
    }
    /// Returns all unconditional rules.
    pub fn unconditional_rules(&self) -> Vec<&RewriteRule> {
        self.rules.iter().filter(|r| !r.conditional).collect()
    }
    /// Looks up a rule by name.
    pub fn get(&self, name: &str) -> Option<&RewriteRule> {
        self.rules.iter().find(|r| r.name == name)
    }
}
/// A counter that can measure elapsed time between snapshots.
#[allow(dead_code)]
pub struct Stopwatch {
    start: crate::wall_clock::Instant,
    splits: Vec<f64>,
}
#[allow(dead_code)]
impl Stopwatch {
    /// Creates and starts a new stopwatch.
    pub fn start() -> Self {
        Self {
            start: crate::wall_clock::Instant::now(),
            splits: Vec::new(),
        }
    }
    /// Records a split time (elapsed since start).
    pub fn split(&mut self) {
        self.splits.push(self.elapsed_ms());
    }
    /// Returns total elapsed milliseconds since start.
    pub fn elapsed_ms(&self) -> f64 {
        self.start.elapsed().as_secs_f64() * 1000.0
    }
    /// Returns all recorded split times.
    pub fn splits(&self) -> &[f64] {
        &self.splits
    }
    /// Returns the number of splits.
    pub fn num_splits(&self) -> usize {
        self.splits.len()
    }
}
/// Statistics collected during type inference.
#[derive(Clone, Debug, Default)]
pub struct InferStats {
    /// Number of types inferred.
    pub infer_calls: usize,
    /// Number of WHNF reductions performed.
    pub whnf_calls: usize,
    /// Number of definitional equality checks.
    pub def_eq_calls: usize,
    /// Number of constant lookups.
    pub const_lookups: usize,
    /// Number of cache hits.
    pub cache_hits: usize,
}
impl InferStats {
    /// Reset all counters to zero.
    pub fn reset(&mut self) {
        *self = InferStats::default();
    }
    /// Total operations performed.
    pub fn total_ops(&self) -> usize {
        self.infer_calls + self.whnf_calls + self.def_eq_calls
    }
}
/// A mutable reference stack for tracking the current "focus" in a tree traversal.
#[allow(dead_code)]
pub struct FocusStack<T> {
    items: Vec<T>,
}
#[allow(dead_code)]
impl<T> FocusStack<T> {
    /// Creates an empty focus stack.
    pub fn new() -> Self {
        Self { items: Vec::new() }
    }
    /// Focuses on `item`.
    pub fn focus(&mut self, item: T) {
        self.items.push(item);
    }
    /// Blurs (pops) the current focus.
    pub fn blur(&mut self) -> Option<T> {
        self.items.pop()
    }
    /// Returns the current focus, or `None`.
    pub fn current(&self) -> Option<&T> {
        self.items.last()
    }
    /// Returns the focus depth.
    pub fn depth(&self) -> usize {
        self.items.len()
    }
    /// Returns `true` if there is no current focus.
    pub fn is_empty(&self) -> bool {
        self.items.is_empty()
    }
}
/// A non-empty list (at least one element guaranteed).
#[allow(dead_code)]
pub struct NonEmptyVec<T> {
    head: T,
    tail: Vec<T>,
}
#[allow(dead_code)]
impl<T> NonEmptyVec<T> {
    /// Creates a non-empty vec with a single element.
    pub fn singleton(val: T) -> Self {
        Self {
            head: val,
            tail: Vec::new(),
        }
    }
    /// Pushes an element.
    pub fn push(&mut self, val: T) {
        self.tail.push(val);
    }
    /// Returns a reference to the first element.
    pub fn first(&self) -> &T {
        &self.head
    }
    /// Returns a reference to the last element.
    pub fn last(&self) -> &T {
        self.tail.last().unwrap_or(&self.head)
    }
    /// Returns the number of elements.
    pub fn len(&self) -> usize {
        1 + self.tail.len()
    }
    /// Returns whether the collection is empty.
    pub fn is_empty(&self) -> bool {
        self.len() == 0
    }
    /// Returns all elements as a Vec.
    pub fn to_vec(&self) -> Vec<&T> {
        let mut v = vec![&self.head];
        v.extend(self.tail.iter());
        v
    }
}
/// A pair of `StatSummary` values tracking before/after a transformation.
#[allow(dead_code)]
pub struct TransformStat {
    before: StatSummary,
    after: StatSummary,
}
#[allow(dead_code)]
impl TransformStat {
    /// Creates a new transform stat recorder.
    pub fn new() -> Self {
        Self {
            before: StatSummary::new(),
            after: StatSummary::new(),
        }
    }
    /// Records a before value.
    pub fn record_before(&mut self, v: f64) {
        self.before.record(v);
    }
    /// Records an after value.
    pub fn record_after(&mut self, v: f64) {
        self.after.record(v);
    }
    /// Returns the mean reduction ratio (after/before).
    pub fn mean_ratio(&self) -> Option<f64> {
        let b = self.before.mean()?;
        let a = self.after.mean()?;
        if b.abs() < f64::EPSILON {
            return None;
        }
        Some(a / b)
    }
}
/// A token bucket rate limiter.
#[allow(dead_code)]
pub struct TokenBucket {
    capacity: u64,
    tokens: u64,
    refill_per_ms: u64,
    last_refill: crate::wall_clock::Instant,
}
#[allow(dead_code)]
impl TokenBucket {
    /// Creates a new token bucket.
    pub fn new(capacity: u64, refill_per_ms: u64) -> Self {
        Self {
            capacity,
            tokens: capacity,
            refill_per_ms,
            last_refill: crate::wall_clock::Instant::now(),
        }
    }
    /// Attempts to consume `n` tokens.  Returns `true` on success.
    pub fn try_consume(&mut self, n: u64) -> bool {
        self.refill();
        if self.tokens >= n {
            self.tokens -= n;
            true
        } else {
            false
        }
    }
    fn refill(&mut self) {
        let now = crate::wall_clock::Instant::now();
        let elapsed_ms = now.duration_since(self.last_refill).as_millis() as u64;
        if elapsed_ms > 0 {
            let new_tokens = elapsed_ms * self.refill_per_ms;
            self.tokens = (self.tokens + new_tokens).min(self.capacity);
            self.last_refill = now;
        }
    }
    /// Returns the number of currently available tokens.
    pub fn available(&self) -> u64 {
        self.tokens
    }
    /// Returns the bucket capacity.
    pub fn capacity(&self) -> u64 {
        self.capacity
    }
}
/// A flat list of substitution pairs `(from, to)`.
#[allow(dead_code)]
pub struct FlatSubstitution {
    pairs: Vec<(String, String)>,
}
#[allow(dead_code)]
impl FlatSubstitution {
    /// Creates an empty substitution.
    pub fn new() -> Self {
        Self { pairs: Vec::new() }
    }
    /// Adds a pair.
    pub fn add(&mut self, from: impl Into<String>, to: impl Into<String>) {
        self.pairs.push((from.into(), to.into()));
    }
    /// Applies all substitutions to `s` (leftmost-first order).
    pub fn apply(&self, s: &str) -> String {
        let mut result = s.to_string();
        for (from, to) in &self.pairs {
            result = result.replace(from.as_str(), to.as_str());
        }
        result
    }
    /// Returns the number of pairs.
    pub fn len(&self) -> usize {
        self.pairs.len()
    }
    /// Returns `true` if empty.
    pub fn is_empty(&self) -> bool {
        self.pairs.is_empty()
    }
}
/// Type-level kind classification of an expression.
#[allow(dead_code)]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum TypeKind {
    /// A proposition (Sort 0 / Prop).
    Prop,
    /// A small type (Sort 1, i.e., Type 0).
    Type0,
    /// A large type (Sort n for n ≥ 2).
    LargeType,
    /// A universe Sort expression itself.
    Universe,
    /// A function type (Pi).
    Pi,
    /// A lambda (not a type).
    Lambda,
    /// An application (not directly a type).
    Application,
    /// A free variable.
    FreeVar,
    /// A constant.
    Constant,
    /// A literal value.
    Literal,
    /// Unknown or uncategorized.
    Unknown,
}
/// A write-once cell.
#[allow(dead_code)]
pub struct WriteOnce<T> {
    value: std::cell::Cell<Option<T>>,
}
#[allow(dead_code)]
impl<T: Copy> WriteOnce<T> {
    /// Creates an empty write-once cell.
    pub fn new() -> Self {
        Self {
            value: std::cell::Cell::new(None),
        }
    }
    /// Writes a value.  Returns `false` if already written.
    pub fn write(&self, val: T) -> bool {
        if self.value.get().is_some() {
            return false;
        }
        self.value.set(Some(val));
        true
    }
    /// Returns the value if written.
    pub fn read(&self) -> Option<T> {
        self.value.get()
    }
    /// Returns `true` if the value has been written.
    pub fn is_written(&self) -> bool {
        self.value.get().is_some()
    }
}
/// Unified type checker state.
///
/// Owns WHNF reduction, definitional equality checking, and type inference.
/// Mirrors LEAN 4's `type_checker` class.
pub struct TypeChecker<'env> {
    env: &'env Environment,
    local_ctx: Vec<LocalDecl>,
    reducer: Reducer,
    def_eq_checker: DefEqChecker<'env>,
    next_fvar: u64,
    /// Whether to perform full checking (vs. infer-only mode).
    check_mode: bool,
    /// The types [`Self::infer_type`] has computed, by term — Lean's
    /// `m_infer_type`. See [`Self::infer_type`] for what makes an entry
    /// valid and when the table is dropped.
    pub(super) infer_cache: crate::term_cache::TermCache<Expr>,
}
impl<'env> TypeChecker<'env> {
    /// Create a new type checker for the given environment.
    pub fn new(env: &'env Environment) -> Self {
        Self {
            env,
            local_ctx: Vec::new(),
            reducer: Reducer::new(),
            def_eq_checker: DefEqChecker::new(env),
            next_fvar: 0,
            check_mode: true,
            infer_cache: crate::term_cache::TermCache::new(),
        }
    }
    /// Create a type checker in infer-only mode (skips some checks).
    pub fn new_infer_only(env: &'env Environment) -> Self {
        Self {
            env,
            local_ctx: Vec::new(),
            reducer: Reducer::new(),
            def_eq_checker: DefEqChecker::new(env),
            next_fvar: 0,
            check_mode: false,
            infer_cache: crate::term_cache::TermCache::new(),
        }
    }
    /// Create a type checker whose local context is pre-seeded with the
    /// given free-variable types (id → type), e.g. the context a [`Reducer`]
    /// mirrors so K-like iota reduction can type majors that mention local
    /// FVars. Ids are installed in ascending order (later locals may depend
    /// on earlier ones).
    ///
    /// Every free variable the new checker mints is distinct from every
    /// seeded one, in BOTH of its id ranges: the checker's own locals
    /// (`fresh_fvar`, low ids) start past the largest seeded low id, and the
    /// binder-opening variables of its def-eq checker (ids from
    /// `DEF_EQ_OPENED_FVAR_BASE`) start past the largest seeded id of that
    /// range. The seeded locals of the second range are the binders the
    /// surrounding def-eq checker has opened; a def-eq checker that restarted
    /// at the base would open its first binder with the id of the surrounding
    /// checker's first one and identify the two variables (see
    /// `DefEqChecker::reserve_opened_fvars_through`).
    pub fn with_fvar_types(
        env: &'env Environment,
        locals: &std::collections::HashMap<u64, Expr>,
    ) -> Self {
        use crate::def_eq::types::DEF_EQ_OPENED_FVAR_BASE;

        let mut tc = Self::new(env);
        let mut ids: Vec<u64> = locals.keys().copied().collect();
        ids.sort_unstable();
        let mut max_own: Option<u64> = None;
        let mut max_opened: Option<u64> = None;
        for id in ids {
            if let Some(ty) = locals.get(&id) {
                tc.push_local(LocalDecl {
                    fvar: FVarId(id),
                    name: Name::anonymous(),
                    ty: ty.clone(),
                    val: None,
                });
            }
            // `ids` is ascending, so the last id seen in each range is its
            // maximum.
            if id < DEF_EQ_OPENED_FVAR_BASE {
                max_own = Some(id);
            } else {
                max_opened = Some(id);
            }
        }
        tc.next_fvar = max_own.map_or(0, |m| m + 1);
        if let Some(m) = max_opened {
            tc.def_eq_checker.reserve_opened_fvars_through(m);
        }
        tc
    }
    /// Create a type checker seeded with the locals a [`Reducer`] or def-eq
    /// checker mirrors: [`Self::with_fvar_types`] over the variables in
    /// scope, with both id ranges of the new checker also kept clear of every
    /// id the mirror has EVER held.
    ///
    /// The mirror forgets a variable when its binder closes, so the variables
    /// in scope are no longer all the variables the surrounding checker has
    /// used. Minting past the ones in scope only would hand the new checker
    /// the id of a closed binder; minting past the largest id ever bound, in
    /// each range, gives it exactly the ids it was given when the mirror kept
    /// every variable — distinct from all of the surrounding checker's,
    /// whatever terms it is asked about.
    pub(crate) fn with_local_types(
        env: &'env Environment,
        locals: &crate::local_types::LocalTypes,
    ) -> Self {
        let mut tc = Self::with_fvar_types(env, locals.live());
        if let Some(m) = locals.max_own_id() {
            tc.next_fvar = tc.next_fvar.max(m.saturating_add(1));
        }
        if let Some(m) = locals.max_opened_id() {
            tc.def_eq_checker.reserve_opened_fvars_through(m);
        }
        tc
    }
    /// The three mirrors of this checker's local context — its reducer's,
    /// its def-eq checker's and that checker's reducer's — and the id the
    /// next binder the def-eq checker opens will get (for tests).
    #[cfg(test)]
    pub(crate) fn local_mirrors(&self) -> ([&crate::local_types::LocalTypes; 3], u64) {
        let (def_eq, def_eq_reducer, next_opened) = self.def_eq_checker.local_types();
        (
            [self.reducer.local_types(), def_eq, def_eq_reducer],
            next_opened,
        )
    }
    /// Set the transparency mode.
    ///
    /// The types inferred so far are dropped with the reduction and def-eq
    /// caches: in checking mode a cached type also records that the term
    /// CHECKED, and what checks depends on what may be unfolded.
    pub fn set_transparency(&mut self, mode: TransparencyMode) {
        self.reducer.set_transparency(mode);
        self.def_eq_checker.set_transparency(mode);
        self.infer_cache.clear();
    }
    /// Mirror a local declaration's type into the def-eq checker and the
    /// reducer, and drop the inferred types if the binding makes them stale:
    /// the variable was in scope with another type, or was in scope before
    /// and its binder has since been closed (`LocalTypes::bind`). A cached
    /// type may rest on the type the variable had then.
    fn mirror_local(&mut self, fvar: FVarId, ty: &Expr) {
        self.def_eq_checker.record_fvar_type(fvar, ty.clone());
        if self.reducer.bind_fvar_type(fvar, ty.clone()) {
            self.infer_cache.clear();
        }
    }
    /// Get the environment.
    pub fn env(&self) -> &Environment {
        self.env
    }
    /// Generate a fresh free variable.
    pub fn fresh_fvar(&mut self, name: Name, ty: Expr) -> FVarId {
        let fvar = FVarId(self.next_fvar);
        self.next_fvar += 1;
        // Mirror the local context into the def-eq checker (whose
        // type-dependent rules — one-sided eta expansion, structure eta,
        // proof irrelevance — must type this free variable) and into the
        // reducer (whose K-like iota reduction must type recursor majors
        // that mention it).
        self.mirror_local(fvar, &ty);
        self.local_ctx.push(LocalDecl {
            fvar,
            name,
            ty,
            val: None,
        });
        fvar
    }
    /// Generate a fresh free variable with a value (let-binding).
    pub fn fresh_fvar_let(&mut self, name: Name, ty: Expr, val: Expr) -> FVarId {
        let fvar = FVarId(self.next_fvar);
        self.next_fvar += 1;
        self.mirror_local(fvar, &ty);
        self.local_ctx.push(LocalDecl {
            fvar,
            name,
            ty,
            val: Some(val),
        });
        fvar
    }
    /// Push a local declaration onto the context.
    pub fn push_local(&mut self, decl: LocalDecl) {
        self.mirror_local(decl.fvar, &decl.ty);
        self.local_ctx.push(decl);
    }
    /// Pop a local declaration from the context.
    ///
    /// The variable leaves scope, so its type also leaves the mirrors the
    /// def-eq checker and the reducers keep of this context (see the
    /// kernel-private `local_types` module) — unless an earlier declaration of the same
    /// variable is still in the context, in which case the mirrors are left
    /// as they are.
    pub fn pop_local(&mut self) -> Option<LocalDecl> {
        let decl = self.local_ctx.pop()?;
        if !self.local_ctx.iter().any(|other| other.fvar == decl.fvar) {
            self.def_eq_checker.forget_fvar_type(decl.fvar);
            self.reducer.forget_fvar_type(decl.fvar);
        }
        Some(decl)
    }
    /// Look up a free variable in the local context.
    #[allow(clippy::result_large_err)]
    fn lookup_fvar(&self, fvar: FVarId) -> Result<&LocalDecl, KernelError> {
        self.local_ctx
            .iter()
            .find(|decl| decl.fvar == fvar)
            .ok_or_else(|| KernelError::Other(format!("free variable not found: {:?}", fvar)))
    }
    /// Get the local context.
    pub fn local_ctx(&self) -> &[LocalDecl] {
        &self.local_ctx
    }
    /// Reduce an expression to WHNF.
    pub fn whnf(&mut self, expr: &Expr) -> Expr {
        self.reducer.whnf_env(expr, self.env)
    }
    /// Ensure an expression is a Sort, returning the level.
    ///
    /// Infers the type, reduces to WHNF, and checks it's a Sort.
    #[allow(clippy::result_large_err)]
    pub fn ensure_sort(&mut self, expr: &Expr) -> Result<Level, KernelError> {
        let ty = self.infer_type(expr)?;
        let ty_whnf = self.whnf(&ty);
        match ty_whnf {
            Expr::Sort(l) => Ok(l),
            _ => Err(KernelError::NotASort(ty_whnf)),
        }
    }
    /// Ensure an expression's type is a Pi type, returning it.
    #[allow(clippy::result_large_err)]
    pub fn ensure_pi(&mut self, expr: &Expr) -> Result<Expr, KernelError> {
        let ty = self.infer_type(expr)?;
        let ty_whnf = self.whnf(&ty);
        if ty_whnf.is_pi() {
            Ok(ty_whnf)
        } else {
            Err(KernelError::NotAFunction(ty_whnf))
        }
    }
    /// Check if two expressions are definitionally equal.
    pub fn is_def_eq(&mut self, t: &Expr, s: &Expr) -> bool {
        self.def_eq_checker.is_def_eq(t, s)
    }
    /// Check that an expression has the expected type.
    #[allow(clippy::result_large_err)]
    pub fn check_type(
        &mut self,
        expr: &Expr,
        inferred: &Expr,
        expected: &Expr,
    ) -> Result<(), KernelError> {
        if self.is_def_eq(inferred, expected) {
            Ok(())
        } else {
            Err(KernelError::TypeMismatch {
                expected: expected.clone(),
                got: inferred.clone(),
                context: format!("checking {}", expr),
            })
        }
    }
    /// [`Self::infer_type`] for a term that is not in the cache (the
    /// caching entry point is in the `cache` module of this directory).
    #[allow(clippy::result_large_err)]
    pub(super) fn infer_type_uncached(&mut self, expr: &Expr) -> Result<Expr, KernelError> {
        match expr {
            Expr::Sort(l) => Ok(Expr::Sort(Level::succ(l.clone()))),
            Expr::BVar(idx) => Err(KernelError::UnboundVariable(*idx)),
            Expr::FVar(fvar) => {
                let decl = self.lookup_fvar(*fvar)?;
                Ok(decl.ty.clone())
            }
            Expr::Const(name, levels) => self.infer_const(name, levels),
            Expr::App(f, a) => self.infer_app(f, a),
            Expr::Lam(bi, name, ty, body) => {
                if self.check_mode {
                    self.ensure_sort(ty)?;
                }
                let fvar = self.fresh_fvar(name.clone(), (**ty).clone());
                let body_open = instantiate(body, &Expr::FVar(fvar));
                let body_ty = self.infer_type(&body_open)?;
                self.pop_local();
                let body_ty_closed = abstract_expr(&body_ty, fvar);
                Ok(Expr::Pi(
                    *bi,
                    name.clone(),
                    ty.clone(),
                    Node::new(body_ty_closed),
                ))
            }
            Expr::Pi(_, _, dom, cod) => {
                let dom_sort = self.ensure_sort(dom)?;
                let fvar = self.fresh_fvar(Name::str("_"), (**dom).clone());
                let cod_open = instantiate(cod, &Expr::FVar(fvar));
                let cod_sort = self.ensure_sort(&cod_open)?;
                self.pop_local();
                // Build the Pi's sort with the SMART imax constructor, matching
                // Lean's kernel `mk_imax`. This simplifies `imax(u, u) -> u`,
                // `imax(_, 0) -> 0`, `imax(0, v) -> v`, etc. so the re-inferred
                // sort lands in the same canonical shape the elaborator stored in
                // the export; without it, e.g. `Sort u -> Sort u` re-infers to
                // `Sort (imax u u)` and (before the def-eq fix) mass-fails.
                Ok(Expr::Sort(crate::level::mk_imax(dom_sort, cod_sort)))
            }
            Expr::Let(_, ty, val, body) => {
                if self.check_mode {
                    self.ensure_sort(ty)?;
                    let val_ty = self.infer_type(val)?;
                    self.check_type(val, &val_ty, ty)?;
                }
                let body_inst = instantiate(body, val);
                self.infer_type(&body_inst)
            }
            Expr::Lit(Literal::Nat(_)) => Ok(Expr::Const(Name::str("Nat"), vec![])),
            Expr::Lit(Literal::Str(_)) => Ok(Expr::Const(Name::str("String"), vec![])),
            Expr::Proj(struct_name, idx, struct_expr) => {
                self.infer_proj(struct_name, *idx, struct_expr)
            }
        }
    }
    /// Infer the type of a constant reference.
    ///
    /// The provided universe-level list must have EXACTLY the constant's
    /// universe-parameter arity (S7). Lean's kernel requires this; the previous
    /// code returned the uninstantiated type when either list was empty, which
    /// let a polymorphic constant's `Param(u)` leak into a context that declares
    /// its own `u` (a capture / soundness hole). We now instantiate only on an
    /// exact-arity match and hard-error otherwise.
    #[allow(clippy::result_large_err)]
    fn infer_const(&self, name: &Name, levels: &[Level]) -> Result<Expr, KernelError> {
        if let Some(ci) = self.env.find(name) {
            return Self::instantiate_const_type(name, ci.level_params(), ci.ty(), levels);
        }
        let decl = self
            .env
            .get(name)
            .ok_or_else(|| KernelError::UnknownConstant(name.clone()))?;
        Self::instantiate_const_type(name, decl.univ_params(), decl.ty(), levels)
    }
    /// Shared arity check + universe-parameter instantiation for a constant
    /// reference, used by both the `ConstantInfo` and legacy `Declaration`
    /// lookup paths.
    #[allow(clippy::result_large_err)]
    fn instantiate_const_type(
        name: &Name,
        params: &[Name],
        ty: &Expr,
        levels: &[Level],
    ) -> Result<Expr, KernelError> {
        if params.len() != levels.len() {
            return Err(KernelError::Other(format!(
                "universe parameter count mismatch for {}: expected {}, got {}",
                name,
                params.len(),
                levels.len()
            )));
        }
        if params.is_empty() {
            // No universe polymorphism: no substitution needed.
            return Ok(ty.clone());
        }
        Ok(instantiate_type_lparams(ty, params, levels))
    }
    /// Infer the type of a function application.
    #[allow(clippy::result_large_err)]
    fn infer_app(&mut self, f: &Expr, a: &Expr) -> Result<Expr, KernelError> {
        let f_ty = self.infer_type(f)?;
        let f_ty_whnf = self.whnf(&f_ty);
        match &f_ty_whnf {
            Expr::Pi(_, _, dom, cod) => {
                if self.check_mode {
                    let a_ty = self.infer_type(a)?;
                    self.check_type(a, &a_ty, dom)?;
                }
                Ok(instantiate(cod, a))
            }
            _ => Err(KernelError::NotAFunction(f_ty_whnf)),
        }
    }
    /// Infer the type of a projection. Which inductive type it may name —
    /// any with exactly one constructor, recursive and indexed ones
    /// included, as in Lean's `infer_proj` — is decided in `proj_target`.
    #[allow(clippy::result_large_err)]
    fn infer_proj(
        &mut self,
        struct_name: &Name,
        idx: u32,
        struct_expr: &Expr,
    ) -> Result<Expr, KernelError> {
        let (ind_val, ctor_val) = proj_target(self.env, struct_name, idx)?;
        let struct_ty = self.infer_type(struct_expr)?;
        self.infer_proj_field_type(ind_val, ctor_val, idx, struct_expr, &struct_ty)
    }
    /// Compute the type of a projection field.
    ///
    /// Telescopes through the constructor's Pi-type, instantiating:
    /// 1. Universe parameters from the struct type's head constant
    /// 2. Inductive parameters from the struct type's applied arguments
    ///    (the leading ones: the indices that follow are arguments of the
    ///    type, not of the constructor)
    /// 3. Preceding fields with `Proj(S, j, struct_expr)` for `j < idx`
    ///
    /// Returns the domain of the `idx`-th Pi binder. Any mismatch — the
    /// operand's type not being the structure type, an argument-count
    /// mismatch, or the constructor telescope running short — is a typed
    /// error rather than a fabricated type.
    #[allow(clippy::result_large_err)]
    fn infer_proj_field_type(
        &mut self,
        ind_val: &InductiveVal,
        ctor_val: &ConstructorVal,
        idx: u32,
        struct_expr: &Expr,
        struct_ty: &Expr,
    ) -> Result<Expr, KernelError> {
        let ctor_ty = ctor_val.common.ty.clone();
        let struct_ty_whnf = self.whnf(struct_ty);
        let levels: Vec<Level> = match get_app_fn(&struct_ty_whnf) {
            Expr::Const(name, lvls) if *name == ind_val.common.name => lvls.clone(),
            _ => {
                return Err(KernelError::Other(format!(
                    "invalid projection: expected an element of {}, but the operand has type {}",
                    ind_val.common.name, struct_ty_whnf
                )))
            }
        };
        let level_params = &ind_val.common.level_params;
        let mut cur_ty = if level_params.is_empty() || levels.is_empty() {
            ctor_ty
        } else {
            instantiate_type_lparams(&ctor_ty, level_params, &levels)
        };
        let struct_args: Vec<Expr> = get_app_args(&struct_ty_whnf).into_iter().cloned().collect();
        let Some(params) = proj_type_params(ind_val, &struct_args) else {
            return Err(KernelError::Other(format!(
                "invalid projection: {} expects {} parameters and {} indices, \
                 but the operand type {} supplies {} arguments",
                ind_val.common.name,
                ind_val.num_params,
                ind_val.num_indices,
                struct_ty_whnf,
                struct_args.len()
            )));
        };
        for param in params {
            match cur_ty {
                Expr::Pi(_, _, _, body) => {
                    cur_ty = instantiate(&body, param);
                }
                _ => {
                    return Err(KernelError::Other(format!(
                        "invalid projection: constructor {} telescope ended while \
                         instantiating the parameters of {}",
                        ctor_val.common.name, ind_val.common.name
                    )))
                }
            }
        }
        // No data out of a proof (Lean's `infer_proj`; see `proj_prop`): of
        // a proposition, the projected field and every earlier field a
        // later field's type depends on must be propositions themselves.
        // The sort is that of `S ps is`: read past the indices too.
        let struct_is_prop = self.proj_struct_is_prop(ind_val, &levels, &struct_args)?;
        for j in 0..idx {
            match cur_ty {
                Expr::Pi(_, _, dom, body) => {
                    if struct_is_prop && has_loose_bvars(&body) {
                        self.ensure_prop_field(ind_val, j, &dom)?;
                    }
                    let field_val = Expr::Proj(
                        ind_val.common.name.clone(),
                        j,
                        Node::new(struct_expr.clone()),
                    );
                    cur_ty = instantiate(&body, &field_val);
                }
                _ => {
                    return Err(KernelError::Other(format!(
                        "invalid projection: constructor {} telescope ended at field {} \
                         while computing field {} of {}",
                        ctor_val.common.name, j, idx, ind_val.common.name
                    )))
                }
            }
        }
        match cur_ty {
            Expr::Pi(_, _, dom, _) => {
                if struct_is_prop {
                    self.ensure_prop_field(ind_val, idx, &dom)?;
                }
                Ok((*dom).clone())
            }
            _ => Err(KernelError::Other(format!(
                "invalid projection: constructor {} telescope has no field {} for {}",
                ctor_val.common.name, idx, ind_val.common.name
            ))),
        }
    }
    /// Check if an expression is a proposition (has type Prop).
    pub fn is_prop(&mut self, expr: &Expr) -> bool {
        if let Ok(ty) = self.infer_type(expr) {
            let ty_whnf = self.whnf(&ty);
            matches!(ty_whnf, Expr::Sort(l) if l.is_zero())
        } else {
            false
        }
    }
    /// Check if an expression is a proof (its type is a proposition).
    pub fn is_proof(&mut self, expr: &Expr) -> bool {
        if let Ok(ty) = self.infer_type(expr) {
            self.is_prop(&ty)
        } else {
            false
        }
    }
    /// Check if an expression is a type (has type Sort u for some u).
    pub fn is_type(&mut self, expr: &Expr) -> bool {
        if let Ok(ty) = self.infer_type(expr) {
            let ty_whnf = self.whnf(&ty);
            ty_whnf.is_sort()
        } else {
            false
        }
    }
    /// Get the universe level of a type expression.
    #[allow(clippy::result_large_err)]
    pub fn get_level(&mut self, expr: &Expr) -> Result<Level, KernelError> {
        let ty = self.infer_type(expr)?;
        let ty_whnf = self.whnf(&ty);
        match ty_whnf {
            Expr::Sort(l) => Ok(l),
            _ => Err(KernelError::NotASort(ty_whnf)),
        }
    }
    /// Try to unfold a constant definition.
    pub fn unfold_definition(&mut self, expr: &Expr) -> Option<Expr> {
        let head = get_app_fn(expr);
        if let Expr::Const(name, levels) = head {
            if let Some(ci) = self.env.find(name) {
                if let Some(val) = ci.value() {
                    let hint = ci.reducibility_hint();
                    if hint.should_unfold() {
                        let val_inst = if ci.level_params().is_empty() || levels.is_empty() {
                            val.clone()
                        } else {
                            instantiate_type_lparams(val, ci.level_params(), levels)
                        };
                        let args: Vec<Expr> = get_app_args(expr).into_iter().cloned().collect();
                        return Some(mk_app(val_inst, &args));
                    }
                }
            }
        }
        None
    }
}
impl<'env> TypeChecker<'env> {
    /// Infer the type of a chain of applications at once.
    #[allow(clippy::result_large_err)]
    pub fn infer_app_chain(
        &mut self,
        f: &Expr,
        args: &[Expr],
    ) -> Result<Expr, crate::error::KernelError> {
        let mut ty = self.infer_type(f)?;
        for arg in args {
            let whnf = self.whnf(&ty);
            match whnf {
                Expr::Pi(_, _, dom, cod) => {
                    if self.check_mode {
                        let arg_ty = self.infer_type(arg)?;
                        if !self.is_def_eq(&arg_ty, &dom) {
                            return Err(crate::error::KernelError::TypeMismatch {
                                expected: (*dom).clone(),
                                got: arg_ty,
                                context: "application argument".to_string(),
                            });
                        }
                    }
                    ty = instantiate(&cod, arg);
                }
                other => return Err(crate::error::KernelError::NotAFunction(other)),
            }
        }
        Ok(ty)
    }
    /// Telescope a type, instantiating leading Pi binders with fresh free variables.
    pub fn telescope_type(&mut self, ty: &Expr, max_pis: usize) -> (Vec<LocalDecl>, Expr) {
        let mut fvars = Vec::new();
        let mut current = ty.clone();
        for _ in 0..max_pis {
            let whnf = self.whnf(&current);
            match whnf {
                Expr::Pi(bi, name, dom, cod) => {
                    let fvar_id = self.fresh_fvar(name.clone(), (*dom).clone());
                    let decl = LocalDecl {
                        fvar: fvar_id,
                        name,
                        ty: (*dom).clone(),
                        val: None,
                    };
                    let body = instantiate(&cod, &Expr::FVar(fvar_id));
                    fvars.push(decl);
                    current = body;
                    let _ = bi;
                }
                _ => break,
            }
        }
        (fvars, current)
    }
    /// Close a type over a list of free variables into Pi types.
    pub fn close_type_over_fvars(&mut self, fvars: &[LocalDecl], ty: Expr) -> Expr {
        let mut result = ty;
        for decl in fvars.iter().rev() {
            result = abstract_expr(&result, decl.fvar);
            result = Expr::Pi(
                crate::BinderInfo::Default,
                decl.name.clone(),
                Node::new(decl.ty.clone()),
                Node::new(result),
            );
        }
        result
    }
    /// Close a term over free variables into lambdas.
    pub fn close_term_over_fvars(&mut self, fvars: &[LocalDecl], term: Expr) -> Expr {
        let mut result = term;
        for decl in fvars.iter().rev() {
            result = abstract_expr(&result, decl.fvar);
            result = Expr::Lam(
                crate::BinderInfo::Default,
                decl.name.clone(),
                Node::new(decl.ty.clone()),
                Node::new(result),
            );
        }
        result
    }
    /// Check that `expr` has type `expected`.
    #[allow(clippy::result_large_err)]
    pub fn check(&mut self, expr: &Expr, expected: &Expr) -> Result<(), crate::error::KernelError> {
        let inferred = self.infer_type(expr)?;
        if self.is_def_eq(&inferred, expected) {
            Ok(())
        } else {
            Err(crate::error::KernelError::TypeMismatch {
                expected: expected.clone(),
                got: inferred,
                context: format!("check({:?})", expr),
            })
        }
    }
    /// Try to check; return true if the type matches.
    pub fn try_check(&mut self, expr: &Expr, expected: &Expr) -> bool {
        if let Ok(inferred) = self.infer_type(expr) {
            self.is_def_eq(&inferred, expected)
        } else {
            false
        }
    }
    /// Get the number of Pi binders in the WHNF of a type.
    pub fn count_pi_binders(&mut self, ty: &Expr) -> usize {
        let mut count = 0;
        let mut current = ty.clone();
        loop {
            let whnf = self.whnf(&current);
            if let Expr::Pi(_, _, _, cod) = whnf {
                count += 1;
                current = (*cod).clone();
            } else {
                break;
            }
        }
        count
    }
    /// Verify a declaration's type and optional value.
    #[allow(clippy::result_large_err)]
    pub fn verify_declaration(
        &mut self,
        name: &Name,
        ty: &Expr,
        val: Option<&Expr>,
    ) -> Result<(), crate::error::KernelError> {
        self.ensure_sort(ty)?;
        if let Some(v) = val {
            let v_ty = self.infer_type(v)?;
            if !self.is_def_eq(&v_ty, ty) {
                return Err(crate::error::KernelError::TypeMismatch {
                    expected: ty.clone(),
                    got: v_ty,
                    context: format!("verifying declaration {}", name),
                });
            }
        }
        Ok(())
    }
    /// Normalize an expression (full normal form).
    pub fn normalize(&mut self, expr: &Expr) -> Expr {
        let whnf = self.whnf(expr);
        match &whnf {
            Expr::App(f, a) => {
                let f_norm = self.normalize(f);
                let a_norm = self.normalize(a);
                Expr::App(Node::new(f_norm), Node::new(a_norm))
            }
            Expr::Lam(bi, name, ty, body) => {
                let ty_norm = self.normalize(ty);
                let body_norm = self.normalize(body);
                Expr::Lam(*bi, name.clone(), Node::new(ty_norm), Node::new(body_norm))
            }
            Expr::Pi(bi, name, ty, body) => {
                let ty_norm = self.normalize(ty);
                let body_norm = self.normalize(body);
                Expr::Pi(*bi, name.clone(), Node::new(ty_norm), Node::new(body_norm))
            }
            Expr::Let(name, ty, val, body) => {
                let ty_norm = self.normalize(ty);
                let val_norm = self.normalize(val);
                let body_norm = self.normalize(body);
                Expr::Let(
                    name.clone(),
                    Node::new(ty_norm),
                    Node::new(val_norm),
                    Node::new(body_norm),
                )
            }
            Expr::Proj(sname, idx, inner) => {
                let inner_norm = self.normalize(inner);
                Expr::Proj(sname.clone(), *idx, Node::new(inner_norm))
            }
            _ => whnf,
        }
    }
    /// Return the arity (number of Pi binders) in the type of a constant.
    pub fn constant_arity(&mut self, name: &Name) -> Option<usize> {
        let ty = if let Some(ci) = self.env.find(name) {
            ci.ty().clone()
        } else {
            self.env.get(name)?.ty().clone()
        };
        Some(self.count_pi_binders(&ty))
    }
    /// Check if two universe levels are definitionally equal.
    ///
    /// Delegates to the complete `level::is_equivalent` decision procedure
    /// (previously this was an essentially-syntactic stub that only recognised
    /// literally-equal or both-zero levels — a trap for callers expecting real
    /// universe defeq).
    pub fn is_level_eq(&self, l1: &Level, l2: &Level) -> bool {
        crate::level::is_equivalent(l1, l2)
    }
}
/// A simple key-value store backed by a sorted Vec for small maps.
#[allow(dead_code)]
pub struct SmallMap<K: Ord + Clone, V: Clone> {
    entries: Vec<(K, V)>,
}
#[allow(dead_code)]
impl<K: Ord + Clone, V: Clone> SmallMap<K, V> {
    /// Creates a new empty small map.
    pub fn new() -> Self {
        Self {
            entries: Vec::new(),
        }
    }
    /// Inserts or replaces the value for `key`.
    pub fn insert(&mut self, key: K, val: V) {
        match self.entries.binary_search_by_key(&&key, |(k, _)| k) {
            Ok(i) => self.entries[i].1 = val,
            Err(i) => self.entries.insert(i, (key, val)),
        }
    }
    /// Returns the value for `key`, or `None`.
    pub fn get(&self, key: &K) -> Option<&V> {
        self.entries
            .binary_search_by_key(&key, |(k, _)| k)
            .ok()
            .map(|i| &self.entries[i].1)
    }
    /// Returns the number of entries.
    pub fn len(&self) -> usize {
        self.entries.len()
    }
    /// Returns `true` if empty.
    pub fn is_empty(&self) -> bool {
        self.entries.is_empty()
    }
    /// Returns all keys.
    pub fn keys(&self) -> Vec<&K> {
        self.entries.iter().map(|(k, _)| k).collect()
    }
    /// Returns all values.
    pub fn values(&self) -> Vec<&V> {
        self.entries.iter().map(|(_, v)| v).collect()
    }
}
/// A versioned record that stores a history of values.
#[allow(dead_code)]
pub struct VersionedRecord<T: Clone> {
    /// Every earlier value, oldest first: version `n` is `earlier[n]`.
    earlier: Vec<T>,
    /// The latest value (version `earlier.len()`), declared last so it drops last.
    current: T,
}
#[allow(dead_code)]
impl<T: Clone> VersionedRecord<T> {
    /// Creates a new record with an initial value.
    pub fn new(initial: T) -> Self {
        Self {
            earlier: Vec::new(),
            current: initial,
        }
    }
    /// Updates the record with a new version.
    pub fn update(&mut self, val: T) {
        let previous = std::mem::replace(&mut self.current, val);
        self.earlier.push(previous);
    }
    /// Returns the current (latest) value.
    pub fn current(&self) -> &T {
        &self.current
    }
    /// Returns the value at version `n` (0-indexed), or `None`.
    pub fn at_version(&self, n: usize) -> Option<&T> {
        match self.earlier.get(n) {
            Some(value) => Some(value),
            None if n == self.earlier.len() => Some(&self.current),
            None => None,
        }
    }
    /// Returns the version number of the current value.
    pub fn version(&self) -> usize {
        self.earlier.len()
    }
    /// Returns `true` if more than one version exists.
    pub fn has_history(&self) -> bool {
        !self.earlier.is_empty()
    }
}
/// A simple LRU-style type inference cache.
///
/// In practice, this is a bounded list of recent (expr → type) pairs.
#[allow(dead_code)]
pub struct InferCache {
    entries: Vec<InferCacheEntry>,
    capacity: usize,
}
impl InferCache {
    /// Create a new cache with a given capacity.
    #[allow(dead_code)]
    pub fn new(capacity: usize) -> Self {
        Self {
            entries: Vec::with_capacity(capacity),
            capacity,
        }
    }
    /// Look up a cached type for an expression.
    #[allow(dead_code)]
    pub fn get(&self, expr: &Expr) -> Option<&Expr> {
        self.entries
            .iter()
            .rev()
            .find(|e| &e.expr == expr)
            .map(|e| &e.ty)
    }
    /// Insert a new (expr, type) pair.
    #[allow(dead_code)]
    pub fn insert(&mut self, expr: Expr, ty: Expr) {
        if self.entries.len() >= self.capacity {
            self.entries.remove(0);
        }
        self.entries.push(InferCacheEntry { expr, ty });
    }
    /// Clear the cache.
    #[allow(dead_code)]
    pub fn clear(&mut self) {
        self.entries.clear();
    }
    /// Number of cached entries.
    #[allow(dead_code)]
    pub fn len(&self) -> usize {
        self.entries.len()
    }
    /// Whether the cache is empty.
    #[allow(dead_code)]
    pub fn is_empty(&self) -> bool {
        self.entries.is_empty()
    }
}
/// A fixed-size sliding window that computes a running sum.
#[allow(dead_code)]
pub struct SlidingSum {
    window: Vec<f64>,
    capacity: usize,
    pos: usize,
    sum: f64,
    count: usize,
}
#[allow(dead_code)]
impl SlidingSum {
    /// Creates a sliding sum with the given window size.
    pub fn new(capacity: usize) -> Self {
        Self {
            window: vec![0.0; capacity],
            capacity,
            pos: 0,
            sum: 0.0,
            count: 0,
        }
    }
    /// Adds a value to the window, removing the oldest if full.
    pub fn push(&mut self, val: f64) {
        let oldest = self.window[self.pos];
        self.sum -= oldest;
        self.sum += val;
        self.window[self.pos] = val;
        self.pos = (self.pos + 1) % self.capacity;
        if self.count < self.capacity {
            self.count += 1;
        }
    }
    /// Returns the current window sum.
    pub fn sum(&self) -> f64 {
        self.sum
    }
    /// Returns the window mean, or `None` if empty.
    pub fn mean(&self) -> Option<f64> {
        if self.count == 0 {
            None
        } else {
            Some(self.sum / self.count as f64)
        }
    }
    /// Returns the current window size (number of valid elements).
    pub fn count(&self) -> usize {
        self.count
    }
}
/// Local declaration (free variable with type).
#[derive(Clone, Debug)]
pub struct LocalDecl {
    /// Free variable ID
    pub fvar: FVarId,
    /// Name (for pretty-printing)
    pub name: Name,
    /// Type of this variable
    pub ty: Expr,
    /// Optional value (for let-bound variables)
    pub val: Option<Expr>,
}
/// A pool of reusable string buffers.
#[allow(dead_code)]
pub struct StringPool {
    free: Vec<String>,
}
#[allow(dead_code)]
impl StringPool {
    /// Creates a new empty string pool.
    pub fn new() -> Self {
        Self { free: Vec::new() }
    }
    /// Takes a string from the pool (may be empty).
    pub fn take(&mut self) -> String {
        self.free.pop().unwrap_or_default()
    }
    /// Returns a string to the pool.
    pub fn give(&mut self, mut s: String) {
        s.clear();
        self.free.push(s);
    }
    /// Returns the number of free strings in the pool.
    pub fn free_count(&self) -> usize {
        self.free.len()
    }
}
/// A simple decision tree node for rule dispatching.
#[allow(dead_code)]
#[allow(missing_docs)]
pub enum DecisionNode {
    /// A leaf with an action string.
    Leaf(String),
    /// An interior node: check `key` equals `val` → `yes_branch`, else `no_branch`.
    Branch {
        key: String,
        val: String,
        yes_branch: Box<DecisionNode>,
        no_branch: Box<DecisionNode>,
    },
}
#[allow(dead_code)]
impl DecisionNode {
    /// Evaluates the decision tree with the given context.
    pub fn evaluate(&self, ctx: &std::collections::HashMap<String, String>) -> &str {
        match self {
            DecisionNode::Leaf(action) => action.as_str(),
            DecisionNode::Branch {
                key,
                val,
                yes_branch,
                no_branch,
            } => {
                let actual = ctx.get(key).map(|s| s.as_str()).unwrap_or("");
                if actual == val.as_str() {
                    yes_branch.evaluate(ctx)
                } else {
                    no_branch.evaluate(ctx)
                }
            }
        }
    }
    /// Returns the depth of the decision tree.
    pub fn depth(&self) -> usize {
        match self {
            DecisionNode::Leaf(_) => 0,
            DecisionNode::Branch {
                yes_branch,
                no_branch,
                ..
            } => 1 + yes_branch.depth().max(no_branch.depth()),
        }
    }
}
/// A generic counter that tracks min/max/sum for statistical summaries.
#[allow(dead_code)]
pub struct StatSummary {
    count: u64,
    sum: f64,
    min: f64,
    max: f64,
}
#[allow(dead_code)]
impl StatSummary {
    /// Creates an empty summary.
    pub fn new() -> Self {
        Self {
            count: 0,
            sum: 0.0,
            min: f64::INFINITY,
            max: f64::NEG_INFINITY,
        }
    }
    /// Records a sample.
    pub fn record(&mut self, val: f64) {
        self.count += 1;
        self.sum += val;
        if val < self.min {
            self.min = val;
        }
        if val > self.max {
            self.max = val;
        }
    }
    /// Returns the mean, or `None` if no samples.
    pub fn mean(&self) -> Option<f64> {
        if self.count == 0 {
            None
        } else {
            Some(self.sum / self.count as f64)
        }
    }
    /// Returns the minimum, or `None` if no samples.
    pub fn min(&self) -> Option<f64> {
        if self.count == 0 {
            None
        } else {
            Some(self.min)
        }
    }
    /// Returns the maximum, or `None` if no samples.
    pub fn max(&self) -> Option<f64> {
        if self.count == 0 {
            None
        } else {
            Some(self.max)
        }
    }
    /// Returns the count of recorded samples.
    pub fn count(&self) -> u64 {
        self.count
    }
}
/// A label set for a graph node.
#[allow(dead_code)]
pub struct LabelSet {
    labels: Vec<String>,
}
#[allow(dead_code)]
impl LabelSet {
    /// Creates a new empty label set.
    pub fn new() -> Self {
        Self { labels: Vec::new() }
    }
    /// Adds a label (deduplicates).
    pub fn add(&mut self, label: impl Into<String>) {
        let s = label.into();
        if !self.labels.contains(&s) {
            self.labels.push(s);
        }
    }
    /// Returns `true` if `label` is present.
    pub fn has(&self, label: &str) -> bool {
        self.labels.iter().any(|l| l == label)
    }
    /// Returns the count of labels.
    pub fn count(&self) -> usize {
        self.labels.len()
    }
    /// Returns all labels.
    pub fn all(&self) -> &[String] {
        &self.labels
    }
}
/// A reusable scratch buffer for path computations.
#[allow(dead_code)]
pub struct PathBuf {
    components: Vec<String>,
}
#[allow(dead_code)]
impl PathBuf {
    /// Creates a new empty path buffer.
    pub fn new() -> Self {
        Self {
            components: Vec::new(),
        }
    }
    /// Pushes a component.
    pub fn push(&mut self, comp: impl Into<String>) {
        self.components.push(comp.into());
    }
    /// Pops the last component.
    pub fn pop(&mut self) {
        self.components.pop();
    }
    /// Returns the current path as a `/`-separated string.
    pub fn as_str(&self) -> String {
        self.components.join("/")
    }
    /// Returns the depth of the path.
    pub fn depth(&self) -> usize {
        self.components.len()
    }
    /// Clears the path.
    pub fn clear(&mut self) {
        self.components.clear();
    }
}
/// A type-erased function pointer with arity tracking.
#[allow(dead_code)]
pub struct RawFnPtr {
    /// The raw function pointer (stored as usize for type erasure).
    ptr: usize,
    arity: usize,
    name: String,
}
#[allow(dead_code)]
impl RawFnPtr {
    /// Creates a new raw function pointer descriptor.
    pub fn new(ptr: usize, arity: usize, name: impl Into<String>) -> Self {
        Self {
            ptr,
            arity,
            name: name.into(),
        }
    }
    /// Returns the arity.
    pub fn arity(&self) -> usize {
        self.arity
    }
    /// Returns the name.
    pub fn name(&self) -> &str {
        &self.name
    }
    /// Returns the raw pointer value.
    pub fn raw(&self) -> usize {
        self.ptr
    }
}
/// A tagged union for representing a simple two-case discriminated union.
#[allow(dead_code)]
pub enum Either2<A, B> {
    /// The first alternative.
    First(A),
    /// The second alternative.
    Second(B),
}
#[allow(dead_code)]
impl<A, B> Either2<A, B> {
    /// Returns `true` if this is the first alternative.
    pub fn is_first(&self) -> bool {
        matches!(self, Either2::First(_))
    }
    /// Returns `true` if this is the second alternative.
    pub fn is_second(&self) -> bool {
        matches!(self, Either2::Second(_))
    }
    /// Returns the first value if present.
    pub fn first(self) -> Option<A> {
        match self {
            Either2::First(a) => Some(a),
            _ => None,
        }
    }
    /// Returns the second value if present.
    pub fn second(self) -> Option<B> {
        match self {
            Either2::Second(b) => Some(b),
            _ => None,
        }
    }
    /// Maps over the first alternative.
    pub fn map_first<C, F: FnOnce(A) -> C>(self, f: F) -> Either2<C, B> {
        match self {
            Either2::First(a) => Either2::First(f(a)),
            Either2::Second(b) => Either2::Second(b),
        }
    }
}