Module ast 

The recursive expression/pattern/type/text grammar. Program expressions embed inline/block text ({…}, '<…>), text embeds commands, and command arguments re-enter program expressions.

Recursion structure. Grammatically this is one big knot, but at the type level every recursion edge except three self-loops is routed through the stream-erasing leaf wrappers defined above (ExprErased, PatErased, TyErased) — see their doc comment for the measured compile-time blowup that forced this. The #[recurse] macro therefore sees exactly three singleton SCCs, each a directly self-referential root:

• Expr (its own variants’ Box<Expr> children — nxlet nesting like if … then if … else … runs on the engine);
• PatBot (CtorApplied’s Box<PatBot> argument — Some Some x);
• TypeExpr (Fun’s right-recursive Box<TypeExpr> codomain).

Every sub-cycle trivially passes through its root. All other nesting (command arguments, parenthesized/tuple bodies, record/list elements, match-arm bodies, …) recurses at runtime through the erasers’ hand-written Parse impls, which is unbounded by construction.

A command’s arguments are still represented as one application-chain Expr (CmdTail::Args) rather than a dedicated argument list — faithful to the OCaml AST, where command arguments are a curried UTApply chain anyway. Elaboration flattens that chain back into the argument list.

Structs

AccessSeg

One #label field-access segment (nxbot ACCESS var).

AndBinding

An and name param* = value continuation of a let-rec.

AppExpr

nxun/nxapp/nxunsub flattened: an optional leading unary minus, an optional leading !/!!/… deref (UNOP_EXCLAM, nxunsub), an atomic head with any #label field accesses (nxbot ACCESS var, left-recursive in parser.mly — flattened to a postfix Vec here, the same technique as PatCons’s ::), and an application-chain tail (nxapp nxunsub / nxapp CONSTRUCTOR / nxapp OPTIONAL nxunsub / nxapp OMISSION, left-folded during elaboration). EXACT_AMP/EXACT_TILDE (&/~) are the staging prefixes, carried in stage (see StagePrefix). First-class command references (command \cmd, upstream’s nxapp: COMMAND hcmd) are modeled one level down, as Atomic::Command — see its doc comment for the rationale.

AsClause

The as name suffix of a pattern.

BarArm

A | pat [when guard] -> body continuation of a match’s arm list.

BeforeTail

The before body suffix of an OpChain (nxbfr).

CommaExpr

A , expr continuation inside a parenthesized tuple.

CommaPattern

A , pat continuation inside a parenthesized tuple pattern.

ConsSeg

One :: patbot continuation of a cons pattern.

CstOptArgEntry

One label = expr entry of a CstOptArgs bundle — a FULL expression (?(bias = 1 + n)), routed through super::ExprErased so this satellite never joins Expr’s SCC.

CstOptArgs

A SATySFi 0.1 ?(l = e, …) optional-argument bundle (for AppArg::Bundled/AppArg::BundledCtor): the ? sigil, then a parenthesized ,-separated list of label = expr entries.

CstOptBinderEntry

One label = binder entry of a CstOptBinders bundle (the last , is optional; = is upstream’s EXACT_EQ, reusing DefEqTok).

CstOptBinders

A SATySFi 0.1 ?(l = x, …) optional-parameter binder bundle (for Expr::FunRows): the ? sigil, then a parenthesized ,-separated list of label = binder entries.

CstRecordOpenField

One l : ty, field of a TypeAtom::RecordOpen (last , optional).

CstRecordOpenInner

A TypeAtom::RecordOpen’s group content: one or more ,-separated fields (nonempty enforced at lowering, matching the closed form), then a mandatory | ?'r row-variable tail.

CstTypeOptDom

?(l = ty, …) — the closed labeled-optional-domain prefix of TypeExpr::OptRowFun. No row-variable-tail field: row-tailed optional domains need signature-level row quantification (parser_v1.mly’s rowquant/quant) — not implemented here; cst_v1’s own TypeOptDomInnerV1 models the tail at parse level and rejects it with a LowerError before ever reaching here (v1/lower.rs).

CstTypeOptEntry

One label : ty, entry of a CstTypeOptDom (last , optional — matching the 0.1 lowering convention this file’s other additive nodes use, e.g. CstOptArgEntry, rather than the frozen grammar’s ;).

Guard

A match arm’s when cond guard.

ListItem

One list element expr; (the last ; is optional).

MatchArm

One pat [when guard] -> body match arm. The pattern and body sit behind the stream-erasing wrappers (deref to reach the inner nodes).

MathElemCst

mathtop: one math element, i.e. a mathbot base with any postfix ^/_/' script combos (mathtop’s seven alternatives, flattened to a Vec in source order — the same Ops/OpChain deferred- precedence technique, since combos 3–6 interleave sub/superscript application order in a way elaboration is better placed to resolve).

OpChain

A flattened binary-operator chain: head (op rhs)*, left-folded (with correct per-operator precedence/associativity) during elaboration. before is nxbfr’s postfix (e1 before e2), attached here rather than modeled at its own precedence level: nxbfr sits between nxif and nxlambda, i.e. above nxlor/OpChain’s own level, so parser.mly’s left operand is actually nxlambda (which also covers Fun/Overwrite) — attaching to OpChain alone misses (fun x -> e1) before e2/(x <- e1) before e2 as the left operand; such input is rejected here (a documented simplification, not a silent misparse). body is threaded through ExprErased (not boxed directly) to keep Expr a singleton SCC: a direct Box<Expr> field on OpChain would make OpChain itself part of Expr’s SCC (a second, non-Expr-variant self-loop edge), which is exactly the multi-type-cycle shape the module doc warns about.

OpRhs

One op rhs continuation of an OpChain.

OptArrowDom

One ty ?-> leading domain of a TypeExpr::Fun’s optional-argument prefix (parser.mly’s txfuncopts, 880-882).

ParenBody

The parenthesized-expression group’s content: one expression, plus any , expr continuations (present only for a tuple).

PatCons

pattr: a patbot, followed by any number of :: patbot segments. parser.mly writes this as right recursion (patbot :: pattr, always fine, unlike left recursion) but it is flattened to a Vec here (the same right-fold-at-elaboration technique as OpChain, :: being right-associative) so that PatCons need not be self-referential: a PatCons/ConsRest pair of mutually-referencing wrapper structs would form a 2-cycle with no self-loop of its own, which the #[recurse] depth engine rejects (“a sub-cycle running entirely through non-root types”).

PatListItem

One list-pattern element pat; (the last ; is optional).

Pattern

patas: a pattern, plus an optional as name binding.

PatternParenBody

The parenthesized-pattern group’s content: one pattern, plus any , pat continuations (present only for a tuple pattern).

RecAscription

A let-rec binding’s optional : ty ascription (see RecBinding’s doc comment). A direct (non-erased) TypeExpr field: RecBinding is already inside this #[recurse] module (embedded directly by Expr::LetRecIn, not through an eraser), and connecting it straight to TypeExpr — one of the module’s three self-recursive SCC roots — is exactly the same kind of cross-root DAG edge RecBinding.params: Vec<PatBot> already makes to the PatBot root; TypeExpr never refers back to Expr/PatBot/RecBinding, so no new cycle results.

RecBinding

One name [: ty] [|] patbot* = value [| patbot* = value]* clause GROUP of a let-rec (also reused, from outside this module, by top-level let-rec). ascription is parser.mly’s rarer COLON ty type-annotated form (recdecargpart’s COLON ty BAR alternative), e.g. the bundled itemize.satyh’s let-rec listing-item : context -> int -> bool -> bool -> itemize -> block-boxes | ctx depth is-first is-last (Item(...)) = ... Parsed but not enforced — there is no enforcement pass for value-level ascriptions (only module val/direct signature items reach typecheck.rs’s command_scheme/sig machinery) — so it is a parse-and-ignore stand-in whose only job is making verbatim upstream source parse. params is patbot* (recdecargpart’s plain argpats form, optionally preceded by a leading_bar — recdecargpart’s BAR argpatlst alternative, used both for the OCaml-style “every clause, including the first, gets a |” layout the bundled packages write, e.g. list.satyg’s let-rec map\n | f [] = []\n | f (x :: xs) = .., and for the COLON ty BAR form above, whose single clause is only reachable via a leading |). extra holds any further | patbot* = value continuation clauses (nxrecdecpar) — SATySFi’s multi-clause pattern-matching function-definition sugar. Every clause in the group must bind the same number of parameters (checked at elaboration — upstream’s IllegalArgumentLength — not here); the (possibly plural) clauses desugar to one curried function that matches a tuple of fresh parameters against each clause’s patterns in turn — see elaborate.rs’s rec_clause_value.

RecClause

A | patbot* = value continuation clause of a multi-clause let-rec binding (see RecBinding’s doc comment).

RecordField

One record field label = expr; (the last ; is optional).

StarType

A * ty continuation of a TypeProd.

TypeApp

txapp — a postfix type application arg1 arg2 … argN ctor, upstream’s N-ary chain flattened into a greedy atom run (the way OpChain/PatCons flatten their own left-recursions). head is always present; when rest is non-empty the LAST atom is the type constructor (a bare or Mod.-qualified name — list/option/ result/Eq.t/implicit) and every atom before it (including head) is one of its arguments. This is unambiguous because SATySFi always parenthesizes a nested single-argument application (('a list) list, ('a t) implicit — never 'a list list), so a flat run of atoms can only be one constructor applied to the preceding arguments:

TypeCmdArgItem

One ;-separated element of a TypeAtom::Cmd’s bracketed argument list: a mandatory ty, or an optional ty? (parser.mly’s txlist, 955-960) — routed through super::TyErased rather than the narrower TypeApp upstream uses, both to stay a DAG leaf (a direct TypeApp field here would close TypeAtom -> Cmd -> ... -> TypeApp -> TypeAtom, a fresh cycle through non-root types — see AppArgErased’s doc comment for the identical hazard) and per this port’s usual permissive-superset simplification.

TypeCmdOptField

One label : ty, field of a TypeCmdArgItem::opt_labels bundle (the last , is optional, matching this port’s other 0.1-additive comma-separated satellite fields — CstOptBinderEntry, CstTypeOptEntry).

TypeProd

txprod: one or more *-separated TypeApps (a product type), or just a single one if there’s no * at all — flattened to a Vec (the same deferred-fold technique as OpChain/PatCons) rather than modeled as its own right-recursive rule, keeping TypeExpr a singleton SCC.

TypeRecordField

One l : ty; field of a TypeAtom::Record (txrecord, parser.mly:962-965) — sibling of super::RecordKindField, but (unlike that struct, defined outside the #[recurse] module and so free to hold a direct ast::TypeExpr field) this one lives inside TypeAtom’s own SCC, so the field type is routed through super::TyErased instead — a direct ast::TypeExpr field here would close a fresh cycle back through TypeAtom itself (the same hazard TypeCmdArgItem’s doc comment explains).

Enums

AppArg

One application-chain argument: an optional-argument value (?: arg), an omitted optional argument (?*), a plain atomic value (with its own optional ! prefix and #access suffixes, mirroring AppExpr’s head position — each nxunsub/nxbot in the nxapp chain is independent), or a bare constructor applied nullarily (nxapp CONSTRUCTOR).

Atomic

nxbot (plus the ctor-head case usually found in nxun): an atomic expression.

BlockElem

One block-text element (vxbot).

CmdTail

A command’s arguments (narg* sargs in parser.mly, upstream’s own dedicated grammar — not a reuse of the general application chain like AppExpr). Either a bare ; (no arguments) or a flat, non-empty sequence of AppArgs: each is ?: value (a supplied optional narg), ?* (an omitted optional narg), or a plain (possibly !/#access-decorated) atomic value — (expr), (|record|), [list], {inline}, <block>, a bare ctor, etc. — covering both narg’s mandatory forms and sargs’s group forms uniformly (this port’s usual simplification: AppArg::Atom’s Atomic already spans every shape upstream splits across narg/ sargs). Optional/omitted nargs may lead (\ref?:(x){text}, \ref?*{text}) since every element is independently one AppArg — an Expr-based encoding could not, its head being a plain atom.

CmdTypeKind

The command-type keyword closing a TypeAtom::Cmd’s bracketed list.

Expr

nxlet: a let/if/match/lambda-headed expression, falling through to the flattened operator chain (Ops, OpChain) at the bottom. Variant order is parse priority; Ops has no distinguishing leading keyword, so it must stay last.

InlineElem

One inline-text element (ih/ihtext/ihcmd in parser.mly).

MathArg

matharg (parser.mly:1138-1146 + narg 1201-1210): one math-mode command argument — a mandatory body, a ?:-supplied optional (UTOptionalArgument), or ?* (UTOmission). The six body shapes live once in MathArgBody; Optional/Omission/Plain are first-token-disjoint.

MathArgBody

The six body shapes shared by mandatory and ?:-optional math args: a math/inline/block group, or a !-escaped program-mode value. The lexer already switches mode on the escape sigil (!( / ![ / !(| / !{ / !< all emit ordinary LParen/BList/BRecord/BHorzGrp/ BVertGrp tokens — see lexer.rs’s lex_math), so at the token level the escapes are indistinguishable from Atomic’s own Paren/List/Record shapes; reusing those bodies directly here (rather than going through a full ExprErased, which would also happily swallow a following matharg bracket group as a trailing application argument) keeps each matharg exactly one bracket group. NOT Box<MathArg>: a direct self-loop on a non-root type is what #[recurse] rejects, and upstream’s grammar is non-recursive here anyway.

MathBot

mathbot.

MathGroupArg

mathgroup: a script’s operand is either a bracketed math group or a bare mathbot.

MathScript

One postfix script combo of a MathElemCst (mathtop’s SUPERSCRIPT/SUBSCRIPT/PRIMES suffixes, one at a time).

Param

One curried parameter of an ordinary (non-let-rec) let, or of a let-inline/let-block/let-math command binding — upstream’s arg nonterminal (nxnonrecdec’s argpart/cmdarglst, parser.mly:622-624: arg: patbot | OPTIONAL defedvar): a full pattern, or the def-site optional-parameter marker ?:name (parser.mly’s OPTIONAL vartok), e.g. stdja.satyh’s let document record ?:configopt inner = .. and annot.satyh’s let-inline ctx \href ?:borderopt uri inner = ... Upstream’s let-rec/fun argument grammar (recdecargpart/argpats — RecBinding/AndBinding/Expr::Fun) has no such alternative, only plain let and the three command-binding forms do — all four keep Vec<Param> (super::TopLet, Expr::LetIn, super::TopBinding::LetInline/LetBlock/LetMath, Expr::LetMathIn). Elaborated (elaborate.rs) by widening Optional to PatBot::Var (params_to_patbots) before the ordinary pattern-currying machinery runs (plain let’s rec_clause_value, or a command binding’s curry_cmd_params) — the ?: marker carries no further semantics of its own in this port (typecheck.rs’s command_scheme doc comment: optionality is inferred structurally, not from this marker); for a command binding, the maximal leading run of ?:-marked params is additionally counted by elaborate.rs’s leading_optional_count and recorded into the binding’s Scope::optional_arity, so a marker-less call site can auto-omit those slots (see cmd_args/math_bot’s Cmd arm).

PatBot

patbot, plus the constructor-pattern forms pattr adds in parser.mly (folded in here to keep PatCons a plain struct).

RecordBody

(| … |)’s content: either a plain field list, or a record update base with l = e; … (nxrecordsynt’s third alternative). Update is tried first (it backtracks cleanly to Fields — parsing base as an expression stops right before a bare label = expr’s =, since = isn’t a valid expression continuation, so the with keyword check fails fast and Fields picks it up). base is nxbot in parser.mly (an atomic expression); routed through ExprErased here instead, which is strictly more permissive (accepts any expression as the base, not just an atomic one) — a deliberate simplification, and also the only way to reference it without adding a second, non-Group recursion edge into Atomic (which — like AppExpr/OpChain — is not itself part of Expr’s SCC, and should stay that way).

StagePrefix

A staging prefix on a nxunsub operand: &e builds code for the next stage, ~e splices the result of a previous-stage computation (parser.mly:796-797, UTNext/UTPrev).

TypeAtom

An atomic type expression.

TypeExpr

A minimal type-expression grammar for type declarations and signature (val .. : ty) annotations (txfunc/txprod/txapppre/ txapp/txbot, simplified). Function arrows (right-associative, with an optional-argument ?-> prefix chain — see OptArrowDom), 2+-way product types (*, TypeProd), a SINGLE-argument postfix type-constructor application ('a option, 'a list; see TypeApp), command-argument-list types ([ty; ty?; ..] inline-cmd/block-cmd/math-cmd; see TypeAtom::Cmd), parenthesized grouping, closed record types ((| l : ty; … |); see TypeAtom::Record), bare/qualified names, and type variables are supported; N-ary applied constructors are not — such input is rejected with a parse error. Self-recursive only through Fun’s codomain (right recursion); parenthesized nesting goes through the super::TyErased leaf.