Convert Python Specs to Lean 4.27 modules #400
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
joehendrix
force-pushed
the
jhx/python_modules
branch
from
8f0a382 to
a354f75
Compare
MikaelMayer
previously approved these changes
Feb 10, 2026
joehendrix
force-pushed
the
jhx/python_modules
branch
from
6cb95c6 to
05fa18a
Compare
Converts the Python specifications infrastructure to use Lean 4.27's module system instead of namespace-based organization: - Add module keyword and public sections to all Python Specs files - Mark keyword helper functions with @[expose] for visibility - Use import all for Fin utilities to access Fin.range - Add necessary imports for generated dialect code (OfAstM, BoolConv, etc.) Files converted: - Strata/Languages/Python/PythonDialect.lean - Strata/Languages/Python/ReadPython.lean - Strata/Languages/Python/Specs/DDM.lean - Strata/Languages/Python/Specs.lean Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
Mark internal implementation details as private to reduce the public API surface: ReadPython.lean: - readPythonStrataBytes: Internal helper for reading Ion format - formatParseFailureStderr: Internal error formatting helper Specs/DDM.lean: - All toDDM/fromDDM conversion functions: Internal serialization helpers - toDDMInt, DDM.Int.ofDDM: Internal type conversion utilities These functions are implementation details not intended for external use. Public APIs (pythonToStrata, readPythonStrata, readDDM, writeDDM, toDDMProgram) remain accessible. Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
Privacy improvements: - Type translation helpers: pySpecType, pySpecValue, pyKeywordValue - Argument processing: pySpecArg, pyDefaultValue - Value translation: translateConstant, translateSubscript, translateDictKey, translateCall - Type translators: fixedTranslator, unionTranslator, literalTranslator, metadataProcessor - Type utilities: valueAsType, checkEq - State management: getNameValue?, setNameValue, recordTypeDef, recordTypeRef - Signature management: pushSignature, pushSignatures Changed PySpecMClass from export to open to reduce exported surface. Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
With the change from export to open for PySpecMClass, several more internal helper functions can now be marked private: - transPred: Internal predicate translation helper - logEvent: Internal logging utility - ModuleName.ofStringAux: Internal parser helper - Pred.not: Internal predicate negation helper All functions are only used within the module implementation. Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
Major refactoring to use module-level privacy by default: Import changes: - Removed public section wrapper - Changed most public imports to regular imports - Only re-export necessary types: Lean.Data.Position, Std.Data.HashSet.Basic, Strata.DDM.Util.SourceRange, and Strata.Languages.Python.Specs.Decls Public API (explicitly marked): - Types: EventType, SpecError, ModuleName, FileMaps - Functions: ModuleName.ofString, ModuleName.strataFileName, translateFile, translateModule - Re-exported from DDM: readDDM, writeDDM, toDDMProgram (via Specs.DDM import) All other declarations (100+) are now implicitly private, including: - Internal helper functions (logEvent, transPred, pySpecValue, etc.) - Type translators (fixedTranslator, unionTranslator, literalTranslator) - State management (PySpecM, PySpecMClass, getNameValue?, setNameValue) - Translation helpers (translate, translateModuleAux, resolveModule) This drastically reduces the exported API surface while maintaining all necessary functionality for external consumers (StrataMain, tests). Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
BoolConv.lean was consolidated into OfAstM.lean in main branch. Since we already import OfAstM, the BoolConv import is no longer needed.
joehendrix
force-pushed
the
jhx/python_modules
branch
from
3b4b671 to
adc738d
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Converts Python/Specs files to use Lean 4.27 module system.
Files converted
PythonDialect.lean: Added@[expose]tokeyword.valueReadPython.lean: Marked helpers privateSpecs/DDM.lean: Added docstringsSpecs.lean: Marked public API explicitly (8 items below)Public API of Specs.lean
Types:
EventType,SpecError,ModuleName,FileMapsFunctions:
ofString,strataFileName,translateFile,translateModuleBy submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.