[ refactor ] move parser into Idris#3652
Draft
wizard7377 wants to merge 1 commit intoidris-lang:mainfrom
Draft
Conversation
Author
|
This is currently failing due to pack having a internal dependency on Idris file structure, so this should be pulled before the pack pr |
Collaborator
|
It looks like it also breaks idris2-lsp and katla. |
This was referenced Oct 16, 2025
Author
Fixed! |
Member
|
I'm not sure I see the point of this type of PR:
all in the name of "improv[ing] readability", a subjective outcome? We have fairly limited people power (with e.g. much higher priority structural PRs |
Author
|
Made some updates to the description |
Contributor
|
Working on #3513 to move forward with coming updates |
Author
Agreeed |
Contributor
|
#3513 is ready for review and merge. |
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
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.
Description
Currently, the Idris 2 parser is split into three places
src/Libraries/Textwhich defines the core parsing environment (independent of the Idris syntax)src/Parser, which defines part of the Idris syntaxsrc/Idris/Parser.idrandsrc/Idris/Parser/Let.idr, which define the rest of the parser (and the final general parsing methods)The last two of these seem like they should be in the same place, preferably in
src/Idris/Parser, as they are Idris front-end components. So, as a part of #3369, this is intended to make the parser organization more understandable for new contributors, as well as new syntaxParser.*toIdris.Parser.Core.*src/Idris/Parser/Basic.idrintosrc/Idris/Parser/Source.idrsrc/Idris/Parser/Repl.idr, and makessrc/Idris/Parser.idrre-exports all of them.Ultimately, this means that the directory
src/Idris/Parsercontains all of the Idris specific parser code, and also splits up the parser to be less large (granted,src/Idris/Parser/Source.idris still nearly 2000 lines long, butsrc/Idris/Parser.idrwas nearly 3000 lines long).Apart from this the changes include:
src/Idris/Parser/Basic.idrandsrc/Idris/Parser/Source.idrthat are used in one of the other files (as they are now separate)While refactors are annoying to deal with and take up time, I believe that this, given its simplicity (almost everything is just copy pasted from one file to another), is worth the time.
I might note that this starts with the following:
Self-check
CONTRIBUTING.mdand I've updated
CONTRIBUTORS.mdwith my name.implementation, I have updated
CHANGELOG_NEXT.md