Recursive EXTENDS module resolution — the driver-level orchestration that locates, lexes, parses, desugars, and checks a module, recursing on its own EXTENDS list for each dependency.

compileModule below is the one function that runs a module's source all the way through to a checked module; Fugue.lean's CLI entry point calls it directly for the main module, and resolveModule calls it again, recursively, for every EXTENDS-ed dependency.

class MonadSourceRegistry (m : Type → Type) : Type

Raw module source text by moduleId, so DriverError can carry just the lightweight key rather than duplicating a (possibly large) source string into every thrown error — looked up again only once, at the point an error is finally rendered.

• registerSource : String → String → m Unit
• lookupSource : String → m (Option String)

@[reducible, inline]

abbrev SourceRegistry : Type

The registry itself, as plain data: moduleId ↦ that module's source text.

Equations

• SourceRegistry = Std.HashMap String String

def DriverError.moduleId? : DriverError → Option String

The moduleId a DriverError is tagged with, if any — none for the position-free structural errors (moduleNotFound/ambiguousModule/cyclicExtends), which carry none.

Equations

• (DriverError.lex moduleId e).moduleId? = some moduleId
• (DriverError.parse moduleId e).moduleId? = some moduleId
• (DriverError.annotation moduleId e).moduleId? = some moduleId
• (DriverError.desugar moduleId e).moduleId? = some moduleId
• (DriverError.typeCheck moduleId e).moduleId? = some moduleId
• (DriverError.moduleNameMismatch moduleId declared expected).moduleId? = some moduleId
• (DriverError.moduleNotFound name).moduleId? = none
• (DriverError.ambiguousModule name foundAt).moduleId? = none
• (DriverError.cyclicExtends chain).moduleId? = none

def DriverError.sourceLines (registry : SourceRegistry) (err : DriverError) : Option (List String.Slice)

The source lines to render err's snippet against — the offending module's own, looked up in registry by moduleId, not whichever module the caller started compiling from. none when err carries no moduleId, or the registry has no entry for it; the caller should fall back to rendering against the main module's own lines.

A pure function of the registry rather than an IO action reading a global ref, so rendering a diagnostic needs no IO at all — which is what lets Driver/Pipeline.lean hand a caller finished diagnostic text and lets the regression runner assert on it directly.

Equations

• DriverError.sourceLines registry err = do let moduleId ← err.moduleId? let __do_lift ← Std.HashMap.get? registry moduleId pure (__do_lift.split fun (x : Char) => x == '\n').toList

def DriverWarning.sourceLines (registry : SourceRegistry) (warning : DriverWarning) : Option (List String.Slice)

DriverError.sourceLines's counterpart for warnings, which always carry a moduleId (DriverWarning.moduleId, Driver/Errors.lean).

Equations

• DriverWarning.sourceLines registry warning = do let __do_lift ← Std.HashMap.get? registry warning.moduleId pure (__do_lift.split fun (x : Char) => x == '\n').toList

@[reducible, inline]

abbrev ResolutionStack : Type

Names of modules currently being resolved, outermost first — pushed via withReader (name :: ·) before recursing into a dependency. A module about to be resolved that's already in this list is a cyclic EXTENDS.

Equations

• ResolutionStack = List String

inductive ModuleOutcome : Type

What happened when compileModule/resolveModule finished with a given module name — the payload onModuleEvent reports (Fugue.lean turns this into Built/Replayed/Failed <name>). .failed is reported once a module's own name is known but something past that point failed; lex/parse failures, which happen before a name is known, just surface as the overall compile failure.

• built (hadWarnings : Bool) : ModuleOutcome
• replayed : ModuleOutcome
• failed : ModuleOutcome

structure CacheEntry (β : Type) : Type

The module cache Ξ. Keyed by module name alone, not name-plus-hash: a candidate file's hash isn't known until after it's been located and read, so resolveModule looks up by name first, then compares the returned CacheEntry.sourceHash against the freshly-read file's hash.

• sourceHash : UInt64

  The hash of the source text that produced value.

• extends : List String

  The EXTENDS list recorded when this entry was written — trustworthy without re-parsing since a matching sourceHash means the file is byte-identical to what produced this entry. Lets resolveModule check whether any dependency changed without re-lexing/parsing an unchanged module.

• value : β

  The checked module itself.

class MonadModuleCache (β : outParam Type) (m : Type → Type) : Type

The module cache Ξ's effect interface — lookupModule/storeModule.

• lookupModule : String → m (Option (CacheEntry β))

  The cache entry recorded under this name, if any — unvalidated against any particular file; the caller compares sourceHash itself.

• storeModule : String → CacheEntry β → m Unit

  Cache a checked module under its name.

structure DriverState : Type

Everything one compile mutates as it runs: the fresh-name counter (Common/Fresh.lean), the source registry (for rendering a diagnostic against its own module's lines), and the module cache Ξ. One value per compile, threaded as a real StateT layer rather than a set of global IO.Refs, so concurrent compiles in one process — which is what the regression runner does — are independent, and a compile's fresh names don't depend on what ran before it.

• fresh : ℕ

  MonadFresh's counter.

• sources : SourceRegistry

  Module sources by moduleId.

• cache : Std.HashMap String (CacheEntry TypedModule)

  The module cache Ξ.

@[implicit_reducible]

instance instInhabitedDriverState : Inhabited DriverState

Equations

• instInhabitedDriverState = { default := instInhabitedDriverState.default }

@[implicit_reducible]

instance instMonadFreshOfMonadOfMonadStateOfDriverState {m : Type → Type} [Monad m] [MonadStateOf DriverState m] : MonadFresh m

The compile's fresh-name counter (Common/Fresh.lean).

Equations

• instMonadFreshOfMonadOfMonadStateOfDriverState = { fresh := modifyGet fun (s : DriverState) => (s.fresh, { fresh := s.fresh + 1, sources := s.sources, cache := s.cache }) }

@[implicit_reducible]

instance instMonadSourceRegistryOfMonadOfMonadStateOfDriverState {m : Type → Type} [Monad m] [MonadStateOf DriverState m] : MonadSourceRegistry m

Equations

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

@[implicit_reducible]

instance instMonadModuleCacheTypedModuleOfMonadOfMonadStateOfDriverState {m : Type → Type} [Monad m] [MonadStateOf DriverState m] : MonadModuleCache TypedModule m

Equations

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

@[reducible, inline]

abbrev Base (α : Type) : Type

What M sits on: the compile's flags and its mutable state, under plain IO. The state layer is below DiagT on purpose — StateT above it would discard everything written before a throw, and the source registry has to survive the throw that consults it.

Equations

• Base = ReaderT FlagsEnv (StateT DriverState IO)

@[reducible, inline]

abbrev M (α : Type) : Type

The concrete monad compileModule/resolveModule run at when actually invoked. ResolutionStack is the one genuinely scoped Reader (push-on-recurse, pop-on-return), which is why it sits above DiagT's own DriverWarning/DriverError reporting rather than in Base. compileModule/resolveModule are concrete against this stack, not polymorphic like everything else here: the per-module warning scoping below (runScoped) needs to actually run DiagT's layer down to a plain value, which is only possible against a fixed concrete stack, not an abstract m.

Equations

• M = ReaderT ResolutionStack (DiagT DriverWarning DriverError Base)

def runM {α : Type} (act : M α) : Base (List DriverWarning × Except DriverError α)

Run an M action from the top, with an empty resolution stack — down to Base, not to IO: whoever runs Base owns the compile's flags and state, and everything past this call (the passes after type checking, and rendering the diagnostics against the sources this action registered) still needs both. Driver/Pipeline.lean is that owner.

Equations

• runM act = (ReaderT.run act []).run

@[implicit_reducible]

instance instMonadForeignLookupOfMonadOfMonadModuleCacheTypedModule {m : Type → Type} [Monad m] [MonadModuleCache TypedModule m] : MonadForeignLookup m

MonadForeignLookup's concrete instance (WellFormedness/Monad.lean) — a module's checked declarations by name: a .file hit via the cache Ξ (reachable this way only once a dependency has actually been resolved and cached), falling back to builtinModules[name]? for a builtin. Mirrors locate's own candidate search, minus the not-found/ambiguous error cases — a name reachable via a checked Origin.module name tag has, by construction, already type-checked.

Constrained to MonadModuleCache alone rather than taking the surrounding variable block's whole bundle, so it applies at plain IO too — Ξ is a global IO.Ref, so the lookup needs nothing the driver's own M uniquely has. That is what lets the passes running past the driver (Fugue.lean's checkWellFormed/toComputable calls, against IO) use this instance instead of declaring a second copy of it.

Equations

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

structure ResolvedDep : Type

What compileModule/resolveModule hand back for one module.

inherited is what that module's own EXTENDS list brought into scope, each entry already tagged with the module that declared it, and bindings below appends the module's own declarations to it — so EXTENDS is transitive, and identically so for a builtin and for a .tla file on disk. Neither field is a choice a construction site gets to make: there is no way to build a ResolvedDep that exports its own declarations but not its dependencies'.

The inherited entries are carried here rather than recomputed by the caller from mod's declaration list because a re-exported declaration is indistinguishable from an own one inside a List Decl: a caller folding Decl.bindings over a merged list has no name to tag with but the re-exporting module's, and would attribute Naturals's < to whichever of Sequences/ Integers/FiniteSets/Bags/user module it arrived through. Origin is what TypedTLAPlus.builtinOpOf? and Network2Go.compileBuiltinCall dispatch on, so that misattribution is not cosmetic: it makes a builtin uncompilable.

• recomputed : Bool

  Whether this module was recomputed just now (as opposed to replayed from Ξ or read out of the builtin table) — threaded up so a dependent can tell whether it must recompute in turn.

• mod : TypedModule

  The checked module itself, exactly as its own compile (or the builtin table) produced it — dependency declarations never spliced in, so it agrees with what MonadForeignLookup.lookupForeign answers for the same name.

• inherited : List (String × Binding)

  Everything mod's own EXTENDS list brings into scope, each entry origin-tagged by its declaring module.

@[implicit_reducible]

instance instInhabitedResolvedDep : Inhabited ResolvedDep

Equations

• instInhabitedResolvedDep = { default := instInhabitedResolvedDep.default }

def ResolvedDep.bindings (dep : ResolvedDep) : List (String × Binding)

Every binding this module brings into scope: what it inherited through EXTENDS, then its own declarations. Order is what makes an own declaration shadow an inherited one of the same name, since compileModule folds this list into Γ₀ with insert.

Equations

• dep.bindings = dep.inherited ++ TypedModule.ownBindings✝ dep.mod

partial def compileModule (source : String) (containingDir : Option System.FilePath) (moduleId : String) (expectedName : Option String := none) (isRoot : Bool := false) (onModuleEvent : String → ModuleOutcome → M Unit := fun (x : String) (x_1 : ModuleOutcome) => pure ()) (onModuleProgress : String → M Unit := fun (x : String) => pure ()) (logLine : String → M Unit := fun (s : String) => liftM (IO.eprintln s)) : M ResolvedDep

Run a module's source all the way through to a checked module: lex, parse, resolve annotations, desugar TLA⁺ expressions and the embedded PlusCal algorithm, resolve every EXTENDS-ed dependency (resolveModule, recursing into compileModule for anything not already satisfied by the cache or a builtin), merge their exported declarations into an initial Γ, and check.

onModuleProgress name fires twice: once as soon as name is known (right after parsing), and again once its EXTENDS dependencies finish resolving, to refocus display back onto this module once its dependencies are no longer "current".

onModuleEvent name .built fires once this module is fully checked, .failed if its own processing throws — the one place either is reported for this module (a dependency's own outcome is reported inside its own recursive compileModule call, never duplicated here).

moduleId is the registry key DriverError's variants tag themselves with, registered against source before lexing runs. For a dependency this is the EXTENDS-requested name; for the main module it's whatever identifier Fugue.lean passes.

isRoot marks the compile's own module, as opposed to an EXTENDS-ed dependency, and suppresses its .built: type checking is where a dependency is finished, but the root goes on through every pass past the driver, so reporting it built here would claim success for a compile that can still fail. Driver/Pipeline.lean reports the root's outcome once it knows it. .failed is not suppressed — a driver failure ends the compile there, so it is already the final word.

Returns a ResolvedDep rather than the bare TypedModule because the bindings this module's EXTENDS list brought in are known only here, and a dependent needs them to re-export them in turn (ResolvedDep.bindings). recomputed is always true: reaching this function is what being recomputed means. A caller that only wants the module itself — Driver/Pipeline.lean, for the root — takes .mod.

partial def resolveModule (containingDir : Option System.FilePath) (name : String) (onModuleEvent : String → ModuleOutcome → M Unit := fun (x : String) (x_1 : ModuleOutcome) => pure ()) (onModuleProgress : String → M Unit := fun (x : String) => pure ()) (logLine : String → M Unit := fun (s : String) => liftM (IO.eprintln s)) : M ResolvedDep

The EXTENDS-specific wrapper around compileModule: locate name (locate above, error on not-found/ambiguous), check Ξ, and recompute if name's source changed or anything it transitively depends on changed. The returned ResolvedDep carries the checked module, the bindings it brings into scope, and whether it was actually recomputed just now — the last threaded up so its dependents can tell whether they need to recompute in turn.

Fires onModuleEvent name .replayed on the one path that never touches compileModule (a cache hit with nothing changed); every other outcome is reported by whichever compileModule call this makes. Not for .builtin, which is static. onModuleProgress name fires once, at the top of the .file case.

EXTENDS is transitive, for a builtin and for a .tla file alike: every path here supplies ResolvedDep.inherited, and ResolvedDep.bindings puts it ahead of the module's own bindings, so a later own declaration still shadows an inherited one of the same name. Each inherited binding keeps the Origin its declaring module gave it — Naturals's < stays Naturals!< whether it is reached through EXTENDS Sequences or through a user module that EXTENDS Naturals itself.

On the one path that replays a cached module without recompiling it, inherited is rebuilt from the dependency resolutions the cache check already had to perform for change detection: nothing recompiles, and by that check's own conclusion — no dependency recomputed — those bindings are what the cached module was compiled against.