feat: More hovering information on the LSP

[MikaelMayer]

Fixes #3281
Fixes dafny-lang/ide-vscode#335
Fixes dafny-lang/ide-vscode#317
Fixes dafny-lang/ide-vscode#210

Example code:

predicate P(i: int) {
  i <= 0
}

predicate Q(i: int, j: int) {
  i == j || -i == j
}

function method Toast(i: int): int
  requires P(i)

method Test(i: int) returns (j: nat)
  ensures Q(i, j)
{
  if i < 0 {
    return -i;
  } else {
    return Toast(i);
  }
}

Before:	After
Hovering Q(i,j)
Hovering the second return
Hovering the call to Toast()
Also, on the diagnostics side (and it's clickable!)
The resolver error appears after all obsolete verification error

I added language server tests and tested it in VSCode, and it works as expected.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[MikaelMayer]

Found bugs if hovering over the "return" in this program:

module ProblemModule {
  datatype X =
    | Cons(head: int, tail: X)
    | Nil
  {
    predicate method Valid() {
      this.Cons? && tail.Valid()
    }
  }
}

method Test() returns (j: int)
  ensures j == 1
{
  return 2;
}

[MikaelMayer]

Disabling auto-merge because the following simple example has garbage hovering message:

datatype Test = Test(i: int)
{
  predicate Valid() {
    i > 0
  }
  predicate CanAct() requires Valid() {
    i > 1
  }
  method Tester(other: Test) {
    assert other.Valid();
    assert other.CanAct();
  }
}

If you hover over other.Valid();, you get

and if you hover over other.CanAct(), you get


Clearly, some ranges are wrong.

[MikaelMayer]

One more failing test case

datatype ValidTester = Tester(next: ValidTester2) | Tester2(next: ValidTester2) | Test3(next: ValidTester2)
{
  predicate Valid() {
    ((this.Tester? || this.Tester2?) && this.next.Valid()) || (this.Test3? && !this.next.Valid())
  }

  function method apply(): int requires Valid() {
    2
  }
  static method Test(c: ValidTester) {
    var x := c.apply();
  }
}

datatype ValidTester2 = MoreTest(i: int, next: ValidTester2) | End {
  predicate Valid(defaultValue: int := 0) {
    0 <= defaultValue &&
    (this.End? || (this.MoreTest? && this.next.Valid() && i > 0))
  }
}

If you hover over the failing c.apply(), it will quote random things. I guess it's because there is a defaultValue whose token is outside of the regular range.