CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
950 stars 83 forks source link

Pancake syntax errors for if/else reported at wrong location #1011

Open talsewell opened 3 months ago

talsewell commented 3 months ago

It happens that pancake doesn't support if ( ) { } else if ( ) { } else { }, that is, the else if pair is not supported and the second if has to be enclosed in { .. }. That is a grumble but not a show stopper.

However, given this syntax, for some reason, the error reported is "failed to see expected token" at var yv = y;, which is much too early:

fun foo (1 x, 1 y) {
  var xv = x;
  while (x < y) {
    var yv = y;
    if (xv <= y) {
      x = x + 8;
    }
    else if (xv > y) {
      x = x + 2;
    }
    else {
      x = x + 1;
    }
  }
  return x;
}

This is quite a nuisance, it requires an overcomplicated process of splicing out sections of the file to try to figure out what the error actually is.

IlmariReissumies commented 3 months ago

Thanks for reporting. Adding else if shouldn't be too hard. The error reporting is pretty bare bones and really just pretty-prints the error messages we get from the PEG infrastructure; there's lots of room for improvement but it's better than nothing.