rustyfi-lang 0.1.1

//! Surface CST → `Ast` elaboration. Does scope resolution, operator-
//! precedence/associativity resolution (the CST leaves that flattened, see
//! `cst.rs`'s module doc comment), pattern lowering, the `let-inline`/
//! `let-block` context-argument desugaring, mutable/`while`/`before`
//! desugaring, field access/record-update folding, itemize-tree
//! reconstruction, quoted-math lowering, and (untyped) module name-mangling.
//! This function's signature is the seam where the typechecker
//! (typechecker.ml / unification.ml port) slots in.

// The elaborator emits the BRANDED tree: every lexical identifier is a
// `Symbol<'s>` interned into the `SymbolStore` carried by [`Scope`]. See
// `crate::ast`'s module doc comment for what `I` covers (environment keys
// only — record labels, constructor tags and optional-argument labels stay
// `String` here exactly as they always were).
use crate::ast::branded::{Ast, BText, CmdArg, IText, MatchArm, MathElem, Pattern};
use crate::symbol::{Symbol, SymbolStore};
use rustyfi_backend::Length;
use rustyfi_syntax::cst::{self, ast as c};
use rustyfi_syntax::leaf::{AnyHorzCmdTok, AnyMathCmdTok, AnyVertCmdTok, UnopExclamTok, VarTok};
use rustyfi_syntax::span::Span;
use rustyfi_syntax::token::Token;
use rustyfi_syntax::RustyfiVersion;
use std::collections::{HashMap, HashSet, VecDeque};
use std::rc::Rc;

#[derive(Debug, thiserror::Error)]
#[error("{span}: {msg}")]
pub struct ElabError {
    pub span: Span,
    pub msg: String,
}

fn err<T>(span: Span, msg: impl Into<String>) -> Result<T, ElabError> {
    Err(ElabError {
        span,
        msg: msg.into(),
    })
}

/// Overlay size at which a [`Scope`]'s name set folds down into a fresh
/// shared base — the same persistent split, and the same reason, as
/// `typecheck::OVERLAY_CAP`.
const NAMES_OVERLAY_CAP: usize = 64;

/// The names in scope (primitives plus, progressively, `let`-bound names).
/// A flat name set — there is no real namespacing, so a module's qualified
/// names (`"M.x"`) are just ordinary strings that happen to contain a dot
/// (see the module doc comment on `qualify_key`).
#[derive(Clone, Debug)]
pub struct Scope<'s> {
    /// The names in scope, split into a large SHARED base (`Rc`, cloned by a
    /// refcount bump) and a small overlay of the most recent bindings, folded
    /// into a fresh base once it reaches [`NAMES_OVERLAY_CAP`].
    ///
    /// `Scope::with` clones the whole scope per binding — the natural way to
    /// write a lexical walk — but a flat `HashSet<String>` made that
    /// O(program x scope): measured at 4-11 MILLION `String` allocations per
    /// corpus document (~4-8k scope clones, each copying 1300-2600 names),
    /// the dominant cost of elaboration. Do not flatten it back.
    ///
    /// `Rc<str>` rather than `String` so even the capped overlay copy is
    /// refcount bumps. The set is insert-only, which is what makes the
    /// shared base sound without tombstones (the two maps below DO support
    /// removal, but stay flat: ~15 entries vs this one's thousands, 1-2% of
    /// the clone traffic).
    names_base: Rc<HashSet<Rc<str>>>,
    names_overlay: HashSet<Rc<str>>,
    /// Per declared parameter position, `true` where that position is a
    /// `Param::Optional` (`?:name`) — recorded for a name bound via a plain
    /// (non-`let-rec`) `let`/`let .. in` or one of the three command-binding
    /// forms. `let to-math ?:iopt e = ..` records `[true, false]`;
    /// `stdja.satyh`'s `let document record ?:configopt inner = ..`
    /// (optional in SECOND position) records `[false, true, false]`.
    ///
    /// This drives marker-less optional-argument defaulting: a bare call
    /// site (`to-math e1`) must still supply `None` for `iopt` and match
    /// `e1` against `e`; `document record body` must supply `None` for
    /// `configopt` and match `body` against `inner`, not `configopt`'s
    /// domain. A scalar LEADING-COUNT encoding can't express that — it
    /// can't tell "optional at position 1" from "no optional" once position
    /// 0 is mandatory — hence the full per-position shape. See
    /// `app_chain_generic`'s use of [`Scope::optional_shape`].
    ///
    /// [`Scope::optional_arity`] (a derived LEADING-RUN count) feeds the
    /// command-argument paths (`cmd_args`, `math_bot`'s `Cmd` arm), which
    /// stay leading-only. Absent from the map means "no known optionals" —
    /// the common case.
    optional_shape: std::collections::HashMap<String, Vec<bool>>,
    /// A module member's bare (sibling-visible) local name → the ACTUAL Ast
    /// key its value is bound under (see `push_named_binding`'s doc comment):
    /// a member of `module M = struct .. end` is bound under a MANGLED key
    /// (`"$M.atan2"`, never a valid surface identifier, so it can't collide
    /// with anything), not a bare `"atan2"` `LetIn` — so a SIBLING member's
    /// bare reference (`Ast::Var("atan2")`, as written) must be redirected to
    /// that mangled key at construction time, deliberately NOT to the
    /// qualified `"M.atan2"` key (that distinction is what makes opaque-type
    /// sealing work). This map is that redirect, consulted by [`scoped_var`]
    /// and the inline/block/math command-key resolution sites. Entries exist
    /// only while processing a module's own `struct` body (`running`, local
    /// to that recursive `walk_bindings` call) and never propagate to the
    /// caller's outer scope (only EXPORTED qualified keys' `names`/
    /// `optional_arity` entries are copied back) — so a rename can only
    /// affect references written inside that same module, never outside it
    /// or after its `end`.
    renames: std::collections::HashMap<String, String>,
    /// The source-language version this scope elaborates under — gates the
    /// SATySFi 0.1-only labeled-optional nodes (`Expr::FunRows`,
    /// `AppArg::Bundled`) so a 0.0.6-compiled file that happens to parse them
    /// (the additive-`cst` accept-surface widening) is rejected with a
    /// version error rather than silently accepted. `V0_0` by default.
    version: RustyfiVersion,
    /// The interner every identifier this scope helps build is minted from.
    ///
    /// The scope's own tables above stay **text**-keyed: elaboration is a
    /// string-manipulation pass (it mangles `"M.x"` / `"$M.atan2"` /
    /// `"%cmd_arg0"` keys, tests command sigils by first character, and scans
    /// by prefix in [`Scope::names_with_prefix`]), so keying them by `Symbol`
    /// would only add a resolve on every probe. Interning happens at the
    /// boundary instead — [`Scope::resolve`] and [`Scope::sym`] are the two
    /// points where a text key becomes the `Symbol` an `Ast` node carries.
    store: &'s SymbolStore,
}

impl<'s> Scope<'s> {
    pub fn new(store: &'s SymbolStore, names: impl IntoIterator<Item = String>) -> Scope<'s> {
        Scope::new_with_version(store, names, RustyfiVersion::V0_0)
    }

    /// Like [`Scope::new`] but elaborating under an explicit source version —
    /// the V0_1 compile path (`lib.rs`) uses this so the 0.1 labeled-optional
    /// nodes are accepted.
    pub fn new_with_version(
        store: &'s SymbolStore,
        names: impl IntoIterator<Item = String>,
        version: RustyfiVersion,
    ) -> Scope<'s> {
        Scope {
            names_base: Rc::new(names.into_iter().map(Rc::from).collect()),
            names_overlay: HashSet::new(),
            optional_shape: std::collections::HashMap::new(),
            renames: std::collections::HashMap::new(),
            version,
            store,
        }
    }

    /// Intern `name` as-is. Use this where a key is *already* the final Ast
    /// key (a mangled module key, a freshly minted `%`-prefixed desugar name);
    /// use [`Scope::resolve`] where a bare source reference is being looked
    /// up, since only that path applies the module-member rename redirect.
    fn sym(&self, name: &str) -> Symbol<'s> {
        self.store.intern(name)
    }

    fn with(&self, name: &str) -> Scope<'s> {
        let mut s = self.clone();
        s.insert(name);
        s
    }

    /// In-place version of [`Scope::with`], for the folds below that thread
    /// one evolving scope through a sequence of bindings without cloning at
    /// every step. Rebinding a name plainly (no known arity) clears any
    /// stale [`Scope::optional_arity`]/[`Scope::rename`] entry, so a local
    /// parameter/pattern binding can never inherit an outer optional-
    /// leading function's arity — or an outer module member's qualified
    /// redirect — just by sharing its name.
    fn insert(&mut self, name: &str) {
        self.names_overlay.insert(Rc::from(name));
        self.promote_names();
        self.optional_shape.remove(name);
        self.renames.remove(name);
    }

    /// Fold the name overlay into a fresh shared base once it reaches
    /// [`NAMES_OVERLAY_CAP`], bounding what every later `with` has to copy.
    /// Amortized O(1) per binding, as in `typecheck::TypeEnv::maybe_promote`.
    fn promote_names(&mut self) {
        if self.names_overlay.len() < NAMES_OVERLAY_CAP {
            return;
        }
        let mut base = (*self.names_base).clone();
        base.extend(self.names_overlay.drain());
        self.names_base = Rc::new(base);
    }

    /// Like [`Scope::insert`], but also records `name`'s full per-position
    /// optional-parameter shape (see the struct doc comment) — used only at
    /// the handful of binding sites that know a def-site `Param` list
    /// (`walk_bindings`'s `TopBinding::Let`/`LetInline`/`LetBlock`/`LetMath`
    /// arms, `Expr::LetIn`/`Expr::LetMathIn`).
    fn insert_with_shape(&mut self, name: &str, shape: Vec<bool>) {
        self.names_overlay.insert(Rc::from(name));
        self.promote_names();
        if shape.iter().any(|&opt| opt) {
            self.optional_shape.insert(name.to_string(), shape);
        } else {
            self.optional_shape.remove(name);
        }
        self.renames.remove(name);
    }

    /// Record that a bare reference to `local` (a module member's own
    /// sibling-visible name) must actually resolve to the Ast key
    /// `actual_key` (its qualified binding — see [`Scope`]'s `renames`
    /// field doc comment and `push_named_binding`). `local` stays `true`
    /// under [`Scope::contains`] (unaffected by this call) — only WHICH KEY
    /// [`Scope::resolve`] returns for it changes.
    fn rename(&mut self, local: &str, actual_key: &str) {
        self.renames
            .insert(local.to_string(), actual_key.to_string());
    }

    /// The Ast key a bare reference to `name` should actually use, interned:
    /// its [`Scope::rename`] redirect, if one is active, else `name` itself
    /// unchanged (the overwhelmingly common case — every name outside a
    /// module's own body).
    ///
    /// This is the elaborator's main text → [`Symbol`] boundary: almost every
    /// identifier an `Ast` node carries is minted right here.
    fn resolve(&self, name: &str) -> Symbol<'s> {
        self.store.intern(self.resolve_text(name))
    }

    /// [`Scope::resolve`] before interning — for the one caller that needs to
    /// *compare* the redirect target against source text rather than embed it
    /// in a node (`app_chain_generic`'s unary-`not` special case, which must
    /// only fire when `not` still resolves to itself).
    fn resolve_text<'a>(&'a self, name: &'a str) -> &'a str {
        self.renames.get(name).map(|s| s.as_str()).unwrap_or(name)
    }

    fn contains(&self, name: &str) -> bool {
        self.names_overlay.contains(name) || self.names_base.contains(name)
    }

    /// `name`'s recorded leading-optional-parameter count (the maximal
    /// prefix of `true`s in its [`Scope::optional_shape`] entry), or `0` if
    /// none is known — the command-argument paths (`cmd_args`, `math_bot`'s
    /// `Cmd` arm) only ever auto-omit a *leading* run.
    fn optional_arity(&self, name: &str) -> usize {
        self.optional_shape
            .get(name)
            .map(|shape| shape.iter().take_while(|&&opt| opt).count())
            .unwrap_or(0)
    }

    /// `name`'s recorded full per-position optional-parameter shape (see the
    /// struct doc comment), or `&[]` if none is known — used by
    /// `app_chain_generic`'s marker-less-optional-defaulting, which (unlike
    /// [`Scope::optional_arity`]) must see optionals anywhere in the param
    /// list, not just a leading run.
    fn optional_shape(&self, name: &str) -> &[bool] {
        self.optional_shape
            .get(name)
            .map(|v| v.as_slice())
            .unwrap_or(&[])
    }

    /// Every currently-known name starting with `prefix` (used by `open`,
    /// which brings a module's `"M."`-prefixed names into unqualified
    /// scope). Sorted for deterministic alias-binding order.
    fn names_with_prefix(&self, prefix: &str) -> Vec<String> {
        // A `BTreeSet` because the result must be DEDUPLICATED as well as
        // sorted: a name re-inserted after a promotion can sit in both
        // layers, and `open` binding an alias twice would not be harmless.
        self.names_overlay
            .iter()
            .chain(self.names_base.iter())
            .filter(|n| n.starts_with(prefix))
            .map(|n| n.to_string())
            .collect::<std::collections::BTreeSet<_>>()
            .into_iter()
            .collect()
    }
}

/// A `Var` node for a name that must already be in scope (primitive
/// operators and the internal `%context`/`read-inline`/`read-block` wiring
/// are all resolved the same way as user variables). Existence is checked
/// against the BARE `name` (unaffected by any active [`Scope::rename`]
/// redirect); the constructed node's own key goes through
/// [`Scope::resolve`], so a module member's sibling reference compiles
/// directly to that member's mangled key when one is active — see
/// `push_named_binding`'s doc comment.
fn scoped_var<'s>(name: &str, span: Span, scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    if scope.contains(name) {
        Ok(Ast::Var(scope.resolve(name), span))
    } else {
        err(span, format!("unbound variable '{name}'"))
    }
}

/// A user type declaration, surfaced (but not yet lowered into
/// [`crate::types::MonoType`] — that's `typecheck::build_variant_decl`'s job)
/// from a CST [`cst::TypeDecl`]. Ctor payload types are kept as raw CST
/// `TypeExpr`s: cheap to clone, and this untyped elaborator has no use for
/// them beyond passing them through to the typechecker.
#[derive(Clone, Debug)]
pub struct UserTypeDecl {
    pub name: String,
    /// Type-parameter names, in declaration order (e.g. `["a"]` for `'a`).
    pub params: Vec<String>,
    /// `(ctor name, payload type expr)`, in declaration order.
    pub ctors: Vec<(String, Option<c::TypeExpr>)>,
}

/// A user type *synonym* declaration (`type point = length * length`),
/// surfaced in parallel with [`UserTypeDecl`] — see that struct's doc
/// comment; the body is kept as a raw CST `TypeExpr` for the same reason.
/// `typecheck::build_synonym_decl` is where it is actually lowered to a
/// `MonoType` template, and `typecheck::expand_synonyms` is where a
/// reference to `name` elsewhere is transparently replaced by it.
#[derive(Clone, Debug)]
pub struct UserSynonymDecl {
    pub name: String,
    /// Type-parameter names, in declaration order. Only the zero-param case
    /// is reachable through a *use* of the synonym today — see
    /// `cst::ast::TypeAtom`'s doc comment (no applied-type-constructor
    /// syntax exists to instantiate one) — but parsing/storing params keeps
    /// this declaration-side path symmetric with `UserTypeDecl`.
    pub params: Vec<String>,
    pub body: c::TypeExpr,
}

/// One lowered `type` declaration: either shape [`lower_type_decl`] can
/// produce, for `walk_bindings` to sort into `Program`'s two decl lists.
enum LoweredTypeDecl {
    Variant(UserTypeDecl),
    Synonym(UserSynonymDecl),
}

/// Lower one `type` binding, including every `and`-clause of a mutual-
/// recursion chain (`type A = … and B = …`), into consecutive lowered decls —
/// all clauses share one program-global decl space, so their mutual references
/// resolve with the same forward-reference tolerance the typechecker already
/// gives the 0.1 lowering's consecutive `type … and …` output.
fn lower_type_decl(
    decl: &cst::TypeDecl,
    mod_path: &[String],
    tymap: &HashMap<String, String>,
) -> Vec<LoweredTypeDecl> {
    let mut out = Vec::with_capacity(1 + decl.ands.len());
    out.push(lower_one_type_clause(
        &decl.tyvars,
        &decl.name,
        &decl.body,
        mod_path,
        tymap,
    ));
    for a in &decl.ands {
        out.push(lower_one_type_clause(
            &a.tyvars, &a.name, &a.body, mod_path, tymap,
        ));
    }
    out
}

/// A module's type declaration is registered under its MODULE-QUALIFIED name
/// (`M.t`), and any within-module reference to a module-local type name in its
/// body is rewritten to the same qualified name (`tymap`, built by
/// `walk_bindings`). This keeps two modules' same-named types (e.g. every
/// `satysfi-base` module's `type t`) from colliding in the program-global
/// synonym/variant tables. The `contains('.')` guard leaves an
/// already-qualified name (the 0.1 lowering emits `"M.t"` directly) alone; a
/// top-level (`mod_path` empty) declaration stays bare.
fn lower_one_type_clause(
    tyvars: &[rustyfi_syntax::leaf::TypeVarTok],
    name: &VarTok,
    body: &cst::TypeDeclBody,
    mod_path: &[String],
    tymap: &HashMap<String, String>,
) -> LoweredTypeDecl {
    let params: Vec<String> = tyvars.iter().map(|v| v.name.clone()).collect();
    let qname = if name.name.contains('.') {
        name.name.clone()
    } else {
        qualify_key(mod_path, &name.name)
    };
    match body {
        cst::TypeDeclBody::Variant { first, rest, .. } => {
            let mut ctors = Vec::with_capacity(1 + rest.len());
            let mut push_ctor = |cname: String, payload: Option<&cst::OfType>| {
                let ty = payload.map(|o| {
                    let mut t = o.ty.clone();
                    qualify_ty(&mut t, tymap);
                    t
                });
                ctors.push((cname, ty));
            };
            push_ctor(first.ctor.name.clone(), first.of_ty.as_ref());
            for bv in rest {
                push_ctor(bv.def.ctor.name.clone(), bv.def.of_ty.as_ref());
            }
            LoweredTypeDecl::Variant(UserTypeDecl {
                name: qname,
                params,
                ctors,
            })
        }
        cst::TypeDeclBody::Synonym(ty) => {
            let mut b = ty.clone();
            qualify_ty(&mut b, tymap);
            LoweredTypeDecl::Synonym(UserSynonymDecl {
                name: qname,
                params,
                body: b,
            })
        }
    }
}

// ---- within-module type-reference qualification ----------------------------
// Rewrite a cloned CST `TypeExpr` in place, replacing every module-local BARE
// type-name reference with its module-qualified name (`tymap`: bare -> `M.t`).
// A `Mod.t` reference (`TypeAtom::NameMod`) is already absolute and left as-is;
// a name not in `tymap` (builtins, external names) is untouched.

fn qualify_ty(ty: &mut c::TypeExpr, map: &HashMap<String, String>) {
    if map.is_empty() {
        return;
    }
    match ty {
        c::TypeExpr::Fun { opts, dom, cod, .. } => {
            for o in opts {
                qualify_prod(&mut o.ty, map);
            }
            qualify_prod(dom, map);
            qualify_ty(cod, map);
        }
        c::TypeExpr::Atom(prod) => qualify_prod(prod, map),
        c::TypeExpr::OptRowFun {
            opt_dom, dom, cod, ..
        } => {
            for e in &mut opt_dom.entries {
                qualify_ty(&mut e.ty.0, map);
            }
            qualify_prod(dom, map);
            qualify_ty(cod, map);
        }
    }
}

fn qualify_prod(p: &mut c::TypeProd, map: &HashMap<String, String>) {
    qualify_app(&mut p.first, map);
    for s in &mut p.rest {
        qualify_app(&mut s.ty, map);
    }
}

fn qualify_app(a: &mut c::TypeApp, map: &HashMap<String, String>) {
    qualify_atom(&mut a.head, map);
    for at in &mut a.rest {
        qualify_atom(at, map);
    }
}

fn qualify_atom(at: &mut c::TypeAtom, map: &HashMap<String, String>) {
    match at {
        c::TypeAtom::Name(n) => {
            if let Some(q) = map.get(&n.name) {
                n.name = q.clone();
            }
        }
        c::TypeAtom::Paren { inner, .. } => qualify_ty(&mut inner.0, map),
        c::TypeAtom::Record { fields, .. } => {
            for f in fields {
                qualify_ty(&mut f.ty.0, map);
            }
        }
        c::TypeAtom::RecordOpen { inner, .. } => {
            for f in &mut inner.fields {
                qualify_ty(&mut f.ty.0, map);
            }
        }
        c::TypeAtom::Cmd { args, .. } => {
            for it in args {
                for l in &mut it.opt_labels {
                    qualify_ty(&mut l.ty.0, map);
                }
                qualify_ty(&mut it.ty.0, map);
            }
        }
        c::TypeAtom::Var(_) | c::TypeAtom::NameMod(_) => {}
    }
}

/// The result of elaborating a whole file: every `type` declaration it
/// surfaced (in source order — a later declaration may reference an earlier
/// one, or itself, since variant types are nominal; see
/// `typecheck::build_variant_decl`), every type *synonym* it surfaced (see
/// `typecheck::build_synonym_decl`), plus the elaborated document body.
#[derive(Clone, Debug)]
pub struct Program<'s> {
    pub type_decls: Vec<UserTypeDecl>,
    pub synonym_decls: Vec<UserSynonymDecl>,
    pub body: Ast<'s>,
    /// The interner every identifier in `body` was minted from. Carried on
    /// the program itself (rather than passed alongside it) so that the
    /// downstream passes — `typecheck`, `v1::module_check`, and the compile
    /// membrane — keep their existing one-argument signatures and cannot be
    /// handed a program and a store that don't belong together.
    pub store: &'s SymbolStore,
}

/// Elaborate a whole file into a [`Program`] (the elaborated body plus any
/// surfaced `type` declarations — see [`elaborate`] for the thin wrapper
/// existing callers that only want the body keep using).
///
/// **Library files.** `File.body` is `None` for a bare `prelude EOI` file (a
/// `.satyh` library with no document expression) — a separate loader crate
/// is responsible for merging a library's `prelude` into a document file's
/// before this function ever sees it, so there is no
/// "top-level bindings must be followed by `in`" check here at all: by the
/// time `elaborate_program` runs, either `body` is present (an ordinary
/// document, or an already-merged file) or it is a genuine library file,
/// which is a (clean) error to hand to `elaborate_program` directly.
pub fn elaborate_program<'s>(
    file: &cst::File,
    prelude_scope: &Scope<'s>,
) -> Result<Program<'s>, ElabError> {
    elaborate_program_with_versions(file, prelude_scope, &HashSet::new(), &HashMap::new(), None)
}

/// [`elaborate_program`] for a loader-merged file, saying which prelude
/// entries came from a file whose `@stage:` header was not the default. Each
/// gets its RHS wrapped in [`Ast::StageScope`] so the typechecker reads it at
/// that stage -- a `@stage: 0` library may quote (`&e`), a document may not.
pub fn elaborate_program_with_stages<'s>(
    file: &cst::File,
    prelude_scope: &Scope<'s>,
    stages: &HashMap<usize, crate::types::Stage>,
) -> Result<Program<'s>, ElabError> {
    elaborate_program_with_versions(file, prelude_scope, &HashSet::new(), stages, None)
}

/// Like [`elaborate_program`], but marking a subset of `file.prelude`'s
/// TOP-LEVEL entries (by index) as originating from a spliced `V0_0`
/// dependency. Every `Binding` from one of those
/// entries — recursively including bindings inside a nested `module .. =
/// struct .. end` — has its elaborated RHS wrapped in
/// [`Ast::VersionScope`]`(V0_0, _)`, so `compile.rs`/`eval.rs`/`typecheck.rs`
/// resolve that subtree's version-forked primitives against `V0_0` instead
/// of the merged program's ambient `V0_1`.
///
/// `v006_indices` is empty on every single-version path, making `this_v006`
/// always `false` there, so no `VersionScope` node is built at all.
///
/// `wrap_body_version`: when `Some(v)`, the file's own
/// document tail expression is additionally wrapped in
/// `Ast::VersionScope(v, _)` — needed beyond the indexed-`prelude`-item
/// wrapping above because a `V0_0` entry's tail (e.g. a bare `page-break doc` with
/// no intermediate `let`) may itself reference forked primitives directly,
/// not just its `prelude` bindings. `None` everywhere else builds no extra
/// node.
pub fn elaborate_program_with_versions<'s>(
    file: &cst::File,
    prelude_scope: &Scope<'s>,
    v006_indices: &HashSet<usize>,
    stages: &HashMap<usize, crate::types::Stage>,
    wrap_body_version: Option<RustyfiVersion>,
) -> Result<Program<'s>, ElabError> {
    let Some(body) = &file.body else {
        return err(
            Span::default(),
            "this file has no document expression - it is a library file",
        );
    };
    let items: Vec<&cst::TopBinding> = file.prelude.iter().collect();
    let mut type_decls = Vec::new();
    let mut synonym_decls = Vec::new();
    let (bindings, _exported, final_scope) = walk_bindings(
        &items,
        prelude_scope,
        &[],
        &mut type_decls,
        &mut synonym_decls,
        &ItemOrigins {
            v006: v006_indices,
            stages,
        },
        &HashMap::new(),
    )?;
    // `final_scope` (mod_path `[]`) already IS `prelude_scope` plus every
    // top-level name — including each one's `Scope::optional_arity` entry,
    // which a manual `insert` per `exported` name would have dropped (see
    // `Scope`'s doc comment) — so the file body sees the same
    // marker-less-optional-call defaulting a top-level function's own
    // sibling declarations do.
    let body_ast = expr(body, &final_scope)?;
    let body_ast = match wrap_body_version {
        Some(v) => Ast::VersionScope(v, Box::new(body_ast)),
        None => body_ast,
    };
    Ok(Program {
        type_decls,
        synonym_decls,
        body: nest(prelude_scope.store, bindings, body_ast),
        store: prelude_scope.store,
    })
}

/// Where each TOP-LEVEL entry of a merged prelude came from.
///
/// The loader concatenates every library's prelude into one file, which drops
/// two per-file properties the bindings still need: which generation authored
/// them (`v006`) and which `@stage:` their file declared
/// (`stages`). Both are keyed by the entry's index at THIS level, and both are
/// empty for a single-file compile. `v006` is carried onto a binding by
/// `maybe_v006_scope`, `stages` by `stage_wrap_item`.
struct ItemOrigins<'a> {
    v006: &'a HashSet<usize>,
    stages: &'a HashMap<usize, crate::types::Stage>,
}

/// Does `value` already carry a stage of its own? True for a nested
/// module's members (`walk_bindings` wrapped them) and for a 0.1 `val ~x`
/// (its own qualifier wins); [`stage_wrap_item`] leaves those alone so the
/// INNER, more specific stage is what the typechecker reads.
///
/// The `ModuleScope`/`VersionScope` peeling mirrors
/// `typecheck::Checker::binding_stage`, which looks for the same node
/// through the same two wrappers — they must agree, or a binding could be
/// wrapped twice with different stages.
///
/// Of the two, only the `ModuleScope` arm is load-bearing today: every
/// `walk_bindings` arm applies [`maybe_v006_scope`] before this runs, and
/// [`stage_wrap_item`] wraps outside whatever it finds, so a doubly-scoped
/// binding is always `StageScope(_, VersionScope(_, ..))`, never the
/// reverse — the `VersionScope` arm can only fire on a nesting no caller
/// builds. Verified by deleting it: nothing in the suite fails. Kept as the
/// cheap half of the agreement contract above (one arm-reordering away from
/// being needed), not because it runs.
fn already_staged(value: &Ast<'_>) -> bool {
    match value {
        Ast::StageScope(..) => true,
        Ast::ModuleScope(_, b) | Ast::VersionScope(_, b) => already_staged(b),
        _ => false,
    }
}

/// Mark every binding one top-level item contributed as belonging to `stage`.
///
/// One item is not one binding: a module member also mints a qualified alias,
/// a `let-rec` group inside a module mints one alias per clause, `open` and
/// `direct` mint one per re-exposed name, a destructuring `let` mints one per
/// pattern variable. Every one of them is code from the SAME file, and so is
/// at that file's stage — wrapping only the "main" value would leave the
/// aliases at the default stage 1, which the per-binding staging matrix then
/// reads as a genuine stage crossing: `list.satyg`'s `@stage: persistent`
/// `let reverse lst = fold-left …` would be refused for naming its own
/// `let-rec` sibling.
fn stage_wrap_item<'s>(bindings: &mut [Binding<'s>], stage: crate::types::Stage) {
    fn wrap<'s>(slot: &mut Ast<'s>, stage: crate::types::Stage) {
        if already_staged(slot) {
            return;
        }
        let taken = std::mem::replace(slot, Ast::Unit);
        *slot = Ast::StageScope(stage, Box::new(taken));
    }
    for b in bindings {
        match b {
            Binding::Let(_, v) | Binding::LetMutable(_, v) | Binding::LetMath(_, v) => {
                wrap(v, stage)
            }
            Binding::LetRec(clauses) => {
                for (_, v) in clauses.iter_mut() {
                    if already_staged(v) {
                        continue;
                    }
                    *v = Rc::new(Ast::StageScope(stage, Box::new((**v).clone())));
                }
            }
        }
    }
}

/// The stage ONE binding declared on itself (`cst::TopStage`), if any — the
/// per-binding half of the question `ItemOrigins::stages` answers per FILE.
/// SATySFi 0.1 writes it as `val ~x = e` / `val persistent ~x = e`
/// (`v1/lower.rs` puts it here); 0.0.6 never sets it, and saying so is this
/// function's other job.
///
/// **Version gate.** `cst::TopBinding` is shared, so the `~` qualifier
/// PARSES under 0.0.6 too — which would let a genuine 0.0.6 file write `let
/// ~x = e`, a form upstream 0.0.6 doesn't have at all (`EXACT_TILDE` appears
/// only as a splice-operand prefix, `v0.0.6 parser.mly:797`, and as macro
/// syntax, `:608`/`:1199`; 0.0.6 declares one stage per FILE via `@stage:`).
/// Elaboration is the first place that knows which generation authored the
/// binding, so it refuses the form here.
///
/// `authored_v006` is that per-ITEM answer, not the file's: a mixed compile's
/// scope carries ONE version (`V0_1` for both cross-version roots, see
/// `lib.rs`) while `ItemOrigins::v006` marks individual prelude slots a
/// 0.0.6 dependency contributed — so a spliced 0.0.6 item is gated even
/// inside a 0.1-rooted program, and vice versa.
fn binding_stage(
    stage: Option<&cst::TopStage>,
    version: RustyfiVersion,
    authored_v006: bool,
) -> Result<Option<crate::types::Stage>, ElabError> {
    let Some(s) = stage else { return Ok(None) };
    if authored_v006 || !version.has_per_binding_stage() {
        return err(
            s.tilde.0,
            "a per-binding stage qualifier (`~`) is SATySFi 0.1 syntax (`val ~x = e`) — \
             this binding is compiled as 0.0.6, which declares its stage per FILE \
             with a `@stage:` header",
        );
    }
    Ok(Some(match s.persistent {
        Some(_) => crate::types::Stage::Persistent0,
        None => crate::types::Stage::Stage0,
    }))
}

/// Wrap `value` in [`Ast::VersionScope`]`(V0_0, _)` iff `this_v006` — the
/// one-line helper every `walk_bindings` binding-construction arm below
/// calls right after building its (fully elaborated) RHS. See
/// [`elaborate_program_with_versions`]'s doc comment.
fn maybe_v006_scope<'s>(value: Ast<'s>, this_v006: bool) -> Ast<'s> {
    if this_v006 {
        Ast::VersionScope(RustyfiVersion::V0_0, Box::new(value))
    } else {
        value
    }
}

/// Elaborate a whole file into one expression, discarding any `type`
/// declarations it surfaces (existing callers that only need the untyped
/// `Ast`; see [`elaborate_program`] for the version the typechecker
/// uses).
pub fn elaborate<'s>(file: &cst::File, prelude_scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    Ok(elaborate_program(file, prelude_scope)?.body)
}

// ---- module name-mangling & the top-level/struct-decl fold ---------------

/// The (untyped) module name-mangling scheme: a qualified name's runtime/
/// scope key is simply `mods.join(".") + "." + local`, where `local` is
/// whatever bare key the unqualified form would have used — a plain
/// variable's own name (`"x"` → `"M.x"`), or a command's sigil-inclusive
/// name (`"\cmd"` → `"M.\cmd"`, *not* the surface-syntax `"\M.cmd"` spelling
/// `Token::HorzCmdWithMod`'s `Display` impl renders — this port's `Scope`
/// and `Env` are both flat string-keyed maps with no separate namespace for
/// commands vs. variables, so one uniform "prefix-join" scheme for every
/// kind of name is simplest, and nothing round-trips through source syntax
/// again once elaborated). Nested modules mangle recursively by construction
/// — `mod_path` is the *full* accumulated path (`["M", "N"]`) at the point a
/// name is bound, never re-qualified after the fact, so `module N = struct
/// let x = .. end` inside `module M = struct .. end` yields key `"M.N.x"`
/// directly.
fn qualify_key(mod_path: &[String], local: &str) -> String {
    if mod_path.is_empty() {
        local.to_string()
    } else {
        format!("{}.{}", mod_path.join("."), local)
    }
}

/// If `item` is a `direct \cmd : ty` / `direct +cmd : ty` signature item
/// (`cst::SigItem::DirectHorzCmd`/`DirectVertCmd` — math commands share the
/// `\` sigil with inline ones, see `command_scheme`'s doc comment in
/// `typecheck.rs`, so there is no separate math case here), its bare command
/// name (sigil included — `"\cmd"`/`"+cmd"`, the same key format
/// `push_named_binding` binds locally) and the name token's span, for
/// the enclosing-scope exposure. `None` for
/// every other `SigItem` (`val`/`type`), which stay module-qualified only.
fn direct_cmd_name(item: &cst::SigItem) -> Option<(String, Span)> {
    match item {
        cst::SigItem::DirectHorzCmd { name, .. } => Some((name.name.clone(), name.span)),
        cst::SigItem::DirectVertCmd { name, .. } => Some((name.name.clone(), name.span)),
        _ => None,
    }
}

/// One step of the top-level/struct-decl fold, deferred (see [`nest`]) so
/// that folding in a `module`'s declarations doesn't require building the
/// "rest of the program" before the module's own bindings are known.
enum Binding<'s> {
    Let(String, Ast<'s>),
    LetRec(Vec<(String, Rc<Ast<'s>>)>),
    LetMutable(String, Ast<'s>),
    /// A `let-math` binding — nests as `Ast::LetMathIn`, not `Ast::LetIn`
    /// (see that variant's doc comment).
    LetMath(String, Ast<'s>),
}

/// Wrap `tail` in every collected `Binding`, innermost (last-pushed) first —
/// i.e. in the same order `elaborate_prelude`/`elaborate_struct_decls` used
/// to build `Ast::LetIn`/`Ast::LetRecIn` directly, just deferred into data
/// first so a `module`'s bindings can be spliced into the flat sequence
/// before any of it is turned into `Ast`.
fn nest<'s>(store: &'s SymbolStore, bindings: Vec<Binding<'s>>, tail: Ast<'s>) -> Ast<'s> {
    // `Binding` carries its key as text (it is minted by string mangling —
    // `qualify_key`, `$`-prefixing, `open`'s prefix suffixing); interning
    // happens here, where the key finally becomes an `Ast` node's identifier.
    let mut ast = tail;
    for b in bindings.into_iter().rev() {
        ast = match b {
            Binding::Let(name, val) => {
                Ast::LetIn(store.intern(&name), Box::new(val), Box::new(ast))
            }
            Binding::LetRec(bs) => Ast::LetRecIn(
                bs.into_iter().map(|(n, v)| (store.intern(&n), v)).collect(),
                Box::new(ast),
            ),
            Binding::LetMutable(name, val) => {
                Ast::LetMutableIn(store.intern(&name), Box::new(val), Box::new(ast))
            }
            Binding::LetMath(name, val) => {
                Ast::LetMathIn(store.intern(&name), Box::new(val), Box::new(ast))
            }
        };
    }
    ast
}

/// After binding `local` (inside a `module M = struct .. end`, i.e.
/// `mod_path` non-empty), also bind the qualified alias `M.local` — an
/// `Ast::Var`-referencing `LetIn`, the same alias-binding technique `open`
/// uses below — so later qualified references (and any enclosing `open`)
/// can resolve it. `local` is added to `running` (so *sibling* declarations
/// still see it unqualified) but never to `exported`: per v0.0.6 semantics,
/// after `end` only the qualified name is visible to what follows.
///
/// Only remaining caller: `TopBinding::LetRec`'s per-name loop, where `local`
/// is ALREADY bound bare (`rec_bindings`'s mutual-recursion scope needs every
/// clause visible to every other by its bare name before this runs) — so
/// there is no single value to re-bind under a mangled key the way
/// `push_named_binding` does. The bare name stays physically present in the
/// flat `nest()` chain and can leak past this module's `end` if it collides
/// with something later. A known, separable gap, narrower than
/// `push_named_binding`'s coverage — it needs a top-level `let rec .. and
/// ..` group directly inside a `module .. = struct .. end`, not any of the
/// far more common plain `val`/`let-inline`/`let-block`/`let-math`/`let
/// mutable` members.
fn export_alias<'s>(
    mod_path: &[String],
    local: String,
    shape: Vec<bool>,
    bindings: &mut Vec<Binding<'s>>,
    running: &mut Scope<'s>,
    exported: &mut Vec<String>,
) {
    if mod_path.is_empty() {
        running.insert_with_shape(&local, shape);
        exported.push(local);
    } else {
        // Same anti-leak scheme as `push_named_binding` (see its doc comment
        // for why the bare key can't be used directly) — e.g. this is what
        // stops satysfi-base's `Float.round : float -> float` from shadowing
        // the builtin `round : float -> int`.
        let qual = qualify_key(mod_path, &local);
        let mangled = format!("${qual}");
        bindings.push(Binding::Let(
            qual.clone(),
            Ast::Var(running.sym(&mangled), Span::default()),
        ));
        running.insert_with_shape(&local, shape.clone());
        running.rename(&local, &mangled);
        running.insert_with_shape(&qual, shape);
        exported.push(qual);
    }
}

/// `shape` is `local`'s recorded per-position optional-parameter shape (see
/// [`Scope`]'s doc comment) — non-empty for `TopBinding::Let` and for
/// `TopBinding::LetInline`/`LetBlock`/`LetMath` (`param_optional_shape`);
/// every other binding kind here passes an empty `Vec`.
///
/// For `mod_path` non-empty (inside `module M = struct .. end`), `value` is
/// bound under a MANGLED key (`"$M.local"` — `$` can't appear in a surface
/// identifier/command name, so it can't collide with anything user-written),
/// NOT under the bare `"local"`. A bare `LetIn` stays PHYSICALLY PRESENT in
/// the one flat `nest()` chain the whole program compiles to, which pops no
/// scopes of its own — so the bare name would stay bound, silently
/// SHADOWING any unrelated same-named binding (a base primitive, or another
/// package's member) for the rest of the merged program rather than until
/// this module's `end`. [`Scope::rename`] redirects a SIBLING member's bare
/// reference to the mangled key — consulted by [`scoped_var`] and the
/// inline/block/math command-key resolution sites in
/// `inline_elems`/`block_elems`/`math_bot`.
///
/// The qualified alias (`"M.local"`) is bound separately, and matters beyond
/// mere lookup: `v1/module_check.rs`'s sealing pass keys its opaque/stamped
/// type rewrite on this EXACT qualified string (`static_env.seals`) and
/// applies it ONLY to a binding whose OWN key matches. A mangled key never
/// matches, so a member's OWN body (and any SIBLING reaching it via the
/// redirect) keeps its naturally-inferred, TRANSPARENT type; only an
/// EXPLICIT qualified reference sees the sig's opaque view. Binding the
/// value directly under the qualified key, or redirecting siblings to it
/// instead of the mangled one, would break sealing for any member whose
/// body uses ANOTHER sealed sibling's value at an opaque type
/// (`v01_sealing.rs`'s `u1_opaque_accept`/`u8_command_decls`/
/// `u9_ctor_hiding`/`t13_escaped_skolem_message` all pin this).
///
/// The redirect and the mangled key both live only in `running`, this
/// recursive call's OWN local scope — never copied back to the caller
/// (only the qualified name's existence/shape is, via
/// `inner_running.optional_shape`) — so they can't affect anything outside
/// this module or after its `end`.
fn push_named_binding<'s>(
    mod_path: &[String],
    local: String,
    value: Ast<'s>,
    shape: Vec<bool>,
    make_binding: impl FnOnce(String, Ast<'s>) -> Binding<'s>,
    bindings: &mut Vec<Binding<'s>>,
    running: &mut Scope<'s>,
    exported: &mut Vec<String>,
) {
    if mod_path.is_empty() {
        bindings.push(make_binding(local.clone(), value));
        running.insert_with_shape(&local, shape);
        exported.push(local);
    } else {
        let qual = qualify_key(mod_path, &local);
        let mangled = format!("${qual}");
        // Mark the member's own RHS as belonging to `mod_path`, so a bare
        // constructor reference inside it resolves against this module's
        // constructors first (see `Ast::ModuleScope`). Transparent to eval /
        // type inference otherwise.
        let value = Ast::ModuleScope(mod_path.to_vec(), Box::new(value));
        bindings.push(make_binding(mangled.clone(), value));
        bindings.push(Binding::Let(
            qual.clone(),
            Ast::Var(running.sym(&mangled), Span::default()),
        ));
        running.insert_with_shape(&local, shape.clone());
        running.rename(&local, &mangled);
        running.insert_with_shape(&qual, shape);
        exported.push(qual);
    }
}

/// The per-position optional shape of a `Param` list (see [`Scope`]'s doc
/// comment for what this encodes and why, with its `stdja.satyh` example):
/// one `bool` per parameter, `true` exactly where it's a `Param::Optional`,
/// in declared order. Shared by a plain `let`'s params and a command
/// binding's (`let-inline`/`let-block`/`let-math`/`Expr::LetMathIn` — all
/// use the same `cst::ast::Param` list now, `cst.rs`'s `Param` doc comment).
/// Recorded into [`Scope::optional_shape`] so a marker-less call can
/// auto-omit any optional slot it reaches, not just a leading one (upstream
/// `typecheck_command_arguments` skips optional slots left unmarked
/// wherever they fall).
fn param_optional_shape(params: &[c::Param]) -> Vec<bool> {
    params
        .iter()
        .map(|p| matches!(p, c::Param::Optional { .. }))
        .collect()
}

/// The optional-parameter shape a *parameter-less alias* binding inherits from
/// its right-hand side. A `let x = y` (or `let x = M.y`) with no parameters of
/// its own is a plain value alias: `x` should carry exactly `y`'s declared
/// optional shape so a marker-less call `x a b` auto-omits `y`'s optionals the
/// same way `y a b` would (`app_chain_generic`). The motivating case is
/// `stdja.satyh`'s top-level `let document = StdJa.document`, re-exporting the
/// module member `document record ?:configopt inner` (shape `[false, true,
/// false]`) under the bare name every real document calls — `document rec
/// '<..>'`, omitting the optional `configopt`; without this the alias records
/// an empty shape and the block-text mis-binds against `configopt`'s domain.
/// Returns `&[]`-equivalent for any RHS that is not a bare (module-qualified)
/// variable reference — a value alias only, never a partial application.
fn alias_optional_shape<'s>(value: &c::Expr, scope: &Scope<'s>) -> Vec<bool> {
    let c::Expr::Ops(chain) = value else {
        return Vec::new();
    };
    if !chain.tail.is_empty() || chain.before.is_some() {
        return Vec::new();
    }
    let a = &chain.head;
    if a.minus.is_some()
        || a.excl.is_some()
        || a.stage.is_some()
        || !a.head_accesses.is_empty()
        || !a.args.is_empty()
    {
        return Vec::new();
    }
    head_optional_shape(&a.head, scope).to_vec()
}

/// Fold one sequence of top-level-shaped bindings — the file's own prelude
/// (`mod_path` empty) or a `module .. = struct .. end` body's decls
/// otherwise (`nxtoplevel`/`nxstruct` share every alternative but `Module`/
/// `Open`, see `cst.rs`'s `StructDecl` doc comment) — into an ordered
/// [`Binding`] list to [`nest`] around whatever follows, plus the names
/// visible *outside* this sequence (every name when `mod_path` is empty;
/// only the qualified aliases otherwise — see [`export_alias`]).
///
/// `Module` recurses with an extended `mod_path`; its bindings splice
/// directly into the flat list (so its `Ast::LetIn`s nest exactly where the
/// `module .. end` appeared textually), and its exported qualified names —
/// together with each one's [`Scope::optional_arity`], read off the
/// recursive call's own final `running` — fold into `running` (visible to
/// later siblings) and bubble up through `exported` (`module N = ..` nested
/// in `module M = ..` reaches `"M.N.x"` all the way to the file level), so a
/// qualified call to a leading-`?:`-optional function still auto-omits even
/// from outside its defining module.
///
/// The final `running` is returned as a third element so callers can reuse
/// it directly as the scope for what follows, rather than rebuild one from
/// `exported` strings alone — which would drop every `optional_arity` entry
/// (see [`elaborate_program`]).
fn walk_bindings<'s>(
    items: &[&cst::TopBinding],
    scope: &Scope<'s>,
    mod_path: &[String],
    type_decls: &mut Vec<UserTypeDecl>,
    synonym_decls: &mut Vec<UserSynonymDecl>,
    origins: &ItemOrigins<'_>,
    tymap: &HashMap<String, String>,
) -> Result<(Vec<Binding<'s>>, Vec<String>, Scope<'s>), ElabError> {
    let mut bindings: Vec<Binding<'s>> = Vec::new();
    let mut running = scope.clone();
    let mut exported: Vec<String> = Vec::new();
    // Module-local type-name qualification map (bare -> `M.t`). A no-op at the
    // top level (`mod_path` empty). Pre-scan ALL of this
    // level's `type` decls first so mutual/forward references (`type 'a state
    // = … and 'a u = ('a state) …`) resolve.
    let mut level_tymap = tymap.clone();
    if !mod_path.is_empty() {
        for top in items {
            if let cst::TopBinding::Type(decl) = top {
                for n in std::iter::once(&decl.name).chain(decl.ands.iter().map(|a| &a.name)) {
                    if !n.name.contains('.') {
                        level_tymap.insert(n.name.clone(), qualify_key(mod_path, &n.name));
                    }
                }
            }
        }
    }
    for (item_idx, top) in items.iter().enumerate() {
        // Is THIS top-level item (and everything nested inside
        // it, e.g. a `module .. = struct .. end`'s own decls — see the
        // `Module` arm below) part of a spliced V0_0 dependency? Always
        // `false` for `elaborate_program`'s empty `v006_indices` (the
        // pure-0.0.6 / pure-0.1 paths), so this is a dead branch there.
        let this_v006 = origins.v006.contains(&item_idx);
        // The stage the file this item came from declared, if not the default.
        // A stage the BINDING declared on itself (0.1's `val ~x`) wins over
        // the one its FILE declared (0.0.6's `@stage:`) — they cannot both be
        // set, since no file is authored in both generations, so the `or` is
        // really a merge of two disjoint sources rather than a precedence
        // rule.
        let own_stage = match top {
            cst::TopBinding::Let(b) => b.stage.as_ref(),
            cst::TopBinding::LetRec { stage, .. }
            | cst::TopBinding::LetInline { stage, .. }
            | cst::TopBinding::LetBlock { stage, .. }
            | cst::TopBinding::LetMath { stage, .. }
            | cst::TopBinding::LetMutable { stage, .. } => stage.as_ref(),
            _ => None,
        };
        let this_stage = binding_stage(own_stage, scope.version, this_v006)?
            .or_else(|| origins.stages.get(&item_idx).copied());
        // Every binding this item is about to append belongs to `this_stage`
        // — including the aliases the arms below mint alongside the value
        // itself. Recorded by index so `stage_wrap_item` can wrap exactly
        // that range once the arm is done (see its doc comment).
        let bindings_before = bindings.len();
        match top {
            cst::TopBinding::Let(top_let) => {
                // Same curry-with-patterns desugaring as `rec_clause_value`
                // (see its doc comment), minus multi-clause `extra`;
                // `gr.satyh`'s tuple-destructuring params hit the general
                // path there.
                let top_let_params = params_to_patbots(&top_let.params);
                let value = rec_clause_value(&top_let_params, &top_let.value, &[], &running)?;
                let value = maybe_v006_scope(value, this_v006);
                // A parameter-less binding may be a plain value alias
                // (`let document = StdJa.document`) — inherit the aliased
                // name's optional shape so a marker-less call auto-omits its
                // optionals (see `alias_optional_shape`).
                let mut shape = param_optional_shape(&top_let.params);
                if shape.is_empty() && top_let.params.is_empty() {
                    shape = alias_optional_shape(&top_let.value, &running);
                }
                push_named_binding(
                    mod_path,
                    top_let.name.name.clone(),
                    value,
                    shape,
                    Binding::Let,
                    &mut bindings,
                    &mut running,
                    &mut exported,
                );
            }
            cst::TopBinding::LetPattern { pat, value, .. } => {
                // Destructuring `let pat = value` at struct/top level (the
                // binding twin of `Expr::LetPatternIn`): evaluate `value` ONCE
                // under a hidden internal name, then bind each pattern
                // variable to `match hidden with pat -> var` — so every name
                // is a normal (module-qualifiable) member. `%`-prefixed names
                // are internal-only and never exported.
                let value_ast = expr(value, &running)?;
                let value_ast = maybe_v006_scope(value_ast, this_v006);
                let lowered_pat = pattern(running.store, pat)?;
                let mut names = Vec::new();
                collect_pattern_names(running.store, &lowered_pat, &mut names);
                let hidden = format!("%patbind.{}.{}", mod_path.join("."), item_idx);
                let scrut = if mod_path.is_empty() {
                    value_ast
                } else {
                    Ast::ModuleScope(mod_path.to_vec(), Box::new(value_ast))
                };
                bindings.push(Binding::Let(hidden.clone(), scrut));
                running.insert_with_shape(&hidden, Vec::new());
                for n in &names {
                    let extract = Ast::Match(
                        Box::new(Ast::Var(running.sym(&hidden), Span::default())),
                        vec![MatchArm {
                            pat: lowered_pat.clone(),
                            guard: None,
                            body: Ast::Var(running.sym(n), Span::default()),
                        }],
                    );
                    push_named_binding(
                        mod_path,
                        n.to_string(),
                        extract,
                        Vec::new(),
                        Binding::Let,
                        &mut bindings,
                        &mut running,
                        &mut exported,
                    );
                }
            }
            cst::TopBinding::LetRec { first, ands, .. } => {
                let (recs, rec_scope) = rec_bindings(first, ands, &running, mod_path)?;
                running = rec_scope;
                // BARE clause names (for `export_alias`) — the `recs` keys are
                // now MANGLED inside a module, so derive names from the source.
                let names: Vec<String> = std::iter::once(&first.name.name)
                    .chain(ands.iter().map(|a| &a.binding.name.name))
                    .cloned()
                    .collect();
                // RHS granularity — wrap EACH recursive clause's
                // own body individually (not the `LetRecIn` node as a
                // whole), matching `elaborate_program_with_versions`'s doc
                // comment.
                let recs = if this_v006 {
                    recs.into_iter()
                        .map(|(n, body)| {
                            (
                                n,
                                Rc::new(Ast::VersionScope(
                                    RustyfiVersion::V0_0,
                                    Box::new((*body).clone()),
                                )),
                            )
                        })
                        .collect()
                } else {
                    recs
                };
                // Same per-clause granularity for the stage: the `LetRecIn`
                // node itself is not an expression the typechecker reads at a
                // stage, its clause BODIES are.
                let recs: Vec<(String, Rc<Ast<'s>>)> = match this_stage {
                    Some(st) => recs
                        .into_iter()
                        .map(|(n, body)| {
                            (n, Rc::new(Ast::StageScope(st, Box::new((*body).clone()))))
                        })
                        .collect(),
                    None => recs,
                };
                // Mark each clause body as belonging to `mod_path` (ctor
                // scoping — see `Ast::ModuleScope`); a no-op at top level.
                let recs: Vec<(String, Rc<Ast<'s>>)> = if mod_path.is_empty() {
                    recs
                } else {
                    recs.into_iter()
                        .map(|(n, body)| {
                            (
                                n,
                                Rc::new(Ast::ModuleScope(
                                    mod_path.to_vec(),
                                    Box::new((*body).clone()),
                                )),
                            )
                        })
                        .collect()
                };
                bindings.push(Binding::LetRec(recs));
                for n in names {
                    export_alias(
                        mod_path,
                        n,
                        Vec::new(),
                        &mut bindings,
                        &mut running,
                        &mut exported,
                    );
                }
            }
            cst::TopBinding::LetInline {
                ctx,
                cmd,
                params,
                value,
                ..
            } => {
                let value_ast =
                    elaborate_let_inline(ctx.as_ref(), params, value, &running, "read-inline")?;
                let value_ast =
                    maybe_v006_scope(value_ast, this_v006);
                push_named_binding(
                    mod_path,
                    cmd.name.clone(),
                    value_ast,
                    param_optional_shape(params),
                    Binding::Let,
                    &mut bindings,
                    &mut running,
                    &mut exported,
                );
            }
            cst::TopBinding::LetBlock {
                ctx,
                cmd,
                params,
                value,
                ..
            } => {
                let value_ast =
                    elaborate_let_inline(ctx.as_ref(), params, value, &running, "read-block")?;
                let value_ast =
                    maybe_v006_scope(value_ast, this_v006);
                push_named_binding(
                    mod_path,
                    cmd.name.clone(),
                    value_ast,
                    param_optional_shape(params),
                    Binding::Let,
                    &mut bindings,
                    &mut running,
                    &mut exported,
                );
            }
            cst::TopBinding::LetMath {
                cmd,
                params,
                value,
                ..
            } => {
                let value_ast = elaborate_let_math(params, value, &running)?;
                let value_ast =
                    maybe_v006_scope(value_ast, this_v006);
                push_named_binding(
                    mod_path,
                    cmd.name.clone(),
                    value_ast,
                    param_optional_shape(params),
                    Binding::LetMath,
                    &mut bindings,
                    &mut running,
                    &mut exported,
                );
            }
            // `type` declarations have no runtime effect in this untyped
            // elaborator: constructors are bare `Ctor` atoms, never scope-
            // checked, and a synonym is never itself a runtime value — so
            // neither needs a scope entry. Both are still surfaced
            // (unqualified; see `UserTypeDecl`/`UserSynonymDecl`) for the
            // typechecker.
            cst::TopBinding::Type(decl) => {
                for lowered in lower_type_decl(decl, mod_path, &level_tymap) {
                    match lowered {
                        LoweredTypeDecl::Variant(v) => type_decls.push(v),
                        LoweredTypeDecl::Synonym(s) => synonym_decls.push(s),
                    }
                }
            }
            cst::TopBinding::LetMutable {
                name, value, ..
            } => {
                let value_ast = expr(value, &running)?;
                // The stage wraps the INITIAL value (the only expression a
                // `let-mutable` holds); `Binding::LetMutable` then makes the
                // ref cell out of it.
                let value_ast =
                    maybe_v006_scope(value_ast, this_v006);
                push_named_binding(
                    mod_path,
                    name.name.clone(),
                    value_ast,
                    Vec::new(),
                    Binding::LetMutable,
                    &mut bindings,
                    &mut running,
                    &mut exported,
                );
            }
            cst::TopBinding::Module {
                name, sig, decls, ..
            } => {
                // Signature annotations (`sig .. end`) are accepted and
                // ignored: this elaborator does no type checking, so
                // `val`/`type` items have nothing to check against (full
                // reconciliation is deferred). `direct` items ARE handled:
                // each exposes its command UNQUALIFIED at the enclosing
                // scope, aliasing the module's qualified binding — the same
                // `Ast::Var`-alias trick `export_alias`/`Open` use below.
                // `typecheck.rs`'s `command_scheme` threads command types
                // through an alias site transparently, so the exposed name
                // gets its command type for free.
                let mut child_path = mod_path.to_vec();
                child_path.push(name.name.clone());
                let inner_items: Vec<&cst::TopBinding> =
                    decls.iter().map(|d| d.0.as_ref()).collect();
                // A nested `module .. = struct .. end` has no
                // index correspondence to the OUTER `v006_indices` (that set
                // indexes THIS level's `items`, not `inner_items`) — if the
                // enclosing item is itself v006-marked, every inner item is
                // too (the whole subtree came from the same spliced 0.0.6
                // file); otherwise none are.
                let inner_v006: HashSet<usize> = if this_v006 {
                    (0..inner_items.len()).collect()
                } else {
                    HashSet::new()
                };
                // Same reasoning for the stage: a nested module's items are
                // indexed against `inner_items`, so the enclosing item's stage
                // (if any) applies to all of them.
                let inner_stages: HashMap<usize, crate::types::Stage> = match this_stage {
                    Some(st) => (0..inner_items.len()).map(|i| (i, st)).collect(),
                    None => HashMap::new(),
                };
                let (inner_bindings, inner_exported, inner_running) = walk_bindings(
                    &inner_items,
                    &running,
                    &child_path,
                    type_decls,
                    synonym_decls,
                    &ItemOrigins {
                        v006: &inner_v006,
                        stages: &inner_stages,
                    },
                    &level_tymap,
                )?;
                // A module's own bare (unqualified) member names never leak
                // past this `end`: `push_named_binding` (used by every
                // ordinary member below) binds each member under a MANGLED
                // key and registers a `Scope::rename` redirect for sibling
                // lookups (see that function's doc comment). Naive scope-
                // popping is NOT an option here, because `nest()` produces
                // one flat `LetIn` chain and
                // `v1/module_check.rs`'s spine-walking sealing pass only
                // recognizes TOP-LEVEL `LetIn`/`LetMathIn`/`LetRecIn`/
                // `LetMutableIn` nodes, not ones nested inside a wrapper
                // sub-expression.
                bindings.extend(inner_bindings);
                // The enclosing context's own module prefix (`Outer.` when
                // this whole `walk_bindings` is elaborating `module Outer`'s
                // body). Each nested member is ALSO exposed under its
                // ENCLOSING-relative name so a sibling's `Inner.double`
                // reference resolves (a nested module `N` inside `M` binds its
                // members as `M.N.x`, but a sibling writes `N.x`).
                let self_prefix = if mod_path.is_empty() {
                    String::new()
                } else {
                    format!("{}.", mod_path.join("."))
                };
                for q in &inner_exported {
                    let shape = inner_running.optional_shape(q).to_vec();
                    running.insert_with_shape(q, shape.clone());
                    if !self_prefix.is_empty() {
                        if let Some(rel) = q.strip_prefix(&self_prefix) {
                            running.insert_with_shape(rel, shape);
                            running.rename(rel, q);
                        }
                    }
                }
                if let Some(sig_annot) = sig {
                    for item in &sig_annot.items {
                        if let Some((local, span)) = direct_cmd_name(item) {
                            let qual = qualify_key(&child_path, &local);
                            // Cheap positive-obligation check (a `direct`-only
                            // slice of the fuller sig-preservation, which
                            // stays deferred for `val`/`type` items): the
                            // struct must actually define what it declares
                            // `direct`, or the alias below would dangle.
                            if !inner_exported.contains(&qual) {
                                return err(
                                    span,
                                    format!(
                                        "module `{}` signature declares `direct {local} : ..` \
                                         but its `struct .. end` body never defines `{local}`",
                                        name.name
                                    ),
                                );
                            }
                            let shape = running.optional_shape(&qual).to_vec();
                            bindings.push(Binding::Let(
                                local.clone(),
                                Ast::Var(running.sym(&qual), Span::default()),
                            ));
                            running.insert_with_shape(&local, shape);
                            exported.push(local);
                        }
                    }
                }
                exported.extend(inner_exported);
            }
            cst::TopBinding::Open { name, .. } => {
                let prefix = format!("{}.", name.name);
                for q in running.names_with_prefix(&prefix) {
                    let suffix = q[prefix.len()..].to_string();
                    let shape = running.optional_shape(&q).to_vec();
                    bindings.push(Binding::Let(
                        suffix.clone(),
                        Ast::Var(running.sym(&q), Span::default()),
                    ));
                    running.insert_with_shape(&suffix, shape);
                    // `open` only re-exposes an *existing* qualified name
                    // under its bare suffix locally; it doesn't itself mint
                    // a new qualified name, so nothing goes into `exported`
                    // here.
                }
                // Also overlay the opened module's DIRECT type members so a
                // later bare reference to one resolves to its qualified name
                // (the type analog of the value re-exposure above). Only
                // direct members (`M.t`, never `M.N.t`), mirroring the value
                // `names_with_prefix` rule; the module is already fully walked
                // (`open` names an earlier module), so `type_decls`/
                // `synonym_decls` hold its qualified entries.
                for q in type_decls
                    .iter()
                    .map(|d| &d.name)
                    .chain(synonym_decls.iter().map(|s| &s.name))
                {
                    if let Some(suffix) = q.strip_prefix(&prefix) {
                        if !suffix.contains('.') {
                            level_tymap.insert(suffix.to_string(), q.clone());
                        }
                    }
                }
            }
        }
        if let Some(st) = this_stage {
            stage_wrap_item(&mut bindings[bindings_before..], st);
        }
    }
    Ok((bindings, exported, running))
}

/// Curry a command binding's (`let-inline`/`let-block`/`let-math`) `Param`
/// list — already widened to `PatBot` by `params_to_patbots` — around a
/// value built from the fully-extended scope, mirroring `rec_clause_value`'s
/// two-path shape but per-param rather than clause-tuple (upstream's
/// `curry_lambda_abstract` builds one `UTFunction` per `cmdarglst` element,
/// `parser.mly:50-63`, unlike `let-rec`'s single tupled match — kept as an
/// intentional divergence because that's what upstream itself does for
/// command arguments).
///
/// The all-variable-parameter fast path emits a plain `Lambda` chain; it
/// must, since `elaborate_let_inline`'s "lightweight" form builds its
/// `read-inline`/`read-block` application *inside* `build_value` (called
/// with the innermost, fully-extended scope), so the wrapping must nest
/// *inside* every curried parameter. The general path instead lowers each
/// parameter to its own `Lambda(%cmd_argN, Match(%cmd_argN, [pat -> rest]))`
/// — a refutable pattern (e.g. `Some(x)`) can fail at *application* time,
/// like any `match` arm (see `eval.rs`'s `Ast::Match` for the resulting
/// runtime error).
fn curry_cmd_params<'s>(
    patbots: &[c::PatBot],
    scope: &Scope<'s>,
    build_value: impl FnOnce(&Scope<'s>) -> Result<Ast<'s>, ElabError>,
) -> Result<Ast<'s>, ElabError> {
    if patbots.iter().all(is_var_patbot) {
        let mut inner = scope.clone();
        for p in patbots {
            inner = inner.with(patbot_var_name(p));
        }
        let mut value_ast = build_value(&inner)?;
        for p in patbots.iter().rev() {
            value_ast = Ast::Lambda(scope.sym(patbot_var_name(p)), Rc::new(value_ast));
        }
        return Ok(value_ast);
    }
    let pats: Vec<Pattern<'s>> = patbots
        .iter()
        .map(|p| patbot(scope.store, p))
        .collect::<Result<_, _>>()?;
    let mut names = Vec::new();
    for p in &pats {
        collect_pattern_names(scope.store, p, &mut names);
    }
    let mut inner = scope.clone();
    for n in &names {
        inner = inner.with(n);
    }
    let mut value_ast = build_value(&inner)?;
    let dummy = Span::default();
    for (i, pat) in pats.into_iter().enumerate().rev() {
        let fresh = scope.sym(&format!("%cmd_arg{i}"));
        value_ast = Ast::Lambda(
            fresh,
            Rc::new(Ast::Match(
                Box::new(Ast::Var(fresh, dummy)),
                vec![MatchArm {
                    pat,
                    guard: None,
                    body: value_ast,
                }],
            )),
        );
    }
    Ok(value_ast)
}

/// `[ctxvar] let-inline \cmd param* = value` / `[ctxvar] let-block +cmd
/// param* = value` (`nxhorzdec`/`nxvertdec` in `parser.mly`, lines 548-577).
/// Each `param` is upstream's `arg` (`cst.rs`'s `Param` doc comment — a full
/// patbot, a `?:`-marked variable, or a
/// `?(l = x, …)` labeled-optional bundle), curried via the bundle-aware
/// `curry_cmd_params_v1` (which delegates wholesale to `curry_cmd_params`
/// when no bundle is present).
///
/// Two forms, confirmed against v0.0.6 `parser.mly`:
/// * with an explicit leading context variable, the value is elaborated
///   as-is (already inline-boxes/block-boxes typed) under
///   `Lambda(ctxvar, Lambda(p1, .., value))`;
/// * without one (the "lightweight" form), `parser.mly` synthesizes an
///   implicit `%context` variable and wraps the (inline-text/block-text
///   typed) value in a `read-inline`/`read-block` call *inside* the
///   curried parameters but *around* the value itself:
///   `curry_lambda_abstract_pattern params (read-inline %context value)`,
///   all wrapped in `Lambda(%context, ..)`. We reproduce that exactly,
///   using `reader` = `"read-inline"` or `"read-block"`.
fn elaborate_let_inline<'s>(
    ctx: Option<&VarTok>,
    params: &[c::Param],
    value: &c::Expr,
    scope: &Scope<'s>,
    reader: &str,
) -> Result<Ast<'s>, ElabError> {
    match ctx {
        Some(ctxvar) => {
            let ctx_scope = scope.with(&ctxvar.name);
            let value_ast = curry_cmd_params_v1(params, &ctx_scope, |inner| expr(value, inner))?;
            Ok(Ast::Lambda(scope.sym(&ctxvar.name), Rc::new(value_ast)))
        }
        None => {
            const IMPLICIT_CTX: &str = "%context";
            let dummy = Span::default();
            let ctx_scope = scope.with(IMPLICIT_CTX);
            let curried = curry_cmd_params_v1(params, &ctx_scope, |inner| {
                let value_ast = expr(value, inner)?;
                let read_fn = scoped_var(reader, dummy, inner)?;
                let ctx_var = scoped_var(IMPLICIT_CTX, dummy, inner)?;
                Ok(Ast::Apply(
                    Box::new(Ast::Apply(Box::new(read_fn), Box::new(ctx_var))),
                    Box::new(value_ast),
                ))
            })?;
            Ok(Ast::Lambda(scope.sym(IMPLICIT_CTX), Rc::new(curried)))
        }
    }
}

/// `let-math \cmd param* = expr` (upstream `nxmathdec`, `parser.mly:586-591`):
/// curry `params` (upstream's `arg`, `cst.rs`'s `Param` doc comment) via
/// `curry_cmd_params`, with **no** implicit/explicit context variable at all
/// (contrast `elaborate_let_inline`, which always threads one) — a math
/// command's own type (`math-cmd`) carries no context argument. A zero-param
/// binding (e.g. `let-math \to = rel \`→\``) elaborates to `value` directly,
/// un-wrapped. Shared by `TopBinding::LetMath` (via `walk_bindings`) and the
/// expression-level `Expr::LetMathIn` (`parser.mly:688`, upstream's only
/// command binding with a local `in`-bodied form — see that variant's doc
/// comment).
fn elaborate_let_math<'s>(
    params: &[c::Param],
    value: &c::Expr,
    scope: &Scope<'s>,
) -> Result<Ast<'s>, ElabError> {
    curry_cmd_params_v1(params, scope, |inner| expr(value, inner))
}

/// Elaborate one `let-rec` clause group (shared by the local `Expr::LetRecIn`
/// and the top-level `TopBinding::LetRec`): every name is in scope in every
/// binding's own value (mutual recursion) as well as in the body, and each
/// binding's own parameters curry into a `Lambda` around its elaborated
/// value. Whether the (possibly zero) curried result is actually a function
/// is a *runtime* check (see `eval.rs`'s `Ast::LetRecIn` handling) — nothing
/// here forces `params` to be non-empty, since a paramterless binding whose
/// `value` is itself e.g. a `fun ...` expression is equally valid.
fn rec_bindings<'s>(
    first: &c::RecBinding,
    ands: &[c::AndBinding],
    scope: &Scope<'s>,
    mod_path: &[String],
) -> Result<(Vec<(String, Rc<Ast<'s>>)>, Scope<'s>), ElabError> {
    let all: Vec<&c::RecBinding> = std::iter::once(first)
        .chain(ands.iter().map(|a| &a.binding))
        .collect();
    let mut rec_scope = scope.clone();
    for rb in &all {
        rec_scope = rec_scope.with(&rb.name.name);
    }
    // Inside a `module M = struct .. end`, bind each clause under a MANGLED key
    // (`$M.name`) and redirect its (self/mutual/sibling) bare references there,
    // so the recursive value never leaks into the flat program scope under its
    // bare name (see `export_alias`). A top-level (`mod_path` empty) `let-rec`
    // keeps bare keys.
    let key_of = |name: &str| -> String {
        if mod_path.is_empty() {
            name.to_string()
        } else {
            format!("${}", qualify_key(mod_path, name))
        }
    };
    if !mod_path.is_empty() {
        for rb in &all {
            rec_scope.rename(&rb.name.name, &key_of(&rb.name.name));
        }
    }
    let mut bindings = Vec::with_capacity(all.len());
    for rb in all {
        let value_ast = rec_clause_value(&rb.params, &rb.value, &rb.extra, &rec_scope)?;
        bindings.push((key_of(&rb.name.name), Rc::new(value_ast)));
    }
    Ok((bindings, rec_scope))
}

/// Elaborate the (possibly multi-clause) value of one `let-rec` binding
/// (`RecBinding`/`RecClause`: `name [|] patbot* = value (| patbot* =
/// value)*`). A multi-clause definition desugars into one curried function
/// of `n` fresh parameters (`n` = every clause's shared arity — an
/// `IllegalArgumentLength`-style error if they disagree) that matches a
/// tuple of them against each clause's patterns in turn, first clause first
/// (`option.satyg`'s `let-rec map | f (None) = None | f (Some(v)) = Some(f
/// v)`: 2 clauses, arity 2). At arity 1 the "tuple" is just the single fresh
/// parameter, no `Ast::Tuple` wrapper (matches `list.satyg`'s single-
/// parameter clauses, e.g. `let-rec append lst1 lst2 = ..`, mixed with
/// genuinely-refutable single clauses elsewhere).
///
/// The single-clause, all-variable-parameter case (`let-rec f x y = ..`, no
/// `|` — the common shape) special-cases to a direct `Lambda` chain:
/// behaviorally identical to the general path, it just skips a throwaway
/// `Match`/fresh-variable indirection.
fn rec_clause_value<'s>(
    params0: &[c::PatBot],
    value0: &c::Expr,
    extra: &[c::RecClause],
    scope: &Scope<'s>,
) -> Result<Ast<'s>, ElabError> {
    let arity = params0.len();
    for cl in extra {
        if cl.params.len() != arity {
            return err(
                cl.bar.0,
                format!(
                    "every clause of a multi-clause 'let-rec' binding must bind the \
                     same number of parameters (expected {arity}, got {})",
                    cl.params.len()
                ),
            );
        }
    }

    if extra.is_empty() && params0.iter().all(is_var_patbot) {
        let mut inner = scope.clone();
        for p in params0 {
            inner = inner.with(patbot_var_name(p));
        }
        let mut value_ast = expr(value0, &inner)?;
        for p in params0.iter().rev() {
            value_ast = Ast::Lambda(scope.sym(patbot_var_name(p)), Rc::new(value_ast));
        }
        return Ok(value_ast);
    }

    let fresh: Vec<Symbol<'s>> = (0..arity)
        .map(|i| scope.sym(&format!("%rec_arg{i}")))
        .collect();
    let mut arms = Vec::with_capacity(1 + extra.len());
    arms.push(rec_clause_arm(params0, value0, scope)?);
    for cl in extra {
        arms.push(rec_clause_arm(&cl.params, &cl.value, scope)?);
    }
    let dummy = Span::default();
    let scrutinee = if arity == 1 {
        Ast::Var(fresh[0], dummy)
    } else {
        Ast::Tuple(fresh.iter().map(|f| Ast::Var(*f, dummy)).collect())
    };
    let mut body = Ast::Match(Box::new(scrutinee), arms);
    for f in fresh.iter().rev() {
        body = Ast::Lambda(*f, Rc::new(body));
    }
    Ok(body)
}

/// Lower a SATySFi 0.1 `fun ?(l = x, …) p -> body` unit (`Expr::FunRows`) to
/// an [`Ast::LambdaOpt`]. Gated on the V0_1 source version (a 0.0.6-parsed
/// occurrence — reachable only via the additive-`cst` accept surface — is
/// rejected here with a version error). Duplicate labels in one binder list
/// are rejected. Each optional binder and the positional param enter scope
/// as plain names (labeled optionals have no marker-less padding, so NO
/// `optional_arity` entry). A pattern param desugars to a fresh var + `Match`
/// exactly as `rec_clause_value` does for a destructuring parameter.
fn fun_rows_to_ast<'s>(
    kw_span: Span,
    opts: &c::CstOptBinders,
    param: &c::PatBot,
    body: &c::Expr,
    scope: &Scope<'s>,
) -> Result<Ast<'s>, ElabError> {
    if !scope.version.has_row_polymorphism() {
        return err(
            kw_span,
            "labeled optional arguments (`?(l = x)`) are SATySFi 0.1 syntax — \
             this file is compiled as 0.0.6",
        );
    }
    let mut inner = scope.clone();
    for e in &opts.entries {
        inner = inner.with(&e.var.name);
    }
    let body_ast = if is_var_patbot(param) {
        let body_scope = inner.with(patbot_var_name(param));
        expr(body, &body_scope)?
    } else {
        let pat = patbot(scope.store, param)?;
        let mut names = Vec::new();
        collect_pattern_names(scope.store, &pat, &mut names);
        let mut body_scope = inner;
        for n in &names {
            body_scope = body_scope.with(n);
        }
        expr(body, &body_scope)?
    };
    lambda_opt_from(scope.store, opts, param, body_ast)
}

/// Build an `Ast::LambdaOpt` from a `?(l = x, …)` binder bundle, its
/// positional param, and an ALREADY-ELABORATED inner body — the shared core
/// factored out of [`fun_rows_to_ast`] (a value-level `fun ?(l = x) p ->
/// body` unit) so [`curry_cmd_params_v1`]'s bundle arm (a command
/// parameter bundle) can reuse the exact
/// same binder logic. Duplicate labels in one binder list are rejected. A
/// `PatBot::Var` param becomes the `LambdaOpt`'s param directly; any other
/// pattern desugars to a fresh `%opt_arg` var + `Match`, exactly like
/// `rec_clause_value`'s destructuring-parameter path.
fn lambda_opt_from<'s>(
    store: &'s SymbolStore,
    opts: &c::CstOptBinders,
    param: &c::PatBot,
    inner_body_ast: Ast<'s>,
) -> Result<Ast<'s>, ElabError> {
    // `(label, binder)`: the label is data and stays text, the binder is a
    // lexical variable and is interned (see `ast::Ast::LambdaOpt`).
    let mut opt_pairs: Vec<(String, Symbol<'s>)> = Vec::with_capacity(opts.entries.len());
    let mut seen = HashSet::new();
    for e in &opts.entries {
        if !seen.insert(e.label.name.clone()) {
            return err(
                e.label.span,
                format!(
                    "duplicate optional label `{}` in one `?(…)` binder list",
                    e.label.name
                ),
            );
        }
        opt_pairs.push((e.label.name.clone(), store.intern(&e.var.name)));
    }
    if is_var_patbot(param) {
        Ok(Ast::LambdaOpt {
            opts: opt_pairs,
            param: store.intern(patbot_var_name(param)),
            body: Rc::new(inner_body_ast),
        })
    } else {
        let fresh = store.intern("%opt_arg");
        let pat = patbot(store, param)?;
        let matched = Ast::Match(
            Box::new(Ast::Var(fresh, Span::default())),
            vec![MatchArm {
                pat,
                guard: None,
                body: inner_body_ast,
            }],
        );
        Ok(Ast::LambdaOpt {
            opts: opt_pairs,
            param: fresh,
            body: Rc::new(matched),
        })
    }
}

/// The bundle-aware command-parameter currier: same overall shape as [`curry_cmd_params`] — extend the scope with
/// every name the parameter list binds, build the innermost value once
/// against the fully-extended scope, then curry back outward — but also
/// handles a `Param::Bundled { opts, body }` entry (`?(l = x, …) pat`) by
/// emitting an `Ast::LambdaOpt` for that slot (via [`lambda_opt_from`])
/// instead of a plain `Ast::Lambda`/`Match`.
///
/// **Delegates wholesale to [`curry_cmd_params`]** when `params` has no
/// `Bundled` entry — every 0.0.6 binding and most V0_1 ones.
///
/// **Version-gated** like `fun_rows_to_ast`: a `Bundled` entry reaching the
/// general fold under `!scope.version.has_row_polymorphism()` is rejected
/// with the same version error — purely defensive, since only
/// `v1/lower.rs::lower_command_params` ever constructs `Param::Bundled`, and
/// `lower_value_math` already rejects it for a `val math` binding before
/// elaboration.
fn curry_cmd_params_v1<'s>(
    params: &[c::Param],
    scope: &Scope<'s>,
    build_value: impl FnOnce(&Scope<'s>) -> Result<Ast<'s>, ElabError>,
) -> Result<Ast<'s>, ElabError> {
    if !params.iter().any(|p| matches!(p, c::Param::Bundled { .. })) {
        let patbots = params_to_patbots(params);
        return curry_cmd_params(&patbots, scope, build_value);
    }
    if !scope.version.has_row_polymorphism() {
        let bundle_span = params
            .iter()
            .find_map(|p| match p {
                c::Param::Bundled { opts, .. } => Some(opts.q.0),
                _ => None,
            })
            .expect("just checked a `Param::Bundled` entry exists");
        return err(
            bundle_span,
            "labeled optional arguments (`?(l = x)`) are SATySFi 0.1 syntax — \
             this file is compiled as 0.0.6",
        );
    }
    let mut inner = scope.clone();
    for p in params {
        inner = match p {
            c::Param::Bundled { opts, body } => {
                for e in &opts.entries {
                    inner = inner.with(&e.var.name);
                }
                extend_with_patbot(inner, body)?
            }
            _ => extend_with_patbot(inner, &param_to_patbot(p))?,
        };
    }
    let mut value_ast = build_value(&inner)?;
    let dummy = Span::default();
    for (i, p) in params.iter().enumerate().rev() {
        value_ast = match p {
            c::Param::Bundled { opts, body } => {
                lambda_opt_from(scope.store, opts, body, value_ast)?
            }
            c::Param::Optional { name, .. } => {
                Ast::Lambda(scope.sym(&name.name), Rc::new(value_ast))
            }
            c::Param::Pat(pat) if is_var_patbot(pat) => {
                Ast::Lambda(scope.sym(patbot_var_name(pat)), Rc::new(value_ast))
            }
            c::Param::Pat(pat) => {
                let pp = patbot(scope.store, pat)?;
                let fresh = scope.sym(&format!("%cmd_arg{i}"));
                Ast::Lambda(
                    fresh,
                    Rc::new(Ast::Match(
                        Box::new(Ast::Var(fresh, dummy)),
                        vec![MatchArm {
                            pat: pp,
                            guard: None,
                            body: value_ast,
                        }],
                    )),
                )
            }
        };
    }
    Ok(value_ast)
}

/// Extend `scope` with every name patbot `p` binds: its single var name if
/// it's a plain `PatBot::Var`, else every name the full pattern binds
/// (`collect_pattern_names`) — the scope half of `curry_cmd_params_v1`'s
/// general fold (mirroring `curry_cmd_params`'s own inline scope-extension,
/// factored out here since the bundle-aware fold interleaves it with a
/// bundle's own binder names).
fn extend_with_patbot<'s>(scope: Scope<'s>, p: &c::PatBot) -> Result<Scope<'s>, ElabError> {
    if is_var_patbot(p) {
        Ok(scope.with(patbot_var_name(p)))
    } else {
        let store = scope.store;
        let pat = patbot(store, p)?;
        let mut names = Vec::new();
        collect_pattern_names(store, &pat, &mut names);
        let mut s = scope;
        for n in &names {
            s = s.with(n);
        }
        Ok(s)
    }
}

/// Widen a plain (non-`let-rec`) `let`'s `Param` down to a `PatBot`, so
/// `TopLet`/`Expr::LetIn` can share `rec_clause_value`'s pattern-currying
/// machinery with `let-rec` unchanged: the def-site optional marker
/// (`Param::Optional`, `?:name`) carries no elaboration-time semantics of
/// its own in this port (see `cst.rs`'s `Param` doc comment) — it is simply
/// a plain variable binder, `PatBot::Var`.
fn param_to_patbot(p: &c::Param) -> c::PatBot {
    match p {
        c::Param::Optional { name, .. } => c::PatBot::Var(name.clone()),
        c::Param::Pat(pat) => pat.clone(),
        // A `?(l = x, …)` command-parameter bundle
        // never reaches this widener: `v1/lower.rs::
        // lower_command_params` is its only constructor, for a command
        // binding's OWN `Param` list, and `curry_cmd_params_v1` — that
        // list's only caller — checks for `Bundled` itself and routes
        // around this widener entirely when found (see its doc comment). A
        // plain `let`/`let-rec`'s `Param` list (this widener's other caller)
        // can't contain one either — `lower_param_units` always right-folds
        // a bundled unit into an `Expr::FunRows` chain, returning an EMPTY
        // `Param` list when any unit is bundled.
        c::Param::Bundled { .. } => {
            unreachable!("a `?(l = x)` command-parameter bundle cannot reach `param_to_patbot`")
        }
    }
}

fn params_to_patbots(params: &[c::Param]) -> Vec<c::PatBot> {
    params.iter().map(param_to_patbot).collect()
}

fn is_var_patbot(p: &c::PatBot) -> bool {
    matches!(p, c::PatBot::Var(_))
}

/// Panics if `p` isn't `PatBot::Var` — callers must check [`is_var_patbot`] first.
fn patbot_var_name(p: &c::PatBot) -> &str {
    match p {
        c::PatBot::Var(v) => &v.name,
        _ => unreachable!("patbot_var_name called on a non-Var PatBot"),
    }
}

/// One `patbot* = value` clause of a multi-clause `let-rec`, lowered to a
/// [`MatchArm`] over the clause's parameter patterns (see
/// [`rec_clause_value`]'s doc comment for the arity-1-vs-N pattern shape) —
/// the body sees every name the patterns bind, exactly like an ordinary
/// `match` arm ([`match_arm`], below).
fn rec_clause_arm<'s>(
    params: &[c::PatBot],
    value: &c::Expr,
    scope: &Scope<'s>,
) -> Result<MatchArm<'s>, ElabError> {
    let pats: Vec<Pattern<'s>> = params
        .iter()
        .map(|p| patbot(scope.store, p))
        .collect::<Result<_, _>>()?;
    let mut names = Vec::new();
    for p in &pats {
        collect_pattern_names(scope.store, p, &mut names);
    }
    let mut inner = scope.clone();
    for n in &names {
        inner = inner.with(n);
    }
    let body = expr(value, &inner)?;
    let pat = if pats.len() == 1 {
        pats.into_iter().next().unwrap()
    } else {
        Pattern::Tuple(pats)
    };
    Ok(MatchArm {
        pat,
        guard: None,
        body,
    })
}

fn expr<'s>(e: &c::Expr, scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    match e {
        c::Expr::LetRecIn {
            first, ands, body, ..
        } => {
            let (bindings, rec_scope) = rec_bindings(first, ands, scope, &[])?;
            let body_ast = expr(body, &rec_scope)?;
            // `rec_bindings` yields text keys (it mangles module members'
            // into `$M.name`); intern them here, as `nest` does for the
            // top-level spine.
            Ok(Ast::LetRecIn(
                bindings
                    .into_iter()
                    .map(|(n, v)| (scope.sym(&n), v))
                    .collect(),
                Box::new(body_ast),
            ))
        }
        c::Expr::LetIn {
            name,
            params,
            value,
            body,
            ..
        } => {
            // `params` is now a full `param*` (`cst::ast::Expr::LetIn`'s doc
            // comment — widened for `hdecoset.satyh`/`vdecoset.satyh`'s `let
            // deco _ _ _ _ = [] in ..`, and further widened to `Param` for
            // `stdja.satyh`'s `let document record ?:configopt inner = ..`),
            // so this reuses the same single-clause pattern-currying path
            // `let-rec`/`Fun` already share, non-recursively (`scope`, not a
            // scope extended with `name` itself) — `params_to_patbots` first
            // widens any `?:name` marker to a plain `PatBot::Var`.
            let let_in_params = params_to_patbots(params);
            let value_ast = rec_clause_value(&let_in_params, value, &[], scope)?;
            // Record `name`'s leading-`?:`-optional-parameter count (see
            // `Scope`'s doc comment) so a later marker-less bare call in
            // `body` (`app_chain_generic`) auto-omits it, e.g. progsynt.satyh's
            // `let to-math ?:iopt e = .. in .. to-math e1 ..`.
            let mut body_scope = scope.clone();
            body_scope.insert_with_shape(&name.name, param_optional_shape(params));
            let body_ast = expr(body, &body_scope)?;
            Ok(Ast::LetIn(
                scope.sym(&name.name),
                Box::new(value_ast),
                Box::new(body_ast),
            ))
        }
        // `let pat = value in body` (`nxnonrecdec`'s general-pattern case —
        // see `cst::ast::Expr::LetPatternIn`'s doc comment for why this is a
        // separate variant from `LetIn` above). Lowered to the same
        // single-arm-`match` machinery a `match` expression's own arms use
        // (`pattern`/`collect_pattern_names`, below): `value` is elaborated
        // under the OUTER scope (a destructuring let's right-hand side never
        // sees its own bound names, same as `LetIn`), then matched against
        // `pat`, whose bound names are in scope for `body`.
        c::Expr::LetPatternIn {
            pat, value, body, ..
        } => {
            let value_ast = expr(value, scope)?;
            let lowered_pat = pattern(scope.store, pat)?;
            let mut names = Vec::new();
            collect_pattern_names(scope.store, &lowered_pat, &mut names);
            let mut inner = scope.clone();
            for n in &names {
                inner = inner.with(n);
            }
            let body_ast = expr(body, &inner)?;
            Ok(Ast::Match(
                Box::new(value_ast),
                vec![MatchArm {
                    pat: lowered_pat,
                    guard: None,
                    body: body_ast,
                }],
            ))
        }
        c::Expr::If {
            cond,
            then_branch,
            else_branch,
            ..
        } => Ok(Ast::IfThenElse(
            Box::new(expr(cond, scope)?),
            Box::new(expr(then_branch, scope)?),
            Box::new(expr(else_branch, scope)?),
        )),
        // `fun patbot+ -> body` (`nxlambda`'s `LAMBDA argpats ARROW nxlor`,
        // `argpats = list(patbot)` — see `cst::ast::Expr::Fun`'s doc
        // comment). Delegates to `rec_clause_value` (below), the SAME
        // arity-preserving pattern-currying `let-rec` already needs for its
        // own `patbot*` clause parameters (`fun`'s `extra` clause list is
        // simply empty — a lambda has no `|`-alternation): the common
        // all-plain-variable case still becomes a direct `Lambda` chain,
        // with no `Match`/fresh-variable indirection, and only a genuine
        // destructuring parameter (e.g. the bundled `list.satyg`'s
        // `mapi-adjacent`: `fun (i, acc) x leftopt rightopt -> ..`) pays for
        // the general path.
        c::Expr::Fun {
            kw, params, body, ..
        } => {
            if params.is_empty() {
                return err(kw.0, "'fun' needs at least one parameter");
            }
            rec_clause_value(params, body, &[], scope)
        }
        // `fun ?(l = x, …) p -> body` — SATySFi 0.1 labeled-optional lambda
        // unit (one bundle, one positional param).
        c::Expr::FunRows {
            kw,
            opts,
            param,
            body,
            ..
        } => fun_rows_to_ast(kw.0, opts, param, body, scope),
        c::Expr::Match {
            scrutinee,
            first,
            rest,
            ..
        } => {
            let scrut = expr(scrutinee, scope)?;
            let mut arms = Vec::with_capacity(1 + rest.len());
            arms.push(match_arm(first, scope)?);
            for bar in rest {
                arms.push(match_arm(&bar.arm, scope)?);
            }
            Ok(Ast::Match(Box::new(scrut), arms))
        }
        // `let-mutable name <- init in body` (`nxletsub`'s `LETMUTABLE` case).
        c::Expr::LetMutableIn {
            name, init, body, ..
        } => {
            let init_ast = expr(init, scope)?;
            let inner = scope.with(&name.name);
            let body_ast = expr(body, &inner)?;
            Ok(Ast::LetMutableIn(
                scope.sym(&name.name),
                Box::new(init_ast),
                Box::new(body_ast),
            ))
        }
        // `let-math \cmd param* = value in body` (`nxletsub`'s `LETMATH`
        // case, `parser.mly:688`) — upstream's only command binding with a
        // local `in`-bodied form (`LETHORZ`/`LETVERT` stay top-level-only,
        // see `cst.rs`'s `Expr::LetMathIn` doc comment). Structurally
        // identical to the top-level `TopBinding::LetMath` arm of
        // `walk_bindings`: elaborate the (curried) value under the OUTER
        // scope via the shared `elaborate_let_math` helper, then record
        // `cmd`'s leading-`?:`-optional-parameter count for `body`, same as
        // `Expr::LetIn` just above.
        c::Expr::LetMathIn {
            cmd,
            params,
            value,
            body,
            ..
        } => {
            let value_ast = elaborate_let_math(params, value, scope)?;
            let mut body_scope = scope.clone();
            body_scope.insert_with_shape(&cmd.name, param_optional_shape(params));
            let body_ast = expr(body, &body_scope)?;
            Ok(Ast::LetMathIn(
                scope.sym(&cmd.name),
                Box::new(value_ast),
                Box::new(body_ast),
            ))
        }
        // `open Name in body` (`nxletsub`'s `OPEN` case) — same alias-binding
        // technique as the top-level `TopBinding::Open` fold above (see
        // `walk_bindings`), just producing the `LetIn` chain directly since
        // there is no further sequence of sibling top bindings to thread a
        // scope through here.
        c::Expr::OpenIn { name, body, .. } => {
            open_module(&name.name, name.span, scope, |s| expr(body, s))
        }
        // `while cond do body` (`nxwhl`).
        c::Expr::WhileDo { cond, body, .. } => Ok(Ast::WhileDo(
            Box::new(expr(cond, scope)?),
            Box::new(expr(body, scope)?),
        )),
        // `name <- value` (`nxlambda`'s `OVERWRITEEQ` case). Existence is
        // checked against the bare `name.name` (unaffected by any active
        // `Scope::rename` redirect); the constructed node's own key goes
        // through `Scope::resolve`, exactly like `scoped_var` — a mutable
        // module member's sibling overwrite (`first-footnote <- Some m`)
        // must target the SAME mangled key its `LetMutableIn` is bound
        // under, or the typechecker's own `Ast::Overwrite` arm (which looks
        // the name up directly in `env`, independent of `Scope`) reports it
        // unbound — see `push_named_binding`'s doc comment.
        c::Expr::Overwrite { name, value, .. } => {
            if !scope.contains(&name.name) {
                return err(
                    name.span,
                    format!("unbound mutable variable '{}'", name.name),
                );
            }
            Ok(Ast::Overwrite(
                scope.resolve(&name.name),
                name.span,
                Box::new(expr(value, scope)?),
            ))
        }
        c::Expr::Ops(chain) => op_chain(chain, scope),
    }
}

// ---- operator-precedence fold --------------------------------------------

/// Precedence-climbing associativity.
#[derive(Clone, Copy)]
enum Assoc {
    Left,
    Right,
}

/// The v0.0.6 `nxlor`..`nxrtimes` precedence ladder, transcribed from
/// `parser.mly` lines 722-780 (loosest to tightest):
///
/// | level | tokens                                    | assoc |
/// |-------|-------------------------------------------|-------|
/// | 1     | `BinopBar` (`\|>`, ...)                    | left  |
/// | 2     | `BinopAmp`                                 | left  |
/// | 3     | `BinopEq`, `BinopGt`, `BinopLt`             | right |
/// | 4     | `BinopHat` (`^`), `Cons` (`::`)             | right |
/// | 5     | `BinopPlus`, `BinopMinus`, `ExactMinus`     | left  |
/// | 6     | `BinopTimes`, `ExactTimes`, `BinopDivides`, `Mod` | right |
///
/// Deviation: v0.0.6's plus/minus level is actually a left/right mix
/// (`nxlplus`/`nxlminus`/`nxrplus`/`nxrminus`, four mutually referencing
/// nonterminals) that differs from plain left-association only in how
/// chains nest — `nxlminus`'s right operand is `nxrtimes`, not `nxrminus`,
/// so `1 - 2 - 3`'s *tree shape* differs subtly from a naive left fold even
/// though both compute `(1 - 2) - 3`. Since `+`/`*` (this level's only
/// concrete instances here) are associative and no surface syntax or test
/// can observe tree shape, we use plain LEFT association, matching `-`
/// exactly and irrelevant for `+`.
///
/// Level 6 (`nxrtimes`) is genuinely right-recursive in the grammar itself
/// (`nxltimes`'s right operand is `nxrtimes`, recursing on itself) — `8 / 4
/// / 2` really does parse as `8 / (4 / 2)` in v0.0.6, not `(8 / 4) / 2`. We
/// keep this fidelity quirk.
///
/// **`&&`/`||` are NOT short-circuited here.** v0.0.6's `bytecomp/
/// vminstdef.yaml` registers them as ordinary strict primitives
/// (`LogicalAnd`/`LogicalOr`, `code: make_bool (binl && binr)`/`(binl ||
/// binr)`), applied like any binop through `parser.mly`'s `binary_operator`
/// (`nxland`/`nxlor`, lines 722-727) — by the time OCaml's `&&`/`||` runs,
/// both VM-stack operands are already popped (fully evaluated), so real
/// SATySFi doesn't short-circuit at the source level either. `primitives.rs`
/// registers `"&&"`/`"||"` as strict 2-arg primitives to match; no
/// `if`-desugaring here.
fn op_prec(tok: &Token) -> (u8, Assoc) {
    match tok {
        Token::BinopBar(_) => (1, Assoc::Left),
        Token::BinopAmp(_) => (2, Assoc::Left),
        Token::BinopEq(_) | Token::BinopGt(_) | Token::BinopLt(_) => (3, Assoc::Right),
        Token::BinopHat(_) | Token::Cons => (4, Assoc::Right),
        Token::BinopPlus(_) | Token::BinopMinus(_) | Token::ExactMinus => (5, Assoc::Left),
        Token::BinopTimes(_) | Token::ExactTimes | Token::BinopDivides(_) | Token::Mod => {
            (6, Assoc::Right)
        }
        _ => unreachable!("BinOpTok::parse only ever matches the operator tokens listed above"),
    }
}

/// `nxbfr`'s postfix `before` (see `OpChain::before`'s doc comment in
/// `cst.rs`): `e1 before e2` → `Ast::Sequential(e1, e2)`, where `e1` is the
/// whole precedence-folded operator chain.
fn op_chain<'s>(chain: &c::OpChain, scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    let head_ast = app_expr(&chain.head, scope)?;
    let folded = if chain.tail.is_empty() {
        head_ast
    } else {
        let mut atoms: VecDeque<Ast<'s>> = VecDeque::with_capacity(chain.tail.len() + 1);
        atoms.push_back(head_ast);
        let mut ops: VecDeque<(String, Span, Token)> = VecDeque::with_capacity(chain.tail.len());
        for rhs in &chain.tail {
            let text = rhs.op.op_text();
            // `|>` is handled entirely by `climb`'s
            // special case below — it is
            // deliberately NOT a `scope`-bound name (no runtime primitive, no
            // `prim_types` entry: `a |> f` lowers straight to `Apply(f, a)`,
            // ordinary application the inferencer/evaluator already handle),
            // so it must skip the "unbound operator" gate every other
            // operator token goes through.
            if text != "|>" && !scope.contains(&text) {
                return err(rhs.op.span, format!("unbound operator '{text}'"));
            }
            // `scope.resolve` redirects a module member's own bare
            // operator (`val (+++) a b = ..` inside `module M = struct ..
            // end`) to its mangled key, exactly like `scoped_var` — `"|>"`
            // is never a `Scope::rename` target (it's deliberately never
            // scope-bound at all, see this arm's own comment above), so
            // resolving it is a no-op.
            ops.push_back((
                scope.resolve_text(&text).to_string(),
                rhs.op.span,
                rhs.op.tok.clone(),
            ));
            atoms.push_back(app_expr(&rhs.rhs, scope)?);
        }
        climb(&mut atoms, &mut ops, 0, scope)
    };
    match &chain.before {
        Some(bt) => Ok(Ast::Sequential(
            Box::new(folded),
            Box::new(expr(&bt.body, scope)?),
        )),
        None => Ok(folded),
    }
}

/// Standard precedence-climbing fold over an already-elaborated flat
/// `atom (op atom)*` sequence (`atoms.len() == ops.len() + 1`). Every binop
/// elaborates uniformly to `Apply(Apply(Var(op_text), lhs), rhs)` — SATySFi
/// binops (including `::`, see the `primitives.rs` note) are just env-bound
/// primitives, no special-cased AST node needed — **except `|>`**, which is
/// reverse application (`a |> f` ≡ `f a`, upstream `primitives.cppo.ml:552`)
/// special-cased directly to `Apply(rhs, lhs)` rather than
/// `Apply(Apply(Var("|>"), lhs), rhs)`: no primitive named `"|>"` is ever
/// registered (see `op_chain`'s matching skip of the scope-contains gate),
/// since applying a user-supplied closure isn't something any current
/// primitive body does. `|>` sits at level 1 (loosest, left-associative,
/// see `op_prec`), so `a |> f |> g` folds as `(a |> f) |> g` = `g (f a)`,
/// matching the bundled `list.satyg`'s pipe-heavy style (`reverse`,
/// `map-adjacent`, `map-with-ends`).
fn climb<'s>(
    atoms: &mut VecDeque<Ast<'s>>,
    ops: &mut VecDeque<(String, Span, Token)>,
    min_prec: u8,
    scope: &Scope<'s>,
) -> Ast<'s> {
    let mut lhs = atoms
        .pop_front()
        .expect("one more atom than consumed operators");
    while let Some((_, _, tok)) = ops.front() {
        let (prec, assoc) = op_prec(tok);
        if prec < min_prec {
            break;
        }
        let (text, span, _) = ops.pop_front().unwrap();
        let next_min = match assoc {
            Assoc::Left => prec + 1,
            Assoc::Right => prec,
        };
        let rhs = climb(atoms, ops, next_min, scope);
        lhs = if text == "|>" {
            Ast::Apply(Box::new(rhs), Box::new(lhs))
        } else {
            Ast::Apply(
                Box::new(Ast::Apply(
                    Box::new(Ast::Var(scope.sym(&text), span)),
                    Box::new(lhs),
                )),
                Box::new(rhs),
            )
        };
    }
    lhs
}

// ---- application chains --------------------------------------------------

fn app_expr<'s>(a: &c::AppExpr, scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    // `not` binds looser than application (upstream `nxbot: NOT nxbot` in
    // parser.mly): `not f x` means `not (f x)`, NOT `(not f) x`. This port's
    // lexer deliberately leaves `not` an ordinary identifier (so it can still
    // be passed first-class in ARGUMENT position — e.g. `List.map not xs`),
    // so we recognise the logical-negation form only in HEAD position with at
    // least one argument: re-fold the arguments into a single inner
    // application and apply the `not` primitive to it. A bare `not` (no args)
    // or a `not` sitting in argument position resolves to the `not`
    // primitive as an ordinary value.
    if a.minus.is_none() && a.excl.is_none() && a.stage.is_none() && a.head_accesses.is_empty() && !a.args.is_empty() {
        if let c::Atomic::Var(v) = &a.head {
            if v.name == "not" && scope.contains("not") && scope.resolve_text("not") == "not" {
                let not_fn = scoped_var("not", v.span, scope)?;
                let mut inner = app_arg_to_ast(&a.args[0], scope)?;
                for rest in &a.args[1..] {
                    inner = apply_one_arg(inner, rest, scope)?;
                }
                return Ok(Ast::Apply(Box::new(not_fn), Box::new(inner)));
            }
        }
    }
    let ast = if a.excl.is_none() && a.stage.is_none() && a.head_accesses.is_empty() {
        if let c::Atomic::Ctor(ctor) = &a.head {
            // A constructor head: the first argument (if any) is its payload
            // (`Some 1`); any further arguments Apply-fold on top of the
            // resulting `Ctor` value, which the evaluator will reject at run
            // time (constructors are not functions).
            let mut args_iter = a.args.iter();
            match args_iter.next() {
                Some(first) => {
                    let payload = app_arg_to_ast(first, scope)?;
                    let mut ast = Ast::Ctor(ctor.name.clone(), Some(Box::new(payload)));
                    for rest in args_iter {
                        ast = apply_one_arg(ast, rest, scope)?;
                    }
                    ast
                }
                None => Ast::Ctor(ctor.name.clone(), None),
            }
        } else {
            app_chain_generic(a, scope)?
        }
    } else {
        // `!Ctor` / `Ctor#field` don't correspond to any valid v0.0.6
        // program (`CONSTRUCTOR` isn't part of `nxbot`, so it can never sit
        // under a `#label`/`UNOP_EXCLAM` prefix there) — fall back to the
        // generic path, which treats the bare constructor as an ordinary
        // (payload-less) atomic value.
        app_chain_generic(a, scope)?
    };
    match &a.minus {
        // Unary minus desugars exactly as v0.0.6's `nxun` does (parser.mly
        // ~line 774): `0 - <the whole application>`.
        Some(m) => {
            let minus = scoped_var("-", m.0, scope)?;
            Ok(Ast::Apply(
                Box::new(Ast::Apply(Box::new(minus), Box::new(Ast::Int(0)))),
                Box::new(ast),
            ))
        }
        None => Ok(ast),
    }
}

fn app_chain_generic<'s>(a: &c::AppExpr, scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    let mut ast =
        atomic_head_with_excl(&a.head, &a.head_accesses, a.excl.as_ref(), a.stage.as_ref(), scope)?;
    // Marker-less optional-argument defaulting (`Scope`'s doc comment /
    // Sub-area 2): if the head is a bare name (no `!`/`#access`) known to
    // have `?:`-optional parameters ANYWHERE in its declared `Param` list
    // (not just leading — see `Scope::optional_shape`'s doc comment), walk
    // `a.args` position by position against that shape:
    //
    //  - at a declared OPTIONAL position, an explicit `?:e`/`?*` marker is
    //    consumed as written; anything else (a bare arg, a `?(l=e)` bundle,
    //    or no argument left) is NOT consumed — a plain `None` is
    //    synthesized instead, and the same argument is re-examined against
    //    the NEXT position. Without this, a positional argument after an
    //    omitted optional mis-binds against the omitted slot: `document
    //    record body` (no marker) must become `Apply(Apply(Apply(document,
    //    record), None), body)`, not unify `body` against `configopt`'s
    //    domain directly.
    //  - at a declared MANDATORY position, the next argument is consumed
    //    positionally, like plain application.
    //  - once every position is visited (or the shape is unknown/empty —
    //    the common case), remaining arguments apply one at a time
    //    (`apply_one_arg`), so a call with MORE arguments than the head's
    //    arity (currying further) is unaffected.
    //
    // Guarded on non-empty `a.args` so a bare function-VALUE reference (no
    // application, e.g. `to-math` passed to `List.map`) is left untouched.
    let shape: &[bool] = if a.excl.is_none() && a.head_accesses.is_empty() && !a.args.is_empty() {
        head_optional_shape(&a.head, scope)
    } else {
        &[]
    };
    let mut args_iter = a.args.iter().peekable();
    let mut pos = 0usize;
    while pos < shape.len() {
        if shape[pos] {
            match args_iter.peek() {
                Some(c::AppArg::Optional { .. }) | Some(c::AppArg::Omission(_)) => {
                    let arg = args_iter.next().unwrap();
                    ast = Ast::Apply(Box::new(ast), Box::new(app_arg_to_ast(arg, scope)?));
                }
                Some(_) => {
                    ast = Ast::Apply(Box::new(ast), Box::new(Ast::Ctor("None".to_string(), None)));
                }
                None => break,
            }
        } else {
            match args_iter.next() {
                Some(arg) => ast = apply_one_arg(ast, arg, scope)?,
                None => break,
            }
        }
        pos += 1;
    }
    for arg in args_iter {
        ast = apply_one_arg(ast, arg, scope)?;
    }
    Ok(ast)
}

/// Apply one application-chain argument to the running `func` AST. A SATySFi
/// 0.1 `?(l = e, …)`-bundled argument becomes an [`Ast::ApplyOpt`] (carrying
/// the labeled optionals plus the paired positional argument); every other
/// argument is an ordinary [`Ast::Apply`].
fn apply_one_arg<'s>(
    func: Ast<'s>,
    arg: &c::AppArg,
    scope: &Scope<'s>,
) -> Result<Ast<'s>, ElabError> {
    match arg {
        c::AppArg::Bundled {
            opts,
            excl,
            atom,
            accesses,
        } => {
            let opt_args = elaborate_opt_args(opts, scope)?;
            let arg_ast = atomic_head_with_excl(atom, accesses, excl.as_ref(), None, scope)?;
            Ok(Ast::ApplyOpt {
                func: Box::new(func),
                opts: opt_args,
                arg: Box::new(arg_ast),
            })
        }
        c::AppArg::BundledCtor { opts, ctor } => {
            let opt_args = elaborate_opt_args(opts, scope)?;
            Ok(Ast::ApplyOpt {
                func: Box::new(func),
                opts: opt_args,
                arg: Box::new(Ast::Ctor(ctor.name.clone(), None)),
            })
        }
        _ => Ok(Ast::Apply(
            Box::new(func),
            Box::new(app_arg_to_ast(arg, scope)?),
        )),
    }
}

/// Elaborate a `?(l = e, …)` optional-argument bundle: version-gate it (a
/// 0.0.6-parsed occurrence is rejected here), reject a duplicate label within
/// the one bundle, and elaborate each label's value expression.
fn elaborate_opt_args<'s>(
    opts: &c::CstOptArgs,
    scope: &Scope<'s>,
) -> Result<Vec<(String, Ast<'s>)>, ElabError> {
    if !scope.version.has_row_polymorphism() {
        return err(
            opts.q.0,
            "labeled optional arguments (`?(l = e)`) are SATySFi 0.1 syntax — \
             this file is compiled as 0.0.6",
        );
    }
    let mut out: Vec<(String, Ast<'s>)> = Vec::with_capacity(opts.entries.len());
    let mut seen = HashSet::new();
    for e in &opts.entries {
        if !seen.insert(e.label.name.clone()) {
            return err(
                e.label.span,
                format!(
                    "duplicate optional label `{}` in one `?(…)` bundle",
                    e.label.name
                ),
            );
        }
        out.push((e.label.name.clone(), expr(&e.value.0, scope)?));
    }
    Ok(out)
}

/// `a.head`'s recorded full per-position optional-parameter shape (`Scope::
/// optional_shape`), for a bare unqualified or module-qualified variable
/// head only — any other head shape (a parenthesized expression, a
/// dereferenced/accessed value, …) can never name a known `let`/`let ..
/// in` binding directly, so it conservatively reports `&[]` (unknown).
fn head_optional_shape<'s, 'a>(head: &c::Atomic, scope: &'a Scope<'s>) -> &'a [bool] {
    match head {
        c::Atomic::Var(v) => scope.optional_shape(&v.name),
        c::Atomic::VarWithMod(v) => scope.optional_shape(&qualify_key(&v.mods, &v.name)),
        _ => &[],
    }
}

/// `!x` / `!x#a#b` (`nxunsub`'s `UNOP_EXCLAM nxbot` — parser.mly:795,
/// `let (rng, varnm) = unop in .. UTApply((rng, UTContentOf([], varnm)),
/// utast2)`): the deref operator binds to the atomic head *plus its own
/// `#access` chain* — `nxbot` itself folds `ACCESS` left-recursively
/// (parser.mly:801, `nxbot ACCESS var`), so `nxunsub`'s `utast2` is already
/// the fully-accessed atomic — but never to a *following application
/// argument*: `nxapp`'s only production combining an application head with
/// more arguments is `nxapp nxunsub` (parser.mly:781), so `!x y` parses as
/// `nxapp(nxunsub(!x), y)` = `(!x) y`, not `!(x y)`. This CST's `AppExpr`
/// mirrors that split directly: `excl`+`head_accesses` sit on the *head*
/// only, `args` is the separate, already-folded-in-elaboration application
/// tail — so this helper (used for both an `AppExpr`'s own head and a
/// command-argument-chain's head, see `cmd_arg_chain`) elaborates to
/// `Apply(Var(excl_text), <head+accesses>)` exactly matching v0.0.6's
/// `UTApply` shape above (`varnm` there is always unqualified — this CST has
/// no qualified-`!` form either, so no module-mangling applies to it).
fn atomic_head_with_excl<'s>(
    head: &c::Atomic,
    accesses: &[c::AccessSeg],
    excl: Option<&UnopExclamTok>,
    stage: Option<&c::StagePrefix>,
    scope: &Scope<'s>,
) -> Result<Ast<'s>, ElabError> {
    let mut ast = atomic(head, scope)?;
    for acc in accesses {
        ast = Ast::AccessField(Box::new(ast), acc.label.name.clone(), acc.label.span);
    }
    if let Some(e) = excl {
        let deref_fn = scoped_var(&e.text, e.span, scope)?;
        ast = Ast::Apply(Box::new(deref_fn), Box::new(ast));
    }
    Ok(match stage {
        Some(c::StagePrefix::Next(_)) => Ast::Next(Box::new(ast)),
        Some(c::StagePrefix::Prev(_)) => Ast::Prev(Box::new(ast)),
        None => ast,
    })
}

/// Desugar one application-chain argument. `?: value`/`?*` (`AppArg::Optional`/
/// `Omission` — v0.0.6's `UTApplyOptional`/`UTApplyOmission`) desugar
/// *untyped*, straight to the same `option` constructors a program could
/// spell by hand: a supplied `?:(e)` becomes `Some(e)`, an omitted `?*`
/// becomes `None`. This is the one runtime model shared by every
/// optional-arg call site this port supports — a plain function's `f
/// ?:(e)`/`f ?*` *and* a command's leading `narg`s (`cst.rs`'s
/// `CmdTail::Args`, whose elements are ALSO `AppArg`s) both go through this
/// same function — so `Some`/`None` is what a `?->`-typed function's
/// `option`-wrapped domain (`typecheck.rs`'s `lower_type_expr`) must unify
/// against. No type-directed insertion is needed: every optional slot this
/// grammar can produce carries an explicit `?:`/`?*` marker at the call
/// site, so elaboration alone fully resolves it.
fn app_arg_to_ast<'s>(arg: &c::AppArg, scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    match arg {
        c::AppArg::Optional { value, .. } => {
            let inner = atomic(value, scope)?;
            Ok(Ast::Ctor("Some".to_string(), Some(Box::new(inner))))
        }
        c::AppArg::Omission(_) => Ok(Ast::Ctor("None".to_string(), None)),
        c::AppArg::Atom {
            stage,
            excl,
            atom,
            accesses,
        } => atomic_head_with_excl(atom, accesses, excl.as_ref(), stage.as_ref(), scope),
        c::AppArg::Ctor(ctor) => Ok(Ast::Ctor(ctor.name.clone(), None)),
        // A `?(l = e, …)` bundle is not a plain argument value — the chain
        // builder (`apply_one_arg`) routes it to `Ast::ApplyOpt` before it
        // ever reaches here. Reaching this arm means a bundle sat where only
        // a value can go (e.g. as a constructor payload).
        c::AppArg::Bundled { opts, .. } | c::AppArg::BundledCtor { opts, .. } => err(
            opts.q.0,
            "a `?(l = e)` labeled-optional bundle cannot be used as a plain \
             argument value here",
        ),
    }
}

/// Shared machinery for `open Name in body` (`Expr::OpenIn`) and `Name.(body)`
/// (`Atomic::OpenModule`, `nxbot`'s `OPENMODULE nxlet RPAREN` production —
/// `Mod.(e)` ≡ `open Mod in e`): bring every `"Name."`-prefixed name
/// currently in scope into unqualified scope, elaborate `body` under that
/// extended scope (via the supplied closure — generic because `Expr::OpenIn`'s
/// body is a plain `Expr` but `Atomic::OpenModule`'s is a `ParenBody`, so
/// `Mod.(e, e, …)` can produce a tuple exactly like `Atomic::Paren`), then
/// wrap the result in one `LetIn` alias per matched name (`x = Name.x`) —
/// there is no separate "module scope" at the `Ast` level, so the aliasing
/// must be visible there too.
fn open_module<'s>(
    module_name: &str,
    name_span: Span,
    scope: &Scope<'s>,
    body: impl FnOnce(&Scope<'s>) -> Result<Ast<'s>, ElabError>,
) -> Result<Ast<'s>, ElabError> {
    let prefix = format!("{module_name}.");
    let matches = scope.names_with_prefix(&prefix);
    let mut inner = scope.clone();
    for q in &matches {
        let shape = scope.optional_shape(q).to_vec();
        inner.insert_with_shape(&q[prefix.len()..], shape);
    }
    let body_ast = body(&inner)?;
    let mut ast = body_ast;
    for q in matches.into_iter().rev() {
        let suffix = q[prefix.len()..].to_string();
        // `q` may itself be a `Scope::rename` alias rather than a real binding
        // key: for a NESTED module opened from a sibling (`Score.(…)` inside
        // `module FssFontSelection`, where `Score`'s members are bound under
        // the fully-qualified `FssFontSelection.Score.<`), the prefix-matched
        // name `Score.<` is only a relative alias registered by
        // `walk_bindings`. Resolve it to the actual Ast key so the emitted
        // `Var` refers to a binding that exists. For a top-level module the
        // rename is identity, so this is a no-op there.
        let key = scope.resolve(&q);
        ast = Ast::LetIn(
            scope.sym(&suffix),
            Box::new(Ast::Var(key, name_span)),
            Box::new(ast),
        );
    }
    Ok(ast)
}

fn atomic<'s>(a: &c::Atomic, scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    match a {
        c::Atomic::Length(l) => match Length::from_unit(l.value, &l.unit) {
            Some(len) => Ok(Ast::Length(len)),
            None => err(l.span, format!("unknown length unit '{}'", l.unit)),
        },
        c::Atomic::Float(f) => Ok(Ast::Float(f.value)),
        c::Atomic::Int(i) => Ok(Ast::Int(i.value)),
        c::Atomic::Literal(l) => Ok(Ast::Str(omit_spaces(l.omit_pre, l.omit_post, &l.body))),
        c::Atomic::True(_) => Ok(Ast::Bool(true)),
        c::Atomic::False(_) => Ok(Ast::Bool(false)),
        // A bare nullary constructor reached as a plain atomic argument
        // (the ctor-with-payload case is handled at the `AppExpr` head
        // level in `app_expr`, above; it never reaches here).
        c::Atomic::Ctor(ctor) => Ok(Ast::Ctor(ctor.name.clone(), None)),
        c::Atomic::Var(v) => scoped_var(&v.name, v.span, scope),
        c::Atomic::VarWithMod(tok) => {
            scoped_var(&qualify_key(&tok.mods, &tok.name), tok.span, scope)
        }
        // `(+++)`/`(-->)` — a bare reference to a (possibly user-defined)
        // operator as a first-class value; resolves exactly like `Var`
        // above, under the same name `x +++ y`/`x --> y` (an `OpChain`'s
        // `op_chain`, below) would look up.
        c::Atomic::OpRef(op) => scoped_var(&op.name, op.span, scope),
        // `(command \cmd)` — a first-class reference to an inline command's
        // own binding. No new binding machinery: the command's own
        // `let-inline` binding is the
        // referent, so this is just its `Var` under the same sigil'd key
        // `InlineElem::Cmd` resolves — reusing `scoped_var` also gives the
        // usual "unbound command" diagnostic for free.
        c::Atomic::Command { name, .. } => {
            let (key, span) = horz_cmd_key(name);
            scoped_var(&key, span, scope)
        }
        c::Atomic::Unit { .. } => Ok(Ast::Unit),
        c::Atomic::Paren { inner, .. } => paren_body(inner, scope),
        c::Atomic::OpenModule { grp, body } => {
            open_module(&grp.open.name, grp.open.span, scope, |s| {
                paren_body(body, s)
            })
        }
        c::Atomic::Record { body, .. } => record_body_to_ast(body, scope),
        c::Atomic::List { items, .. } => {
            let mut out = Vec::with_capacity(items.len());
            for it in items {
                out.push(expr(&it.value, scope)?);
            }
            Ok(Ast::List(out))
        }
        c::Atomic::InlineText { elems, .. } => inline_text_ast(elems, scope),
        c::Atomic::BlockText { elems, .. } => {
            Ok(Ast::BlockText(Rc::new(block_elems(elems, scope)?)))
        }
        c::Atomic::MathText { elems, .. } => math_block_ast(elems, scope),
    }
}

/// `( expr )` → itself; `( expr, expr, … )` → `Ast::Tuple`.
fn paren_body<'s>(pb: &c::ParenBody, scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    let first = expr(&pb.first, scope)?;
    if pb.rest.is_empty() {
        Ok(first)
    } else {
        let mut items = Vec::with_capacity(pb.rest.len() + 1);
        items.push(first);
        for r in &pb.rest {
            items.push(expr(&r.value, scope)?);
        }
        Ok(Ast::Tuple(items))
    }
}

/// `(| l = e; … |)` → `Ast::Record`; `(| base with l = e; … |)` → a left
/// fold of `Ast::UpdateField` over `base` (`nxrecordsynt`, parser.mly:
/// 833-840 — `rcd |> List.fold_left (fun utast1 (fldnm, utastF) ->
/// UTUpdateField(utast1, fldnm, utastF)) utast`, i.e. exactly one
/// `UpdateField` per field, left-to-right, threading the accumulator).
fn record_body_to_ast<'s>(body: &c::RecordBody, scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    match body {
        c::RecordBody::Fields(fields) => {
            let mut out = Vec::with_capacity(fields.len());
            for f in fields {
                out.push((f.name.name.clone(), expr(&f.value, scope)?));
            }
            Ok(Ast::Record(out))
        }
        c::RecordBody::Update { base, fields, .. } => {
            let mut ast = expr(base, scope)?;
            for f in fields {
                let v = expr(&f.value, scope)?;
                ast = Ast::UpdateField(Box::new(ast), f.name.name.clone(), Box::new(v));
            }
            Ok(ast)
        }
    }
}

// ---- patterns -------------------------------------------------------------

/// `patas`: a `PatCons`, plus an optional `as name` binding.
fn pattern<'s>(store: &'s SymbolStore, p: &c::Pattern) -> Result<Pattern<'s>, ElabError> {
    let head = pat_cons(store, &p.head)?;
    match &p.as_clause {
        Some(ac) => Ok(Pattern::As(Box::new(head), store.intern(&ac.name.name))),
        None => Ok(head),
    }
}

/// `pattr`: `patbot (:: patbot)*`, folded RIGHT (`::` is right-associative):
/// `a :: b :: c` → `Cons(a, Cons(b, c))`.
fn pat_cons<'s>(store: &'s SymbolStore, pc: &c::PatCons) -> Result<Pattern<'s>, ElabError> {
    let mut segs: Vec<&c::PatBot> = Vec::with_capacity(pc.tail.len() + 1);
    segs.push(&pc.head);
    for seg in &pc.tail {
        segs.push(&seg.tail);
    }
    let mut iter = segs.into_iter().rev();
    let last = iter.next().expect("PatCons always has a head");
    let mut acc = patbot(store, last)?;
    for pb in iter {
        acc = Pattern::Cons(Box::new(patbot(store, pb)?), Box::new(acc));
    }
    Ok(acc)
}

fn patbot<'s>(store: &'s SymbolStore, pb: &c::PatBot) -> Result<Pattern<'s>, ElabError> {
    match pb {
        c::PatBot::CtorApplied { ctor, arg } => Ok(Pattern::Ctor(
            ctor.name.clone(),
            Some(Box::new(patbot(store, arg)?)),
        )),
        c::PatBot::Ctor(ctor) => Ok(Pattern::Ctor(ctor.name.clone(), None)),
        c::PatBot::Int(i) => Ok(Pattern::Int(i.value)),
        c::PatBot::True(_) => Ok(Pattern::Bool(true)),
        c::PatBot::False(_) => Ok(Pattern::Bool(false)),
        c::PatBot::Str(l) => Ok(Pattern::Str(l.body.clone())),
        c::PatBot::Wild(_) => Ok(Pattern::Wild),
        c::PatBot::Var(v) => Ok(Pattern::Var(store.intern(&v.name))),
        c::PatBot::Unit { .. } => Ok(Pattern::Unit),
        c::PatBot::Paren { inner, .. } => {
            let first = pattern(store, &inner.first)?;
            if inner.rest.is_empty() {
                Ok(first)
            } else {
                let mut items = Vec::with_capacity(inner.rest.len() + 1);
                items.push(first);
                for r in &inner.rest {
                    items.push(pattern(store, &r.value)?);
                }
                Ok(Pattern::Tuple(items))
            }
        }
        c::PatBot::List { items, .. } => {
            let mut acc = Pattern::EmptyList;
            for it in items.iter().rev() {
                acc = Pattern::Cons(Box::new(pattern(store, &it.value)?), Box::new(acc));
            }
            Ok(acc)
        }
    }
}

/// Collect every name a (lowered) pattern binds — `Var` occurrences plus any
/// `as name` clauses — so the elaborator can extend the scope for a match
/// arm's guard and body.
fn collect_pattern_names<'s>(store: &'s SymbolStore, p: &Pattern<'s>, out: &mut Vec<&'s str>) {
    match p {
        Pattern::Var(n) => out.push(store.resolve(*n)),
        Pattern::As(inner, n) => {
            collect_pattern_names(store, inner, out);
            out.push(store.resolve(*n));
        }
        Pattern::Tuple(ps) => {
            for p in ps {
                collect_pattern_names(store, p, out);
            }
        }
        Pattern::Cons(head, tail) => {
            collect_pattern_names(store, head, out);
            collect_pattern_names(store, tail, out);
        }
        Pattern::Ctor(_, Some(inner)) => collect_pattern_names(store, inner, out),
        Pattern::Wild
        | Pattern::Unit
        | Pattern::Bool(_)
        | Pattern::Int(_)
        | Pattern::Str(_)
        | Pattern::EmptyList
        | Pattern::Ctor(_, None) => {}
    }
}

fn match_arm<'s>(arm: &c::MatchArm, scope: &Scope<'s>) -> Result<MatchArm<'s>, ElabError> {
    let pat = pattern(scope.store, &arm.pat)?;
    let mut names = Vec::new();
    collect_pattern_names(scope.store, &pat, &mut names);
    let mut inner = scope.clone();
    for n in &names {
        inner = inner.with(n);
    }
    let guard = match &arm.guard {
        Some(g) => Some(expr(&g.cond, &inner)?),
        None => None,
    };
    let body = expr(&arm.body, &inner)?;
    Ok(MatchArm { pat, guard, body })
}

// ---- inline/block text ----------------------------------------------------

/// `AnyHorzCmdTok`/`AnyVertCmdTok`'s scope key + span: a plain command uses
/// its own sigil-inclusive name unchanged; a module-qualified one mangles
/// via [`qualify_key`] (see its doc comment on the module name-mangling
/// scheme).
fn horz_cmd_key(name: &AnyHorzCmdTok) -> (String, Span) {
    match name {
        AnyHorzCmdTok::Plain(t) => (t.name.clone(), t.span),
        AnyHorzCmdTok::Mod(t) => (qualify_key(&t.mods, &t.name), t.span),
    }
}

fn vert_cmd_key(name: &AnyVertCmdTok) -> (String, Span) {
    match name {
        AnyVertCmdTok::Plain(t) => (t.name.clone(), t.span),
        AnyVertCmdTok::Mod(t) => (qualify_key(&t.mods, &t.name), t.span),
    }
}

/// [`AnyMathCmdTok`]'s scope key + span — the math-mode analogue of
/// [`horz_cmd_key`]/[`vert_cmd_key`].
fn math_cmd_key(name: &AnyMathCmdTok) -> (String, Span) {
    match name {
        AnyMathCmdTok::Plain(t) => (t.name.clone(), t.span),
        AnyMathCmdTok::Mod(t) => (qualify_key(&t.mods, &t.name), t.span),
    }
}

/// An inline-text group's content (`{ .. }`): itemize-aware entry point.
/// `sxsep`'s two alternatives (parser.mly:1039-1042) are a `nonempty_list`
/// of `*`-headed items (→ `UTItemize`, see [`itemize`]) or plain content;
/// since `InlineElem`'s `ItemBullet` markers are kept flat rather than
/// grouped in-grammar (see `cst.rs`'s doc comment on `InlineElem`), the
/// dispatch happens here instead of in the parser.
fn inline_text_ast<'s>(elems: &[c::InlineElem], scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    // `{| a | b | … |}` horizontal-LIST literal (`sxlist` in parser.mly): a
    // leading `|` (`Sep`) immediately after `{` marks the inline-text-list
    // form — a value of type `inline-text list` — distinct from a plain
    // `{ … }` inline text. The elements arrive flat and `Sep`-delimited (see
    // `InlineElem`'s doc comment); regroup them into one inline-text per cell.
    if matches!(elems.first(), Some(c::InlineElem::Sep(_))) {
        return inline_text_list(elems, scope);
    }
    if elems
        .iter()
        .any(|e| matches!(e, c::InlineElem::ItemBullet(_)))
    {
        itemize(elems, scope)
    } else {
        Ok(Ast::InlineText(Rc::new(inline_elems(elems, scope)?)))
    }
}

/// Regroup a `{| a | b | … |}` inline-text-list literal's flat, `Sep`-delimited
/// elements (see [`inline_text_ast`]) into an [`Ast::List`] of one inline-text
/// per cell. The leading/trailing empty groups produced by the framing `{|`
/// and `|}` are structural and dropped; an interior empty group is a real
/// empty cell (`{| a | | b |}`). Each cell is elaborated recursively, so a
/// cell may itself be an itemize (`{* … }`).
fn inline_text_list<'s>(elems: &[c::InlineElem], scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    let mut groups: Vec<&[c::InlineElem]> = Vec::new();
    let mut start = 0usize;
    for (i, e) in elems.iter().enumerate() {
        if matches!(e, c::InlineElem::Sep(_)) {
            groups.push(&elems[start..i]);
            start = i + 1;
        }
    }
    groups.push(&elems[start..]);
    if groups.first().is_some_and(|g| g.is_empty()) {
        groups.remove(0);
    }
    if groups.last().is_some_and(|g| g.is_empty()) {
        groups.pop();
    }
    let mut items = Vec::with_capacity(groups.len());
    for g in groups {
        items.push(inline_text_ast(g, scope)?);
    }
    Ok(Ast::List(items))
}

/// Coalesce chars/spaces/breaks into text runs; commands become
/// `IText::Cmd`; `#var;` embeds become `IText::Embed`; `${..}` embeds become
/// `IText::EmbedMath`. Never sees an `ItemBullet` in a well-formed call (the
/// itemize splitter in [`itemize`] always calls this on a bullet-free
/// slice) — one showing up here is reported as an error rather than
/// panicking, since a defensive diagnostic is friendlier than a panic even
/// though the shape should be unreachable.
fn inline_elems<'s>(
    elems: &[c::InlineElem],
    scope: &Scope<'s>,
) -> Result<Vec<IText<'s>>, ElabError> {
    let mut out = Vec::new();
    let mut text = String::new();
    for el in elems {
        match el {
            c::InlineElem::Char(ch) => text.push_str(&ch.text),
            c::InlineElem::CodeText(t) => {
                if !text.is_empty() {
                    out.push(IText::Text(std::mem::take(&mut text)));
                }
                out.push(IText::CodeText(t.text.clone()));
            }
            c::InlineElem::Space(_) => text.push(' '),
            c::InlineElem::Break(_) => text.push('\n'),
            c::InlineElem::Cmd { name, tail } => {
                if !text.is_empty() {
                    out.push(IText::Text(std::mem::take(&mut text)));
                }
                let (key, span) = horz_cmd_key(name);
                if !scope.contains(&key) {
                    return err(span, format!("unbound inline command '{key}'"));
                }
                out.push(IText::Cmd {
                    name: scope.resolve(&key),
                    span,
                    args: cmd_args(tail, scope, scope.optional_shape(&key))?,
                });
            }
            c::InlineElem::Embed { var, .. } => {
                if !text.is_empty() {
                    out.push(IText::Text(std::mem::take(&mut text)));
                }
                let key = qualify_key(&var.mods, &var.name);
                if !scope.contains(&key) {
                    return err(var.span, format!("unbound variable '{key}'"));
                }
                out.push(IText::Embed {
                    expr: Ast::Var(scope.resolve(&key), var.span),
                    span: var.span,
                });
            }
            c::InlineElem::EmbedMath { mgrp, elems } => {
                if !text.is_empty() {
                    out.push(IText::Text(std::mem::take(&mut text)));
                }
                if let Some(first) = elems.first() {
                    if let c::MathBot::Sep(tok) = &first.base {
                        return err(tok.0, "a '|'-separated math list cannot be embedded directly in inline text: `${| … |}` here would be a `math list`, but an embedded formula must be a single `math`");
                    }
                }
                let span = mgrp.open.0.unite(mgrp.close.0);
                out.push(IText::EmbedMath {
                    elems: Rc::new(lower_math_elems(elems, scope)?),
                    span,
                });
            }
            c::InlineElem::ItemBullet(tok) => {
                return err(
                    tok.span,
                    "unexpected itemize bullet '*' outside a bullet list",
                );
            }
            c::InlineElem::Sep(tok) => {
                return err(tok.0, "'|' separator is not supported here yet");
            }
        }
    }
    if !text.is_empty() {
        out.push(IText::Text(text));
    }
    Ok(out)
}

fn block_elems<'s>(elems: &[c::BlockElem], scope: &Scope<'s>) -> Result<Vec<BText<'s>>, ElabError> {
    let mut out = Vec::with_capacity(elems.len());
    for el in elems {
        match el {
            c::BlockElem::Cmd { name, tail } => {
                let (key, span) = vert_cmd_key(name);
                if !scope.contains(&key) {
                    return err(span, format!("unbound block command '{key}'"));
                }
                out.push(BText::Cmd {
                    name: scope.resolve(&key),
                    span,
                    args: cmd_args(tail, scope, scope.optional_shape(&key))?,
                });
            }
            c::BlockElem::Embed { var, .. } => {
                let key = qualify_key(&var.mods, &var.name);
                if !scope.contains(&key) {
                    return err(var.span, format!("unbound variable '{key}'"));
                }
                out.push(BText::Embed {
                    expr: Ast::Var(scope.resolve(&key), var.span),
                    span: var.span,
                });
            }
        }
    }
    Ok(out)
}

/// Flatten a command tail back into its argument list. `CmdTail::Args` is a
/// flat, non-empty `AppArg` sequence (`cst.rs`'s own dedicated grammar, not
/// a reuse of the general application chain), so this is just
/// `cmd_arg_to_ast` per element; a supplied/omitted optional (`?:`/`?*`)
/// desugars to `Some`/`None` exactly like a plain function's optional
/// application (`app_arg_to_ast`'s doc comment). A `?(l = e, …)`-bundled
/// element carries its labels on the
/// returned [`CmdArg`]'s `opts` instead of desugaring to `Some`/`None` — the
/// 0.0.6 leading-padding loop below only ever matches `Optional`/`Omission`,
/// never `Bundled`/`BundledCtor`, and a V0_1 command's `leading` is always
/// `0`, so the two mechanisms never interact.
fn cmd_args<'s>(
    tail: &c::CmdTail,
    scope: &Scope<'s>,
    shape: &[bool],
) -> Result<Vec<CmdArg<'s>>, ElabError> {
    let args: Vec<&c::AppArg> = match tail {
        c::CmdTail::Semi(_) => Vec::new(),
        c::CmdTail::Args { first, rest, .. } => {
            let mut v: Vec<&c::AppArg> = Vec::with_capacity(1 + rest.len());
            v.push(first);
            for a in rest {
                v.push(a);
            }
            v
        }
    };
    // Marker-less optional-argument defaulting against the command's declared
    // `Param` shape — the command-argument twin of `app_chain_generic`'s
    // algorithm (see its comment for the slot-by-slot rule; e.g. `enumitem`'s
    // `+item : [cfg?; inline-text; cfg?; block-text]` has an optional after a
    // mandatory argument). Unlike that one, a command's arity is fixed by its
    // declared type, so a trailing omitted optional IS filled with `None`
    // rather than left uncurried.
    let mut out = Vec::with_capacity(args.len().max(shape.len()));
    let mut args_iter = args.into_iter().peekable();
    let mut pos = 0usize;
    while pos < shape.len() {
        if shape[pos] {
            match args_iter.peek() {
                Some(c::AppArg::Optional { .. }) | Some(c::AppArg::Omission(_)) => {
                    out.push(CmdArg {
                        opts: Vec::new(),
                        arg: app_arg_to_ast(args_iter.next().unwrap(), scope)?,
                    });
                }
                _ => out.push(CmdArg {
                    opts: Vec::new(),
                    arg: Ast::Ctor("None".to_string(), None),
                }),
            }
        } else {
            match args_iter.next() {
                Some(a) => out.push(cmd_arg_to_ast(a, scope)?),
                None => break,
            }
        }
        pos += 1;
    }
    for a in args_iter {
        out.push(cmd_arg_to_ast(a, scope)?);
    }
    Ok(out)
}

/// One command-application argument, the `?(l = e, …)`-bundle-aware twin of
/// `app_arg_to_ast`: a `Bundled`/
/// `BundledCtor` arg becomes a [`CmdArg`] whose `opts` carries the labeled
/// optionals — elaborated via `elaborate_opt_args`, exactly like a plain
/// function application's `f ?(l = e) x` (`apply_one_arg`'s `Ast::ApplyOpt`
/// arm); every other `AppArg` shape becomes a `CmdArg` with empty `opts` (the
/// unbundled call — the ONLY shape every
/// 0.0.6-reachable call ever emits).
fn cmd_arg_to_ast<'s>(arg: &c::AppArg, scope: &Scope<'s>) -> Result<CmdArg<'s>, ElabError> {
    match arg {
        c::AppArg::Bundled {
            opts,
            excl,
            atom,
            accesses,
        } => Ok(CmdArg {
            opts: elaborate_opt_args(opts, scope)?,
            arg: atomic_head_with_excl(atom, accesses, excl.as_ref(), None, scope)?,
        }),
        c::AppArg::BundledCtor { opts, ctor } => Ok(CmdArg {
            opts: elaborate_opt_args(opts, scope)?,
            arg: Ast::Ctor(ctor.name.clone(), None),
        }),
        _ => Ok(CmdArg {
            opts: Vec::new(),
            arg: app_arg_to_ast(arg, scope)?,
        }),
    }
}

// ---- itemize ---------------------------------------------------------------

/// One node of the itemize tree being built, before it is lowered to the
/// `Ctor("Item", ..)` value shape by [`item_node_to_ast`].
struct ItemNode<'s> {
    text: Ast<'s>,
    children: Vec<ItemNode<'s>>,
}

fn inline_elem_span(el: &c::InlineElem) -> Span {
    match el {
        c::InlineElem::Char(t) => t.span,
        c::InlineElem::CodeText(t) => t.span,
        c::InlineElem::Space(t) => t.0,
        c::InlineElem::Break(t) => t.0,
        c::InlineElem::Embed { var, .. } => var.span,
        c::InlineElem::EmbedMath { mgrp, .. } => mgrp.open.0.unite(mgrp.close.0),
        c::InlineElem::Cmd { name, .. } => horz_cmd_key(name).1,
        c::InlineElem::ItemBullet(t) => t.span,
        c::InlineElem::Sep(t) => t.0,
    }
}

/// Consecutive `ItemBullet`-headed runs of an inline-text group elaborate to
/// a single itemize `Ctor("Item", (text, list))` tree instead of plain
/// `InlineText` — transcribed from `parser.mly`'s `make_list_to_itemize`/
/// `insert_last` (lines 331-356) and `typecheck_itemize`/`typecheck_itemize_list`
/// (typechecker.ml:1359-1374, which lower each `UTItem(utast1, utitmzlst)`
/// node to `NonValueConstructor("Item", PrimitiveTuple([e1; e2]))` — the
/// `Item` constructor's `(inline-text * itemize list)` payload shape from
/// `primitives.cppo.ml:159`).
fn itemize<'s>(elems: &[c::InlineElem], scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    // `sxsep`'s itemize alternative is `nonempty_list(sxitem)` (parser.mly:
    // 1042) — i.e. the *whole* group must be bullets-and-their-content, no
    // leading plain text before the first bullet.
    let mut i = 0;
    while i < elems.len() && !matches!(elems[i], c::InlineElem::ItemBullet(_)) {
        i += 1;
    }
    if i != 0 {
        return err(
            inline_elem_span(&elems[0]),
            "content before the first itemize bullet '*' is not supported",
        );
    }
    let mut segments: Vec<(usize, Span, &[c::InlineElem])> = Vec::new();
    while i < elems.len() {
        let (depth, span) = match &elems[i] {
            c::InlineElem::ItemBullet(tok) => (tok.depth, tok.span),
            _ => unreachable!("loop invariant: elems[i] is always an ItemBullet here"),
        };
        let start = i + 1;
        let mut j = start;
        while j < elems.len() && !matches!(elems[j], c::InlineElem::ItemBullet(_)) {
            j += 1;
        }
        segments.push((depth, span, &elems[start..j]));
        i = j;
    }
    // `make_list_to_itemize_sub`'s accumulator starts as a dummy root item
    // with empty inline text and no children (parser.mly:332,
    // `UTItem((.., UTInputHorz([])), [])`).
    let mut root = ItemNode {
        text: Ast::InlineText(Rc::new(Vec::new())),
        children: Vec::new(),
    };
    let mut crrntdp = 0usize;
    for (depth, span, content) in segments {
        if depth > crrntdp + 1 {
            return err(span, format!("illegal item depth {depth} after {crrntdp}"));
        }
        let text_ast = Ast::InlineText(Rc::new(inline_elems(content, scope)?));
        insert_last(&mut root, 1, depth, text_ast);
        crrntdp = depth;
    }
    Ok(item_node_to_ast(root))
}

/// `insert_last` (parser.mly:346-356), simplified: the OCaml version rebuilds
/// an immutable list by peeling `hditmz :: tlitmzlst` heads into an
/// accumulator until exactly one child remains, then either recurses into it
/// (if not yet at the target depth) or appends a new sibling after it —
/// which is equivalent (and much simpler to transcribe with a mutable tree)
/// to just always operating on `node.children`'s *last* element: recurse
/// into it while `i < depth`, otherwise push a new sibling leaf.
fn insert_last<'s>(node: &mut ItemNode<'s>, i: usize, depth: usize, new_text: Ast<'s>) {
    if node.children.is_empty() {
        node.children.push(ItemNode {
            text: new_text,
            children: Vec::new(),
        });
        return;
    }
    if i < depth {
        insert_last(node.children.last_mut().unwrap(), i + 1, depth, new_text);
    } else {
        node.children.push(ItemNode {
            text: new_text,
            children: Vec::new(),
        });
    }
}

fn item_node_to_ast<'s>(node: ItemNode<'s>) -> Ast<'s> {
    let children = Ast::List(node.children.into_iter().map(item_node_to_ast).collect());
    Ast::Ctor(
        "Item".to_string(),
        Some(Box::new(Ast::Tuple(vec![node.text, children]))),
    )
}

// ---- quoted math ------------------------------------------------------------

fn lower_math_elems<'s>(
    elems: &[cst::MathErased],
    scope: &Scope<'s>,
) -> Result<Vec<MathElem<'s>>, ElabError> {
    elems.iter().map(|e| math_elem_cst(e, scope)).collect()
}

/// `mathblock` (parser.mly:1059-1066): a LEADING `|` puts the math area in
/// list mode — `${| m | m |}` is upstream-desugared in-grammar to an
/// ordinary list literal of `math` values (make_cons over UTMath; there is
/// NO matrix/grid node anywhere in the frontend or math backend) —
/// otherwise the area is one plain `math` (today's single-MathText path).
/// Edge cases replicated exactly: list mode triggers only on a LEADING `|`
/// (`${a|b}` is upstream a parse error); the trailing `|` is mandatory
/// (`${|a|b}` rejected); `${|}` = empty list, `${||}` = one empty cell;
/// `|` never carries scripts. Split is over the flat erased stream so the
/// sibling inline `{| … |}` (sxsep) can reuse it later.
fn math_block_ast<'s>(elems: &[cst::MathErased], scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    let leading_sep = matches!(elems.first(), Some(e) if matches!(&e.base, c::MathBot::Sep(_)));
    if !leading_sep {
        return Ok(Ast::MathText(Rc::new(lower_math_elems(elems, scope)?)));
    }
    for e in elems {
        if let c::MathBot::Sep(tok) = &e.base {
            if !e.scripts.is_empty() {
                return err(
                    tok.0,
                    "a '|' math-list separator cannot carry a script ('^'/'_'/primes)",
                );
            }
        }
    }
    if !matches!(elems.last(), Some(e) if matches!(&e.base, c::MathBot::Sep(_))) {
        let c::MathBot::Sep(first) = &elems[0].base else {
            unreachable!()
        };
        return err(
            first.0,
            "a '|'-separated math list must end with a trailing '|' (write `${| a | b |}`)",
        );
    }
    let mut segments: Vec<Ast<'s>> = Vec::new();
    let mut seg_start = 1usize;
    for (i, e) in elems.iter().enumerate().skip(1) {
        if matches!(&e.base, c::MathBot::Sep(_)) {
            let seg = &elems[seg_start..i];
            segments.push(Ast::MathText(Rc::new(lower_math_elems(seg, scope)?)));
            seg_start = i + 1;
        }
    }
    Ok(Ast::List(segments))
}

fn math_elem_cst<'s>(m: &c::MathElemCst, scope: &Scope<'s>) -> Result<MathElem<'s>, ElabError> {
    let base = math_bot(&m.base, scope)?;
    fold_math_scripts(base, &m.scripts, scope)
}

fn math_bot<'s>(b: &c::MathBot, scope: &Scope<'s>) -> Result<MathElem<'s>, ElabError> {
    match b {
        c::MathBot::Cmd { name, args } => {
            let (key, span) = math_cmd_key(name);
            if !scope.contains(&key) {
                return err(span, format!("unbound math command '{key}'"));
            }
            // Marker-less optional defaulting — the command mirror of
            // app_chain_generic (upstream typecheck_command_arguments skips
            // optional slots left unmarked). No non-empty-args guard: a
            // MathElem::Cmd is always an application (a bare command VALUE is
            // `command \cmd`), so `${\cmd}` with `[t?] math-cmd` pads too.
            let leading = scope.optional_arity(&key);
            let mut arg_asts = Vec::with_capacity(args.len().max(leading));
            let mut args_iter = args.iter().peekable();
            let mut supplied = 0;
            while supplied < leading {
                match args_iter.peek() {
                    Some(c::MathArg::Optional { .. }) | Some(c::MathArg::Omission(_)) => {
                        arg_asts.push(math_arg_to_ast(args_iter.next().unwrap(), scope)?);
                        supplied += 1;
                    }
                    _ => break,
                }
            }
            for _ in supplied..leading {
                arg_asts.push(Ast::Ctor("None".to_string(), None));
            }
            for a in args_iter {
                arg_asts.push(math_arg_to_ast(a, scope)?);
            }
            // `CmdArg`-shaped for uniformity with `IText::Cmd`/`BText::Cmd`
            // (see `MathElem::Cmd`'s doc
            // comment) — `opts` is always empty: the math-mode application
            // grammar (`c::MathArg`) has no `?(l=e)` bundle form at all.
            Ok(MathElem::Cmd {
                name: scope.resolve(&key),
                span,
                args: arg_asts
                    .into_iter()
                    .map(|arg| CmdArg { opts: Vec::new(), arg })
                    .collect(),
            })
        }
        c::MathBot::Chars(tok) => Ok(MathElem::Chars(tok.text.clone())),
        c::MathBot::Embed(tok) => {
            // Math commands are qualified via `math_cmd_key` the same way
            // `horz_cmd_key`/`vert_cmd_key` handle `\Mod.cmd`; `#var`/
            // `#Mod.var` embeds already carry a `mods` list (`VarInMathTok`),
            // so those are mangled the same as everywhere else.
            let key = qualify_key(&tok.mods, &tok.name);
            if !scope.contains(&key) {
                return err(tok.span, format!("unbound variable '{key}'"));
            }
            Ok(MathElem::Embed {
                expr: Ast::Var(scope.resolve(&key), tok.span),
                span: tok.span,
            })
        }
        c::MathBot::Sep(tok) => err(tok.0, "'|' builds a math list and may only be used when the math area starts with '|' (e.g. `${| a | b |}`); it cannot appear mid-formula or inside a `{ … }` math group"),
        c::MathBot::Group { elems, .. } => Ok(MathElem::Group(lower_math_elems(elems, scope)?)),
    }
}

fn math_group_arg<'s>(
    g: &c::MathGroupArg,
    scope: &Scope<'s>,
) -> Result<Vec<MathElem<'s>>, ElabError> {
    match g {
        c::MathGroupArg::Group { elems, .. } => lower_math_elems(elems, scope),
        c::MathGroupArg::Bot(b) => Ok(vec![math_bot(b, scope)?]),
    }
}

/// `mathtop`'s seven script-combo alternatives (parser.mly:1078-1116),
/// folded left over `MathElemCst`'s flat `scripts` vector (see its doc
/// comment in `cst.rs`). Combos with only a subscript, only a superscript,
/// or a sub+superscript pair (either written order) transcribe exactly:
/// whichever token is spelled `SUBSCRIPT` becomes the inner `Sub` operand
/// and `SUPERSCRIPT` the outer `Sup`, regardless of source order
/// (parser.mly's rules 3 and 5 both produce `Sup(Sub(base,subgrp),supgrp)`).
///
/// **Deviation for `PRIMES` combined with an explicit script** (rules 4 and
/// 6): v0.0.6 encodes primes-plus-script by *reusing* the
/// `UTMSubScript`/`UTMSuperScript` nodes as an internal slot-assignment
/// trick, so one rendering routine can lay out the prime mark and the real
/// script in one corner-glyph slot (rule 4 puts primes in `Sub` and the
/// explicit `^group` in the outer `Sup`; rule 6 swaps them — an explicit
/// script and primes trade slots depending on which was explicit). This
/// port's `MathElem` has a *distinct* `Primes(base, count)` node with no
/// v0.0.6 counterpart, so there's no slot to reuse; primes fold in as their
/// own step and any immediately-following explicit script applies on top of
/// that, in source order — same information (script, count, shared base)
/// without the internal rendering hack, which has no meaning yet anyway
/// (typesetting is deferred).
fn fold_math_scripts<'s>(
    base: MathElem<'s>,
    scripts: &[c::MathScript],
    scope: &Scope<'s>,
) -> Result<MathElem<'s>, ElabError> {
    let mut acc = base;
    let mut i = 0;
    while i < scripts.len() {
        match &scripts[i] {
            c::MathScript::Sub { group, .. } => {
                if let Some(c::MathScript::Super { group: g2, .. }) = scripts.get(i + 1) {
                    let subg = math_group_arg(group, scope)?;
                    let supg = math_group_arg(g2, scope)?;
                    acc = MathElem::Sup(Box::new(MathElem::Sub(Box::new(acc), subg)), supg);
                    i += 2;
                } else {
                    let subg = math_group_arg(group, scope)?;
                    acc = MathElem::Sub(Box::new(acc), subg);
                    i += 1;
                }
            }
            c::MathScript::Super { group, .. } => {
                if let Some(c::MathScript::Sub { group: g2, .. }) = scripts.get(i + 1) {
                    let supg = math_group_arg(group, scope)?;
                    let subg = math_group_arg(g2, scope)?;
                    acc = MathElem::Sup(Box::new(MathElem::Sub(Box::new(acc), subg)), supg);
                    i += 2;
                } else {
                    let supg = math_group_arg(group, scope)?;
                    acc = MathElem::Sup(Box::new(acc), supg);
                    i += 1;
                }
            }
            c::MathScript::Primes(tok) => {
                acc = MathElem::Primes(Box::new(acc), tok.count);
                i += 1;
            }
        }
    }
    Ok(acc)
}

/// `matharg` (parser.mly:1138-1146 + narg 1201-1210): `?:`-supplied desugars
/// to `Some(<body>)`, `?*` to `None` — the math-command mirror of
/// `app_arg_to_ast`'s `AppArg::Optional`/`Omission` arms. A mandatory
/// (`Plain`) argument elaborates its body directly with no wrapping.
fn math_arg_to_ast<'s>(arg: &c::MathArg, scope: &Scope<'s>) -> Result<Ast<'s>, ElabError> {
    match arg {
        c::MathArg::Plain(body) => math_arg_body_to_ast(body, scope),
        c::MathArg::Optional { body, .. } => Ok(Ast::Ctor(
            "Some".to_string(),
            Some(Box::new(math_arg_body_to_ast(body, scope)?)),
        )),
        c::MathArg::Omission(_) => Ok(Ast::Ctor("None".to_string(), None)),
    }
}

/// The six `matharg` body shapes (`cst.rs`'s `MathArgBody` doc comment):
/// recurse into math (`Math`), program-mode escapes (`!(..)`/`![..]`/
/// `!(|..|)`, elaborated exactly like their `Atomic`/`Expr` counterparts), or
/// inline/block text escapes (`!{..}`/`!<..>`, elaborated to
/// `InlineText`/`BlockText` Asts).
fn math_arg_body_to_ast<'s>(
    body: &c::MathArgBody,
    scope: &Scope<'s>,
) -> Result<Ast<'s>, ElabError> {
    match body {
        c::MathArgBody::Math { elems, .. } => math_block_ast(elems, scope),
        c::MathArgBody::Inline { elems, .. } => inline_text_ast(elems, scope),
        c::MathArgBody::Block { elems, .. } => {
            Ok(Ast::BlockText(Rc::new(block_elems(elems, scope)?)))
        }
        c::MathArgBody::ParenEscape { inner, .. } => paren_body(inner, scope),
        c::MathArgBody::ListEscape { items, .. } => {
            let mut out = Vec::with_capacity(items.len());
            for it in items {
                out.push(expr(&it.value, scope)?);
            }
            Ok(Ast::List(out))
        }
        c::MathArgBody::RecordEscape { body, .. } => record_body_to_ast(body, scope),
    }
}

// ---- string-literal space omission -----------------------------------------

/// `omit_spaces`/`omit_pre_spaces`/`omit_post_spaces`/`min_indent_space`/
/// `shave_indent` (parser.mly's header section, lines 72-152), transcribed
/// faithfully (byte-for-byte algorithm, but over `char`s rather than bytes so
/// it stays correct on non-ASCII source text — the original indexes
/// `String.length`/`String.sub` byte-wise, which coincides with `char`-wise
/// indexing everywhere the original relies on it, since it only ever tests
/// for `' '`/`'\n'`, both single-byte in UTF-8).
fn omit_spaces(omit_pre: bool, omit_post: bool, raw: &str) -> String {
    let s1 = if omit_pre {
        omit_pre_spaces(raw)
    } else {
        raw.to_string()
    };
    let s2 = if omit_post { omit_post_spaces(&s1) } else { s1 };
    let min_indent = min_indent_space(&s2);
    let shaved = shave_indent(&s2, min_indent);
    let mut chars: Vec<char> = shaved.chars().collect();
    if chars.last() == Some(&'\n') {
        chars.pop();
    }
    chars.into_iter().collect()
}

/// Strip every leading `' '` (not `'\n'` or other whitespace).
fn omit_pre_spaces(s: &str) -> String {
    s.trim_start_matches(' ').to_string()
}

/// Strip trailing `' '`s; once a `'\n'` is reached, strip that single
/// newline and stop (no further recursion past it).
fn omit_post_spaces(s: &str) -> String {
    let mut chars: Vec<char> = s.chars().collect();
    loop {
        match chars.last() {
            Some(' ') => {
                chars.pop();
            }
            Some('\n') => {
                chars.pop();
                break;
            }
            _ => break,
        }
    }
    chars.into_iter().collect()
}

/// The minimum leading-space count of every line (including the very first,
/// since `min_indent_space_sub`'s initial state is `ReadingSpace`, not
/// `Normal` — so unlike every *subsequent* line, the first line's leading
/// spaces count even without a preceding `'\n'`). A line consisting only of
/// spaces does not update the minimum ("does not take space-only line into
/// account").
fn min_indent_space(s: &str) -> usize {
    let chars: Vec<char> = s.chars().collect();
    let mut reading_space = true;
    let mut spnum = 0usize;
    let mut minspnum = chars.len();
    for ch in chars {
        if reading_space {
            match ch {
                ' ' => spnum += 1,
                '\n' => spnum = 0,
                _ => {
                    if spnum < minspnum {
                        minspnum = spnum;
                    }
                    reading_space = false;
                }
            }
        } else if ch == '\n' {
            reading_space = true;
            spnum = 0;
        }
    }
    minspnum
}

fn shave_indent(s: &str, minspnum: usize) -> String {
    let mut out = String::new();
    let mut reading_space = false;
    let mut spnum = 0usize;
    for ch in s.chars() {
        if reading_space {
            match ch {
                ' ' => {
                    if spnum >= minspnum {
                        out.push(' ');
                    }
                    spnum += 1;
                }
                '\n' => {
                    out.push('\n');
                    spnum = 0;
                }
                _ => {
                    out.push(ch);
                    reading_space = false;
                }
            }
        } else if ch == '\n' {
            out.push('\n');
            reading_space = true;
            spnum = 0;
        } else {
            out.push(ch);
        }
    }
    out
}