vj-codegen 0.1.0

//! T3 (`docs/superpowers/plans/2026-10-03-sva.md`): recovering a sequence
//! `##`-delay or `[...]`-repetition operator's `(min, max)` bounds.
//!
//! LRM 16.7's `cycle_delay_range` and 16.9.2's `consecutive_repetition`/
//! `nonconsecutive_repetition`/`goto_repetition` are bound by slang into a
//! plain `uint32_t min; std::optional<uint32_t> max;` struct
//! (`slang::ast::SequenceRange`, `include/slang/ast/expressions/
//! AssertionExpr.h`) stored directly on the folded AST node (`
//! SimpleAssertionExpr::repetition`, `SequenceConcatExpr::Element::delay`)
//! -- already an elaboration-time integer, with no accessor exposing it:
//! `sv_lang::AssertionExpr`'s whole surface is `.kind()`/`.op()`/
//! `.children()`/`.syntax()` (checked against the real tree, not assumed;
//! see the plan's §1.1). This module recovers the same bounds
//! independently, by walking the *syntax* tree slang already exposes
//! (`sv_lang::nodes::{SequenceRepetitionSyntax, DelayedSequenceElementSyntax,
//! ...}`, generated typed accessors) and folding the bound
//! `constant_expression`(s) with a small, closed evaluator. That's legal
//! because 16.7/16.9.2 require every such bound to be an elaboration-time
//! integer constant, so this folder's input domain is exactly: an integer
//! literal, a named parameter/constant reference, a `+`/`-`/`*` combination
//! of those (optionally parenthesized), and the `$` token (meaning
//! "unbounded") -- never a general expression.
//!
//! This workaround lives entirely in `sv-sim-codegen`; it adds no file to
//! `sv-lang`, `sv-lang-sys`, or `sv-lang-kinds` (plan §1.1).
//!
//! ## Formal arguments (T12, LRM 16.8)
//!
//! Inside a named sequence declaration a bound may name one of the
//! sequence's FORMAL arguments (`x ##delay1 y[*min:max]`). slang substitutes
//! actuals into the semantic tree but not into these syntax-level bounds, so
//! the folder takes a [`FormalEnv`]: the stack of named-sequence instances
//! being expanded, each with its formals' [`Bound`] values. An identifier
//! resolves in the frame whose DECLARATION text contains it (a bound written
//! in a sequence ACTUAL is call-site text, so it lands in the caller's
//! frame, 16.8's "evaluated in the context of the instance"); a formal
//! shadows a same-named module constant, and an identifier that no frame
//! binds falls through to `scope.find`, exactly as before. Every pre-T12
//! entry point is a wrapper over an empty environment.
//!
//! T3 is a pure foundation task: its own consumer is T9/T10's automaton
//! builder (`sva::build::build_automaton`, not yet written), so nothing
//! outside this module's own `#[cfg(test)] mod tests` calls these public
//! functions yet. `#![allow(dead_code)]` below reflects exactly that --
//! not a correctness gap, since the inline tests are this task's own
//! required proof of correctness (same precedent as `sched::
//! reschedule_req_proposal`'s module doc comment).
#![allow(dead_code)]

use std::ops::Range;

use sv_lang::kinds::{AssertionExprKind, SymbolKind, SyntaxKind};
use sv_lang::nodes::{
    ArgumentSyntax, BinaryExpressionSyntax, ConditionalExpressionSyntax,
    DelayedSequenceElementSyntax, DelayedSequenceExprSyntax, FunctionDeclarationSyntax,
    IdentifierNameSyntax, IntegerVectorExpressionSyntax, InvocationExpressionSyntax,
    ParenthesizedExpressionSyntax, ParenthesizedSequenceExprSyntax, PrefixUnaryExpressionSyntax,
    PropertyExprSyntax, PropertySpecSyntax, SelectorSyntax, SequenceRepetitionSyntax,
    SimplePropertyExprSyntax, SimpleSequenceExprSyntax,
};
use sv_lang::{AssertionExpr, AstNode, Node, ScriptSession, Symbol};

use super::trees::{Trees, key};

use crate::error::LoweringError;

/// What one formal argument of a named sequence instance stands for, as far as
/// a `##`/`[...]` bound is concerned (T12, LRM 16.8).
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Bound {
    /// An elaboration-time integer (already cast to the formal's type when it
    /// is typed, 16.8.1).
    Value(i64),
    /// The `$` actual: legal only as the upper bound of a range.
    Dollar,
    /// An actual that is not an elaboration-time integer (a signal, a
    /// sequence, an event, `$` into a typed formal ...). Harmless unless a
    /// bound names the formal, in which case the lookup fails with this text.
    Unfoldable(String),
}

/// One declaration on a dependency chain (see [`FormalFrame::origins`]): its
/// name (for messages) and its byte range in the syntax tree (its identity).
pub type ChainLink = (String, Range<usize>);

/// One named-sequence instance being expanded: its declaration's byte range
/// in the syntax tree and its formals' bindings.
#[derive(Debug, Clone)]
pub struct FormalFrame {
    pub name: String,
    pub decl: Range<usize>,
    pub bindings: Vec<(String, Bound)>,
    /// For each formal, the chain of declarations that LRM 16.8's dependency
    /// graph puts above an instance written as that formal's actual: the chain
    /// at the call site plus the instantiated declaration itself (an instance
    /// of X that instantiates Y within an actual argument is an edge X -> Y).
    /// A reference to the formal expands the actual under THIS chain, not the
    /// chain of the body that happens to hold the reference.
    pub origins: Vec<(String, Vec<ChainLink>)>,
}

/// The stack of [`FormalFrame`]s of the instances currently being expanded,
/// outermost first (see the module doc).
#[derive(Debug, Clone, Default)]
pub struct FormalEnv {
    frames: Vec<FormalFrame>,
}

impl FormalEnv {
    pub fn push(&mut self, frame: FormalFrame) {
        self.frames.push(frame);
    }

    pub fn pop(&mut self) {
        self.frames.pop();
    }

    pub fn depth(&self) -> usize {
        self.frames.len()
    }

    /// The frame for an identifier written at byte range `at`: the INNERMOST
    /// frame whose declaration contains `at`. (A declaration can be on the
    /// stack twice: `outer(inner(a))` expands `inner` for the actual inside
    /// `outer`'s own expansion of `inner`; the text being folded belongs to the
    /// expansion in progress.)
    fn frame_at(&self, at: &Range<usize>) -> Option<&FormalFrame> {
        self.frames
            .iter()
            .rev()
            .find(|f| f.decl.start <= at.start && at.end <= f.decl.end)
    }

    /// The binding of formal `name` for an identifier written at byte range
    /// `at`: the frame whose declaration contains `at`, if it binds `name`.
    fn lookup(&self, at: &Range<usize>, name: &str) -> Option<&Bound> {
        self.frame_at(at)?
            .bindings
            .iter()
            .find(|(n, _)| n == name)
            .map(|(_, b)| b)
    }

    /// The dependency chain the actual bound to formal `name` is expanded
    /// under (see [`FormalFrame::origins`]), for an identifier written at
    /// byte range `at`; `None` when the identifier is not a formal of the
    /// frame whose declaration contains it.
    pub fn origin_of(&self, at: &Range<usize>, name: &str) -> Option<&[ChainLink]> {
        self.frame_at(at)?
            .origins
            .iter()
            .find(|(n, _)| n == name)
            .map(|(_, o)| o.as_slice())
    }
}

/// The `bit_width`/signedness a typed integral formal casts its actual to
/// (16.8.1).
#[derive(Debug, Clone, Copy)]
pub struct FormalCast {
    pub width: u64,
    pub signed: bool,
}

/// Binds one formal to the actual argument whose syntax is `actual` (`None`
/// when the actual has no expression syntax: a sequence, an event). The
/// actual is folded in `env`, the CALLER's environment -- the frame of the
/// instance being bound is not pushed yet. `cast` is `Some` for a typed
/// integral formal: the value is cast to its type (`bit`: truncated to one
/// bit; `shortint`: 16 bits, sign-extended), and `$` is refused (16.8: a `$`
/// actual needs an untyped formal).
pub fn bind_actual(
    actual: Option<Node<'_>>,
    cast: Option<FormalCast>,
    scope: &Symbol,
    env: &FormalEnv,
) -> Bound {
    let Some(node) = actual else {
        return Bound::Unfoldable("the actual argument is not an expression".into());
    };
    match fold(node, scope, env) {
        Err(e) => Bound::Unfoldable(e.message),
        Ok(FoldedConst::Dollar) if cast.is_some() => Bound::Unfoldable(
            "`$` is bound to a typed formal argument (16.8: a `$` actual requires an untyped \
             formal)"
                .into(),
        ),
        Ok(FoldedConst::Dollar) => Bound::Dollar,
        Ok(FoldedConst::Value(v)) => Bound::Value(match cast {
            Some(c) => cast_value(v, c),
            None => v,
        }),
    }
}

/// `v` cast to a `c.width`-bit integer: truncation, then sign extension for a
/// signed type. Widths of 64 or more leave `v` as is.
fn cast_value(v: i64, c: FormalCast) -> i64 {
    if c.width == 0 || c.width >= 64 {
        return v;
    }
    let mask = (1i64 << c.width) - 1;
    let low = v & mask;
    if c.signed && low >> (c.width - 1) == 1 {
        low - (1i64 << c.width)
    } else {
        low
    }
}

/// The [`FormalFrame`] of a checker instance (LRM 17.2, 17.3): its formals bound
/// to the instance's actuals as far as a `##`/`[...]` bound is concerned (an
/// elaboration-time integer, or `$` for an upper bound), over the byte range
/// `decl` of the checker declaration. A formal whose actual is not such a
/// constant (a signal, an event, an omitted default) is `Unfoldable`, harmless
/// unless a bound names it.
pub fn checker_frame(
    instance: &Symbol,
    decl: Range<usize>,
    trees: &[sv_lang::SyntaxTree],
) -> FormalFrame {
    let formals = instance.members().filter(|m| {
        matches!(
            m.kind(),
            sv_lang::kinds::SymbolKind::AssertionPort | sv_lang::kinds::SymbolKind::FormalArgument
        )
    });
    let bindings = formals
        .zip(instance.checker_instance_connections())
        .map(|(f, conn)| {
            // An untyped formal's actual is an assertion expression (a `Simple`
            // wrapper around the expression), a typed one's an expression.
            let expr = conn.actual().and_then(|a| {
                a.as_expression().or_else(|| {
                    a.as_assertion_expr()
                        .filter(|x| x.kind() == AssertionExprKind::Simple)
                        .and_then(|x| {
                            x.as_sem_node()
                                .children()
                                .into_iter()
                                .find_map(|c| c.as_expression())
                        })
                })
            });
            let node = expr.and_then(|e| trees.iter().find_map(|t| e.syntax(t)));
            let b = match (node, instance.parent()) {
                (Some(n), Some(s)) => bind_actual(Some(n), None, &s, &FormalEnv::default()),
                _ => Bound::Unfoldable("the checker formal has no explicit actual (17.3)".into()),
            };
            (f.name().to_string(), b)
        })
        .collect();
    FormalFrame {
        name: instance.name().to_string(),
        decl,
        bindings,
        origins: Vec::new(),
    }
}

/// The recovered bounds of one `##`/`[...]` operator (16.7, 16.9.2): `min`
/// cycles/repetitions, and `max` -- `None` for the unbounded `$` form
/// (`##[0:$]`, `[*]`, ...).
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct SequenceRangeValue {
    pub min: u32,
    pub max: Option<u32>,
}

/// Recovers every delay/repetition range directly attached to one
/// `AssertionExpr` node -- the entry point T9/T10's automaton builder calls
/// once per `Simple`/`SequenceConcat` node it walks:
///
/// - [`AssertionExprKind::Simple`]: the sequence's own optional `[*n]`/
///   `[+]`/`[->n]`/`[=n]` repetition (16.9.2) -- an empty `Vec` if the
///   simple sequence has none (legal: a bare boolean leaf has no
///   repetition at all).
/// - [`AssertionExprKind::SequenceConcat`]: one range per `##` operator in
///   the concatenation chain (16.7), in source order
///   (`DelayedSequenceExprSyntax::elements().len()` entries -- the chain's
///   first operand itself has no preceding delay, matching
///   `AssertionExpr::children()`'s own `[first, elements[0].sequence, ...]`
///   shape, confirmed live against a compiled `a ##3 b`).
///
/// Any other `AssertionExprKind`, or a semantic/syntax shape this
/// function's own cast chain cannot follow (a future slang change, or
/// `expr` carrying no syntax node in `tree` at all), is a named
/// [`LoweringError`], never a panic: this module's whole reason to exist is
/// recovering a value slang's typed accessors do not expose, so an
/// unexpected shape here is exactly the "shout, don't guess" case
/// ARCHITECTURE §7 item 9 requires of every kind-enum match.
pub fn sequence_range_of<'d>(
    expr: AssertionExpr<'d>,
    tree: Trees<'_>,
    scope: &Symbol<'d>,
) -> Result<Vec<SequenceRangeValue>, LoweringError> {
    sequence_range_of_in(expr, tree, scope, &FormalEnv::default())
}

/// [`sequence_range_of`] with the bounds' formal-argument references resolved
/// in `env` (see the module doc).
pub fn sequence_range_of_in<'d>(
    expr: AssertionExpr<'d>,
    tree: Trees<'_>,
    scope: &Symbol<'d>,
    env: &FormalEnv,
) -> Result<Vec<SequenceRangeValue>, LoweringError> {
    let syn = tree.syntax(&expr).ok_or_else(|| {
        LoweringError::unsupported_at(
            "sequence range recovery: assertion expression has no syntax node in the given tree",
            scope,
        )
    })?;
    // T10: a plain `( ... )` around a simple sequence or a `##` chain is
    // transparent in the semantic tree (slang binds `(a ##1 b)` to the same
    // `SequenceConcat` as `a ##1 b`) but still present in the syntax tree.
    let syn = peel_sequence_parens(syn);
    match expr.kind() {
        AssertionExprKind::Simple => {
            let simple = SimpleSequenceExprSyntax::cast(syn)
                .ok_or_else(|| cast_mismatch("SimpleSequenceExprSyntax", syn.kind(), scope))?;
            match simple.repetition() {
                Some(rep) => Ok(vec![repetition_range_in(rep, scope, env)?]),
                None => Ok(Vec::new()),
            }
        }
        AssertionExprKind::SequenceConcat => {
            let concat = DelayedSequenceExprSyntax::cast(syn)
                .ok_or_else(|| cast_mismatch("DelayedSequenceExprSyntax", syn.kind(), scope))?;
            concat
                .elements()
                .into_iter()
                .map(|elem| delay_range_in(elem, scope, env))
                .collect()
        }
        other => Err(LoweringError::unsupported_at(
            &format!(
                "sequence range recovery: expected an AssertionExprKind of Simple or \
                 SequenceConcat (the only two shapes that carry a 16.7/16.9.2 range), found {other:?}"
            ),
            scope,
        )),
    }
}

/// Strips every outer `( sequence_expr )` that carries neither a match-item
/// list nor a `[...]` repetition (16.7's `"(" sequence_expr { "," match_item }
/// ")" [ sequence_abbrev ]`, used with both optional parts absent), returning
/// the first node that is not such a paren. A paren WITH a repetition or a
/// match list is a different construct (`AssertionExprKind::SequenceWithMatch`)
/// and is returned unchanged.
///
/// Confirmed live against slang: `(a ##1 b)` binds to the same
/// `SequenceConcat` semantic node as `a ##1 b`, with a
/// `ParenthesizedSequenceExpr` syntax node; likewise `(a[*2])` binds to a
/// `Simple` whose syntax is the paren around the `SimpleSequenceExpr` that
/// actually owns the `[*2]`. Nested parens (`((a ##1 b))`) peel repeatedly.
///
/// T12: the same holds one level up. An assertion's root whose property is
/// nothing but a sequence (`assert property (rule);`, no `@(...)` and no
/// `disable iff` of its own) is bound to the sequence's own semantic node,
/// but its syntax node is the whole `PropertySpec` (the two cover the same
/// text), so a `PropertySpec` with neither a clocking event nor a `disable
/// iff` and a simple-sequence property is peeled to that sequence as well.
pub fn peel_sequence_parens<'t>(syn: Node<'t>) -> Node<'t> {
    let mut cur = syn;
    loop {
        if let Some(spec) = PropertySpecSyntax::cast(cur) {
            if spec.clocking().is_some() || spec.disable().is_some() {
                break;
            }
            match spec.expr() {
                PropertyExprSyntax::SimplePropertyExpr(simple) => cur = simple.syntax(),
                _ => break,
            }
        } else if let Some(simple) = SimplePropertyExprSyntax::cast(cur) {
            cur = simple.expr().syntax();
        } else if let Some(paren) = ParenthesizedSequenceExprSyntax::cast(cur) {
            if paren.repetition().is_some() || paren.match_list().is_some() {
                break;
            }
            cur = paren.expr().syntax();
        } else {
            break;
        }
    }
    cur
}

fn cast_mismatch(expected: &str, found: SyntaxKind, scope: &Symbol) -> LoweringError {
    LoweringError::unsupported_at(
        &format!("sequence range recovery: expected {expected} syntax, found {found:?}"),
        scope,
    )
}

/// Recovers the `(min, max)` of one `[*n]`/`[*n:m]`/`[*]`/`[+]`/
/// `[->n[:m]]`/`[=n[:m]]` syntax node (16.9.2's `boolean_abbrev`/
/// `sequence_abbrev` productions: `consecutive_repetition`,
/// `nonconsecutive_repetition`, `goto_repetition`).
pub fn repetition_range<'t>(
    rep: SequenceRepetitionSyntax<'t>,
    scope: &Symbol,
) -> Result<SequenceRangeValue, LoweringError> {
    repetition_range_in(rep, scope, &FormalEnv::default())
}

/// [`repetition_range`] with formal-argument references resolved in `env`.
pub fn repetition_range_in<'t>(
    rep: SequenceRepetitionSyntax<'t>,
    scope: &Symbol,
    env: &FormalEnv,
) -> Result<SequenceRangeValue, LoweringError> {
    let op = rep.op().map(|t| t.text()).ok_or_else(|| {
        LoweringError::unsupported_at("sequence repetition: `[...]` has no operator token", scope)
    })?;
    match rep.selector() {
        None => match op {
            // `[*]` == `[*0:$]` (16.9.2, consecutive_repetition's bare form).
            "*" => Ok(SequenceRangeValue { min: 0, max: None }),
            // `[+]` == `[*1:$]` (16.9.2, consecutive_repetition's bare form).
            "+" => Ok(SequenceRangeValue { min: 1, max: None }),
            other => Err(LoweringError::unsupported_at(
                &format!(
                    "sequence repetition: bare `[{other}]` has no selector -- only `[*]`/`[+]` \
                     are legal without one per 16.9.2's grammar"
                ),
                scope,
            )),
        },
        Some(sel) => range_of_selector(sel, scope, env),
    }
}

/// Recovers the `(min, max)` of one `##N`/`##[m:n]`/`##[*]`/`##[+]` syntax
/// node (16.7's `cycle_delay_range` production).
pub fn delay_range<'t>(
    elem: DelayedSequenceElementSyntax<'t>,
    scope: &Symbol,
) -> Result<SequenceRangeValue, LoweringError> {
    delay_range_in(elem, scope, &FormalEnv::default())
}

/// [`delay_range`] with formal-argument references resolved in `env`.
pub fn delay_range_in<'t>(
    elem: DelayedSequenceElementSyntax<'t>,
    scope: &Symbol,
    env: &FormalEnv,
) -> Result<SequenceRangeValue, LoweringError> {
    // `## constant_expression` -- a single fixed delay.
    if let Some(delay_val) = elem.delay_val() {
        let n = fold_to_u32(delay_val.syntax(), scope, env)?;
        return Ok(SequenceRangeValue {
            min: n,
            max: Some(n),
        });
    }
    // `##[*]` / `##[+]` -- the bare bracketed forms (no `m:n` selector).
    if let Some(op) = elem.op() {
        return match op.text() {
            "*" => Ok(SequenceRangeValue { min: 0, max: None }), // `##[0:$]`
            "+" => Ok(SequenceRangeValue { min: 1, max: None }), // `##[1:$]`
            other => Err(LoweringError::unsupported_at(
                &format!("cycle delay range: unexpected `##[{other}]` operator"),
                scope,
            )),
        };
    }
    // `##[m:n]` / `##[m:$]` -- the ranged bracketed form.
    let range = elem.range().ok_or_else(|| {
        LoweringError::unsupported_at(
            "cycle delay range: `##[...]` has neither a `*`/`+` operator nor an `m:n` range",
            scope,
        )
    })?;
    range_of_selector(range, scope, env)
}

pub(super) fn range_of_selector<'t>(
    sel: SelectorSyntax<'t>,
    scope: &Symbol,
    env: &FormalEnv,
) -> Result<SequenceRangeValue, LoweringError> {
    match sel {
        SelectorSyntax::BitSelect(b) => {
            let n = fold_to_u32(b.expr().syntax(), scope, env)?;
            Ok(SequenceRangeValue {
                min: n,
                max: Some(n),
            })
        }
        SelectorSyntax::RangeSelect(r) => {
            let min = fold_to_u32(r.left().syntax(), scope, env)?;
            let max = fold_to_u32_or_dollar(r.right().syntax(), scope, env)?;
            Ok(SequenceRangeValue { min, max })
        }
    }
}

/// The closed constant folder's result: either a concrete value, or the `$`
/// (unbounded) token -- distinguished so a caller that only accepts a
/// concrete bound (e.g. the `min` side of a range, or a bare `##N`) can
/// reject a `$` found there as a named error instead of miscomputing.
enum FoldedConst {
    Value(i64),
    Dollar,
}

/// Folds `node` and requires a concrete value (rejects `$`), converting to
/// `u32` -- the shape every "min" bound, and every single-count `##N`/
/// `[*n]` bound, needs.
fn fold_to_u32(node: Node, scope: &Symbol, env: &FormalEnv) -> Result<u32, LoweringError> {
    match fold(node, scope, env)? {
        FoldedConst::Value(v) => u32_from_i64(v, scope),
        FoldedConst::Dollar => Err(LoweringError::unsupported_at(
            "sequence range constant folder: `$` is only legal as a range's upper bound, not here",
            scope,
        )),
    }
}

/// Folds `node`, mapping `$` to `None` (unbounded) -- the shape a range's
/// "max" bound needs (16.7/16.9.2's `cycle_delay_const_range_expression`/
/// `const_or_range_expression` both allow `$` only on the right).
fn fold_to_u32_or_dollar(
    node: Node,
    scope: &Symbol,
    env: &FormalEnv,
) -> Result<Option<u32>, LoweringError> {
    match fold(node, scope, env)? {
        FoldedConst::Value(v) => Ok(Some(u32_from_i64(v, scope)?)),
        FoldedConst::Dollar => Ok(None),
    }
}

fn u32_from_i64(v: i64, scope: &Symbol) -> Result<u32, LoweringError> {
    u32::try_from(v).map_err(|_| {
        LoweringError::unsupported_at(
            &format!(
                "sequence range constant folder: {v} is not representable as a sequence range \
                 bound (must be 0..=u32::MAX per 16.7/16.9.2's unsigned `min`/`max`)"
            ),
            scope,
        )
    })
}

/// A call of a user constant function in a sequence range bound (16.7: each
/// bound is a `constant_expression`; 13.4.3: a constant function call is one).
/// The callee's declaration is found in the call's own syntax tree, its ordered
/// arguments are folded here, and slang's own constant evaluator runs the
/// declaration in a [`ScriptSession`] that also holds the enclosing scope's integer
/// parameters. A callee that reads a name the session does not know (another
/// function, a non-parameter), or one that is not a constant function, is a named
/// refusal -- never a guess.
fn fold_user_call(
    call: Node,
    callee: &str,
    args: &[ArgumentSyntax],
    scope: &Symbol,
    env: &FormalEnv,
) -> Result<FoldedConst, LoweringError> {
    let refuse = |why: &str| {
        LoweringError::unsupported_at(
            &format!(
                "sequence range constant folder: call of `{callee}` in a sequence range bound: \
                 {why} (16.7/13.4.3)"
            ),
            scope,
        )
    };
    let mut root = call;
    while let Some(p) = root.parent() {
        root = p;
    }
    let decls: Vec<(String, FunctionDeclarationSyntax)> = root
        .descendants()
        .filter_map(FunctionDeclarationSyntax::cast)
        .map(|d| (d.prototype().name().syntax().text().trim().to_string(), d))
        .collect();
    let Some(start) = decls.iter().position(|(n, _)| n == callee) else {
        return Err(refuse(
            "no declaration of a function by that name in the source",
        ));
    };
    let mut actuals = Vec::with_capacity(args.len());
    for a in args {
        // Named arguments (`.x(3)`) are handed to slang's own call binding.
        let (label, expr) = match a {
            ArgumentSyntax::OrderedArgument(a) => (String::new(), a.expr().syntax()),
            ArgumentSyntax::NamedArgument(a) => {
                let (Some(n), Some(e)) = (a.name(), a.expr()) else {
                    return Err(refuse("an empty named argument is not folded"));
                };
                (format!(".{}", n.text().trim()), e.syntax())
            }
            ArgumentSyntax::EmptyArgument(_) => {
                return Err(refuse("an omitted argument is not folded"));
            }
        };
        let v = fold_operand(unwrap_property_wrapper(expr), scope, env, callee)?;
        actuals.push(format!("{label}({v})"));
    }
    let mut session = ScriptSession::new()
        .map_err(|e| refuse(&format!("cannot start a constant evaluation session: {e}")))?;
    // The enclosing scope's integer parameters, so a constant function may read them
    // (13.4.3: a constant function may reference parameters of its scope).
    for m in scope.members() {
        if m.kind() == SymbolKind::Parameter
            && let Some(v) = m.constant_value().and_then(|v| v.as_i64())
        {
            session.eval(&format!("localparam longint {} = {v};", m.name()));
        }
    }
    // The callee and every user function it transitively calls (13.4.3 lets a
    // constant function call other constant functions), callees first so each
    // declaration is elaborated after what it calls.
    let mut order: Vec<usize> = Vec::new();
    let mut seen = vec![false; decls.len()];
    callees_first(&decls, start, &mut seen, &mut order);
    for i in order {
        session.eval(&decls[i].1.syntax().text());
    }
    let value = session
        .eval(&format!("{callee}({})", actuals.join(", ")))
        .and_then(|v| v.as_i64())
        .ok_or_else(|| {
            refuse(
                "the function is not evaluable as a constant function over its arguments and the \
                 enclosing scope's integer parameters (it reads another name or is not constant)",
            )
        })?;
    Ok(FoldedConst::Value(value))
}

/// Post-order walk over the user functions a declaration names followed by `(`:
/// pushes every transitive callee of `decls[i]` before `i` itself (a cycle is
/// left to slang's evaluator to reject).
fn callees_first(
    decls: &[(String, FunctionDeclarationSyntax)],
    i: usize,
    seen: &mut [bool],
    order: &mut Vec<usize>,
) {
    if std::mem::replace(&mut seen[i], true) {
        return;
    }
    let text = decls[i].1.syntax().text();
    for (j, (name, _)) in decls.iter().enumerate() {
        if j == i || seen[j] {
            continue;
        }
        let mut from = 0;
        while let Some(at) = text[from..].find(name.as_str()) {
            let at = from + at;
            let end = at + name.len();
            let word_start = !text[..at]
                .chars()
                .next_back()
                .is_some_and(|c| c.is_alphanumeric() || c == '_' || c == '$');
            if word_start && text[end..].trim_start().starts_with('(') {
                callees_first(decls, j, seen, order);
                break;
            }
            from = end;
        }
    }
    order.push(i);
}

/// The closed evaluator itself (plan §1.1: "a small, self-contained
/// constant folder"). Its whole input domain, exhaustively: an integer
/// literal, the `$` token, a named-identifier lookup (`scope.find(name)`'s
/// `constant_value()`), `+`/`-`/`*` of two such values, and parentheses
/// around any of the above. Anything else is a named [`LoweringError`],
/// never a guess -- 16.7/16.9.2 require every bound to already be an
/// elaboration-time integer constant, so a `constant_expression` this
/// folder cannot reduce is either a genuinely unsupported construct (e.g. a
/// ternary or a function call) or a malformed syntax node passed in by a
/// caller bug, and the two cases are indistinguishable from here -- both
/// get the same loud, named error.
fn fold(node: Node, scope: &Symbol, env: &FormalEnv) -> Result<FoldedConst, LoweringError> {
    match node.kind() {
        SyntaxKind::IntegerLiteralExpression => {
            let tok = node.first_token().ok_or_else(|| {
                LoweringError::unsupported_at(
                    "sequence range constant folder: integer literal has no token",
                    scope,
                )
            })?;
            let digits: String = tok.text().chars().filter(|c| *c != '_').collect();
            let v: i64 = digits.parse().map_err(|_| {
                LoweringError::unsupported_at(
                    &format!(
                        "sequence range constant folder: could not parse integer literal {:?}",
                        tok.text()
                    ),
                    scope,
                )
            })?;
            Ok(FoldedConst::Value(v))
        }
        SyntaxKind::WildcardLiteralExpression => Ok(FoldedConst::Dollar),
        SyntaxKind::IdentifierName => {
            let ident = IdentifierNameSyntax::cast(node)
                .and_then(|n| n.identifier())
                .ok_or_else(|| {
                    LoweringError::unsupported_at(
                        "sequence range constant folder: identifier name has no token",
                        scope,
                    )
                })?;
            let name = ident.value_text();
            // A formal argument of an enclosing named-sequence instance
            // shadows any module-level constant of the same name (16.8).
            if let Some(bound) = env.lookup(&key(node), name) {
                return match bound {
                    Bound::Value(v) => Ok(FoldedConst::Value(*v)),
                    Bound::Dollar => Ok(FoldedConst::Dollar),
                    Bound::Unfoldable(why) => Err(LoweringError::unsupported_at(
                        &format!(
                            "sequence range constant folder: formal argument {name:?} is bound \
                             to an actual argument that is not an elaboration-time constant \
                             ({why}); 16.7/16.9.2 bounds must be elaboration-time integers"
                        ),
                        scope,
                    )),
                };
            }
            let sym = scope.find(name).ok_or_else(|| {
                LoweringError::unsupported_at(
                    &format!(
                        "sequence range constant folder: no constant named {name:?} found in scope"
                    ),
                    scope,
                )
            })?;
            let cv = sym.constant_value().ok_or_else(|| {
                LoweringError::unsupported_at(
                    &format!(
                        "sequence range constant folder: {name:?} has no elaboration-time \
                         constant value"
                    ),
                    scope,
                )
            })?;
            let v = cv.as_i64().ok_or_else(|| {
                LoweringError::unsupported_at(
                    &format!(
                        "sequence range constant folder: {name:?}'s value is not representable \
                         as an i64"
                    ),
                    scope,
                )
            })?;
            Ok(FoldedConst::Value(v))
        }
        SyntaxKind::AddExpression => fold_binary(node, scope, env, i64::checked_add, "+"),
        SyntaxKind::SubtractExpression => fold_binary(node, scope, env, i64::checked_sub, "-"),
        SyntaxKind::MultiplyExpression => fold_binary(node, scope, env, i64::checked_mul, "*"),
        SyntaxKind::ParenthesizedExpression => {
            let paren = ParenthesizedExpressionSyntax::cast(node).ok_or_else(|| {
                LoweringError::unsupported_at(
                    "sequence range constant folder: malformed parenthesized expression",
                    scope,
                )
            })?;
            fold(paren.expression().syntax(), scope, env)
        }
        SyntaxKind::DivideExpression => fold_binary(node, scope, env, i64::checked_div, "/"),
        SyntaxKind::ModExpression => fold_binary(node, scope, env, i64::checked_rem, "%"),
        SyntaxKind::PowerExpression => fold_binary(
            node,
            scope,
            env,
            |l, r| u32::try_from(r).ok().and_then(|e| l.checked_pow(e)),
            "**",
        ),
        SyntaxKind::LogicalShiftLeftExpression | SyntaxKind::ArithmeticShiftLeftExpression => {
            fold_binary(
                node,
                scope,
                env,
                |l, r| u32::try_from(r).ok().and_then(|e| l.checked_shl(e)),
                "<<",
            )
        }
        SyntaxKind::LogicalShiftRightExpression | SyntaxKind::ArithmeticShiftRightExpression => {
            fold_binary(
                node,
                scope,
                env,
                |l, r| u32::try_from(r).ok().and_then(|e| l.checked_shr(e)),
                ">>",
            )
        }
        SyntaxKind::BinaryAndExpression => fold_binary(node, scope, env, |l, r| Some(l & r), "&"),
        SyntaxKind::BinaryOrExpression => fold_binary(node, scope, env, |l, r| Some(l | r), "|"),
        SyntaxKind::BinaryXorExpression => fold_binary(node, scope, env, |l, r| Some(l ^ r), "^"),
        SyntaxKind::EqualityExpression => {
            fold_binary(node, scope, env, |l, r| Some(i64::from(l == r)), "==")
        }
        SyntaxKind::InequalityExpression => {
            fold_binary(node, scope, env, |l, r| Some(i64::from(l != r)), "!=")
        }
        SyntaxKind::LessThanExpression => {
            fold_binary(node, scope, env, |l, r| Some(i64::from(l < r)), "<")
        }
        SyntaxKind::LessThanEqualExpression => {
            fold_binary(node, scope, env, |l, r| Some(i64::from(l <= r)), "<=")
        }
        SyntaxKind::GreaterThanExpression => {
            fold_binary(node, scope, env, |l, r| Some(i64::from(l > r)), ">")
        }
        SyntaxKind::GreaterThanEqualExpression => {
            fold_binary(node, scope, env, |l, r| Some(i64::from(l >= r)), ">=")
        }
        SyntaxKind::LogicalAndExpression => fold_binary(
            node,
            scope,
            env,
            |l, r| Some(i64::from(l != 0 && r != 0)),
            "&&",
        ),
        SyntaxKind::LogicalOrExpression => fold_binary(
            node,
            scope,
            env,
            |l, r| Some(i64::from(l != 0 || r != 0)),
            "||",
        ),
        SyntaxKind::UnaryPlusExpression
        | SyntaxKind::UnaryMinusExpression
        | SyntaxKind::UnaryLogicalNotExpression => {
            let un = PrefixUnaryExpressionSyntax::cast(node).ok_or_else(|| {
                LoweringError::unsupported_at(
                    "sequence range constant folder: malformed unary expression",
                    scope,
                )
            })?;
            let v = fold_operand(un.operand().syntax(), scope, env, "unary")?;
            Ok(FoldedConst::Value(match node.kind() {
                SyntaxKind::UnaryPlusExpression => v,
                SyntaxKind::UnaryMinusExpression => v.checked_neg().ok_or_else(|| {
                    LoweringError::unsupported_at(
                        "sequence range constant folder: unary minus overflowed i64 arithmetic",
                        scope,
                    )
                })?,
                SyntaxKind::UnaryLogicalNotExpression => i64::from(v == 0),
                other => unreachable!("outer arm admits only the three unary kinds, got {other:?}"),
            }))
        }
        SyntaxKind::ConditionalExpression => {
            let c = ConditionalExpressionSyntax::cast(node).ok_or_else(|| {
                LoweringError::unsupported_at(
                    "sequence range constant folder: malformed `?:` expression",
                    scope,
                )
            })?;
            let cond = c
                .predicate()
                .conditions()
                .iter()
                .next()
                .ok_or_else(|| {
                    LoweringError::unsupported_at(
                        "sequence range constant folder: `?:` with no condition",
                        scope,
                    )
                })?
                .expr();
            let pick = if fold_operand(cond.syntax(), scope, env, "?:")? != 0 {
                c.left()
            } else {
                c.right()
            };
            fold(pick.syntax(), scope, env)
        }
        SyntaxKind::IntegerVectorExpression => {
            let lit = IntegerVectorExpressionSyntax::cast(node).ok_or_else(|| {
                LoweringError::unsupported_at(
                    "sequence range constant folder: malformed vector literal",
                    scope,
                )
            })?;
            let bad = |why: &str| {
                LoweringError::unsupported_at(
                    &format!("sequence range constant folder: vector literal {why}"),
                    scope,
                )
            };
            let base = lit
                .base()
                .map(|t| t.text().to_ascii_lowercase())
                .unwrap_or_default();
            let radix = match base
                .trim_start_matches('\'')
                .trim_start_matches('s')
                .chars()
                .next()
            {
                Some('h') => 16,
                Some('d') => 10,
                Some('o') => 8,
                Some('b') => 2,
                _ => return Err(bad("has an unrecognised base")),
            };
            let digits: String = lit
                .value()
                .map(|t| t.text().chars().filter(|c| *c != '_').collect())
                .unwrap_or_default();
            let v = i64::from_str_radix(&digits, radix)
                .map_err(|_| bad("has x/z digits or does not fit i64"))?;
            Ok(FoldedConst::Value(v))
        }
        SyntaxKind::InvocationExpression => {
            let inv = InvocationExpressionSyntax::cast(node).ok_or_else(|| {
                LoweringError::unsupported_at(
                    "sequence range constant folder: malformed call expression",
                    scope,
                )
            })?;
            let name = inv
                .left()
                .syntax()
                .first_token()
                .map(|t| t.text().to_string());
            let args: Vec<_> = inv
                .arguments()
                .map(|a| a.parameters().iter().collect())
                .unwrap_or_default();
            match (name.as_deref(), args.as_slice()) {
                (Some("$clog2"), [ArgumentSyntax::OrderedArgument(a)]) => {
                    let x = fold_operand(
                        unwrap_property_wrapper(a.expr().syntax()),
                        scope,
                        env,
                        "$clog2",
                    )?;
                    // $clog2(0) = 0; otherwise the bits needed for x - 1 (20.8.1).
                    let r = if x <= 1 {
                        0
                    } else {
                        64 - (x - 1).leading_zeros()
                    };
                    Ok(FoldedConst::Value(i64::from(r)))
                }
                (Some(callee), _) if !callee.starts_with('$') => {
                    fold_user_call(node, callee, &args, scope, env)
                }
                _ => Err(LoweringError::unsupported_at(
                    &format!(
                        "sequence range constant folder: call of {name:?} -- only `$clog2` and \
                         a call of a constant function with ordered arguments are folded in a \
                         sequence range bound"
                    ),
                    scope,
                )),
            }
        }
        SyntaxKind::SimplePropertyExpr | SyntaxKind::SimpleSequenceExpr => {
            fold(unwrap_property_wrapper(node), scope, env)
        }
        other => Err(LoweringError::unsupported_at(
            &format!(
                "sequence range constant folder: unsupported syntax kind {other:?} -- 16.7/16.9.2 \
                 bounds must be an integer literal, a named parameter/constant, an integer \
                 constant expression over those (`+ - * / % ** << >> & | ^`, comparisons, `?:`, \
                 `$clog2`), or `$`"
            ),
            scope,
        )),
    }
}

/// A property/sequence expression wrapper around a plain expression (the shape a
/// system-call argument has in the syntax tree), peeled to the expression.
fn unwrap_property_wrapper(node: Node) -> Node {
    let mut cur = node;
    loop {
        if let Some(p) = SimplePropertyExprSyntax::cast(cur) {
            cur = p.expr().syntax();
        } else if let Some(q) = SimpleSequenceExprSyntax::cast(cur) {
            cur = q.expr().syntax();
        } else {
            return cur;
        }
    }
}

/// Shared body of the three binary-operator arms: fold both operands
/// (neither may be `$` -- `$` never participates in arithmetic), apply
/// `op`, and report overflow by name rather than silently wrapping.
fn fold_binary(
    node: Node,
    scope: &Symbol,
    env: &FormalEnv,
    op: fn(i64, i64) -> Option<i64>,
    op_text: &str,
) -> Result<FoldedConst, LoweringError> {
    let bin = BinaryExpressionSyntax::cast(node).ok_or_else(|| {
        LoweringError::unsupported_at(
            &format!("sequence range constant folder: malformed `{op_text}` expression"),
            scope,
        )
    })?;
    let l = fold_operand(bin.left().syntax(), scope, env, op_text)?;
    let r = fold_operand(bin.right().syntax(), scope, env, op_text)?;
    let v = op(l, r).ok_or_else(|| {
        LoweringError::unsupported_at(
            &format!(
                "sequence range constant folder: `{l} {op_text} {r}` overflowed i64 arithmetic"
            ),
            scope,
        )
    })?;
    Ok(FoldedConst::Value(v))
}

fn fold_operand(
    node: Node,
    scope: &Symbol,
    env: &FormalEnv,
    op_text: &str,
) -> Result<i64, LoweringError> {
    match fold(node, scope, env)? {
        FoldedConst::Value(v) => Ok(v),
        FoldedConst::Dollar => Err(LoweringError::unsupported_at(
            &format!(
                "sequence range constant folder: `$` cannot be an operand of `{op_text}` -- it \
                 is only legal as a range's own upper bound"
            ),
            scope,
        )),
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use sv_lang::{AnalysisFlags, Compilation, Session};

    /// Compiles `rhs_and_body` as the body of a clocked `assert property`
    /// inside an `always_ff`, then returns the `AnalyzedAssertion`'s root
    /// `AssertionExpr` with the `Clocking` wrapper already stripped (its
    /// `[event, body]` children, confirmed live -- see the plan's own
    /// §1.1 "Clocking's children" note), ready for [`sequence_range_of`].
    /// `extra_decls` is for anything the property body references besides
    /// `clk`/`a`/`b` (e.g. a parameter the delay/repetition bound names).
    fn compiled_root_body(extra_decls: &str, property_body: &str) -> (sv_lang::Design, String) {
        let src = format!(
            "module m;\n\
             {extra_decls}\n\
             logic clk, a, b;\n\
             always_ff @(posedge clk) begin\n\
               assert property (@(posedge clk) {property_body});\n\
             end\n\
             endmodule\n"
        );
        let session = Session::new();
        let mut comp = Compilation::new(&session).unwrap();
        comp.add_source(&src).unwrap();
        let design = comp.compile().unwrap();
        assert!(
            !design.has_fatal_errors(),
            "fixture failed to compile: {src}"
        );
        (design, src)
    }

    /// Runs [`sequence_range_of`] against the single `AssertionExpr` body
    /// of a property whose root, after stripping its `Clocking` wrapper, is
    /// directly the `Simple`/`SequenceConcat` node under test -- the shared
    /// scaffolding every range-recovery unit test below reuses.
    fn ranges_of_property(
        extra_decls: &str,
        property_body: &str,
    ) -> Result<Vec<SequenceRangeValue>, LoweringError> {
        let (design, _src) = compiled_root_body(extra_decls, property_body);
        let body = design
            .top_instances()
            .next()
            .unwrap()
            .instance_body()
            .unwrap();
        let analysis = design.analyze(AnalysisFlags::NONE, 1).unwrap();
        let proc = analysis
            .procedures(body)
            .next()
            .expect("fixture has exactly one always_ff procedure");
        let assertion = analysis
            .assertions(proc.symbol())
            .next()
            .expect("fixture has exactly one concurrent assertion");
        let tree = design.syntax_trees().into_iter().next().unwrap();
        let root = assertion.root();
        let clocking = root
            .as_assertion_expr()
            .expect("assertion root is an AssertionExpr");
        assert_eq!(clocking.kind(), AssertionExprKind::Clocking);
        let kids = clocking.children();
        assert_eq!(kids.len(), 2, "Clocking's children are [event, body]");
        let property_root = kids[1]
            .as_assertion_expr()
            .expect("Clocking's second child is the property body");
        sequence_range_of(property_root, (&tree).into(), &body)
    }

    fn one(extra_decls: &str, property_body: &str) -> SequenceRangeValue {
        let mut v = ranges_of_property(extra_decls, property_body).unwrap();
        assert_eq!(v.len(), 1, "expected exactly one recovered range");
        v.remove(0)
    }

    #[test]
    fn delay_fixed_count_hash_3() {
        assert_eq!(
            one("", "a ##3 b"),
            SequenceRangeValue {
                min: 3,
                max: Some(3)
            }
        );
    }

    #[test]
    fn delay_bracket_range_2_5() {
        assert_eq!(
            one("", "a ##[2:5] b"),
            SequenceRangeValue {
                min: 2,
                max: Some(5)
            }
        );
    }

    #[test]
    fn delay_bracket_range_0_to_dollar() {
        assert_eq!(
            one("", "a ##[0:$] b"),
            SequenceRangeValue { min: 0, max: None }
        );
    }

    #[test]
    fn delay_bracket_star() {
        assert_eq!(
            one("", "a ##[*] b"),
            SequenceRangeValue { min: 0, max: None }
        );
    }

    #[test]
    fn delay_bracket_plus() {
        assert_eq!(
            one("", "a ##[+] b"),
            SequenceRangeValue { min: 1, max: None }
        );
    }

    #[test]
    fn delay_named_parameter_to_dollar() {
        assert_eq!(
            one("parameter int my_param = 2;", "a ##[my_param:$] b"),
            SequenceRangeValue { min: 2, max: None }
        );
    }

    #[test]
    fn delay_named_parameter_arithmetic() {
        // Not in T3's own required test list, but the plan's folder design
        // explicitly includes `+`/`-`/`*` of a named parameter -- this is
        // the regression that would fail if that arm broke.
        assert_eq!(
            one("parameter int my_param = 2;", "a ##[my_param+1:$] b"),
            SequenceRangeValue { min: 3, max: None }
        );
    }

    #[test]
    fn repetition_consecutive_fixed_count() {
        assert_eq!(
            one("", "a[*3]"),
            SequenceRangeValue {
                min: 3,
                max: Some(3)
            }
        );
    }

    #[test]
    fn repetition_consecutive_range() {
        assert_eq!(
            one("", "a[*2:7]"),
            SequenceRangeValue {
                min: 2,
                max: Some(7)
            }
        );
    }

    #[test]
    fn repetition_consecutive_bare_star() {
        assert_eq!(one("", "a[*]"), SequenceRangeValue { min: 0, max: None });
    }

    #[test]
    fn repetition_consecutive_bare_plus() {
        assert_eq!(one("", "a[+]"), SequenceRangeValue { min: 1, max: None });
    }

    #[test]
    fn repetition_nonconsecutive_range() {
        assert_eq!(
            one("", "a[=2:5]"),
            SequenceRangeValue {
                min: 2,
                max: Some(5)
            }
        );
    }

    #[test]
    fn repetition_goto_range() {
        assert_eq!(
            one("", "a[->1:3]"),
            SequenceRangeValue {
                min: 1,
                max: Some(3)
            }
        );
    }

    #[test]
    fn malformed_cast_on_wrong_assertion_expr_kind_is_a_named_error_not_a_panic() {
        // A `Unary` AssertionExprKind (`not a`) never carries a 16.7/16.9.2
        // range at all -- `sequence_range_of` must reject it loudly, not
        // panic trying to cast its syntax to `SimpleSequenceExprSyntax`/
        // `DelayedSequenceExprSyntax`.
        let (design, _src) = compiled_root_body("", "not a");
        let body = design
            .top_instances()
            .next()
            .unwrap()
            .instance_body()
            .unwrap();
        let analysis = design.analyze(AnalysisFlags::NONE, 1).unwrap();
        let proc = analysis.procedures(body).next().unwrap();
        let assertion = analysis.assertions(proc.symbol()).next().unwrap();
        let tree = design.syntax_trees().into_iter().next().unwrap();
        let root = assertion.root();
        let clocking = root.as_assertion_expr().unwrap();
        let kids = clocking.children();
        let property_root = kids[1].as_assertion_expr().unwrap();
        assert_eq!(property_root.kind(), AssertionExprKind::Unary);
        let err = sequence_range_of(property_root, (&tree).into(), &body)
            .expect_err("a Unary node has no range to recover");
        assert!(err.message.contains("Unary"), "error was: {err}");
    }

    #[test]
    fn malformed_bound_expression_is_a_named_error_not_a_panic() {
        // 16.7's `cycle_delay_const_range_expression` grammar is permissive
        // (its bound is a plain `constant_expression`, syntactically any
        // expression) -- the *constant-ness* is a semantic rule this
        // module's own closed folder enforces, not slang's parser. A
        // concatenation (`{2'b01}`) is syntactically legal there and
        // compiles with no fatal diagnostic, but is outside the folder's
        // closed domain -- it must be a named `LoweringError`, never a
        // panic or a silently-wrong answer.
        let err = ranges_of_property("", "a ##[{2'b01}:5] b")
            .expect_err("a concatenation bound is outside the closed constant folder's domain");
        assert!(
            err.message.contains("ConcatenationExpression"),
            "error was: {err}"
        );
    }
}