Preserve orders of symbols in scope

[timsueberkrueb]

For the holes panel, based on our own experiments and feedback from @jiribenes, I propose to display the bound names in the order they were defined in. I.e., if you have the program

def foo(x: Int, y: Int, z: Int) = {
  val boo = "whatever"

  def bar(a: Int, b: Int) = <>

  val quack = "whatever"
}

I would expect the holes panel to display the context as follows:

--- Local scope (bar) ---

a: Int
b: Int

--- Local scope (foo) ---

x: Int
y: Int
z: Int
boo: String
quack: String

--- Global scope ---

...

In particular, within a scope, the variables are ordered as they were defined, rather than displayed in an arbitrary order (as they are now).

Based on the discussion in the last Effekt meeting, it is not clear if:

1. We want to preserve the order at all (I think it is important)
2. If so, how to implement it (at the moment, Scope does not preserve the order at all)

For point (1), I checked prior work:

• VSCoq preserves the order of definitions in the goals panel
• Lean (web demo) preserves the order of definitions in the goals panel

Based on user feedback so far and prior work it seems sensible not to present the terms in an arbitrary order. Of course, we can in the future experiment with other semantic orderings.

If you agree, I would like some feedback on how this should be implemented. The code currently contained in this PR is just a proof of concept, it is not the final code I would find acceptable.

Depends on #1029.

[b-studios]

I like this behavior! How to implement it is a different question.

We are again in this state where we have two seemingly orthogonal set of constraints.

1. batch compilation should be fast (and the compiler should be simple)
2. editor services might require some info, so we need to maintain it

Just some random observations:

• right now we only ever need this info whenever there is a hole (we could however also use it later at a cursor position).
• in other places we spam the annotations DB with additional info

Right now it looks like you could use a custom "OrderedMap" as a drop-in replacement (like https://scastie.scala-lang.org/eHJNORkYRGKoBnrCIIAtqQ).

However, I don't understand why you keep a list of Strings and not a list of symbols.

[timsueberkrueb]

Good idea with the OrderedMap. There are two more constraints.

1. As we have overloading, we want to track the order of terms/types with the same name. This means we need OrderedMap[String, List[TermSymbol] rather than OrderedMap[String, Set[TermSymbol]
2. We probably don't want separate maps for types and terms, but rather a single OrderedMap.

[timsueberkrueb]

This is further complicated by the fact that Namer has two phases: resolve and preresolve. Some things like namespaces and definitions are inserted in preresolve, others in resolve. This means we cannot rely on the insertion order.

[timsueberkrueb]

We could use the spans of definitions, though this is complicated by the symbols not carrying spans.

[b-studios]

A symbol should link to its definition, which has the span, no?

[jiribenes]

RE last commit: does this now fix https://github.com/effekt-lang/effekt/issues/430? 🤔

[timsueberkrueb]

Looks like it might? At least the reproducing examples in the issue seem to show better errors now.