Module cst 

The SATySFi 0.0.6 surface grammar (a subset of the v0.0.6 parser.mly), parsed with syan derives over the SATySFi token atoms.

Application and the nxlor..nxrtimes binary-operator levels are left-recursive in the Menhir grammar; here they are head-plus-arguments Vecs, folded left during elaboration — recursive descent must never see left recursion. All ten binop precedence levels are flattened into one OpChain, deferring precedence/associativity to the elaborator — a deliberate deviation from parser.mly’s structure, not its token set (every operator it accepts is accepted here too).

let-inline/let-block are top-level-only, matching parser.mly: LETHORZ/LETVERT only appear in nxtoplevel/nxstruct (via nxhorzdec/nxvertdec), never in nxletsub — unlike let/let-rec they have no local (in-bodied) form, only as one of a file’s leading TopBindings.

Re-exports

pub use crate::parse_error::ParseFileError;

Modules

ast

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

Structs

AndTypeClause

One and 'a name = body continuation of a TypeDecl’s mutual-recursion chain (mirrors ast::AndBinding for let-rec).

AppArgErased

An ast::AppArg behind a stream-erasing parse (see above). Bridges a command tail’s argument chain (CmdTail::Args, below) into AppArg’s own parser without a direct field reference: CmdTail is reached from Expr’s SCC via Atomic::InlineText/BlockText -> InlineElem/BlockElem -> CmdTail, so a direct AppArg field here would close a brand-new cycle back into Atomic (AppArg::Atom.atom: Atomic) entirely through non-root types — the exact “sub-cycle running entirely through non-root types” shape the #[recurse] engine rejects (see PatCons’s doc comment for the same hazard). Routing through this eraser keeps CmdTail a DAG leaf, same as every other cross-reference here.

BarVariantDef

A | Ctor [of ty] continuation of a variant list.

BindName

A binding-position NAME: a plain variable, or ( ‹op› ) — a parenthesized (possibly user-defined) operator name (OpNameTok), e.g. let (+++>) = ... Upstream’s var nonterminal folds VAR and LPAREN binop RPAREN into one production; this is that nonterminal, reused by TopLet::name, ast::Expr::LetIn’s name, ast::RecBinding::name, and SigItem::Val’s name — the four binding positions upstream admits it in. .name/.span mirror VarTok’s own public fields exactly, so an elaborate.rs/typecheck.rs callsite reading foo.name.name/ foo.name.span works against either type. See also ast::Atomic::OpRef, the matching atomic-expression form.

ExprErased

An ast::Expr behind a stream-erasing parse (see above).

File

A whole .saty/.satyh file: headers, top-level bindings, in, the document expression (main/nxtoplevel/nxtopsubseq in parser.mly).

MathErased

An ast::MathElemCst behind a stream-erasing parse (see above). Unlike the other three erasers this one isn’t bridging a self-loop of its target’s own SCC — MathElemCst turns out to have no direct self-loop at all (see its doc comment) — but every nested reference to “one math element” still goes through here, for the same monomorphize-once reason.

OfType

The of ty suffix of a variant definition.

PatBotErased

An ast::PatBot behind a stream-erasing parse (see above). Kept separate from PatErased because a constructor pattern’s argument is a patbot, not a full patas (Some x as y binds y to the whole value, not to x).

PatErased

An ast::Pattern behind a stream-erasing parse (see above).

RecordKind

kxtop: (| l1 : ty1; … |), a record-kind bound — “the constrained type variable must be a record containing at least these labels” (upstream MRecordKind; lowers to this port’s Kind::Record row obligation, presence-only — see typecheck.rs).

RecordKindField

One l : ty; field of a RecordKind (txrecord, parser.mly:962-965). The field type is parsed but currently dropped during lowering (only the label is kept, matching Kind::Record’s label-only representation) — a documented limitation, not a grammar gap.

SigAnnot

: sig ... end (nxsigopt/nxsigelem, drastically simplified — see SigItem).

SigConstraint

One constrnt: constraint 'a :: (| l1 : ty1; l2 : ty2; … |) (parser.mly:526-530), a per-item suffix binding that item’s type variable to a row-kind obligation — not a standalone SigItem (a reader expecting the latter should see this doc: upstream attaches constrnts to SigValue/SigDirect/SigType directly, so the suffix form here is the faithful one and avoids an ambiguous “which item does this constrain?”).

StructDecl

One declaration inside a module ... = struct ... end body (nxstruct). nxstruct’s alternatives are a strict subset of nxtoplevel’s (every form it has, TopBinding also has, once Module/Open are added), so this simply re-parses a TopBinding — but not by naming TopBinding as a field type directly: TopBinding lives outside the #[recurse] module, so TopBinding -> Module -> Vec<StructDecl> -> TopBinding would be a self-recursive cycle through a plain #[derive(Parse)], which (without the #[recurse] engine to back it) is an E0275 hazard (an unbounded recursive trait-bound obligation). Hand-writing Parse/Unparse here — the same trick as ExprErased et al. — sidesteps that: the impl has no recursive where-bound for the compiler to try to satisfy, it just calls TopBinding::parse through the stream-erasing adapter at runtime.

TopLet

A top-level non-recursive binding: let name param* = expr. params is Vec<ast::PatBot> (not merely Vec<VarTok>) — nxnonrecdec’s argpart is patbot* upstream too, matching ast::RecBinding’s field of the same name. Elaborated by the same rec_clause_value helper RecBinding uses (elaborate.rs), with no multi-clause extra.

TopStage

A binding’s own stage qualifier: ~ (stage 0) or persistent ~ (persistent stage), the prefix SATySFi 0.1 writes between val and the bound name (parser_v1.mly:417-421, UTBindValue(Stage0 | Persistent0, _); the absent prefix is Stage1, the document stage).

TyErased

An ast::TypeExpr behind a stream-erasing parse (see above).

TypeDecl

A type declaration, optionally with mutual (and) recursion between several type declarations (parser.mly’s nxvariantdec and-chain, e.g. satysfi-base’s stream.satyg: type 'a state = … and 'a u = ('a state) Promise.t). The head clause is kw..body; every further and-clause is an AndTypeClause. All clauses in one chain are mutually visible — they lower to consecutive UserTypeDecl/UserSynonymDecls, exactly the shape the 0.1 lowering (v1/lower.rs) already produces for type … and …, which the typechecker resolves with the same forward-reference tolerance.

VariantDef

One Ctor [of ty] variant definition.

Enums

Header

@require: / @import: / @stage: header element.

SigItem

One nxsigelem. Type parameters/type synonyms on type items are not supported — such input is rejected with a parse error. Each item may carry a trailing constrnts (parser.mly:526-530) — see SigConstraint.

TopBinding

One top-level declaration (nxtoplevel/nxstruct’s per-declaration alternatives). LetInline/LetBlock only exist here — see the module doc comment.

TypeDeclBody

The right-hand side of a type declaration: either a variant’s constructor list, or (transparently) a type-synonym body. Trying the variant shape first is unambiguous: a type name is always a bare VAR in this grammar (txbot), so no type expression can ever start with the BarTok/CtorTok a variant list requires — any input that isn’t a variant list falls through to Synonym cleanly, exactly like upstream’s nxvariantdec telling variants (always CONSTRUCTOR-headed) apart from txfunc by lookahead.

Functions

parse_file

Lex and parse a whole .saty source file.