Replace empty module name strings with validated ModuleName type

[joehendrix]

Summary

PythonIdent.pythonModule was a raw String, allowing empty module names to propagate silently through the system and cause downstream failures (see #1143). This PR changes pythonModule to use ModuleName — which now guarantees at least one non-empty component — and adopts it more widely through the PySpec pipeline, eliminating this class of bugs at the type level.

Approach

Rather than adding runtime checks at each use site, ModuleName gains a strengthened invariant via a private constructor enforcing non-empty components. PythonIdent.ofComponent uses decide to verify non-emptiness at compile time for literal module names (used in Decls.lean). Runtime parsing goes through ModuleName.ofString? which returns Option.

Key changes

• PythonIdent.lean: PythonIdent.pythonModule changed from String to ModuleName. New ofComponent constructor with compile-time proof for single-component literals. ModuleName API extended: back, parent (n), push, append/++, toString (sep)
• PythonIdent.lean: New ModuleName.ofRelativePath provides a single canonical function for deriving a ModuleName from a .py file path relative to a search root, handling both regular files and __init__.py packages. This eliminates redundant ad-hoc implementations scattered across discoverModules, RelativeImportTest, and findInPath — each of which had slightly different __init__.py handling, creating inconsistency and latent bugs (e.g., pySpecToLaurelCommand silently failed for package modules)
• Specs.lean: findInPath simplified to return (FilePath × Bool) instead of (FilePath × Array ModuleComponent) — the Bool is isInit, and callers use ModuleOfPath.modulePrefix to derive the package prefix. Deleted unused ofFile function
• Specs/DDM.lean: Converted fromDDM functions to monadic FromDDM (Except (SourceRange × String)) for proper error propagation instead of panics
• Specs/ToLaurel.lean: signaturesToLaurel takes ModuleName instead of String prefix. Overload extraction factored into dedicated ExtractM monad (no dependency on ToLaurelContext)
• PySpecPipeline.lean: buildPySpecLaurel takes Array (ModuleName × String) instead of Array (String × String)
• Specs.lean: Import resolution uses ModuleName throughout; translateFile requires a ModuleName (no longer optional)
• Specs/Decls.lean: Builtin idents use ofComponent with compile-time proof

Unrelated cleanup

• Deleted Strata.Python.containsSubstr helper and replaced all call sites with String.contains (which accepts substring patterns in Lean 4.29)

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

[MikaelMayer]

🤖🔍 Well-designed PR that eliminates a class of bugs at the type level. The ModuleName invariant is clean, ofRelativePath consolidates scattered logic, and the FromDDM monad properly replaces panic! with structured errors. A few issues below.

[MikaelMayer]

🤖🔍 None of the 7 previous review comments have been addressed — the latest commits all predate the review. Specifically:

1. PythonIdent.lean:77 — still missing s! prefix in panic! message
2. PythonIdent.lean:117 — typo Stata still present (should be Strata)
3. DDM.lean:357 — still missing s! prefix in .throw string
4. Decls.lean:112 — SpecType.ofComponent still not renamed back to mk
5. ToLaurel.lean:201-202 — stale docstring still says "Returns the name unchanged if the prefix is empty"
6. ToLaurel.lean:10,16 — duplicate OverloadTable import still present
7. Specs.lean:25 — since := "FIXME" placeholder still present

[MikaelMayer]

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

[tautschnig]

Nothing fundamentally blocking, but a couple of suggestions that would seem like genuine improvements.

[MikaelMayer]

🤖🔍 All actionable comments from tautschnig's review are addressed in commit 225b37b:

• ✅ ofRelativePath now uses System.FilePath.components (portability fix)
• ✅ Warning restored in SimpleAPI.lean (behavior regression fixed)
• ✅ extractFunctionSignatures takes ModuleName directly, dead isEmpty branch removed
• ✅ pushOverloadEntry cleaned up: match replaces .get!, extractError .overloadParamDisagree replaces dbg_trace, branches deduplicated
• ✅ modulePrefix? added and call site simplified in Specs.lean
• ✅ #guard cases added for round-trips, back, append, and parent

Items explicitly declined by author (with justification): Inhabited instance removal, back refactoring, parent rename. These are design choices for the reviewer to accept or push back on.

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.

[MikaelMayer]

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