Skip to content

Method refactor#3619

Merged
dunhamsteve merged 3 commits into
idris-lang:mainfrom
andrevidela:method-refactor
Aug 20, 2025
Merged

Method refactor#3619
dunhamsteve merged 3 commits into
idris-lang:mainfrom
andrevidela:method-refactor

Conversation

@andrevidela
Copy link
Copy Markdown
Collaborator

Description

Prerequisite for #3615

  • replace Method
  • harmonise and merge Signature and Declaration
  • replace (String, Name) by WithData [Doc', FC'] Name

Copy link
Copy Markdown
Member

@mattpolzin mattpolzin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks like there are some places where you've chosen val . name or .name.val over .nameVal -- I'm guessing that was arbitrary and it may make sense to refactor to use the helper everywhere it is applicable. Not a big deal to me though.

@andrevidela
Copy link
Copy Markdown
Collaborator Author

the nameVal helper was actually a necessary change because.name.val was too complicated to disambiguate in the cases where .nameVal is present.
I'm not sure what to make of this in that I don't think it makes sense to change all the instances of .name.val but I also don't feel like .nameVal should even be necessary

Copy link
Copy Markdown
Member

@mattpolzin mattpolzin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The changes look sane to me, but ideally this PR is left open a bit longer in case someone with more experience with the compiler internals than me sees something that could regress performance or be a breaking change downstream.

Copy link
Copy Markdown
Collaborator

@dunhamsteve dunhamsteve left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me.

@dunhamsteve dunhamsteve merged commit 1ffbc7e into idris-lang:main Aug 20, 2025
22 checks passed
@andrevidela andrevidela mentioned this pull request Aug 20, 2025
14 tasks
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.

3 participants