AST for KeY Scripts

[wadoon]

Synopsis

JMLScripts and KeY scripts use the same backend, but the ProofScriptEngine is currently bound to the KeY language's parser. This PR introduces a simple AST class to abstract the source of a script, which is a simple record containing the command name, positional and keyword arguments, sub-commands, and positional information.

classDiagram
  direction TB

  class ScriptCommandAst { 
  name : String 
  positionalArgs : List<Object>
  keywordArgs    : Map<String,Object>
  loc            : Location
 }

ScriptCommandAst "*" <-- ScriptCommandAst : sub-commands

Loading

Along the road, the interface of script commands is simplified: There is no need for preparing the parameter class instance anymore. Instead, execute(..) is called directly, and any command implementation can deal with the AST as they like.

classDiagram 
  direction TB

   class ProofScriptCommand {
    execute(uiControl, cmdAst, engineState) 

    getArguments() : List<ProofScriptArgument>
    getName() : String
    getAlias() : List<String>
    getDocumentation()
  }

Loading

Also, proof script commands can announce a list of aliases. This allows the implementation of multiple (similar) commands with one implementation. The implementation can adapt its behavior using the given AST representation. For example, the let command is also callable via letf, the latter forces/overwrites the abbreviation.

Using List<Object> and Map<String,Object> for the representation inside of the AST allows the use within JML scripts, as custom objects can be provided within the AST. Later, the ValueInjector should know the conversion rules to get from the custom object to the required types, e.g., how to come from a JMLTerm to a JTerm.

Builds upon: #3021

Intended Change

ProofScriptEngine is free of ANTLR classes.
An AST for the execution of proof scripts exists, which is useable

Plan

• Do it.
• Test it.
• Ship it.

Type of pull request

• Refactoring (behaviour should not change or only minimally change)

  • Breaking change:
    breaks the internal API of proof script execution, and script commands.

• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: ...
• I have checked that runtime performance has not deteriorated.

[mattulbrich]

Nice.

Thanks for the comments. Appreciate that.
Made a few suggestions. Mostly on naming and documentation.

Have not actually run it, but since we plan to extend this to JML scripts, it will be tested thoroughly soon.

[wadoon]

Removed the merge commit and rebased on main. Reviewer comments addressed.