Expand description
Abstract syntax tree, elaboration, evaluator, and primitives — the language core of the SATySFi port.
Modules§
- ast
- The elaborated abstract syntax tree (a subset of
abstract_treein types.cppo.ml). Produced from the surface CST byelaborate; consumed by the evaluator. - crossref
- Cross-reference table + the fixpoint verdict, a small port of
crossRef.ml. Owned by the compile driver (lib.rs::compile_document_cst), not reset per trial — it is the fixpoint state that persists while everything else (hooks, images, mutable store) resets each trial. - elaborate
- Surface CST →
Astelaboration. Does scope resolution, operator- precedence/associativity resolution (the CST leaves that flattened, seecst.rs’s module doc comment), pattern lowering, thelet-inline/let-blockcontext-argument desugaring, mutable/while/beforedesugaring, 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. - eval
- Interpreter state and beta-reduction.
- exhaustive
- Match exhaustiveness and redundancy checking — a row-major
reimplementation of the Maranget “usefulness”
matrix algorithm v0.0.6 uses in
src/frontend/exhchecker.ml. Non-fatal: this module only producesMatchWarnings, never acrate::typecheck::TypeError(mirrorsexhchecker.ml’s own warn-and-continue policy — see that module’smain, lines 391-424). - hyphenation
- Knuth–Liang hyphenation engine.
- prim_
types - Type signatures for every primitive registered in
primitives.rs’sprims!table (plus theinline-filconstant), transcribed from v0.0.6’stools/gencode/vminst.ml~type_:fields (cited by line number at each entry below) and fromsrc/frontend/primitives.cppo.mlfor the handful of names vminst.ml doesn’t define directly (::,!, the comparison trio derived ingeneral_table). - primitives
- The primitive registry. Shaped so the ~300 vminst instructions can be
ported one
prims!line at a time; primitives are registered under their real v0.0.6 names so later stdlib loading finds them. - quoted
- Quoted text in its compiled form — what
{ … }/'< … >/${ … }become oncecrate::compilehas lowered them, and whatcrate::value::Value’sInlineText/BlockText/MathTextvariants carry. - symbol
- Interned identifiers:
SymbolStore(an append-only unique-string registry) andSymbol(aCopy,u32-sized handle into one). - typecheck
- The Hindley–Milner type inferencer: walks an
crate::elaborate::Programand reports the first type error it finds, mirroring v0.0.6’stypecheck/typecheck_sub(src/frontend/typechecker.ml) — unification itself lives incrate::unify, generalization/instantiation incrate::types, this module only walks the AST applying those primitives at each rule, exactly astypechecker.mldoes over its ownunify/Typeenv. - types
- The type language: base types, the mutable (union-find) representation
of type/row variables, monomorphic and polymorphic types, and
level-based generalization. Mirrors
mono_type_main/poly_type/kindin v0.0.6’ssrc/frontend/types.cppo.ml, with two deliberate departures documented at their definitions: - unify
- Structural unification over
crate::types::MonoType, mirroring v0.0.6’sunify_sub(src/frontend/typechecker.ml:360-522): occurs check (extended to look through rows, since rows are first-class here — see the module doc comment oncrate::types::Row), record/row unification, and theKind::Recordbridging case. - v1
- SATySFi 0.1 (
dev-0-1-0) support: lowering thecst_v1CST into the shared 0.0.6-shaped pipeline (lower.rs), plus the module system. - value
- Runtime values (a subset of
syntactic_value). - visit
- One generated, exhaustive traversal of the type representation —
MonoType,RowandCmdArgType.
Enums§
Functions§
- check_
document_ cst_ with_ stages compile_document_cst_with_stages’s front half and nothing else: elaborate and typecheck, then STOP — no closure tree, no font store, no evaluation. The 0.0.6 sibling ofcheck_document_v1; see that function for what the distinction is for.- check_
document_ program - Typecheck a whole loader-resolved program, whichever of the three shapes it is, without evaluating it.
- check_
document_ v006_ xver compile_document_v006_xver_with_aux’s front half and nothing else — the reverse-direction sibling ofcheck_document_v1, with the same rationale.- check_
document_ v1 compile_document_v1_with_aux’s front half and nothing else: assemble, elaborate, typecheck, enforce every:>seal — then STOP, without compiling a closure tree, without a font store, and without evaluating anything.- compile_
document - Compile a
.satysource string down to a typeset document: lex → parse → elaborate → evaluate. - compile_
document_ cst - Compile an already-parsed (possibly loader-merged) file. The multi-file
loader concatenates library preludes into one synthetic
cst::Fileand enters here. - compile_
document_ cst_ with_ aux compile_document_cst_with_trialsthreading an AUXILIARY cross-reference table:auxseeds the fixpoint from a previous run and is overwritten with the final table. Seeding only affects how fast the fixpoint converges — seecrossref::CrossRefs::seededandcrossref::CrossRefs::seed_unvalidated, which together guarantee the output is the same as a cold run’s.- compile_
document_ cst_ with_ stages compile_document_cst_with_auxtold which merged prelude entries came from a file that declared a non-default@stage:.- compile_
document_ cst_ with_ trials - Same as
compile_document_cst, but also returns how many fixpoint trials it took (& the fixpoint) — exposed for tests that must confirm the fixpoint actually iterated, not just that it produced the right answer on a lucky first pass. - compile_
document_ v006_ xver - Compile a loader-resolved SATySFi 0.0.6 program (
LoadOptions { version: V0_0, .. }) whose entry (or one of its native 0.0.6 co-dependencies)@require:s at least one foreign 0.1 package. - compile_
document_ v006_ xver_ with_ aux compile_document_v006_xver_with_trialsthreading an AUXILIARY cross-reference table — seecompile_document_cst_with_aux’s doc comment for what seedingauxdoes and why it can’t change the output.- compile_
document_ v006_ xver_ with_ trials - Trial-count-reporting sibling, mirroring
compile_document_v1_with_trials. - compile_
document_ v1 - Compile a loader-resolved SATySFi 0.1 program (
LoadOptions { version: V0_1, .. }): dependency libraries (files[..n-1], loader dependency-first order) are each lowered to oneTopBinding::Module(qualified exports — seev1/lower.rs’s module doc) viav1::lower::lower_file_v1, the entry (files[n-1], always last —LoadedProgram::files’s contract) viav1::lower::lower_document_v1, assembled into ONE syntheticcst::File— the same shape the CLI’smerge_programbuilds for 0.0.6 — and pushed through the SHARED elaborate -> typecheck(V0_1) -> compile -> fixpoint-eval pipeline. Signature ascriptions (:>) are enforced per binding byv1::module_check::check_program. - compile_
document_ v1_ with_ aux compile_document_v1_with_trialsthreading an AUXILIARY cross-reference table — seecompile_document_cst_with_aux’s doc comment for what seedingauxdoes and why it can’t change the output.- compile_
document_ v1_ with_ trials - Trial-count-reporting sibling, mirroring
compile_document_cst_with_trials(same rationale: fixture tests that must see the fixpoint iterate). - declared_
stage - The stage a file’s
@stage:header declares, if any. - fire_
hooks - Fire every placed page-break hook and decoration, in document order, now
that final page numbers and points are known. This is the port’s
callback architecture:
make_hook+handlePdf.ml:234/337’s invocation (hooks) andEvHorzFrame/EvVertFrame(decos), relocated to the one place that legally holds&mut Interp— the backend produced the geometry (PODHookId/DecoIdtokens riding inside placed boxes, perhbox.rs); this reads them back and re-enters the evaluator. - merge_
v006_ program - Concatenate a loader-resolved 0.0.6 program’s dependency-ordered library
preludes ahead of the entry document’s own, producing the one synthetic
file
compile_document_cst_with_stagesandcheck_document_cst_with_stageselaborate — plus the per-slot@stage:table the concatenation would otherwise lose.