Use KeYParser.g4 for parsing proof scripts

[wadoon]

This PR removes the hand-written parser for proof scripts and uses a few rules in KeYParser.g4 instead.

Since the start of proof scripts, the KeYParser has changed and became an ANTLR4 grammar. This allows us to easily write a grammar for our proof scripts. (Or just copy the few rules from Sarah and mine proof script parser). This eliminates the handwritten proof script parser with the following benefits:

1. Proof Scripts are a first-class citizen in KeY files. You do not need to put your proof script into a string literal:

   \proofscript {
       andLeft;
       andRight;  
       rule a ==> b;
   }
   

   Please note an ambiguity in the grammar: rule b ==> c could either be interpreted as a command with one or two arguments:

   1. a semi-sequent b ==> and a term c, or
   2. a sequent b ==> c.
   3. or a term b and a semi-sequent ==> c.

   Use quotes or better backticks to clarify these situations.

   Also, avoid using hyphens in identifiers. The grammar should follow the KeY grammar as best as possible. Backwards-compatiblity is tried to preserve.

2. Earlier and better syntax errors. (during reading the KeY file)

3. Better positioning information, as these are tucked to gather on the ParseContexts.

4. Proper data structure: no triple of strings is pushed through KeY.

5. You do not need to put your arguments in quotes. Literals, terms and sequents are parsed.

Tried to achieve backward-compatibility. If the proof script is given as a string, the parsing is delayed until the execution. The same is valid for arguments.

Note there is a difference between f(x) and "f(x)". The first one is parsed directly as a term and can only passed to term or string arguments. The second one is parsed as a string. By meta-information on commands, the string is lazily converted to a term if necessary.

The term f(x) might be parsed early with the input file, but the expression is evaluated (translated from parse tree to Term) on command-execution time, hence, the use of goal-local variables should be possible.

Additions to Proof Scripts

The interface of commands and the syntax received an extension to support commands like AllCommand in a uniform way. AllCommand (onAll hide \f(x)`) executes the sub-command specified by the arguments on all goals. In SaG scripts we used foreach { ... }` to achieve this behavior.

The extension adapts the command syntax to take a list of sub-commands in curly brackets.

proofScriptCommand: 
    name  args  (  '{'   <sub-command>  '}' ';'? | ';' )
    ; 

The new syntax for onAll is also onAll { hide \f(x)`; }. Commands receive the code block using the key #blockinside the map as a parse tree, that can be sent back to theScriptEngineusing#execute(state, statements)`. The new syntax allows to build new commands like

• try {<sub>} -- executes <sub> ignoring errors
• repeat { <sub> } -- executes <sub> as long as there are changes on the sequent.
• matching <term> { <sub> } -- execute on all goals where <term> is prescense.

[mattulbrich]

I agree that the current parser is more a proof-of-concept solution than future-proof.

However: With many ideas around proof scripts, which should possibly discuss how this should go now: The script debugger has its ways of communicating to the server, scripts can be in .key files, they were at a point interactively editable, and the plan is to have them in JML code. Do they all go to the same background linear script language or is the base language itself more than a sequence of commands?

@WolframPfeifer @jwiesler

[mattulbrich]

First round of review. Some feedback. Could not review the whole thing.

[mattulbrich]

I really do not like the ambiguity.
Can we make this IDENTIFIER without ticks and any composed term/seq in ticks?
I would prefer single ticks compared to back ticks. I do not think we need single-character parameters (and if: Use strings ...)

[wadoon]

I really do not like the ambiguity.

Not my language.

Can we make this IDENTIFIER without ticks and any composed term/seq in ticks?

What do you mean by this IDENTIFIER?

In macro tryclose, the tryclose is still evaluated as a string and not sent to the expression evaluation. This adds unnecessary complexity.

I would prefer single ticks compared to back ticks

• single quotes ' are often used currently as string quotes in proof scripts
• backticks are only necessary to avoid ambiguous situations: command p=2 could be a formula or the parameter p to be 2.

(and if: Use strings ...)

No. The advantage of separation is that the parser is eager to give feedback on syntactical correctness. Otherwise, these errors appears only on evaluation of commands.

[mattulbrich]

Reply to me-from-the-past:

However: With many ideas around proof scripts, which should possibly discuss how this should go now: The script debugger has its ways of communicating to the server, scripts can be in .key files, they were at a point interactively editable, and the plan is to have them in JML code. Do they all go to the same background linear script language or is the base language itself more than a sequence of commands?

After implementing a/the script language for JML: This was compiled down to a linear script. So it seems that a list of individual proof commands looks like the right level of abstraction.

[wadoon]

After implementing a/the script language for JML: This was compiled down to a linear script. So it seems that a list of individual proof commands looks like the right level of abstraction.

This PR gives the current state a proper syntax in alignment with the KeY grammar. So the list of proof commands are still preserved. Giving the commands the possibility to receive a block of sub-commands arises from your AllCommand and allows future extensions w/o needing syntax changes.

We need a quoting symbol for terms for the ambiguities, " is used for string values, and ' is also occupied (do we use it for char literals?). So backticks \`` are a possible option, but we can also go for parentheses, e.g., let @A=(f(x))` etc. I do not care.