Skip to content

Move PythonIdent and OverloadTable to Strata.Languages.Python#643

Open
joehendrix wants to merge 1 commit intomainfrom
jhx/move_overload_table
Open

Move PythonIdent and OverloadTable to Strata.Languages.Python#643
joehendrix wants to merge 1 commit intomainfrom
jhx/move_overload_table

Conversation

@joehendrix
Copy link
Contributor

Move PythonIdent, FunctionOverloads, and OverloadTable out of the Specs sub-namespace into Strata.Python so they can be shared across the Python pipeline without requiring a Specs dependency. This is a prerequisite for upcoming work to establish a cleaner API boundary for the Python pipeline.

  • Create Strata/Languages/Python/OverloadTable.lean as the canonical home for PythonIdent, FunctionOverloads, and OverloadTable, all in the Strata.Python namespace.
  • Remove duplicate definitions from Specs/Decls.lean (PythonIdent) and Specs/ToLaurel.lean (FunctionOverloads, OverloadTable); both now re-export from the new module.
  • Delete Specs/OverloadTable.lean since its contents are fully superseded by the new module.
  • Move PythonIdent.toDDM in Specs/DDM.lean into the Strata.Python namespace to match the type's new home.
  • Make Strata.Util.DecideProp a private import in Specs/ToLaurel.lean (it is an implementation detail) and add explicit imports in PythonToLaurel.lean and PySpecPipeline.lean which need it directly.
  • Update all open statements and qualified references across the codebase (IdentifyOverloads.lean, PythonToLaurel.lean, PySpecPipeline.lean, SimpleAPI.lean, IdentifyOverloadsTest.lean).

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

Lift PythonIdent, FunctionOverloads, and OverloadTable out of the
Specs sub-namespace into Strata.Python so they can be shared across
the Python pipeline without requiring a Specs dependency.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@joehendrix joehendrix force-pushed the jhx/move_overload_table branch from e5907c2 to 60b2612 Compare March 24, 2026 06:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant