Fix fstar-syntax-block-start-re to consider attributes

[mtzguido]

Hey Clément, I noticed that attributes were confusing the detection of the next block. I have this patch that seems to fix it, but it could sure use your expert eye to check I'm not doing something stupid :).

Thanks!

---

Before this change, running C-c C-n on a fragment like this

  let _ = 0

  [@] let _ = 2

  [@] let _ = 2

  [@] let _ = 2

Would blast through all of them instead of going one at a time.

[cpitclaudel]

Where do qualifiers (like abstract, private, etc.) go? With this patch they go before the attributes.

[mtzguido]

Qualifiers and attributes can appear in either order before a definition (and mixed too), so you're right that the case when one has [@blah] private let x = ... is funny, but then the regex will match an empty set of qualifiers and stop at the [@. I though this was fine since the regex is only used to detect the start of a block, but maybe not?

The thing is that a faithful regex for attributes would be enormous since it contains the entire language (provided one can even express it, since it's obviously not a regular language, but maybe emacs' regexes go beyond regular languages, as PCRE does).

[cpitclaudel]

Fair enough. Can there only be attributes on definitions, so it's always safe to use @[?

The thing is that a faithful regex for attributes would be enormous since it contains the entire language

We wouldn't want to do that anyway, because we'd like to be a bit robust to incorrect syntax.

[mtzguido]

Hmmm good point. No, internal lets can have attributes too. Here's a case that regresses:

module Attr

let _ =

[@] let x = 2 in

  x

Previously this would have taken the whole definition, but now it stops at the attribute and attempts to check the let _ = fragment. This doesn't happen when there's no empty line though, or if the line with the attribute is indented.

Though that second bit also seems fishy: this is taken as a single block:

let _ = 1

 let _ = 2

But I suppose if we made it ignore whitespace it would stop at internal lets too. Not sure what to do here.

[cpitclaudel]

Previously this would have taken the whole definition, but now it stops at the attribute and attempts to check the let _ = fragment. This doesn't happen when there's no empty line though, or if the line with the attribute is indented.

Yup, this stuff is ful of heuristics to try to guess where terms stop. That's the problem with complicated grammars in the ML family.

Not sure what to do here.

How common is it to have an attribute in column 0, like below?

let _ =

[@] let x = 2 in

Maybe this regression doesn't matter.

[mtzguido]

I doubt there's a single case anywhere. I believe the only attribute we care about for internal lets is inline_let, and the only use I could find that is not indented is this:

inline_for_extraction
let parse_bounded_der_length32_kind
  (min: der_length_t)
  (max: der_length_t { min <= max /\ max < 4294967296 } )
: Tot parser_kind
= 
[@inline_let]
let k = parse_bounded_der_length_payload32_kind min max in
strong_parser_kind (1 + der_length_payload_size_of_tag (tag_of_der_length32' min)) (1 + der_length_payload_size_of_tag (tag_of_der_length32' max)) None

And it doesn't have an empty line in between, so it should be good. I'd be fine with the new behaviour myself.

[cpitclaudel]

Thanks, I'm sold :)

[mtzguido]

:) Thanks!