Skip to content

Track pyspec procedure names for targeted inlining#729

Closed
MikaelMayer wants to merge 18 commits intomainfrom
feat/pyspec-inline-marking
Closed

Track pyspec procedure names for targeted inlining#729
MikaelMayer wants to merge 18 commits intomainfrom
feat/pyspec-inline-marking

Conversation

@MikaelMayer
Copy link
Copy Markdown
Contributor

@MikaelMayer MikaelMayer commented Apr 1, 2026

Track pyspec procedure names for targeted inlining

Previously, pyspec procedure inlining was gated on whether --pyspec flags were passed on the CLI, and when triggered, it inlined all non-main, non-prelude procedures indiscriminately. Tests also had to manually construct the inlining predicate.

This PR tracks which procedure names originate from pyspec files through the pipeline and provides inlinePySpecProcedures so callers don't need to know the inlining details.

Changes

  • PySpecLaurelResult gains a pyspecProcedureNames field, populated during buildPySpecLaurel
  • pyAnalyzeLaurel returns a PyAnalyzeResult struct containing both the Laurel program and the pyspec procedure names
  • inlinePySpecProcedures encapsulates the inlining logic — callers just pass the Core program and the pyspec names
  • Inlining is now automatic (no CLI flag gate) and precise (only pyspec procedures)

Testing

Existing AnalyzeLaurelTest tests pass — these exercise the full pyspec dispatch + inlining + verification pipeline.

PySpec procedures are now explicitly tracked by name through the pipeline
so that inlining targets only pyspec-originating procedures rather than
relying on heuristics (non-main, non-prelude).

- Add pyspecProcedureNames field to PySpecLaurelResult
- Add PyAnalyzeResult struct returned by pyAnalyzeLaurel
- Inlining predicate uses pyspecProcedureNames instead of file count gate
- Update all callers: StrataMain, SimpleAPI, AnalyzeLaurelTest, TestExamples
Callers no longer need to manually construct the inlining predicate.
Both StrataMain and AnalyzeLaurelTest now call inlinePySpecProcedures.
Comment thread StrataMain.lean
Comment thread Strata/SimpleAPI.lean Outdated
Comment thread Strata/Languages/Python/PySpecPipeline.lean
- Prefix unused preludeNames with underscore in StrataMain
- Call inlinePySpecProcedures in pyTranslateLaurel so all pipelines
  get automatic pyspec inlining
- Add clarifying comment on seenProcs fold
@MikaelMayer
Copy link
Copy Markdown
Contributor Author

Addressed all three review comments:

  1. preludeNames unused — renamed to _preludeNames in StrataMain.
  2. pyTranslateLaurel discards pyspec names — now calls inlinePySpecProcedures on the Core result, so all pipelines using pyTranslateLaurel get automatic pyspec inlining.
  3. Clarifying comment on seenProcs fold — added -- Extract procedure names as a set for targeted inlining.

@MikaelMayer
Copy link
Copy Markdown
Contributor Author

This PR is not adding anything significant.

@MikaelMayer MikaelMayer closed this Apr 3, 2026
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