Document Laurel passes and their dependencies, and other documentation updates

[keyboardDrummer]

Changes

Update Laurel documentation based on inspiration from #1144 and by making the dependencies between passes explicit

Testing

Refactoring, no additional tests needed

[MikaelMayer]

🤖🔍 Good refactoring — extracting pass definitions to their respective modules and making the pipeline declarative is a clear improvement. The comesBefore dependency tracking is a nice addition for documentation generation. A few nits below.

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

[keyboardDrummer]

@keyboardDrummer-bot please resolve merge conflicts

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

[tautschnig]

Restore the computeExprType-based target typing, or add a regression test that pins this narrowed coverage.

Why

This block replaces computeExprType model target (the prior implementation in TypeHierarchy.lean) with a 4-case approximation. computeExprType (LaurelTypes.lean:39) also resolves .AsType casts, .StaticCall/.InstanceCall results, .PureFieldUpdate, .Block, and .IfThenElse; those now fall to .Unknown and are skipped, so (b as Bottom)#xValue and getBottom()#xValue no longer error where they did before this PR.

The narrowing is forced by the move into Resolution.lean: LaurelTypes.lean publicly imports Resolution, so Resolution cannot call computeExprType without a cycle. Either keep validateDiamondFieldAccesses in a module downstream of LaurelTypes and run it as the first pipeline pass, or — if the narrowing is intended — pin it with a test, e.g. extend T5 with a cast target:

b2 := (b as Bottom)#xValue   // errored before this PR; silently accepted now

Either way "refactoring, no additional tests needed" doesn't hold — the set of rejected programs changed.

[keyboardDrummer]

Nice find, thanks. I brought back the original computeExprType model target call.

[tautschnig]

Confirm diamond-access errors should now be suppressed when emitResolutionErrors := false.

Why

Before this PR validateDiamondFieldAccesses ran in runLaurelPasses and its result was added to allDiags unconditionally. Now the errors are folded into ResolutionResult.errors, which the pipeline keeps only via resolutionErrors := if options.emitResolutionErrors then result.errors.toList else [] (LaurelCompilationPipeline.lean:128). The field defaults to true, so in-tree tests are unaffected, but any caller passing false loses diamond diagnostics it previously received. If diamond errors are intended as resolution-phase errors this is fine — worth a line in the PR description.

[keyboardDrummer]

I've removed the emitResolutionErrors option now so it's always true.

[tautschnig]

Add a #guard that laurelPipeline satisfies every declared comesBefore, so reordering can't silently violate a constraint.

Why

comesBefore is consumed only by the doc generator; nothing checks it against the actual order. The line-99 resolution ("whoever reorders and runs into an issue will be prompted") only holds if something prompts them — this is that mechanism, and it also catches a comesBefore target that isn't in the pipeline at all.

/-- Every `comesBefore` constraint is respected by the pipeline order. -/
def comesBeforeRespected : Bool :=
  let names := laurelPipeline.toList.map (·.name)
  laurelPipeline.toList.enum.all fun (i, p) =>
    p.comesBefore.all fun cb =>
      match names.findIdx? (· == cb.pass.name) with
      | some j => i < j
      | none   => false   -- target not in laurelPipeline

#guard comesBeforeRespected

Compare by name since LaurelPass has a function field and thus no DecidableEq. Independent of the String-vs-struct discussion on LaurelPass.lean.

[keyboardDrummer]

I've added the snippet you pasted, thanks.

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

[tautschnig]

Make comesBeforeRespected evaluate at elaboration — this #guard currently fails to build (CI red on both Build and test Lean and Build documentation).

Why + verified fix

#guard runs in the interpreter, which has no IR for the cross-module LaurelPass values laurelPipeline holds:

(interpreter) IR of declaration 'Strata.Laurel.constrainedTypeElimPass' not available;
this may point to a missing `meta` check in a metaprogram

decide gets stuck (kernel can't reduce the Array/String operations) and native_decide hits the same IR gap. Two fixes that build:

• meta import the pass-defining modules in this file (DesugarShortCircuit, MergeAndLiftReturns, EliminateValueInReturns, ModifiesClauses, HeapParameterization, TypeHierarchy, InferHoleTypes, EliminateDeterministicHoles, LiftImperativeExpressions, ConstrainedTypeElim, TypeAliasElim). I verified lake build then succeeds (194 jobs).
• Or move comesBeforeRespected + the #guard into a StrataTest module that does meta import all Strata.Languages.Laurel.LaurelCompilationPipeline (the pattern LiftHolesTest.lean already uses), keeping meta imports out of the core library.

Build documentation fails for the same reason — LaurelDoc.lean imports this module.

[tautschnig]

Remove the now-dead emitResolutionErrors field at LaurelToCoreTranslator.lean:619.

Why

This line was its last reader. After this commit, grep -rn emitResolutionErrors Strata/ matches only the field definition (emitResolutionErrors : Bool := true), so it is dead config.