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

[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 :%: [<])))