fix(lsp): show success hints on the introducing keyword of commands and tactics

[ciaran-matthew-dunne]

Stacked on #1450 (bare open parsing fix): the first commit in the diff belongs to that PR; review the last three here.

The LSP server emits severity-4 "OK" diagnostics for every successfully checked command and tactic. These previously spanned the whole command or tactic, so the success underline covered symbol bodies, entire proofs and rule right-hand sides. With this PR the hint is shown on the introducing keyword only (symbol, rule, require, …; assume, rewrite, …).

Notes:

• For most commands the keyword position is computed as a prefix of the command's position (Pos.prefix). This is not possible for symbol (modifiers may precede the keyword), inductive (modifiers and parameters may) and open (a private modifier may), so for these three constructors the parser records the keyword position in the AST. Syntax.command_keyword_pos handles all cases, and falls back to the whole command's position when no keyword position was recorded (Dedukti input). require needs no recorded position: with fix parsing of bare open: do not load modules as require open does #1450 it is always the first keyword of its command.
• Tactic hints keep the start of their position unchanged: the same (position, goals) records anchor the goals panel, and its lookup (closest_before) only reads position starts. Only the end of the range shrinks, so proof/goals answers are unchanged. The keyword is used rather than the tactic's end because the end is ill-defined once a tactic has subproofs.
• Symbol declarations always create proof data, so their "OK" goes through the proof path. The initial goals stay anchored at the symbol name (the goals panel shows the initial proof state there); the visible hint goes on the symbol keyword.
• The keyword tables (tactic_keyword, query_keyword) have no wildcard case, so adding a constructor is a compile error until they are updated.
• Error diagnostics are unchanged: they still span the whole command or tactic.
• Also renames the lp_doc node field ast to cmd.

[ciaran-matthew-dunne]

Looks good to me.

[fblanqui]

There are several problems here:

• start_offset and end_offset should be set properly as well

• Why not taking end_col = p.end_col + 1 (";" is one character long only)?

• But this position is wrong if the semicolon is at the beginning of the line as in:

command ...
;

In this case, we should use {p with start_line = p.end_line; start_col = 0; end_col = 0} instead.
Problem:

command ...
 ; // semicolon with one space before

gives the same position as the previous case because of the current definition of extend_pos which extends a position until the previous column of the next token if it is >0.

So we should instead do:

let at_semicolon (pos:Pos.popt): Pos.popt =
  match pos with
  | None -> None
  | Some p ->
    if p.end_col = 0 then {p with start_offset=p.end_offset; start_line=p.end_line; start_col=0;
                                                        end_offset=p.end_offset+1; end_col=1}
      (* in this case we don't know whether ";" is at position 0 or 1, so we include both columns *)
    else {p with start_offset=p.end_offset+1; start_line=p.end_line; start_col=p.end_col+1;
                            end_offset=P.end_offset+1; end_col=p.end_col+1}

To be fully precise and not include a useless space, we need to include ";" in the position of a command.

[sacerdot]

Wait. The problem with the position of the trailing ";" comes from line 1719 of lpParser.ml. Instead of
| SEMICOLON -> c
one should do
| SEMICOLON -> extend_pos lb ... c

I think that that should fix the issue(*)

(*) In truth, the fact that the "command" parser is not allowed to consume the terminator is just plain weird and a symptom of bad coding elsewhere. The point is that in pure.ml (if I remember correctly) every time a new command is to be parsed, the lexbuf at the char Stream.t level is passed again. Instead the lexbuf at the lookahead level (the one I implemented) should be passed around. Right now the main parser functions exported by parser take in input the lexbuf at char level and build on-the-fly a new lexbuf at the backtracking level. Instead one should export a function to turn a lexbuf into an higher level lexbuf and then pass that again and again. Or, a less impacting alternative on the code, the parse_lexbuf function in parsing should take the low level lexbuf and return a closure that goes from unit to command, remembering the high level lexbuf inside the closure. Then pure.ml could just iterate this closure.

[ciaran-matthew-dunne]

Oh well, I decided that the diagnostic should sit on the keyword of the command anyway.

e.g., the diagnostic for the command constant symbol foo : TYPE; is placed on symbol,
and similarly the diagnostic for [a : Set] inductive T : TYPE ≔ ... is placed on inductive.

Frédéric talked to me this morning about the possibility of retiring the use of the semicolon in lambdapi. So hopefully these changes in this PR are compatible with any future changes to the parser.

[sacerdot]

The fix at line 1719 I proposed should be implemented anyway since it is nevertheless a bug IMHO. About the idea of retiring the ; terminator: in that case it will be MANDATORY to also apply the long explanation improvement I described, because otherwise with no semicolon to stop at one character will be definitely lost at the next call.

[fblanqui]

end_offset should be set properly as well, I believe to the same value as for end_col