The pipeline's stages, as data.

Lives under Common/ rather than next to the pipeline that runs them (Driver/Pipeline.lean) because two things below the driver need to name a stage without depending on it: the diagnostic registry (Common/Diagnostics/Registry.lean), which records which stage each code comes from, and anything reporting where a compile stopped.

inductive Stage : Type

Where a compile is, or where it stopped. Constructor order is pipeline order — Stage.reaches compares two stages by it.

• read : Stage

  Source text read; nothing compiled yet.

• lex : Stage

  Lexing (Parser_/Tokens).

• parse : Stage

  Parsing (Parser_/TLAPlus.lean).

• annotation : Stage

  @type/@mailbox/@parameter annotation resolution.

• desugar : Stage

  Surface → Core desugaring.

• resolve : Stage

  EXTENDS resolution: locating, and recursively compiling, each dependency.

• typeCheck : Stage

  Type checking (Elaborator).

• wellFormedness : Stage

  The well-formedness restrictions (WellFormedness).

• computable : Stage

  Typed2Computable.

• guarded : Stage

  Computable2Guarded.

• network : Stage

  Guarded2Network.

• go : Stage

  Network2Go, the Go backend.

@[implicit_reducible]

instance instDecidableEqStage : DecidableEq Stage

Equations

• instDecidableEqStage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instReprStage : Repr Stage

Equations

• instReprStage = { reprPrec := instReprStage.repr }

def instReprStage.repr : Stage → ℕ → Std.Format

Equations

• instReprStage.repr Stage.read prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stage.read")).group prec✝
• instReprStage.repr Stage.lex prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stage.lex")).group prec✝
• instReprStage.repr Stage.parse prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stage.parse")).group prec✝
• instReprStage.repr Stage.annotation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stage.annotation")).group prec✝
• instReprStage.repr Stage.desugar prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stage.desugar")).group prec✝
• instReprStage.repr Stage.resolve prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stage.resolve")).group prec✝
• instReprStage.repr Stage.typeCheck prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stage.typeCheck")).group prec✝
• instReprStage.repr Stage.wellFormedness prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stage.wellFormedness")).group prec✝
• instReprStage.repr Stage.computable prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stage.computable")).group prec✝
• instReprStage.repr Stage.guarded prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stage.guarded")).group prec✝
• instReprStage.repr Stage.network prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stage.network")).group prec✝
• instReprStage.repr Stage.go prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stage.go")).group prec✝

@[implicit_reducible]

instance instInhabitedStage : Inhabited Stage

Equations

• instInhabitedStage = { default := instInhabitedStage.default }

def instOrdStage.ord : Stage → Stage → Ordering

Equations

• instOrdStage.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[implicit_reducible]

instance instOrdStage : Ord Stage

Equations

• instOrdStage = { compare := instOrdStage.ord }

def instBEqStage.beq : Stage → Stage → Bool

Equations

• instBEqStage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance instBEqStage : BEq Stage

Equations

• instBEqStage = { beq := instBEqStage.beq }

def Stage.name : Stage → String

The -d dump-<name>/expectation-file spelling of a stage.

Equations

• Stage.read.name = "read"
• Stage.lex.name = "lex"
• Stage.parse.name = "parse"
• Stage.annotation.name = "annotation"
• Stage.desugar.name = "desugar"
• Stage.resolve.name = "resolve"
• Stage.typeCheck.name = "typecheck"
• Stage.wellFormedness.name = "wellformedness"
• Stage.computable.name = "computable"
• Stage.guarded.name = "guarded"
• Stage.network.name = "network"
• Stage.go.name = "go"

@[implicit_reducible]

instance Stage.instToString : ToString Stage

Equations

• Stage.instToString = { toString := Stage.name }

def Stage.artifact? : Stage → Option String

What -d dump-<name> writes out for this stage, and none for a stage with nothing worth writing. Four have nothing: read has only the source text the user already has, resolve produces its dependencies' modules rather than one of its own (each dumps itself as it is compiled), and annotation/wellFormedness transform nothing — they check, and hand their input onward unchanged.

One function rather than a Bool and a separate description because the two answers must agree: fugue help -d lists exactly the stages with an artifact, labelled with what that artifact is. Matched exhaustively on purpose: a stage added later must say what it dumps, rather than defaulting to dumpable and acquiring a -d flag that writes nothing.

Equations

• Stage.read.artifact? = none
• Stage.annotation.artifact? = none
• Stage.resolve.artifact? = none
• Stage.wellFormedness.artifact? = none
• Stage.lex.artifact? = some "the token stream"
• Stage.parse.artifact? = some "the surface AST, annotations still attached"
• Stage.desugar.artifact? = some "the Core AST, annotations resolved into fields"
• Stage.typeCheck.artifact? = some "the typed AST"
• Stage.computable.artifact? = some "the computable fragment"
• Stage.guarded.artifact? = some "Guarded PlusCal"
• Stage.network.artifact? = some "Network PlusCal"
• Stage.go.artifact? = some "the emitted Go"

def Stage.dumpable (s : Stage) : Bool

Does this stage produce an artifact worth writing out?

Equations

• s.dumpable = s.artifact?.isSome

def Stage.dumpOption (s : Stage) : String

The -d dump-<name> option that dumps this stage's artifact. Spelled from name, so the flag, the file it writes (<dump-dir>/<module>-<name>) and the stage a diagnostic reports all use one spelling.

Equations

• s.dumpOption = toString "dump-" ++ toString s.name

def Stage.list : List Stage

Every stage, in pipeline order.

Equations

• One or more equations did not get rendered due to their size.

def Stage.ofName? (s : String) : Option Stage

The stage s names, if it names one.

Equations

• Stage.ofName? s = List.find? (fun (x : Stage) => x.name == s) Stage.list

def Stage.predecessor : Stage → Stage

The stage immediately before s: the last one that must have completed for s to have started. .read is its own predecessor — it is the floor, reached as soon as there is any source text at all.

Equations

• Stage.read.predecessor = Stage.read
• Stage.lex.predecessor = Stage.read
• Stage.parse.predecessor = Stage.lex
• Stage.annotation.predecessor = Stage.parse
• Stage.desugar.predecessor = Stage.annotation
• Stage.resolve.predecessor = Stage.desugar
• Stage.typeCheck.predecessor = Stage.resolve
• Stage.wellFormedness.predecessor = Stage.typeCheck
• Stage.computable.predecessor = Stage.wellFormedness
• Stage.guarded.predecessor = Stage.computable
• Stage.network.predecessor = Stage.guarded
• Stage.go.predecessor = Stage.network

def Stage.reaches (self target : Stage) : Bool

Did a compile that reached self get at least as far as target? A plain Bool function rather than an LE/Decidable instance pair: comparing two stages is a question about pipeline progress, and nothing here wants order-class machinery.

Equations

• self.reaches target = (compare self target != Ordering.lt)