Improve error correction in the parser to enable resolution to happen while there are still parse errors

[seebees]

When I'm editing a Dafny file I find that I take 3 passes. First I have to get all the tokens to "line up". Like if I'm makeing extensive changes to an included file, in the files includes it, I'll get an error at the "include site" and maybe in some places where I use tokens that no longer exists.

Once I fix the last of these errors, then the type checker runs through and gives me LOTS of nice new errors about how I'm using my new types incorrectly.

It would be great if a single Dafny file could be... "parsed more granularly"? So if the whole file still has some large structural errors, but a specific method is "clean", then the type checker could fully evaluate the use of types, only in that specific method.

Anyway, fixing 15 errors in a file and then finding that when I fix the last error I now have another 40 errors.... is sub-fun :)

[seebees]

This is just a simple example

In the following case baz will have an error "unresolved identifier: baz"

  function Foo(bar: string)
    :(ret:string)
  {
    bar + baz
  }

However if I break the parsing like this:

function Foo(bar: string)
    :(ret:string)
  {
    bar + baz
  }

  function BBB(
    missing: string
    comma: string
  )
    :(ret:string)
  {
    missing + comma
  }

The error around baz goes away and you get an error around comma: string and :(ret:string)

To work around this I tend to comment out swaths of a file so that I can completely work through a section. You can see that the same problem exists for verification :) e.g. If I only fix the issue in Foo I could not only verify Foo without first fixing BBB

I don't think that this is a feature that works nicely in the command line tools, this is more something for the language server as it integrates with the IDE.

[keyboardDrummer]

There's a feature in parsers which is called error correction, which allows parts of a file to parse while other parts have parse errors. Error correction is important for parsers used by IDEs, mostly to enable code completion while the file has parse errors, but also to enable other IDE features to continue working while you have parse errors. Parse error correction also allows showing errors from later stages, like resolution, while you have parse errors.

I'm not aware of Dafny's parser doing error correction at the moment, it might do so in a limited capacity, but it is something we will add.

What we can also do is allow modules that have successfully resolved, to be verified even when other modules have not parsed or resolved successfully. I think we will change this when we make the Dafny compiler execute more parallelly.