Convert DDM files to Lean 4 modules and fix mkScopedIdent for module support#431
Merged
joehendrix merged 3 commits intomainfrom Feb 17, 2026
Merged
Convert DDM files to Lean 4 modules and fix mkScopedIdent for module support#431joehendrix merged 3 commits intomainfrom
joehendrix merged 3 commits intomainfrom
Conversation
aqjune-aws
approved these changes
Feb 17, 2026
…module support Parse.lean is now a Lean 4 module with public imports and a public section for #strata_gen. The mkScopedIdent function in Gen.lean is updated to handle module files by using mkPrivateName for the pre-resolution hint when not in a public section. Removed duplicate scopedIdent/currScopedIdent/arrayLit definitions from Util/Lean.lean. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Convert all 23 StrataTest/DDM test files to modules, exercising the mkScopedIdent fix across DDM test scenarios. Add public re-exports to Strata.DDM.Integration.Lean so test files need minimal explicit imports. Remove unused atArg from OfAstM. Update #guard_msgs expected output for private name mangling in module context. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…t comments - Rename `hint` to `preresolution` in mkScopedIdent for clarity - Replace direct mkScopedIdent calls with getCategoryOpIdent in toAstIdentM, ofAstIdentM, and createNameIndexMap - Add comments explaining public import vs public meta import distinction - Shorten import comments to stay within 80-char soft limit Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
joehendrix
force-pushed
the
jhx/core_module
branch
from
bd5dd39 to
4d2bbc3
Compare
shigoel
approved these changes
Feb 17, 2026
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 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.
Summary
Enable
#strata_gento work correctly in Lean 4 module files and convert all DDM test files to modules.Details
mkScopedIdentin#strata_genso generated types resolve correctly in module filesStrata.Languages.Core.DDMTransform.Parseand all 23StrataTest/DDM/test files to modulespublic importre-exports toStrata.DDM.Integration.Leanso downstream files need minimal explicit importsatArghelper from OfAstM and unusedStrata.DDM.Util.Lean#guard_msgsexpected output in test files for private name mangling in module contextgetCategoryOpIdenthelper, clarify variable names and commentsBy submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.