[ refactor ] ScopedSnocList: Swap `Scope` on `SnocList` (Phase 2) #3513

GulinSS · 2025-03-19T10:13:51Z

Introduces the actual swap of List on SnocList for Scope.

Should this change go in the CHANGELOG?

If this is a fix, user-facing change, a compiler change, or a new paper
implementation, I have updated CHANGELOG_NEXT.md (and potentially also
CONTRIBUTORS.md).

GulinSS · 2025-03-25T19:03:32Z

@spcfox prepared a report of building packages.

TLDR; all builds reached complete step of compilation. 🎉

GulinSS · 2025-06-05T08:05:56Z

@mjustus
@gallais

Kindly asking for the review! 🙏

gallais · 2025-06-05T09:00:53Z

Be aware that it may take a while!

Next week is the TYPES conference
The week after that is the CALCO/MFPS joint conferences

We may be able to meet after that but then annual leave may kick in (I'll be away late June to early July).

GulinSS · 2025-07-22T07:49:59Z

@gallais a reminder at the middle/end of July probably after annual leave

gallais · 2025-07-29T10:39:25Z

We're meeting tomorrow for a first go at this PR.

GulinSS · 2025-08-08T12:49:27Z

@gallais
@mjustus

should we solve these conflicts or better wait the review?

mjustus · 2025-08-08T13:20:09Z

I think solving merge conflicts later is the better approach. We tend to do some refactoring during review (e.g. PR #3593) when we spot opportunities that are too tempting to ignore but those shouldn't be too difficult to merge. I am sure Guillaume and I can help resolving conflicts once we are done reviewing.

EDIT: wrong PR number.

GulinSS · 2025-08-19T18:12:31Z

hm, I've tried to track the changes but this commit is unclear for me. Could you put more info there?

@gallais
@mjustus

gallais · 2025-08-20T09:08:39Z

That last one is ongoing changes that are not thematically linked beyond being part of the review as a whole.
We reset the commit before each new session, moving pure refactoring commits past it and then add it back
on with all the stuff we've accumulated during the day to it.

GulinSS · 2025-08-26T10:26:40Z

@gallais
@mjustus

FYI Not-so-trivial rebase may occur here

spcfox · 2025-08-26T11:35:02Z

FYI Not-so-trivial rebase may occur here

I can help with that

GulinSS · 2025-09-04T10:18:26Z

@gallais
@mjustus

Might be better to merge current refactor progress "as is"?

gallais · 2025-09-04T10:20:01Z

The new academic year is about to start so unfortunately I don't think I'll be able to come back to this for a while.

GulinSS · 2025-09-04T12:56:39Z

The new academic year is about to start so unfortunately I don't think I'll be able to come back to this for a while.

I mean I could take the branch, make a rebase, and finally propose all these changes to merge at this pr. What do you think?

GulinSS · 2025-10-31T10:27:16Z

I've collected commits from mjustus@3578f70, then added holes to make it compilable as is to see the needed surface to fix. Applied trivial fixes. Working on filling holes.

GulinSS · 2025-11-05T08:51:15Z

@mjustus
@gallais

I've rolled out your refactor intentions over the full codebase and now it compiles just fine, see CI. Actually it only compiles now, not work. My next steps are focused on coming back the working state.

Howbeit I noted that your refactor ideas are a very delicious and at same time pretty accurate. I think while I am busy on coming back working state (that's why I moved this issue to Draft state again) it would be perfect if you would come with more.

I know your time is limited but the deal is to get more your ideas and implement them by my hands as I can.

cc @buzden

Co-authored-by: Justus Matthiesen <[email protected]>

+ Cherry-picked refactor from #16 Co-authored-by: Viktor Yudov <[email protected]>

…sing cases to substName

… List Name This refactor changes the representation of constructor arguments throughout the compiler from `Scope` to `List Name`. This simplifies the API and reduces complexity in handling variable indices. Key changes: - Updated `MkConAlt` and related types to use `List Name` instead of `Scope` for constructor arguments - Modified variable binding and weakening operations to work with list-based arguments - Adjusted pattern matching and case analysis code throughout the compiler - Added new helper functions for list-based variable operations The change affects multiple compiler modules including ANF, LambdaLift, CaseOpts, and optimization passes, ensuring consistent handling of constructor arguments across the compilation pipeline.

GulinSS · 2025-11-27T12:21:40Z

Short list of all test errors ATM:

idris2/basic/basic055
base/data_bits001
contrib/list_alternating
chez/channels008
chez/chez004
chez/integers
chez/chez032
chez/chez027
refc/buffer
refc/integers
refc/strings
node/node024
node/node004
node/integers

Unfortunately, I am unable to reproduce them locally.
crush.Dockerfile.txt

But locally my list of bad tests are:

chez/channels009
chez/channels008
chez/futures001

Continue digging.

Co-authored-by: Viktor Yudov <[email protected]>

GulinSS mentioned this pull request Mar 19, 2025

[ refactor ] ScopedSnocList: WIP #3368

Closed

1 task

GulinSS force-pushed the scoped-snoc-list-swap branch from 2a9fa0b to b68532b Compare March 24, 2025 17:15

GulinSS mentioned this pull request Mar 25, 2025

[ refactor ] ScopedSnocList: Swap Scope on SnocList (idris2-lsp part) idris-community/idris2-lsp#242

Open

GulinSS mentioned this pull request Apr 3, 2025

[ refactor ] ScopedSnocList: Preparing for the long jump (Phase 1) #3512

Merged

GulinSS force-pushed the scoped-snoc-list-swap branch 4 times, most recently from bed6788 to ff61ad5 Compare April 21, 2025 13:29

GulinSS force-pushed the scoped-snoc-list-swap branch from ff61ad5 to 9367788 Compare May 12, 2025 11:42

GulinSS force-pushed the scoped-snoc-list-swap branch from 9367788 to 5278b55 Compare June 3, 2025 07:20

GulinSS marked this pull request as ready for review June 3, 2025 07:22

GulinSS force-pushed the scoped-snoc-list-swap branch from 33f2799 to 749fa54 Compare June 5, 2025 07:16

GulinSS force-pushed the scoped-snoc-list-swap branch from 749fa54 to c128cdf Compare July 8, 2025 07:25

GulinSS force-pushed the scoped-snoc-list-swap branch from c128cdf to cf57ff6 Compare July 17, 2025 13:45

gallais mentioned this pull request Oct 17, 2025

[ refactor ] move parser into Idris #3652

Draft

2 tasks

GulinSS force-pushed the scoped-snoc-list-swap branch 2 times, most recently from 9b903ec to edbdf25 Compare November 4, 2025 17:11

GulinSS marked this pull request as draft November 5, 2025 08:51

GulinSS force-pushed the scoped-snoc-list-swap branch 5 times, most recently from e01b32a to dde0bf4 Compare November 16, 2025 11:14

spcfox mentioned this pull request Nov 18, 2025

[ cleanup ] Remove redundant imports and some minor changes #3681

Merged

2 tasks

GulinSS force-pushed the scoped-snoc-list-swap branch from f7ed03c to 0c882af Compare November 21, 2025 23:17

GulinSS and others added 12 commits November 25, 2025 20:41

[ refactor ] replace showSep and join by Data.String.joinBy

47a9081

Co-authored-by: Justus Matthiesen <[email protected]>

[ refactor ] ScopedSnocList: Swap Scope on SnocList (Phase 2)

c119d1c

+ Cherry-picked refactor from #16 Co-authored-by: Viktor Yudov <[email protected]>

[ refactor ] NatSet: correct indexing logic

333d74d

[ refactor ] generalised lookup

4c3f1c5

[ refactor ] define resolveRef as the weakening of findBound, add mis…

d6b2a04

…sing cases to substName

[ refactor ] define underBinders, fix argument order

1e58106

[ refactor ] added underBinderz, more GenWeakenable instances

0520775

[ refactor ] complete refactors regarding swapping inner/outer

a118f1a

[ refactor ] fix test regression

33840b7

[ refactor ] fix test regression

9161a97

[ refactor ] fix import regression

5b57541

GulinSS force-pushed the scoped-snoc-list-swap branch from f77ebd4 to 5b57541 Compare November 26, 2025 09:01

GulinSS and others added 3 commits December 1, 2025 22:38

[ refactor ] remove useless toLists

c49a2c4

[ refactor ] reverse variable usage initialization logic

4bdbf2f

[ libs, tmp ] Add 1 minute timeout in Golden

2b055b7

Co-authored-by: Viktor Yudov <[email protected]>

GulinSS force-pushed the scoped-snoc-list-swap branch from de1736f to 2b055b7 Compare December 1, 2025 19:40

[ refactor ] ScopedSnocList: Swap Scope on SnocList (Phase 2) #3513

Are you sure you want to change the base?

[ refactor ] ScopedSnocList: Swap Scope on SnocList (Phase 2) #3513

Uh oh!

Conversation

GulinSS commented Mar 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Should this change go in the CHANGELOG?

Uh oh!

GulinSS commented Mar 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

GulinSS commented Jun 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

gallais commented Jun 5, 2025

Uh oh!

GulinSS commented Jul 22, 2025

Uh oh!

gallais commented Jul 29, 2025

Uh oh!

GulinSS commented Aug 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mjustus commented Aug 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

GulinSS commented Aug 19, 2025

Uh oh!

gallais commented Aug 20, 2025

Uh oh!

GulinSS commented Aug 26, 2025

Uh oh!

spcfox commented Aug 26, 2025

Uh oh!

GulinSS commented Sep 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

gallais commented Sep 4, 2025

Uh oh!

GulinSS commented Sep 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

GulinSS commented Oct 31, 2025

Uh oh!

GulinSS commented Nov 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

GulinSS commented Nov 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

[ refactor ] ScopedSnocList: Swap `Scope` on `SnocList` (Phase 2) #3513

[ refactor ] ScopedSnocList: Swap `Scope` on `SnocList` (Phase 2) #3513

GulinSS commented Mar 19, 2025 •

edited

Loading

GulinSS commented Mar 25, 2025 •

edited

Loading

GulinSS commented Jun 5, 2025 •

edited

Loading

GulinSS commented Aug 8, 2025 •

edited

Loading

mjustus commented Aug 8, 2025 •

edited

Loading

GulinSS commented Sep 4, 2025 •

edited

Loading

GulinSS commented Sep 4, 2025 •

edited

Loading

GulinSS commented Nov 5, 2025 •

edited

Loading