brink-analyzer 0.0.16

//! NS-A5: the inhabited-range refinement under `types = strict` (E117;
//! issue #1111, `docs/stdlib-spec.md` §7, F7/F8 ruled 2026-07-19).
//!
//! `rand::int` — spelled `int(r)` over a range — is **total by type**: its
//! parameter is the language's first value refinement, the inhabited range
//! (`NonEmptyRange`, the S2 spelling). This module is the strict-mode
//! evidence check, and deliberately THE TEMPLATE for every future value
//! refinement (F8's general rule):
//!
//! - **Strict-only.** Under `types = gradual` this module is never invoked
//!   — the refinement is inert and the runtime fault
//!   (`RuntimeError::EmptyRangeDraw`) is the residual. This is exactly the
//!   `int()`/E078 precedent (`conversions`), whose structure this module
//!   mirrors seam for seam.
//! - **Evidence is minted, never asserted.** A range literal in argument
//!   position with statically-foldable bounds (integer literals, unary
//!   minus, CONST refs — "CONST refs fold" per the F7 ruling) coerces in
//!   free when provably inhabited, and is E117 when provably empty
//!   (`int(0..0)` — the "statically-empty literal" compile error). A
//!   non-literal argument must carry `Ty::Range { non_empty: true }`
//!   evidence from the inference substrate — minted by a provably-inhabited
//!   literal initializer or by `non_empty(r)`'s `some` payload
//!   (parse-don't-validate: the Option tax sits once at the boundary).
//! - **Unknown stays unchecked.** An `Unknown`/`Conflicted`-typed argument
//!   is left to the escape checks (E065/E066) and the runtime backstop —
//!   the same "Unknown never disagrees" posture `conversions`/`structs`
//!   take. A non-range-typed argument is the *conversion* leg of `int(x)`
//!   and belongs to E078's domain check, not this one.
//!
//! Shadowing: an unresolved call to `int` is the builtin; a resolved one
//! (an author-defined `int` knot) is an ordinary call, never checked here.

use std::collections::BTreeMap;

use brink_format::DefinitionId;
use brink_ir::hir::visit::{self, HirVisitor};
use brink_ir::{
    Diagnostic, DiagnosticCode, Expr, FileId, HirFile, Knot, PrefixOp, ResolutionMap, Stitch,
    SymbolIndex, SymbolKind,
};

use crate::annotations;
use crate::infer::{InferenceResult, InferredSig, Ty};
use crate::structs::{self, MistypeCtx};
use rowan::TextRange;

/// Strict-mode-only range-refinement checks over every `int(r)` call in the
/// project. Callers only reach this once `strict::config_error` has
/// confirmed `types = strict` + `dialect = brink` (mirrors
/// `conversions::check`'s entry condition — same wiring point,
/// `strict::check`).
#[must_use]
pub fn check(
    files: &[(FileId, &HirFile)],
    index: &SymbolIndex,
    inference: &InferenceResult,
    resolutions: &ResolutionMap,
) -> Vec<Diagnostic> {
    let globals = crate::infer::collect_globals(files, index, None);
    // The CONST fold table (the "CONST refs fold" leg of the F7 evidence
    // rule): every project CONST whose initializer folds to an int, keyed
    // by `(declaring file, name)` — the pair a resolved `DefinitionId`'s
    // `SymbolInfo` gives back. Built once; deterministic (BTreeMap).
    let mut const_ints: BTreeMap<(FileId, String), i64> = BTreeMap::new();
    for &(file, hir) in files {
        for c in &hir.constants {
            if let Some(v) = fold_literal_bound(&c.value) {
                const_ints.insert((file, c.name.text.clone()), v);
            }
        }
    }
    let mut out = Vec::new();
    for &(file, hir) in files {
        let resolution_by_range = resolution_index(resolutions, file);
        let mut v = RefinementVisitor {
            file,
            index,
            globals: &globals,
            signatures: &inference.signatures,
            bodies: &inference.bodies,
            resolution_by_range: &resolution_by_range,
            const_ints: &const_ints,
            current_knot_name: None,
            knot_locals: None,
            stitch_locals: None,
            lambda_locals: Vec::new(),
            diagnostics: &mut out,
        };
        // Issue #2098: `RefinementVisitor::enter_expr` has no state that
        // needs resetting between the block tree and a file-level
        // declaration's own initializer (`locals` is already `None` at this
        // scope) — so the shared entry point covers both in one drive, and
        // the hand-rolled `check_expr`/`expr_children` mirror of
        // `visit::visit`'s own descent this used to need is gone.
        visit::visit_with_decl_initializers(hir, &mut v);
    }
    out
}

/// Everything the bound folder needs to resolve a CONST reference.
struct FoldCtx<'a> {
    index: &'a SymbolIndex,
    resolution_by_range: &'a BTreeMap<(u32, u32), DefinitionId>,
    const_ints: &'a BTreeMap<(FileId, String), i64>,
}

struct RefinementVisitor<'a> {
    file: FileId,
    index: &'a SymbolIndex,
    globals: &'a BTreeMap<DefinitionId, Ty>,
    signatures: &'a BTreeMap<DefinitionId, InferredSig>,
    bodies: &'a BTreeMap<DefinitionId, crate::infer::BodyTypes>,
    resolution_by_range: &'a BTreeMap<(u32, u32), DefinitionId>,
    const_ints: &'a BTreeMap<(FileId, String), i64>,
    current_knot_name: Option<String>,
    knot_locals: Option<&'a BTreeMap<String, Ty>>,
    stitch_locals: Option<&'a BTreeMap<String, Ty>>,
    /// Issue #2773: a stack of pruned-locals frames, one per currently-open
    /// lambda literal (innermost last). Mirrors
    /// `structs::ConstructionVisitor`'s identical field/hook pair exactly —
    /// see that field's own doc.
    lambda_locals: Vec<BTreeMap<String, Ty>>,
    diagnostics: &'a mut Vec<Diagnostic>,
}

impl<'a> RefinementVisitor<'a> {
    fn current_locals(&self) -> Option<&BTreeMap<String, Ty>> {
        self.lambda_locals
            .last()
            .or_else(|| self.stitch_locals.or(self.knot_locals))
    }

    fn fold_ctx(&self) -> FoldCtx<'a> {
        FoldCtx {
            index: self.index,
            resolution_by_range: self.resolution_by_range,
            const_ints: self.const_ints,
        }
    }

    fn knot_def_id(&self, knot: &Knot) -> Option<DefinitionId> {
        let kind = knot.symbol_kind();
        annotations::def_id_for(self.index, self.file, kind, &knot.name.text)
    }
}

impl HirVisitor for RefinementVisitor<'_> {
    fn visit_exprs(&self) -> bool {
        true
    }

    fn enter_knot(&mut self, knot: &Knot) {
        self.current_knot_name = Some(knot.name.text.clone());
        self.knot_locals = self
            .knot_def_id(knot)
            .and_then(|id| self.bodies.get(&id))
            .map(|b| &b.locals);
    }

    fn exit_knot(&mut self, _knot: &Knot) {
        self.current_knot_name = None;
        self.knot_locals = None;
    }

    fn enter_stitch(&mut self, stitch: &Stitch) {
        self.stitch_locals = self.current_knot_name.as_ref().and_then(|knot_name| {
            let qualified = format!("{knot_name}.{}", stitch.name.text);
            annotations::def_id_for(self.index, self.file, SymbolKind::Stitch, &qualified)
                .and_then(|id| self.bodies.get(&id))
                .map(|b| &b.locals)
        });
    }

    fn exit_stitch(&mut self, _stitch: &Stitch) {
        self.stitch_locals = None;
    }

    fn enter_expr(&mut self, expr: &Expr) {
        // Built from direct field projections (not `self.ctx()`) so the
        // borrow checker sees this only borrows the locals-shaped fields,
        // disjoint from the `self.diagnostics` reborrow below — see
        // `structs::ConstructionVisitor::enter_expr`'s identical comment.
        let ctx = MistypeCtx {
            index: self.index,
            globals: self.globals,
            signatures: self.signatures,
            resolution_by_range: self.resolution_by_range,
            locals: self
                .lambda_locals
                .last()
                .or_else(|| self.stitch_locals.or(self.knot_locals)),
        };
        let fold = self.fold_ctx();
        check_call(expr, self.file, &ctx, &fold, self.diagnostics);
    }

    /// ⚠ VACUOUS TODAY, kept deliberately (issue #2773 review finding).
    ///
    /// Unlike this fix's sibling consumers, E117 has **no reachable
    /// fixture**: a range literal (`a..b`) parses only on the ink/brink
    /// surface (`brink-syntax`), while a lambda literal (`|x| …`) parses
    /// only on the native surface (`brink-syntax-native`) — the two are
    /// mutually exclusive, so no source can put a range inside a lambda
    /// body. `brink-syntax-native` has no `..` grammar at all, and
    /// `annotations::resolve` has no `Range` arm, so a lambda param cannot
    /// be annotated into `Ty::Range` either. `check_call`'s other leg needs
    /// `Ty::Range { non_empty: false }`, which is only ever minted from a
    /// range literal or `non_empty(...)` — both `..`-dependent.
    ///
    /// The frame is therefore installed for **uniformity, not coverage**:
    /// the moment the native surface grows range literals, this consumer
    /// would otherwise inherit the shadowing hazard silently, exactly as
    /// this file and `contains_domain.rs` did before #2773 — so the hooks
    /// stay rather than being removed and re-derived later.
    /// `crates/brink-compiler/tests/driver.rs`'s
    /// `compile_ink_brink_range_refinement_direct_var_initializer_is_e117`
    /// records the same surface-disjointness finding for issue #1774.
    ///
    /// Stated here rather than papered over with a "test" that would only
    /// prove the two surfaces don't mix.
    fn enter_lambda(&mut self, l: &brink_ir::LambdaExpr) {
        let pruned = structs::pruned_locals_for_lambda(l, self.index, self.current_locals());
        self.lambda_locals.push(pruned);
    }

    fn exit_lambda(&mut self, _l: &brink_ir::LambdaExpr) {
        self.lambda_locals.pop();
    }
}

/// If `expr` is an unresolved (builtin) call to `int` whose single argument
/// is range-shaped, run the refinement check (module doc). Everything else
/// — resolved (shadowed) calls, other names, wrong arity (E031's job), a
/// conversion-leg argument (E078's domain), an `Unknown`-typed argument —
/// is silently clean here.
fn check_call(
    expr: &Expr,
    file: FileId,
    ctx: &MistypeCtx<'_>,
    fold: &FoldCtx<'_>,
    out: &mut Vec<Diagnostic>,
) {
    let Expr::Call(path, args) = expr else {
        return;
    };
    let [seg] = path.segments.as_slice() else {
        return;
    };
    if seg.text != "int" {
        return;
    }
    if ctx.resolution_by_range.contains_key(&range_key(path.range)) {
        return; // author-shadowed — an ordinary call
    }
    let [arg] = args.as_slice() else {
        return; // wrong arity — E031's job
    };

    // Leg (a): a range literal directly in argument position — fold the
    // bounds (literals + CONST refs).
    if let Expr::Range(r) = arg {
        match (fold_bound(&r.start, fold), fold_bound(&r.end, fold)) {
            (Some(start), Some(end)) => {
                let inhabited = if r.inclusive {
                    start <= end
                } else {
                    start < end
                };
                if !inhabited {
                    out.push(diag(
                        file,
                        path.range,
                        format!(
                            "{}: this range is provably empty — `int` draws one element, \
                             and there is nothing to draw",
                            DiagnosticCode::E117.title(),
                        ),
                    ));
                }
            }
            _ => {
                // Computed bounds written literally in position:
                // `int(a..b)` — no evidence can be minted statically.
                out.push(diag(
                    file,
                    path.range,
                    format!(
                        "{}: these bounds are not statically provable — validate with \
                         `non_empty(a..b)` and draw from its `some` payload",
                        DiagnosticCode::E117.title(),
                    ),
                ));
            }
        }
        return;
    }

    // Leg (b): a non-literal argument — the evidence must already be on
    // its inferred type.
    // Evidence carried (`non_empty: true`) is free; a non-range type is
    // the conversion leg (E078's domain, not ours); Unknown/Conflicted/
    // unclassifiable is left to the escape checks + the runtime fault.
    // Only the evidence-free range errs.
    if let Some(Ty::Range { non_empty: false }) = structs::classify_expr_ty(arg, ctx) {
        out.push(diag(
            file,
            path.range,
            format!(
                "{}: this range is possibly empty — validate with `non_empty(r)` \
                 (the evidence is minted once; every later draw is free)",
                DiagnosticCode::E117.title(),
            ),
        ));
    }
}

/// `TextRange` has no `Ord`; the `(start, end)` pair is the map key — the
/// same private copy every sibling checker keeps (`conversions`, `structs`,
/// `strict`…).
fn range_key(range: TextRange) -> (u32, u32) {
    (range.start().into(), range.end().into())
}

/// One file's resolutions re-keyed by [`range_key`] — the same private copy
/// `conversions::resolution_index` keeps.
fn resolution_index(
    resolutions: &ResolutionMap,
    file: FileId,
) -> BTreeMap<(u32, u32), DefinitionId> {
    resolutions
        .iter()
        .filter(|r| r.file == file)
        .map(|r| (range_key(r.range), r.target))
        .collect()
}

fn diag(file: FileId, range: TextRange, message: String) -> Diagnostic {
    Diagnostic {
        file,
        range,
        message,
        code: DiagnosticCode::E117,
    }
}

/// Fold a range bound to its compile-time int value: an integer literal, a
/// unary-negated foldable bound, or a resolved CONST whose own initializer
/// folds ("CONST refs fold" — the F7 evidence rule). `None` for anything
/// else.
fn fold_bound(expr: &Expr, fold: &FoldCtx<'_>) -> Option<i64> {
    match expr {
        Expr::Path(p) => {
            let def = fold.resolution_by_range.get(&range_key(p.range))?;
            let info = fold.index.symbols.get(def)?;
            if info.kind != SymbolKind::Constant {
                return None;
            }
            fold.const_ints
                .get(&(info.file, info.name.clone()))
                .copied()
        }
        _ => fold_literal_bound(expr),
    }
}

/// The literal-only fold shared with the CONST-table builder: an integer
/// literal or a unary-negated one. `i64` so `-2147483648` folds cleanly.
fn fold_literal_bound(expr: &Expr) -> Option<i64> {
    match expr {
        Expr::Int(n) => Some(i64::from(*n)),
        Expr::Prefix(PrefixOp::Negate, inner) => fold_literal_bound(inner).map(|n| -n),
        _ => None,
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use brink_ir::hir::lower;

    /// Real resolutions + a whole-project [`InferenceResult`] — mirrors
    /// `conversions::tests::build_with_inference`. This module had no unit
    /// tests at all before issue #2793's audit (coverage previously lived
    /// only in `crates/brink-compiler/tests/driver.rs`'s
    /// `compile_ink_brink_range_refinement_direct_var_initializer_is_e117`)
    /// — this harness is new, not a refactor of an existing one.
    fn check_all(src: &str) -> Vec<Diagnostic> {
        let parsed = brink_syntax::parse(src);
        let (hir, manifest, _diag) = lower(FileId(0), &parsed.tree());
        let (index, _diag) = crate::symbol_index(&[(FileId(0), &manifest)]);
        let (resolutions, _diag) =
            crate::resolve(FileId(0), &manifest, &index, &crate::ImportScope::default());
        let inference = crate::infer_project(
            &[(FileId(0), &hir)],
            &index,
            &resolutions,
            None,
            &BTreeMap::new(),
        );
        check(&[(FileId(0), &hir)], &index, &inference, &resolutions)
    }

    // ─── issue #2793: the ordinary (non-lambda) fn/knot annotated-param
    // half of #2786's `BodyTypes::locals` visibility fix — structurally
    // vacuous here, same as the lambda half `enter_lambda`'s own doc
    // records ────────────────────────────────────────────────────────

    /// #2793 audit finding for this file specifically: unlike its five
    /// sibling consumers, an *ordinary* `fn`/knot param's own written
    /// annotation can **never** make a new `E117` positive reachable here,
    /// for the identical reason [`RefinementVisitor::enter_lambda`]'s own
    /// doc records for the *lambda* half — `annotations::resolve` has no
    /// `Range` arm at all (only `Named`/`Generic`/`Fn` `TypeExpr` shapes
    /// resolve, and none of those names `Range`), so a param can never be
    /// *annotated* into `Ty::Range { non_empty: false }` — the one shape
    /// [`check_call`]'s leg (b) treats as evidence-free and flags. `r`'s
    /// declared `int` annotation therefore reaches `pass.locals` (via
    /// #2786's own overlay, same as every other consumer) but is simply the
    /// wrong *kind* of evidence for this check to act on — `int(r)` here is
    /// TM-3's plain conversion leg (`conversions.rs`'s own E078 domain,
    /// which `int` already permits), not the range-draw leg at all. Pinned
    /// as a negative control rather than left undocumented, mirroring
    /// `enter_lambda`'s own "stated here rather than papered over with a
    /// 'test' that would only prove the two surfaces don't mix" posture.
    #[test]
    fn annotated_fn_param_non_range_type_never_reaches_e117() {
        let diags = check_all("=== main(r: int) ===\n~ x = int(r)\n-> DONE\n");
        assert!(diags.is_empty(), "{diags:?}");
    }

    /// Positive control alongside
    /// [`annotated_fn_param_non_range_type_never_reaches_e117`]: `check`
    /// still does its job on the one evidence-free shape it *can* see — a
    /// provably-empty range *literal* directly in argument position (leg
    /// (a), no annotation or locals involved at all) — so the test above is
    /// pinning a real absence of reach, not a broken harness.
    #[test]
    fn empty_range_literal_argument_is_still_e117() {
        let diags = check_all("=== main ===\n~ x = int(0..0)\n-> DONE\n");
        assert_eq!(diags.len(), 1, "{diags:?}");
        assert_eq!(diags[0].code, DiagnosticCode::E117);
    }
}