Skip to content

Conversation

@wizard7377
Copy link

@wizard7377 wizard7377 commented Oct 15, 2025

Description

Currently, the Idris 2 parser is split into three places

  1. src/Libraries/Text which defines the core parsing environment (independent of the Idris syntax)
  2. src/Parser, which defines part of the Idris syntax
  3. src/Idris/Parser.idr and src/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 syntax

  1. Moves Parser.* to Idris.Parser.Core.*
  2. Splits up src/Idris/Parser/Basic.idr into src/Idris/Parser/Source.idr src/Idris/Parser/Repl.idr, and makes src/Idris/Parser.idr re-exports all of them.

Ultimately, this means that the directory src/Idris/Parser contains all of the Idris specific parser code, and also splits up the parser to be less large (granted, src/Idris/Parser/Source.idr is still nearly 2000 lines long, but src/Idris/Parser.idr was nearly 3000 lines long).

Apart from this the changes include:

  • Exporting some things from src/Idris/Parser/Basic.idr and src/Idris/Parser/Source.idr that are used in one of the other files (as they are now separate)
  • Changing all the imports of these modules to have the correct names

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:

[epistemic status: Not very confident on a lot of this. High level should be ok, but lot of details could be wrong]

So the idris2 repo has a lot of parsers, and I spent the last few weeks being confused by which is which. After a lot of grepping, I think this is where they all are and their general purpose. This is mostly just notes from what I found when rewriting the idrall parser, but maybe it’s useful to others.

Self-check

  • This is my first time contributing, I've carefully read CONTRIBUTING.md
    and I've updated CONTRIBUTORS.md with my name.
  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG_NEXT.md

@wizard7377
Copy link
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

@dunhamsteve
Copy link
Collaborator

It looks like it also breaks idris2-lsp and katla.

@wizard7377
Copy link
Author

It looks like it also breaks idris2-lsp and katla.

Fixed!

@wizard7377 wizard7377 changed the title internal: move parser into Idris [ internal ] move parser into Idris Oct 16, 2025
@gallais
Copy link
Member

gallais commented Oct 17, 2025

I'm not sure I see the point of this type of PR:

  • it touches a lot of files which makes reviewing involved
  • it breaks downstream projects which makes deployment complex
  • it breaks everyone's current mental map of what is where

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
opened since March #3513 and not yet fully
merged in) and I'm not sure this kind of shuffling around of things is worth it tbh.

@wizard7377 wizard7377 changed the title [ internal ] move parser into Idris [ refactor ] move parser into Idris Oct 17, 2025
@wizard7377
Copy link
Author

Made some updates to the description

@GulinSS
Copy link
Contributor

GulinSS commented Oct 31, 2025

Working on #3513 to move forward with coming updates

@wizard7377
Copy link
Author

Working on #3513 to move forward with coming updates

Agreeed

@wizard7377 wizard7377 marked this pull request as draft October 31, 2025 19:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants