[ refactor ] ScopedSnocList: WIP

[GulinSS]

Description

We are going to take again a turn to solve TODO, related to the usage of SnocList at Scope. This change is heavily intrusive and its older attempt was already here.

By suggestion of @buzden we are going to start this heavy change from a very conceptually simple step: collect all usages and mark them. It would help us to schedule further changes at closed volume of overall affected codebase.

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).

[gallais]

I haven't looked at the whole PR but I have tagged a couple of issues.
This is why I was concerned: there's a lot of domain-specific knowledge
in the choice to represent something as a list vs. a snoclist.

[gallais]

It's debatable whether the constructor arguments should be listed right-to-left.
Also they would become the most local variables so the nested case tree would
have a type of the form CaseTree (vars <>< args) rather than args flowing into
the global scope.

[GulinSS]

Left for now as marked as you said it is a debatable question.

[gallais]

appendAssociative is still List-specific

[GulinSS]

Yep, current step is only renaming to mark existing usages of List in context of Scope. No structural changes for current step. Or I didn't get you correctly?

[GulinSS]

Took into consideration @gallais points where I did replacements where it should not be. Also asked @buzden how to determine where such replacements should be and should not be. He suggested to everytime take a look at https://github.com/edwinb/Yaffle/ for reference when I am getting stuck with questions does it should be Snoc or not. Reviewed my progress and changed code according to Yaffle.

@gallais,
@buzden,
much thanks!

I continue my work.

[GulinSS]

Well, I am in progress

229/286: Building Core.Case.CaseBuilder (src/Core/Case/CaseBuilder.idr)

[GulinSS]

It compiles!

The next steps are to

1. group all changes by their semantics
2. groke translate rules from cons to snoc style
3. apply them.

Starting work on the grouping.

[GulinSS]

Stuck tests running. The difference between the commit and main:

% diff tests/build/exec/runtests_app/runtests.ss tests/build/exec/runtests_app/runtests.ss.back
3c3
< ;; @generated by Idris 0.7.0-7098a379f, Chez backend
---
> ;; @generated by Idris 0.7.0-2482ebb43, Chez backend
654,655c654,655
< (define PrimIO-unsafeCreateWorld (lambda (arg-1) (arg-1 )))
< (define PrimIO-unsafePerformIO (lambda (arg-1) (PrimIO-unsafeCreateWorld (lambda (u--w) (let ((eff-0 (arg-1 ))) eff-0)))))
---
> (define PrimIO-unsafeCreateWorld (lambda (arg-1) (arg-1 #f)))
> (define PrimIO-unsafePerformIO (lambda (arg-1) (PrimIO-unsafeCreateWorld (lambda (u--w) (let ((eff-0 (arg-1 u--w))) eff-0)))))
688c688
<   
---
> 

For some reason (arg-1 <X>) writes into (arg-1 ) instead of (arg-1 #f) and (arg-1 u--w). #f and u--w are missed. 🤔

[GulinSS]

Added special inverted operators for current ScopedList. They purpose will be simulate usage of SnocList.

> (1 :%: 2 :%: Lin) +%+ (3 :%: 4 :%: Lin)
1 :%: (2 :%: (3 :%: (4 :%: [<])))
> (Core.Name.ScopedList.Lin :<%: 1 :<%: 2) +<%+ (Core.Name.ScopedList.Lin :<%: 3 :<%: 4)
4 :%: (3 :%: (2 :%: (1 :%: [<])))

[GulinSS]

Closed in favor

• [ refactor ] ScopedSnocList: Preparing for the long jump (Phase 1) #3512
• [ refactor ] ScopedSnocList: Swap Scope on SnocList (Phase 2)  #3513