Eliminate need for forward type declarations in recursive datatypes

[joehendrix]

Summary

Mutually recursive datatypes previously required users to manually write
forward type declarations before a mutual block. This PR eliminates
that boilerplate by having the elaborator automatically discover and
pre-register type names before elaborating the block's children.

Key changes

• Automatic pre-registration replaces forward declarations. The
  @[preRegisterTypes(scope)] annotation on command_mutual triggers
  two-phase elaboration: Phase 1 partially elaborates each child to
  extract type names and params, then pre-registers them in the
  GlobalContext; Phase 2 elaborates the full block with mutual
  references already resolved.
• GlobalContext simplified. The DeclState enum
  (.forward / .defined) and its bookkeeping are removed. define
  now requires a non-membership proof, making illegal states
  unrepresentable. defineChecked takes a preRegistered flag to
  handle both fresh definitions and pre-registered confirmations.
• Error propagation instead of silent failure.
  extractConstructorInfo and helpers return Except String instead
  of silently returning empty arrays. Template expansion uses an atomic
  buildAndDefine that checks freshness and defines in one step.
• Template expansion validated during elaboration.
  evalBindingSpec's .datatype branch calls expandFunctionTemplates
  to catch constructor and template function name collisions early via
  logError, rather than panicking in addCommand. Constructor names
  are no longer required to be globally unique — only the generated
  template function names must be distinct.
• Elaboration refactors. Extracted elabSyntaxArg, resultContext,
  extractParamNames, and scopeSepFormat from the monolithic
  runSyntaxElaborator. Lifted extractConstructorInfo out of the
  GlobalContext namespace (it only depends on DialectMap).
• O(1) argument lookup via argElabIndex. A precomputed
  Array (Option Nat) maps each argLevel to its position in
  argElaborators, replacing linear searches.
• Translation layer adapted. translateMutualBlock allocates
  placeholder entries on the fly when a datatype isn't already
  pre-registered, rather than requiring forward declarations.

Test changes

• StrataTest/DDM/MutualDatatypes.lean (new): DDM-level test
  dialect with function templates (perConstructor tester,
  perField accessor). Tests mutual block visibility, three-way
  recursion, empty blocks, multi-constructor template expansion, and
  negative cases (undefined type, duplicate type, type clash, duplicate
  constructor name collisions, reused constructor name collisions).
• StrataTest/Languages/Core/Examples/MutualDatatypes.lean (new):
  Core-level integration tests verifying tester functions, accessor
  functions, equality, polymorphic havoc, and complex Stmt/StmtList
  patterns on mutually recursive types.
• StrataTest/Languages/Core/TestASTtoCST.lean (new):
  Round-trip tests for AST-to-CST translation.
• Removed all forward type declarations from existing test files.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[MikaelMayer]

Clean, well-motivated PR that removes a real source of user friction. The two-phase elaboration design in elaborateWithPreRegistration is sound, the GlobalContext simplification is a clear win, and the removal of DeclState/forward declarations is thorough — no dangling references remain.

One minor inconsistency between extractParamNames and the inline code in runSyntaxElaborator (.tvar handling) is worth a look. The rest is solid.

I'd approve after the one question below is addressed.

[MikaelMayer]

extractParamNames matches both .type _ [] _ and .tvar _ _, but the analogous inline code in runSyntaxElaborator (around line 1101) only matches .type _ [] _:

|>.filterMap fun b =>
  match b.kind with
  | .type _ [] _ => some b.ident
  | _ => none

Is the .tvar case intentionally included here but not there? If both should behave the same, consider extracting the shared logic into extractParamNames and calling it from both sites.

[joehendrix]

I've cleaned up this code quite a bit and added additional test cases.