Compiler pipeline#

What happens to a source file, in order, and what each step may decide.

bytes
  -> lossless lexemes and trivia          Alpha.Surface.Source
  -> concrete syntax tree (CST)           Alpha.Surface.Source.parseCst
  -> surface module                       Alpha.Surface.Module.parseAlphaModule
  -> core terms                           Alpha.Surface.Elaborate
  -> CHECKED terms                        Alpha.Core.Trusted.Kernel
  -> checked interface (cached)           Alpha.Surface.Interface
  -> sealed program                       Alpha.Surface.Module.sealCheckedSharedModuleProgram
  -> erased runtime term                  Alpha.Core.Erasure
  -> either: reduced erased term          Alpha.Compiler.ErasedReduction (evaluator lane)
             -> runtime graph + evaluator Alpha.Compiler.RuntimeGraph
     or:     typed control flow -> code   Alpha.IR.Semantic + Alpha.Compiler.ControlFlowNative (direct lane)
  -> native object                        Alpha.Compiler.NativeObject
  -> ELF                                  Alpha.Compiler.Link + Alpha.Target.X86_64 (or Alpha.Target.AArch64)

Step by step#

Lexing is lossless. Every byte of the file belongs to exactly one lexeme, including whitespace and comments, so the file can be rebuilt from the lexemes. A line break is its own lexeme because declaration ownership is decided per line.

Parsing builds a CST over those lexemes. Malformed structure becomes an error node rather than an exception, which is why the formatter can refuse a file precisely ("unterminated list at line 143") instead of failing.

Module parsing reads the line-oriented declaration grammar: module, import, family blocks and def. Import order is significant — it fixes the closure order and therefore the artifact's bytes — so no tool sorts imports.

Elaboration turns surface terms into core terms. It resolves names through the module grammar's visibility rules and inserts nothing the source did not say. It may not decide well-typedness.

Checking is the kernel: inference, definitional equality, quantity accounting, effect rows, totality and positivity. A definition that checks yields a CheckedTerm, which is the only evidence the rest of the pipeline accepts.

Interfaces are what the cache stores: a header, a lazily decoded body, a semantic digest that excludes the source digest, and an integrity digest. Two files that differ only in comments produce the same semantic digest, which is what keeps a comment edit from re-checking the whole cone.

Sealing turns the checked modules into one program: a single main, family uniqueness, and the program term.

Erasure removes everything that is compile-time only. The measured effect is large: 5735 definitions encoding 1.64 MB of core produce an erased program of 536 runtime nodes.

Emission takes one of the two lanes described in docs/compiler/ARCHITECTURE.md. The direct lane additionally verifies its own work: it interprets the lowered control flow and compares the result with the defunctionalized residual before emitting anything.

That self-check has one honest limit, and the certificate records it. A program that READS a file has no compile-time answer to compare against — the interpreter has no file — so for those programs the value comparison is skipped and only the structural verification remains: the x86 verifier decodes and re-encodes every instruction it emitted.

Linking places objects, resolves symbols, applies relocations and rebases source maps. It refuses rather than guessing.

What each step may report#

Every step reports through the same record: a stable ALPHA-* code, an exact span, a message, and optional detail (expected, actual, related spans, fixes). docs/language/DIAGNOSTICS.md lists the codes; the JSON shape is frozen by tests/golden/protocol/diagnostic-v1.json.

Where the pipeline is measured#

alpha profile times a cold check by phase from inside the engine. On the 134-module application closure the split is parse 3158 ms, check 1834 ms, interface 423 ms — parsing dominates a cold check, which is the opposite of the usual assumption and worth re-measuring before optimising the checker again.