oxilean_kernel/check/

functions.rs

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

use crate::declaration::{ConstantInfo, ConstructorVal, InductiveVal, QuotVal, RecursorVal};
use crate::env::EnvError;
use crate::Node;
use crate::{Declaration, Environment, KernelError, TypeChecker};
#[cfg(test)]
use crate::{Expr, Name};
use std::rc::Rc;

use super::types::{
    BatchCheckResult, CheckConfig, CheckStats, ConfigNode, DecisionNode, DeclKind, DeclSummary,
    Either2, EnvBuilder, FlatSubstitution, FocusStack, LabelSet, NonEmptyVec, PathBuf, RewriteRule,
    RewriteRuleSet, SimpleDag, SlidingSum, SmallMap, SparseVec, StackCalc, StatSummary, Stopwatch,
    StringPool, TempEnvScope, TokenBucket, TransformStat, TransitiveClosure, VersionedRecord,
    WellFormedResult, WindowIterator, WriteOnce,
};

/// Check a declaration and add it to the environment.
///
/// Validates that the declaration is well-formed and type-correct, then
/// inserts it into the environment. Returns an error if the declaration
/// fails type checking or if the name is already declared.
#[allow(clippy::result_large_err)]
pub fn check_declaration(env: &mut Environment, decl: Declaration) -> Result<(), KernelError> {
    let name = decl.name().clone();
    // Universe-parameter hygiene (S8): reject duplicate univ params, undeclared
    // `Param`s appearing in the type/value, and any `Level` metavariable — all
    // of which Lean's kernel rejects and any of which a hostile/malformed export
    // could otherwise smuggle through.
    check_univ_param_hygiene(&decl)?;
    match &decl {
        Declaration::Axiom { ty, .. } => {
            let mut tc = TypeChecker::new(env);
            tc.ensure_sort(ty)?;
        }
        Declaration::Definition { ty, val, .. } => {
            let mut tc = TypeChecker::new(env);
            tc.ensure_sort(ty)?;
            let val_ty = tc.infer_type(val)?;
            tc.check_type(val, &val_ty, ty)?;
        }
        Declaration::Theorem { ty, val, .. } => {
            let mut tc = TypeChecker::new(env);
            check_theorem_type(&mut tc, &name, ty)?;
            let val_ty = tc.infer_type(val)?;
            tc.check_type(val, &val_ty, ty)?;
        }
        Declaration::Opaque { ty, val, .. } => {
            let mut tc = TypeChecker::new(env);
            tc.ensure_sort(ty)?;
            let val_ty = tc.infer_type(val)?;
            tc.check_type(val, &val_ty, ty)?;
        }
    }
    env.add(decl).map_err(|e| match e {
        EnvError::DuplicateDeclaration(_) => {
            KernelError::Other(format!("duplicate declaration: {}", name))
        }
        EnvError::NotFound(_) => KernelError::Other(format!("declaration not found: {}", name)),
        EnvError::InvalidQuotient(msg) => KernelError::Other(msg),
    })
}
/// A theorem states a proposition: its declared type must be a type, and
/// the sort of that type must be `Prop`.
///
/// Lean's kernel refuses a theorem whose type is not a proposition
/// (`theorem t : Nat := 5`, `theorem t : Type := Nat`: "type of theorem 't'
/// is not a proposition"), and so does this one. The sort is the one the
/// type's own type reduces to, and it is compared with `Sort 0` up to the
/// equivalence of universe levels: a type in `Sort (imax u 0)` is a
/// proposition for every `u`.
#[allow(clippy::result_large_err)]
fn check_theorem_type(
    tc: &mut TypeChecker<'_>,
    name: &crate::Name,
    ty: &crate::Expr,
) -> Result<(), KernelError> {
    let sort = tc.ensure_sort(ty)?;
    if !crate::level::is_equivalent(&sort, &crate::Level::zero()) {
        return Err(KernelError::Other(format!(
            "type of theorem '{name}' is not a proposition: it is a type in Sort {sort}, not in \
             Prop"
        )));
    }
    Ok(())
}
/// Enforce universe-parameter hygiene for a declaration (S8).
///
/// Three checks, all of which Lean's kernel performs and none of which the
/// pre-Wave-2 checker did:
///
/// 1. **No duplicate universe parameters** in the declaration's `univ_params`.
/// 2. **Every `Level::Param` occurring in the type or value is declared** in
///    `univ_params` (an undeclared param is a free universe variable and must
///    be rejected, else a hostile export can capture it).
/// 3. **No `Level::MVar` anywhere** in the type or value — a kernel-checked
///    declaration must be metavariable-free.
#[allow(clippy::result_large_err)]
pub(super) fn check_univ_param_hygiene(decl: &Declaration) -> Result<(), KernelError> {
    check_univ_param_hygiene_parts(
        decl.name(),
        decl.univ_params(),
        std::iter::once(decl.ty()).chain(decl.value()),
    )
}
/// Enforce universe-parameter hygiene for a `ConstantInfo` (S8).
///
/// Identical checks to [`check_univ_param_hygiene`], but over the richer
/// `ConstantInfo` variants (`Inductive`, `Constructor`, `Recursor`,
/// `Quotient`, in addition to `Axiom`/`Definition`/`Theorem`/`Opaque`). Every
/// variant exposes its `level_params`, `ty`, and optional `value` uniformly,
/// so a hostile or malformed export cannot smuggle a duplicate universe
/// parameter, a free (undeclared) universe variable, or a level metavariable
/// through the `check_constant_info` path either.
#[allow(clippy::result_large_err)]
pub(super) fn check_univ_param_hygiene_ci(ci: &ConstantInfo) -> Result<(), KernelError> {
    check_univ_param_hygiene_parts(
        ci.name(),
        ci.level_params(),
        std::iter::once(ci.ty()).chain(ci.value()),
    )
}
/// Shared core of the S8 universe-parameter hygiene checks, over the raw
/// pieces (name, declared universe params, and the expressions to scan — the
/// type followed by any value). Used by both [`check_univ_param_hygiene`]
/// (`Declaration`) and [`check_univ_param_hygiene_ci`] (`ConstantInfo`).
///
/// Three checks, all of which Lean's kernel performs and none of which the
/// pre-Wave-2 checker did:
///
/// 1. **No duplicate universe parameters** in `params`.
/// 2. **Every `Level::Param` occurring in an `expr` is declared** in `params`
///    (an undeclared param is a free universe variable and must be rejected,
///    else a hostile export can capture it).
/// 3. **No `Level::MVar` anywhere** in any `expr` — a kernel-checked
///    declaration must be metavariable-free.
#[allow(clippy::result_large_err)]
fn check_univ_param_hygiene_parts<'a>(
    name: &crate::Name,
    params: &[crate::Name],
    exprs: impl Iterator<Item = &'a crate::Expr>,
) -> Result<(), KernelError> {
    use std::collections::HashSet;

    // (1) duplicate parameter names.
    let mut declared: HashSet<&crate::Name> = HashSet::new();
    for p in params {
        if !declared.insert(p) {
            return Err(KernelError::Other(format!(
                "declaration {}: duplicate universe parameter `{}`",
                name, p
            )));
        }
    }

    // (2) + (3): walk type and value.
    for expr in exprs {
        // (0) closed terms only, and none deeper than this thread's limit
        // (where it has one) — before anything below walks the term.
        check_term_depth(name, expr)?;
        check_closed_term(name, expr)?;
        // (3) metavariables.
        if crate::expr_util::has_level_mvar(expr) {
            return Err(KernelError::Other(format!(
                "declaration {}: universe metavariable in kernel-checked declaration",
                name
            )));
        }
        // (2) undeclared parameters.
        let mut used = Vec::new();
        collect_expr_level_params(expr, &mut used);
        for u in &used {
            if !declared.contains(u) {
                return Err(KernelError::Other(format!(
                    "declaration {}: undeclared universe parameter `{}`",
                    name, u
                )));
            }
        }
    }
    Ok(())
}
/// A term of a kernel-checked declaration — its type, its value, a recursor
/// rule — must be CLOSED: no free variable and no loose bound variable.
/// Lean's kernel makes the same check before it looks at a declaration
/// (`check_no_metavar_no_fvar`).
///
/// Free variables are the checker's own device: it mints one for each
/// binder it opens, by number, and types what it finds under the binder
/// against it. A declaration that arrives already containing a free variable
/// can only be naming one of those numbers. Under a binder the checker
/// happens to have opened with that number the variable passes for the
/// bound one — and the declaration would then go into the environment with
/// the free variable still in it, to be unfolded later in a context where
/// the same number means something else. Since the checker remembers the
/// types it has inferred ([`TypeChecker::infer_type`]), such a variable
/// would also keep its type AFTER its binder closed:
/// `(fun (x : False) => x) (FVar 0)` would check as a proof of `False`.
/// No export can spell a free variable — the format has no record for one —
/// so this concerns a declaration built through the Rust API; it is refused
/// here, before any of it is typed. Both facts are read off the term in O(1).
#[allow(clippy::result_large_err)]
pub(crate) fn check_closed_term(name: &crate::Name, expr: &crate::Expr) -> Result<(), KernelError> {
    if crate::expr_util::has_any_fvar(expr) {
        return Err(KernelError::Other(format!(
            "declaration {}: free variable in kernel-checked declaration",
            name
        )));
    }
    if crate::expr_util::has_loose_bvars(expr) {
        return Err(KernelError::Other(format!(
            "declaration {}: loose bound variable in kernel-checked declaration",
            name
        )));
    }
    Ok(())
}
/// A term of a declaration offered for checking — its type, its value, a
/// recursor rule — must not be deeper than the limit of
/// [`crate::fuel::set_term_depth_limit`], where one is set and the depth of
/// terms is tracked ([`crate::fuel::TERM_DEPTH_TRACKED`]).
///
/// The limit stands for the stack of the thread the kernel runs on: every
/// walk of a term is a recursion as deep as the term. A term built WHILE a
/// declaration is checked spends the budget when it crosses the limit; this
/// is the same refusal for a term that arrives already too deep, made
/// before any of it is walked (the depth is read off the root in O(1)). The
/// error is not a verdict on the declaration: the limit is recorded
/// ([`crate::fuel::term_depth_limit_hit`]), and the caller reports a
/// resource limit.
#[allow(clippy::result_large_err)]
pub(crate) fn check_term_depth(name: &crate::Name, expr: &crate::Expr) -> Result<(), KernelError> {
    #[cfg(feature = "term-depth")]
    {
        let depth = expr.depth();
        if crate::fuel::term_depth_limit().is_some_and(|limit| depth > limit) {
            crate::fuel::note_term_depth(depth);
            return Err(KernelError::Other(format!(
                "declaration {name}: a term {depth} deep is over the term-depth limit"
            )));
        }
    }
    #[cfg(not(feature = "term-depth"))]
    let _ = (name, expr);
    Ok(())
}
/// Collect all `Level::Param` names referenced anywhere in an expression,
/// including inside `Proj`'s struct expression (which the declaration-module
/// collector skips). Deduplicated.
///
/// Every shared subterm is looked at once (the set of addresses already
/// seen — sound for the duration of this walk, during which `expr` is
/// borrowed and none of its subterms can be freed), and a subterm that
/// mentions no universe parameter is not entered at all (the fact is cached
/// on the node). A declaration whose value is a few thousand shared nodes
/// used to be walked here as the millions of nodes of its tree.
pub(super) fn collect_expr_level_params(expr: &crate::Expr, out: &mut Vec<crate::Name>) {
    use crate::{Expr, Node};
    let mut seen: std::collections::HashSet<*const Expr, crate::node_memo::WordBuildHasher> =
        std::collections::HashSet::default();
    let mut pending: Vec<&Node> = Vec::new();
    let mut current: Option<&Expr> = Some(expr);
    loop {
        let cur = match current.take() {
            Some(cur) => cur,
            None => match pending.pop() {
                Some(node) => {
                    if !node.has_level_param() || !seen.insert(node.as_ptr()) {
                        continue;
                    }
                    node
                }
                None => break,
            },
        };
        match cur {
            Expr::Sort(l) => collect_level_params_in_level(l, out),
            Expr::Const(_, levels) => {
                for l in levels {
                    collect_level_params_in_level(l, out);
                }
            }
            Expr::App(f, a) => {
                pending.push(a);
                pending.push(f);
            }
            Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
                pending.push(body);
                pending.push(ty);
            }
            Expr::Let(_, ty, val, body) => {
                pending.push(body);
                pending.push(val);
                pending.push(ty);
            }
            Expr::Proj(_, _, e) => pending.push(e),
            Expr::BVar(_) | Expr::FVar(_) | Expr::Lit(_) => {}
        }
    }
}
fn collect_level_params_in_level(l: &crate::Level, out: &mut Vec<crate::Name>) {
    use crate::LevelView;
    match l.view() {
        LevelView::Param(n) => {
            if !out.contains(n) {
                out.push(n.clone());
            }
        }
        LevelView::Succ(inner) => collect_level_params_in_level(inner, out),
        LevelView::Max(a, b) | LevelView::IMax(a, b) => {
            collect_level_params_in_level(a, out);
            collect_level_params_in_level(b, out);
        }
        LevelView::Zero | LevelView::MVar(_) => {}
    }
}
/// Check multiple declarations in sequence.
///
/// Processes the declarations in the given order, stopping at the first
/// error. Each successfully-checked declaration is added to the environment
/// so that later declarations can refer to earlier ones.
#[allow(clippy::result_large_err)]
pub fn check_declarations(
    env: &mut Environment,
    decls: Vec<Declaration>,
) -> Result<(), KernelError> {
    for decl in decls {
        check_declaration(env, decl)?;
    }
    Ok(())
}
/// Check a `ConstantInfo` (inductive, constructor, recursor, or quotient) and add
/// it to the environment.
///
/// Unlike `check_declaration`, this function handles the richer LEAN 4-style
/// constant info types that include inductive types, constructors, recursors, and
/// quotient type components.
///
/// A term of `ci` is in the environment afterwards only if it was
/// type-checked here — with one kind of exception, a constant the kernel
/// derives itself. For a `Recursor` the constant that is added is **the
/// kernel's own derivation** (under the supplied name and universe parameter
/// names); the supplied type and rules are compared with it and dropped.
#[allow(clippy::result_large_err)]
pub fn check_constant_info(env: &mut Environment, ci: ConstantInfo) -> Result<(), KernelError> {
    let name = ci.name().clone();
    // Universe-parameter hygiene (S8): reject duplicate univ params, undeclared
    // `Param`s in the type/value, and any `Level` metavariable — for every
    // `ConstantInfo` variant, mirroring the `check_declaration` path.
    check_univ_param_hygiene_ci(&ci)?;
    let mut derived_recursor: Option<RecursorVal> = None;
    match &ci {
        ConstantInfo::Axiom(av) => {
            let mut tc = TypeChecker::new(env);
            tc.ensure_sort(&av.common.ty)?;
        }
        ConstantInfo::Definition(dv) => {
            let mut tc = TypeChecker::new(env);
            tc.ensure_sort(&dv.common.ty)?;
            let val_ty = tc.infer_type(&dv.value)?;
            tc.check_type(&dv.value, &val_ty, &dv.common.ty)?;
        }
        ConstantInfo::Theorem(tv) => {
            let mut tc = TypeChecker::new(env);
            check_theorem_type(&mut tc, &name, &tv.common.ty)?;
            let val_ty = tc.infer_type(&tv.value)?;
            tc.check_type(&tv.value, &val_ty, &tv.common.ty)?;
        }
        ConstantInfo::Opaque(ov) => {
            let mut tc = TypeChecker::new(env);
            tc.ensure_sort(&ov.common.ty)?;
            let val_ty = tc.infer_type(&ov.value)?;
            tc.check_type(&ov.value, &val_ty, &ov.common.ty)?;
        }
        ConstantInfo::Inductive(iv) => {
            check_inductive_val(env, iv)?;
        }
        ConstantInfo::Constructor(cv) => {
            check_constructor_val(env, cv)?;
        }
        ConstantInfo::Recursor(rv) => {
            // The rule right-hand sides are terms of the declaration too
            // (closed lambdas over params, motives, minors and fields).
            for rule in &rv.rules {
                check_term_depth(&name, &rule.rhs)?;
                check_closed_term(&name, &rule.rhs)?;
            }
            // A recursor is not checked, it is derived: what is added is
            // the kernel's own recursor, and the supplied declaration was
            // only held against it.
            derived_recursor = Some(check_recursor_val(env, rv)?);
        }
        ConstantInfo::Quotient(qv) => {
            check_quotient_val(env, qv)?;
        }
    }
    let ci = match derived_recursor {
        Some(derived) => ConstantInfo::Recursor(derived),
        None => ci,
    };
    env.add_constant(ci).map_err(|e| match e {
        crate::env::EnvError::DuplicateDeclaration(_) => {
            KernelError::Other(format!("duplicate declaration: {}", name))
        }
        crate::env::EnvError::NotFound(_) => {
            KernelError::Other(format!("declaration not found: {}", name))
        }
        crate::env::EnvError::InvalidQuotient(msg) => KernelError::Other(msg),
    })
}
/// Check multiple `ConstantInfo` declarations, stopping on the first error.
#[allow(clippy::result_large_err)]
pub fn check_constant_infos(
    env: &mut Environment,
    cis: Vec<ConstantInfo>,
) -> Result<(), KernelError> {
    for ci in cis {
        check_constant_info(env, ci)?;
    }
    Ok(())
}
/// Check a group of `ConstantInfo` declarations in order and add them as a
/// unit: every one of them, or none.
///
/// Each constant is checked against the environment that already holds the
/// ones before it, as with [`check_constant_infos`] — a constructor is
/// checked against its inductive type, a recursor against the type and its
/// constructors. Unlike [`check_constant_infos`], a failure takes the
/// earlier members of the group out again before the error is returned, so
/// the environment is exactly what it was before the call.
///
/// This is the entry point for a declaration that arrives as several
/// constants (an exported inductive family). Left half installed, a refused
/// family would still answer for the names it did install: a later
/// declaration that names only those would be checked against a type the
/// kernel never accepted as a whole — for one, a type that lists fewer
/// constructors than it was declared with.
///
/// **The guard.** Once every member is in, the recursors the group
/// installed — the kernel's derivations — are held to the names they
/// mention: their rules call the sibling recursors of the family by name,
/// and each constant a derived term names must resolve in the environment
/// as it now stands, a name the derivation gives a recursor or a type of
/// the family to that constant of the family
/// ([`crate::inductive::installed`]). A name that does not takes the whole
/// group out again: a rule calling a recursor that is not installed would
/// let a later declaration define it with another type.
#[allow(clippy::result_large_err)]
pub fn check_constant_infos_atomic(
    env: &mut Environment,
    cis: Vec<ConstantInfo>,
) -> Result<(), KernelError> {
    let mut added: Vec<crate::Name> = Vec::with_capacity(cis.len());
    for ci in cis {
        let name = ci.name().clone();
        if let Err(e) = check_constant_info(env, ci) {
            env.remove_constants(&added);
            return Err(e);
        }
        added.push(name);
    }
    let guarded = {
        let installed: Vec<&ConstantInfo> = added.iter().filter_map(|n| env.find(n)).collect();
        crate::inductive::installed::check_derived_references(
            env,
            &installed,
            crate::inductive::installed::DerivedTerms::Recursors,
        )
    };
    if let Err(e) = guarded {
        env.remove_constants(&added);
        return Err(e);
    }
    Ok(())
}
/// Validate an `InductiveVal`.
///
/// Beyond the sort check, the declared telescope must match the announced
/// `num_params + num_indices`, universe parameters must be distinct and
/// actually declared, and the `is_prop` flag must agree with the declared
/// sort — a caller cannot lie about propositionality (large elimination is
/// recomputed from the type when the recursor is checked anyway).
/// Constructor types are checked via `check_constructor_val` when each
/// constructor `ConstantInfo` is added; recursors are re-derived and
/// compared in `check_recursor_val`, and the re-derived one is what is
/// added. Empty inductives (0 constructors, like
/// `Empty`) are valid.
#[allow(clippy::result_large_err)]
pub(super) fn check_inductive_val(
    env: &mut Environment,
    iv: &InductiveVal,
) -> Result<(), KernelError> {
    crate::inductive::derive::validate_inductive_val(env, iv)
}
/// Validate a `ConstructorVal` against the environment's inductive family:
/// the parameter telescope must match the inductive's (definitionally),
/// each field's universe must fit the inductive's universe (with the Prop
/// exception), the fields must be strictly positive (WHNF-hardened,
/// mutual-aware), and the codomain must be the parent type applied to
/// exactly the parameters. Metadata (`cidx`, `num_params`, `num_fields`,
/// level params) must agree with the parent inductive.
#[allow(clippy::result_large_err)]
pub(super) fn check_constructor_val(
    env: &mut Environment,
    cv: &ConstructorVal,
) -> Result<(), KernelError> {
    crate::inductive::derive::verify_constructor_val(env, cv)
}
/// Validate a `RecursorVal` by *re-deriving* it, and return the derived
/// recursor: the kernel reconstructs the recursors for the declared
/// inductive family (motives, minor premises with induction hypotheses,
/// elimination universe, K flag, iota rules) and requires the supplied
/// declaration to be the derivation — as written, or type-checked and then
/// definitionally equal. An externally-supplied recursor is never
/// installed: the caller adds the returned one, which is the kernel's own
/// under the supplied name and universe parameter names.
#[allow(clippy::result_large_err)]
pub(super) fn check_recursor_val(
    env: &mut Environment,
    rv: &RecursorVal,
) -> Result<RecursorVal, KernelError> {
    crate::inductive::derive::verify_recursor_val(env, rv)
}
/// Validate a `QuotVal`: verify the supplied type is definitionally equal to
/// the kernel's canonical type for its [`QuotKind`].
///
/// Defense-in-depth: the kernel constructs the canonical quotient types itself
/// (see [`crate::env::canonical_quot_type`]) and *never* trusts a
/// caller-supplied type. A `ConstantInfo::Quotient` whose type is not defeq to
/// the canonical shape is rejected here (in addition to being rejected outright
/// by `Environment::add_constant`, which only accepts quotients through the
/// once-only `add_quot` entry point).
#[allow(clippy::result_large_err)]
pub(super) fn check_quotient_val(env: &mut Environment, qv: &QuotVal) -> Result<(), KernelError> {
    let canonical = crate::env::canonical_quot_type(qv.kind);
    let expected_params = crate::env::canonical_quot_level_params(qv.kind);
    if qv.common.level_params != expected_params {
        return Err(KernelError::Other(format!(
            "quotient `{}` has unexpected universe parameters: expected {:?}, got {:?}",
            qv.common.name, expected_params, qv.common.level_params
        )));
    }
    let mut tc = TypeChecker::new(env);
    tc.ensure_sort(&qv.common.ty)?;
    if !tc.is_def_eq(&qv.common.ty, &canonical) {
        return Err(KernelError::TypeMismatch {
            expected: canonical,
            got: qv.common.ty.clone(),
            context: format!("canonical type of quotient `{}`", qv.common.name),
        });
    }
    Ok(())
}
/// Summarize a declaration without checking it.
pub fn summarize_declaration(decl: &Declaration) -> DeclSummary {
    match decl {
        Declaration::Axiom {
            name, univ_params, ..
        } => DeclSummary {
            name: format!("{}", name),
            kind: DeclKind::Axiom,
            has_body: false,
            num_univ_params: univ_params.len(),
        },
        Declaration::Definition {
            name, univ_params, ..
        } => DeclSummary {
            name: format!("{}", name),
            kind: DeclKind::Definition,
            has_body: true,
            num_univ_params: univ_params.len(),
        },
        Declaration::Theorem {
            name, univ_params, ..
        } => DeclSummary {
            name: format!("{}", name),
            kind: DeclKind::Theorem,
            has_body: true,
            num_univ_params: univ_params.len(),
        },
        Declaration::Opaque {
            name, univ_params, ..
        } => DeclSummary {
            name: format!("{}", name),
            kind: DeclKind::Opaque,
            has_body: true,
            num_univ_params: univ_params.len(),
        },
    }
}
/// Check multiple declarations, collecting all errors rather than stopping at first.
///
/// Unlike `check_declarations`, this function continues even after encountering
/// errors, and returns a summary of all results.
pub fn check_declarations_collect_errors(
    env: &mut Environment,
    decls: Vec<Declaration>,
) -> BatchCheckResult {
    let mut num_ok = 0;
    let mut num_failed = 0;
    let mut errors = Vec::new();
    for decl in decls {
        let name = format!("{}", decl.name());
        match check_declaration(env, decl) {
            Ok(()) => num_ok += 1,
            Err(e) => {
                num_failed += 1;
                errors.push((name, format!("{:?}", e)));
            }
        }
    }
    BatchCheckResult {
        num_ok,
        num_failed,
        errors,
    }
}
/// Check multiple declarations and collect statistics.
///
/// Returns `(stats, first_error)` where `first_error` is `Some(err)` if any
/// declaration failed, and `None` if all succeeded.
#[allow(clippy::result_large_err)]
pub fn check_declarations_with_stats(
    env: &mut Environment,
    decls: Vec<Declaration>,
) -> (CheckStats, Option<KernelError>) {
    let mut stats = CheckStats::new();
    for decl in decls {
        let kind = summarize_declaration(&decl).kind;
        match check_declaration(env, decl) {
            Ok(()) => match kind {
                DeclKind::Axiom => stats.num_axioms += 1,
                DeclKind::Definition => stats.num_definitions += 1,
                DeclKind::Theorem => stats.num_theorems += 1,
                DeclKind::Opaque => stats.num_opaques += 1,
            },
            Err(e) => {
                stats.num_failures += 1;
                return (stats, Some(e));
            }
        }
    }
    (stats, None)
}
/// Check that a declaration name is valid (non-empty, no invalid characters).
pub fn is_valid_decl_name(name: &str) -> bool {
    !name.is_empty()
        && name
            .chars()
            .all(|c| c.is_alphanumeric() || c == '_' || c == '.' || c == '\'')
        && !name.starts_with('.')
        && !name.ends_with('.')
}
/// Check that a declaration's universe parameter list has no duplicates.
pub fn has_unique_univ_params(params: &[crate::Name]) -> bool {
    let mut seen = std::collections::HashSet::new();
    params.iter().all(|p| seen.insert(format!("{}", p)))
}
/// Check that two universe parameter lists are compatible (same length, same names).
pub fn univ_params_compatible(p1: &[crate::Name], p2: &[crate::Name]) -> bool {
    p1.len() == p2.len()
        && p1
            .iter()
            .zip(p2.iter())
            .all(|(a, b)| format!("{}", a) == format!("{}", b))
}
/// Format a declaration summary for display.
pub fn format_decl_summary(summary: &DeclSummary) -> String {
    let body_str = if summary.has_body { " := ..." } else { "" };
    let params_str = if summary.num_univ_params > 0 {
        format!(".{{u{}}}", summary.num_univ_params)
    } else {
        String::new()
    };
    format!(
        "{} {}{}{} : ...",
        summary.kind, summary.name, params_str, body_str
    )
}
/// Format a batch check result for display.
pub fn format_batch_result(result: &BatchCheckResult) -> String {
    if result.all_ok() {
        format!("All {} declarations OK", result.total())
    } else {
        let mut s = format!(
            "{}/{} declarations OK. Failures:\n",
            result.num_ok,
            result.total()
        );
        for msg in result.error_messages() {
            s.push_str("  - ");
            s.push_str(&msg);
            s.push('\n');
        }
        s
    }
}
/// Check the integrity of an environment by re-type-checking all declarations.
///
/// This is an expensive operation intended for debugging and testing. It verifies
/// that every declaration in the environment is still consistent.
pub fn verify_environment_integrity(env: &Environment) -> Vec<String> {
    let mut issues = Vec::new();
    for name in env
        .constant_names()
        .cloned()
        .collect::<Vec<_>>()
        .into_iter()
    {
        if let Some(info) = env.get(&name) {
            let ty = info.ty();
            if !is_structurally_valid_expr(ty) {
                issues.push(format!("{}: type is not structurally valid", name));
            }
        }
    }
    issues
}
/// Perform a basic structural validity check on an expression.
///
/// This checks that bound variable indices are in range, but does not
/// perform full type checking.
pub fn is_structurally_valid_expr(expr: &crate::Expr) -> bool {
    check_expr_bvars(expr, 0)
}
pub(super) fn check_expr_bvars(expr: &crate::Expr, depth: u32) -> bool {
    use crate::Expr;
    match expr {
        Expr::BVar(i) => *i < depth,
        Expr::FVar(_) | Expr::Sort(_) | Expr::Const(_, _) | Expr::Lit(_) => true,
        Expr::App(f, a) => check_expr_bvars(f, depth) && check_expr_bvars(a, depth),
        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
            check_expr_bvars(ty, depth) && check_expr_bvars(body, depth + 1)
        }
        Expr::Let(_, ty, val, body) => {
            check_expr_bvars(ty, depth)
                && check_expr_bvars(val, depth)
                && check_expr_bvars(body, depth + 1)
        }
        Expr::Proj(_, _, e) => check_expr_bvars(e, depth),
    }
}
/// Collect the names of all constants referenced in a declaration.
///
/// This includes references in both the type and the value (if present).
pub fn declaration_dependencies(decl: &Declaration) -> Vec<crate::Name> {
    use crate::collect_const_names;
    let mut deps = collect_const_names(decl.ty());
    if let Some(val) = decl.value() {
        deps.extend(collect_const_names(val));
    }
    deps.sort_by(|a, b| format!("{}", a).cmp(&format!("{}", b)));
    deps.dedup_by(|a, b| format!("{}", a) == format!("{}", b));
    deps
}
/// Check that all dependencies of a declaration exist in the environment.
///
/// Returns the names of any missing dependencies.
pub fn check_dependencies_exist(env: &Environment, decl: &Declaration) -> Vec<crate::Name> {
    let deps = declaration_dependencies(decl);
    deps.into_iter()
        .filter(|name| env.get(name).is_none())
        .collect()
}
#[cfg(test)]
mod tests {
    use super::*;
    use crate::{Level, Literal, ReducibilityHint};
    fn mk_type0() -> Expr {
        Expr::Sort(Level::succ(Level::zero()))
    }
    fn mk_nat_axiom() -> Declaration {
        Declaration::Axiom {
            name: Name::str("Nat"),
            univ_params: vec![],
            ty: mk_type0(),
        }
    }
    fn mk_nat_const() -> Expr {
        Expr::Const(Name::str("Nat"), vec![])
    }
    #[test]
    fn test_check_axiom() {
        let mut env = Environment::new();
        let nat_ty = Expr::Sort(Level::succ(Level::zero()));
        let axiom = Declaration::Axiom {
            name: Name::str("Nat"),
            univ_params: vec![],
            ty: nat_ty,
        };
        check_declaration(&mut env, axiom).expect("value should be present");
        assert!(env.contains(&Name::str("Nat")));
    }
    #[test]
    fn test_check_definition() {
        let mut env = Environment::new();
        env.add(mk_nat_axiom()).expect("value should be present");
        let nat_ty = mk_nat_const();
        let val = Expr::Lit(Literal::nat(42));
        let def = Declaration::Definition {
            name: Name::str("answer"),
            univ_params: vec![],
            ty: nat_ty,
            val,
            hint: ReducibilityHint::Regular(1),
        };
        check_declaration(&mut env, def).expect("value should be present");
        assert!(env.contains(&Name::str("answer")));
    }
    #[test]
    fn test_type_mismatch() {
        let mut env = Environment::new();
        let type0 = mk_type0();
        env.add(Declaration::Axiom {
            name: Name::str("String"),
            univ_params: vec![],
            ty: type0.clone(),
        })
        .expect("value should be present");
        env.add(Declaration::Axiom {
            name: Name::str("Nat"),
            univ_params: vec![],
            ty: type0,
        })
        .expect("value should be present");
        let string_ty = Expr::Const(Name::str("String"), vec![]);
        let val = Expr::Lit(Literal::nat(42));
        let def = Declaration::Definition {
            name: Name::str("bad"),
            univ_params: vec![],
            ty: string_ty,
            val,
            hint: ReducibilityHint::Regular(1),
        };
        let result = check_declaration(&mut env, def);
        assert!(result.is_err());
    }
    #[test]
    fn test_check_declarations_sequence() {
        let mut env = Environment::new();
        let decls = vec![
            Declaration::Axiom {
                name: Name::str("A"),
                univ_params: vec![],
                ty: mk_type0(),
            },
            Declaration::Axiom {
                name: Name::str("B"),
                univ_params: vec![],
                ty: mk_type0(),
            },
        ];
        check_declarations(&mut env, decls).expect("value should be present");
        assert!(env.contains(&Name::str("A")));
        assert!(env.contains(&Name::str("B")));
    }
    #[test]
    fn test_decl_kind_display() {
        assert_eq!(DeclKind::Axiom.as_str(), "axiom");
        assert_eq!(DeclKind::Definition.as_str(), "def");
        assert_eq!(DeclKind::Theorem.as_str(), "theorem");
        assert_eq!(DeclKind::Opaque.as_str(), "opaque");
        assert!(DeclKind::Theorem.is_proven());
        assert!(DeclKind::Axiom.is_assumed());
        assert!(DeclKind::Definition.is_definition());
        assert!(!DeclKind::Axiom.is_definition());
    }
    #[test]
    fn test_summarize_declaration() {
        let decl = mk_nat_axiom();
        let summary = summarize_declaration(&decl);
        assert_eq!(summary.name, "Nat");
        assert_eq!(summary.kind, DeclKind::Axiom);
        assert!(!summary.has_body);
        assert_eq!(summary.num_univ_params, 0);
    }
    #[test]
    fn test_is_valid_decl_name() {
        assert!(is_valid_decl_name("Nat"));
        assert!(is_valid_decl_name("Nat.succ"));
        assert!(is_valid_decl_name("foo_bar"));
        assert!(!is_valid_decl_name(""));
        assert!(!is_valid_decl_name(".leading_dot"));
        assert!(!is_valid_decl_name("trailing_dot."));
    }
    #[test]
    fn test_has_unique_univ_params() {
        let u = Name::str("u");
        let v = Name::str("v");
        let params = vec![u.clone(), v.clone()];
        assert!(has_unique_univ_params(&params));
        let dup_params = vec![u.clone(), u.clone()];
        assert!(!has_unique_univ_params(&dup_params));
    }
    #[test]
    fn test_check_config_default() {
        let cfg = CheckConfig::default();
        assert!(cfg.check_type_is_sort);
        assert!(cfg.check_value_type);
        assert!(cfg.check_no_free_vars);
    }
    #[test]
    fn test_check_config_lenient() {
        let cfg = CheckConfig::lenient();
        assert!(cfg.check_type_is_sort);
        assert!(!cfg.check_value_type);
    }
    #[test]
    fn test_check_config_strict() {
        let cfg = CheckConfig::strict();
        assert!(!cfg.allow_axioms);
        assert!(cfg.max_depth > 0);
    }
    #[test]
    fn test_batch_check_all_ok() {
        let mut env = Environment::new();
        let decls = vec![
            Declaration::Axiom {
                name: Name::str("X"),
                univ_params: vec![],
                ty: mk_type0(),
            },
            Declaration::Axiom {
                name: Name::str("Y"),
                univ_params: vec![],
                ty: mk_type0(),
            },
        ];
        let result = check_declarations_collect_errors(&mut env, decls);
        assert!(result.all_ok());
        assert_eq!(result.num_ok, 2);
        assert_eq!(result.num_failed, 0);
    }
    #[test]
    fn test_batch_check_with_error() {
        let mut env = Environment::new();
        let decls = vec![
            Declaration::Axiom {
                name: Name::str("M"),
                univ_params: vec![],
                ty: mk_type0(),
            },
            Declaration::Definition {
                name: Name::str("bad_def"),
                univ_params: vec![],
                ty: Expr::Const(Name::str("UndefinedType"), vec![]),
                val: Expr::Lit(Literal::nat(0)),
                hint: ReducibilityHint::Regular(1),
            },
        ];
        let result = check_declarations_collect_errors(&mut env, decls);
        assert!(!result.all_ok());
        assert_eq!(result.num_ok, 1);
        assert_eq!(result.num_failed, 1);
    }
    #[test]
    fn test_env_builder_clean() {
        let mut builder = EnvBuilder::new();
        let added = builder.add(Declaration::Axiom {
            name: Name::str("P"),
            univ_params: vec![],
            ty: mk_type0(),
        });
        assert!(added);
        assert!(builder.is_clean());
        assert_eq!(builder.stats().num_axioms, 1);
    }
    #[test]
    fn test_env_builder_with_error() {
        let mut builder = EnvBuilder::new();
        let added = builder.add(Declaration::Definition {
            name: Name::str("oops"),
            univ_params: vec![],
            ty: Expr::Const(Name::str("NoSuchType"), vec![]),
            val: Expr::Lit(Literal::nat(0)),
            hint: ReducibilityHint::Regular(1),
        });
        assert!(!added);
        assert!(!builder.is_clean());
        assert_eq!(builder.errors().len(), 1);
    }
    #[test]
    fn test_well_formed_result_display() {
        let ok = WellFormedResult::Ok;
        assert!(ok.is_ok());
        assert_eq!(ok.description(), "well-formed");
        let mismatch = WellFormedResult::TypeMismatch {
            description: "Nat vs String".to_string(),
        };
        assert!(!mismatch.is_ok());
        assert!(mismatch.description().contains("Nat vs String"));
    }
    #[test]
    fn test_is_structurally_valid_expr() {
        let bad = Expr::BVar(0);
        assert!(!is_structurally_valid_expr(&bad));
        let sort = Expr::Sort(Level::zero());
        assert!(is_structurally_valid_expr(&sort));
        let lam = Expr::Lam(
            crate::BinderInfo::Default,
            Name::str("x"),
            Node::new(Expr::Sort(Level::zero())),
            Node::new(Expr::BVar(0)),
        );
        assert!(is_structurally_valid_expr(&lam));
    }
    #[test]
    fn test_format_decl_summary() {
        let summary = DeclSummary {
            name: "Nat.add".to_string(),
            kind: DeclKind::Definition,
            has_body: true,
            num_univ_params: 0,
        };
        let s = format_decl_summary(&summary);
        assert!(s.contains("Nat.add"));
        assert!(s.contains("def"));
    }
    #[test]
    fn test_check_stats_totals() {
        let stats = CheckStats {
            num_axioms: 2,
            num_definitions: 3,
            num_theorems: 1,
            num_opaques: 0,
            num_failures: 1,
        };
        assert_eq!(stats.total(), 6);
        assert_eq!(stats.num_ok(), 6);
    }
    #[test]
    fn test_format_batch_result_all_ok() {
        let result = BatchCheckResult {
            num_ok: 3,
            num_failed: 0,
            errors: vec![],
        };
        let s = format_batch_result(&result);
        assert!(s.contains("3"));
    }
    #[test]
    fn test_temp_env_scope() {
        let mut env = Environment::new();
        {
            let mut scope = TempEnvScope::new(&mut env);
            let ok = scope.add(Declaration::Axiom {
                name: Name::str("TempDecl"),
                univ_params: vec![],
                ty: mk_type0(),
            });
            assert!(ok.is_ok());
            assert_eq!(scope.num_added(), 1);
        }
        assert!(env.contains(&Name::str("TempDecl")));
    }
    #[allow(dead_code)]
    fn mk_type1() -> Expr {
        Expr::Sort(Level::succ(Level::succ(Level::zero())))
    }
    #[test]
    fn test_check_constant_info_axiom() {
        use crate::declaration::{AxiomVal, ConstantVal};
        let mut env = Environment::new();
        let ci = ConstantInfo::Axiom(AxiomVal {
            common: ConstantVal {
                name: Name::str("MyAxiom"),
                level_params: vec![],
                ty: mk_type0(),
            },
            is_unsafe: false,
        });
        check_constant_info(&mut env, ci).expect("value should be present");
        assert!(env.contains(&Name::str("MyAxiom")));
    }
    #[test]
    fn test_check_constant_info_inductive_simple() {
        use crate::declaration::{ConstantVal, InductiveVal};
        let mut env = Environment::new();
        let iv = InductiveVal {
            common: ConstantVal {
                name: Name::str("Bool"),
                level_params: vec![],
                ty: mk_type0(),
            },
            num_params: 0,
            num_indices: 0,
            all: vec![Name::str("Bool")],
            ctors: vec![Name::str("Bool.true"), Name::str("Bool.false")],
            num_nested: 0,
            is_rec: false,
            is_unsafe: false,
            is_reflexive: false,
            is_prop: false,
        };
        let ci = ConstantInfo::Inductive(iv);
        check_constant_info(&mut env, ci).expect("value should be present");
        assert!(env.contains(&Name::str("Bool")));
    }
    #[test]
    fn test_check_constant_info_inductive_empty() {
        use crate::declaration::{ConstantVal, InductiveVal};
        let mut env = Environment::new();
        let iv = InductiveVal {
            common: ConstantVal {
                name: Name::str("Empty"),
                level_params: vec![],
                ty: mk_type0(),
            },
            num_params: 0,
            num_indices: 0,
            all: vec![Name::str("Empty")],
            ctors: vec![],
            num_nested: 0,
            is_rec: false,
            is_unsafe: false,
            is_reflexive: false,
            is_prop: false,
        };
        let ci = ConstantInfo::Inductive(iv);
        check_constant_info(&mut env, ci).expect("value should be present");
        assert!(env.contains(&Name::str("Empty")));
    }
    #[test]
    fn test_check_constant_info_constructor_valid() {
        use crate::declaration::{ConstantVal, ConstructorVal, InductiveVal};
        let mut env = Environment::new();
        let ind_ci = ConstantInfo::Inductive(InductiveVal {
            common: ConstantVal {
                name: Name::str("Bool"),
                level_params: vec![],
                ty: mk_type0(),
            },
            num_params: 0,
            num_indices: 0,
            all: vec![Name::str("Bool")],
            ctors: vec![Name::str("Bool.true")],
            num_nested: 0,
            is_rec: false,
            is_unsafe: false,
            is_reflexive: false,
            is_prop: false,
        });
        check_constant_info(&mut env, ind_ci).expect("value should be present");
        let ctor_ci = ConstantInfo::Constructor(ConstructorVal {
            common: ConstantVal {
                name: Name::str("Bool.true"),
                level_params: vec![],
                ty: Expr::Const(Name::str("Bool"), vec![]),
            },
            induct: Name::str("Bool"),
            cidx: 0,
            num_params: 0,
            num_fields: 0,
            is_unsafe: false,
        });
        check_constant_info(&mut env, ctor_ci).expect("value should be present");
        assert!(env.contains(&Name::str("Bool.true")));
    }
    #[test]
    fn test_check_constant_info_constructor_wrong_return_type() {
        use crate::declaration::{ConstantVal, ConstructorVal, InductiveVal};
        let mut env = Environment::new();
        env.add_constant(ConstantInfo::Inductive(InductiveVal {
            common: ConstantVal {
                name: Name::str("Bool"),
                level_params: vec![],
                ty: mk_type0(),
            },
            num_params: 0,
            num_indices: 0,
            all: vec![Name::str("Bool")],
            ctors: vec![Name::str("Bool.bad")],
            num_nested: 0,
            is_rec: false,
            is_unsafe: false,
            is_reflexive: false,
            is_prop: false,
        }))
        .expect("value should be present");
        env.add_constant(ConstantInfo::Inductive(InductiveVal {
            common: ConstantVal {
                name: Name::str("Nat"),
                level_params: vec![],
                ty: mk_type0(),
            },
            num_params: 0,
            num_indices: 0,
            all: vec![Name::str("Nat")],
            ctors: vec![],
            num_nested: 0,
            is_rec: false,
            is_unsafe: false,
            is_reflexive: false,
            is_prop: false,
        }))
        .expect("value should be present");
        let ctor_ci = ConstantInfo::Constructor(ConstructorVal {
            common: ConstantVal {
                name: Name::str("Bool.bad"),
                level_params: vec![],
                ty: Expr::Const(Name::str("Nat"), vec![]),
            },
            induct: Name::str("Bool"),
            cidx: 0,
            num_params: 0,
            num_fields: 0,
            is_unsafe: false,
        });
        let result = check_constant_info(&mut env, ctor_ci);
        assert!(result.is_err(), "expected error for wrong return type");
    }
    #[test]
    fn test_check_constant_info_recursor_rejects_bogus() {
        // Recursors are RE-DERIVED by the kernel and compared against the
        // supplied declaration: a recursor whose type is literally `Type`
        // with no rules must be rejected, never trusted (audit item S3).
        use crate::declaration::{ConstantVal, InductiveVal, RecursorVal};
        let mut env = Environment::new();
        env.add_constant(ConstantInfo::Inductive(InductiveVal {
            common: ConstantVal {
                name: Name::str("Bool"),
                level_params: vec![],
                ty: mk_type0(),
            },
            num_params: 0,
            num_indices: 0,
            all: vec![Name::str("Bool")],
            ctors: vec![],
            num_nested: 0,
            is_rec: false,
            is_unsafe: false,
            is_reflexive: false,
            is_prop: false,
        }))
        .expect("value should be present");
        let rec_ty = mk_type0();
        let rec_ci = ConstantInfo::Recursor(RecursorVal {
            common: ConstantVal {
                name: Name::str("Bool.rec"),
                level_params: vec![],
                ty: rec_ty,
            },
            all: vec![Name::str("Bool")],
            num_params: 0,
            num_indices: 0,
            num_motives: 1,
            num_minors: 2,
            rules: vec![],
            k: false,
            is_unsafe: false,
        });
        let result = check_constant_info(&mut env, rec_ci);
        assert!(
            result.is_err(),
            "hand-supplied bogus recursor must be rejected"
        );
        assert!(!env.contains(&Name::str("Bool.rec")));
    }
    #[test]
    fn test_check_constant_info_quotient_rejects_noncanonical() {
        // Quotient constants must have their kernel-canonical type. A caller
        // supplying `Quot : Sort 0` (with no universe params) must be rejected:
        // both by `check_quotient_val` (wrong type / universe params) and by
        // `Environment::add_constant` (quotients only via `add_quot`).
        use crate::declaration::{ConstantVal, QuotKind, QuotVal};
        let mut env = Environment::new();
        let quot_ci = ConstantInfo::Quotient(QuotVal {
            common: ConstantVal {
                name: Name::str("Quot"),
                level_params: vec![],
                ty: mk_type0(),
            },
            kind: QuotKind::Type,
        });
        assert!(
            check_constant_info(&mut env, quot_ci).is_err(),
            "non-canonical quotient type must be rejected"
        );
        assert!(!env.contains(&Name::str("Quot")));
    }
    #[test]
    fn test_check_constant_infos_sequence() {
        use crate::declaration::{AxiomVal, ConstantVal};
        let mut env = Environment::new();
        let cis = vec![
            ConstantInfo::Axiom(AxiomVal {
                common: ConstantVal {
                    name: Name::str("P"),
                    level_params: vec![],
                    ty: mk_type0(),
                },
                is_unsafe: false,
            }),
            ConstantInfo::Axiom(AxiomVal {
                common: ConstantVal {
                    name: Name::str("Q"),
                    level_params: vec![],
                    ty: mk_type0(),
                },
                is_unsafe: false,
            }),
        ];
        check_constant_infos(&mut env, cis).expect("value should be present");
        assert!(env.contains(&Name::str("P")));
        assert!(env.contains(&Name::str("Q")));
    }
    #[test]
    fn test_check_constant_info_duplicate() {
        use crate::declaration::{AxiomVal, ConstantVal};
        let mut env = Environment::new();
        let make_ci = || {
            ConstantInfo::Axiom(AxiomVal {
                common: ConstantVal {
                    name: Name::str("Dup"),
                    level_params: vec![],
                    ty: mk_type0(),
                },
                is_unsafe: false,
            })
        };
        check_constant_info(&mut env, make_ci()).expect("value should be present");
        let result = check_constant_info(&mut env, make_ci());
        assert!(result.is_err(), "duplicate should fail");
    }
}
#[cfg(test)]
mod tests_padding_infra {
    use super::*;
    #[test]
    fn test_stat_summary() {
        let mut ss = StatSummary::new();
        ss.record(10.0);
        ss.record(20.0);
        ss.record(30.0);
        assert_eq!(ss.count(), 3);
        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
    }
    #[test]
    fn test_transform_stat() {
        let mut ts = TransformStat::new();
        ts.record_before(100.0);
        ts.record_after(80.0);
        let ratio = ts.mean_ratio().expect("ratio should be present");
        assert!((ratio - 0.8).abs() < 1e-9);
    }
    #[test]
    fn test_small_map() {
        let mut m: SmallMap<u32, &str> = SmallMap::new();
        m.insert(3, "three");
        m.insert(1, "one");
        m.insert(2, "two");
        assert_eq!(m.get(&2), Some(&"two"));
        assert_eq!(m.len(), 3);
        let keys = m.keys();
        assert_eq!(*keys[0], 1);
        assert_eq!(*keys[2], 3);
    }
    #[test]
    fn test_label_set() {
        let mut ls = LabelSet::new();
        ls.add("foo");
        ls.add("bar");
        ls.add("foo");
        assert_eq!(ls.count(), 2);
        assert!(ls.has("bar"));
        assert!(!ls.has("baz"));
    }
    #[test]
    fn test_config_node() {
        let mut root = ConfigNode::section("root");
        let child = ConfigNode::leaf("key", "value");
        root.add_child(child);
        assert_eq!(root.num_children(), 1);
    }
    #[test]
    fn test_versioned_record() {
        let mut vr = VersionedRecord::new(0u32);
        vr.update(1);
        vr.update(2);
        assert_eq!(*vr.current(), 2);
        assert_eq!(vr.version(), 2);
        assert!(vr.has_history());
        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
    }
    #[test]
    fn test_simple_dag() {
        let mut dag = SimpleDag::new(4);
        dag.add_edge(0, 1);
        dag.add_edge(1, 2);
        dag.add_edge(2, 3);
        assert!(dag.can_reach(0, 3));
        assert!(!dag.can_reach(3, 0));
        let order = dag.topological_sort().expect("order should be present");
        assert_eq!(order, vec![0, 1, 2, 3]);
    }
    #[test]
    fn test_focus_stack() {
        let mut fs: FocusStack<&str> = FocusStack::new();
        fs.focus("a");
        fs.focus("b");
        assert_eq!(fs.current(), Some(&"b"));
        assert_eq!(fs.depth(), 2);
        fs.blur();
        assert_eq!(fs.current(), Some(&"a"));
    }
}
#[cfg(test)]
mod tests_extra_iterators {
    use super::*;
    #[test]
    fn test_window_iterator() {
        let data = vec![1u32, 2, 3, 4, 5];
        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
        assert_eq!(windows.len(), 3);
        assert_eq!(windows[0], &[1, 2, 3]);
        assert_eq!(windows[2], &[3, 4, 5]);
    }
    #[test]
    fn test_non_empty_vec() {
        let mut nev = NonEmptyVec::singleton(10u32);
        nev.push(20);
        nev.push(30);
        assert_eq!(nev.len(), 3);
        assert_eq!(*nev.first(), 10);
        assert_eq!(*nev.last(), 30);
    }
}
#[cfg(test)]
mod tests_padding2 {
    use super::*;
    #[test]
    fn test_sliding_sum() {
        let mut ss = SlidingSum::new(3);
        ss.push(1.0);
        ss.push(2.0);
        ss.push(3.0);
        assert!((ss.sum() - 6.0).abs() < 1e-9);
        ss.push(4.0);
        assert!((ss.sum() - 9.0).abs() < 1e-9);
        assert_eq!(ss.count(), 3);
    }
    #[test]
    fn test_path_buf() {
        let mut pb = PathBuf::new();
        pb.push("src");
        pb.push("main");
        assert_eq!(pb.as_str(), "src/main");
        assert_eq!(pb.depth(), 2);
        pb.pop();
        assert_eq!(pb.as_str(), "src");
    }
    #[test]
    fn test_string_pool() {
        let mut pool = StringPool::new();
        let s = pool.take();
        assert!(s.is_empty());
        pool.give("hello".to_string());
        let s2 = pool.take();
        assert!(s2.is_empty());
        assert_eq!(pool.free_count(), 0);
    }
    #[test]
    fn test_transitive_closure() {
        let mut tc = TransitiveClosure::new(4);
        tc.add_edge(0, 1);
        tc.add_edge(1, 2);
        tc.add_edge(2, 3);
        assert!(tc.can_reach(0, 3));
        assert!(!tc.can_reach(3, 0));
        let r = tc.reachable_from(0);
        assert_eq!(r.len(), 4);
    }
    #[test]
    fn test_token_bucket() {
        let mut tb = TokenBucket::new(100, 0);
        assert_eq!(tb.available(), 100);
        assert!(tb.try_consume(50));
        assert_eq!(tb.available(), 50);
        assert!(!tb.try_consume(60));
        assert_eq!(tb.capacity(), 100);
    }
    #[test]
    fn test_rewrite_rule_set() {
        let mut rrs = RewriteRuleSet::new();
        rrs.add(RewriteRule::unconditional(
            "beta",
            "App(Lam(x, b), v)",
            "b[x:=v]",
        ));
        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
        assert_eq!(rrs.len(), 2);
        assert_eq!(rrs.unconditional_rules().len(), 1);
        assert_eq!(rrs.conditional_rules().len(), 1);
        assert!(rrs.get("beta").is_some());
        let disp = rrs
            .get("beta")
            .expect("element at \'beta\' should exist")
            .display();
        assert!(disp.contains("→"));
    }
}
#[cfg(test)]
mod tests_padding3 {
    use super::*;
    #[test]
    fn test_decision_node() {
        let tree = DecisionNode::Branch {
            key: "x".into(),
            val: "1".into(),
            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
            no_branch: Box::new(DecisionNode::Leaf("no".into())),
        };
        let mut ctx = std::collections::HashMap::new();
        ctx.insert("x".into(), "1".into());
        assert_eq!(tree.evaluate(&ctx), "yes");
        ctx.insert("x".into(), "2".into());
        assert_eq!(tree.evaluate(&ctx), "no");
        assert_eq!(tree.depth(), 1);
    }
    #[test]
    fn test_flat_substitution() {
        let mut sub = FlatSubstitution::new();
        sub.add("foo", "bar");
        sub.add("baz", "qux");
        assert_eq!(sub.apply("foo and baz"), "bar and qux");
        assert_eq!(sub.len(), 2);
    }
    #[test]
    fn test_stopwatch() {
        let mut sw = Stopwatch::start();
        sw.split();
        sw.split();
        assert_eq!(sw.num_splits(), 2);
        assert!(sw.elapsed_ms() >= 0.0);
        for &s in sw.splits() {
            assert!(s >= 0.0);
        }
    }
    #[test]
    fn test_either2() {
        let e: Either2<i32, &str> = Either2::First(42);
        assert!(e.is_first());
        let mapped = e.map_first(|x| x * 2);
        assert_eq!(mapped.first(), Some(84));
        let e2: Either2<i32, &str> = Either2::Second("hello");
        assert!(e2.is_second());
        assert_eq!(e2.second(), Some("hello"));
    }
    #[test]
    fn test_write_once() {
        let wo: WriteOnce<u32> = WriteOnce::new();
        assert!(!wo.is_written());
        assert!(wo.write(42));
        assert!(!wo.write(99));
        assert_eq!(wo.read(), Some(42));
    }
    #[test]
    fn test_sparse_vec() {
        let mut sv: SparseVec<i32> = SparseVec::new(100);
        sv.set(5, 10);
        sv.set(50, 20);
        assert_eq!(*sv.get(5), 10);
        assert_eq!(*sv.get(50), 20);
        assert_eq!(*sv.get(0), 0);
        assert_eq!(sv.nnz(), 2);
        sv.set(5, 0);
        assert_eq!(sv.nnz(), 1);
    }
    #[test]
    fn test_stack_calc() {
        let mut calc = StackCalc::new();
        calc.push(3);
        calc.push(4);
        assert_eq!(calc.add(), Some(7));
        assert_eq!(calc.peek(), Some(7));
        calc.push(2);
        assert_eq!(calc.mul(), Some(14));
        assert_eq!(calc.peek(), Some(14));
    }
}