Use KeYParser.g4 for parsing proof scripts (#3021)

Author: wadoon

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.13-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/blueprint_rifl.key

@@ -47,7 +47,7 @@
 	"class": "de.uka.ilkd.key.informationflow.po.InfFlowContractPO",
  }
 
-\proofScript "macro 'infflow-autopilot';"
+\proofScript { macro "infflow-autopilot"; }
 
 \proof {
 (autoModeTime "0")

key.core/src/main/antlr4/KeYLexer.g4

@@ -391,7 +391,6 @@ RGUILLEMETS: '>''>' | '»' | '›';
 IMPLICIT_IDENT: '<' '$'? (LETTER)+ '>' ('$lmtd')? -> type(IDENT);
 
 EQV:	'<->' | '\u2194';
-PRIMES:	('\'')+;
 CHAR_LITERAL
 : '\''
                 ((' '..'&') |
@@ -481,6 +480,7 @@ MODAILITYGENERIC:
       -> more, pushMode(modGeneric);
 */
 //BACKSLASH:  '\\';
+ERROR_UKNOWN_ESCAPE: '\\' IDENT;
 ERROR_CHAR: .;
 
 mode modDiamond;

key.core/src/main/antlr4/KeYParser.g4

@@ -41,7 +41,7 @@ problem
   | CHOOSECONTRACT (chooseContract=string_value SEMI)?
   | PROOFOBLIGATION  (proofObligation=cvalue)? SEMI?
   )
-  proofScript?
+  proofScriptEntry?
 ;
 
 
@@ -852,10 +852,34 @@ preferences
 	            |  c=cvalue ) // LBRACE, RBRACE included in cvalue#table
 ;
 
-proofScript
+proofScriptEntry
 :
-  PROOFSCRIPT ps = STRING_LITERAL
+  PROOFSCRIPT
+    ( STRING_LITERAL SEMI?
+    | LBRACE proofScript RBRACE
+    )
 ;
+proofScriptEOF: proofScript EOF;
+proofScript: proofScriptCommand+;
+proofScriptCommand: cmd=IDENT proofScriptParameters?
+	( LBRACE sub=proofScript RBRACE SEMI?
+	| SEMI);
+
+proofScriptParameters: proofScriptParameter+;
+proofScriptParameter :  ((pname=proofScriptParameterName (COLON|EQUALS))? expr=proofScriptExpression);
+proofScriptParameterName: AT? IDENT; // someone thought, that the let-command parameters should have a leading "@"
+proofScriptExpression:
+    boolean_literal
+  | char_literal
+  | integer
+  | floatnum
+  | string_literal
+  | LPAREN (term | seq) RPAREN
+  | simple_ident
+  | abbreviation
+  | literals
+  ;
+
 
 // PROOF
 proof: PROOF EOF;

key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java

@@ -14,7 +14,7 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.logic.op.IObserverFunction;
-import de.uka.ilkd.key.nparser.ProofScriptEntry;
+import de.uka.ilkd.key.nparser.KeyAst.ProofScript;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.Profile;
@@ -56,7 +56,7 @@ public class KeYEnvironment<U extends UserInterfaceControl> {
     /**
      * An optional field denoting a script contained in the proof file.
      */
-    private final @Nullable ProofScriptEntry proofScript;
+    private final @Nullable ProofScript proofScript;
 
     /**
      * Indicates that this {@link KeYEnvironment} is disposed.
@@ -83,9 +83,10 @@ public KeYEnvironment(U ui, InitConfig initConfig) {
      *
      * @param ui The {@link UserInterfaceControl} in which the {@link Proof} is loaded.
      * @param initConfig The loaded project.
+     * @param proofScript add an optional proof script
      */
     public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof,
-            @Nullable ProofScriptEntry proofScript, ReplayResult replayResult) {
+            @Nullable ProofScript proofScript, ReplayResult replayResult) {
         this.ui = ui;
         this.initConfig = initConfig;
         this.loadedProof = loadedProof;
@@ -251,8 +252,10 @@ public static KeYEnvironment<DefaultUserInterfaceControl> load(Profile profile,
      * @param poPropertiesToForce Some optional PO {@link Properties} to force.
      * @param ruleCompletionHandler An optional {@link RuleCompletionHandler}.
      * @param forceNewProfileOfNewProofs {@code} true
-     *        {@code AbstractProblemLoader.profileOfNewProofs} will be used as {@link Profile} of
-     *        new proofs, {@code false} {@link Profile} specified by problem file will be used for
+     *        {@code AbstractProblemLoader.profileOfNewProofs} will
+     *        be used as {@link Profile} of
+     *        new proofs, {@code false} {@link Profile}
+     *        specified by problem file will be used for
      *        new proofs.
      * @return The {@link KeYEnvironment} which contains all references to the loaded location.
      * @throws ProblemLoaderException Occurred Exception
@@ -290,7 +293,8 @@ public static KeYEnvironment<DefaultUserInterfaceControl> load(Profile profile,
             List<File> classPaths, File bootClassPath, List<File> includes,
             Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler,
             Consumer<Proof> callbackProofLoaded,
-            boolean forceNewProfileOfNewProofs) throws ProblemLoaderException {
+            boolean forceNewProfileOfNewProofs)
+            throws ProblemLoaderException {
         DefaultUserInterfaceControl ui = new DefaultUserInterfaceControl(ruleCompletionHandler);
         AbstractProblemLoader loader = ui.load(profile, location, classPaths, bootClassPath,
             includes, poPropertiesToForce, forceNewProfileOfNewProofs, callbackProofLoaded);
@@ -319,13 +323,13 @@ public void dispose() {
      * Checks if this {@link KeYEnvironment} is disposed meaning that {@link #dispose()} was already
      * executed at least once.
      *
-     * @return {@code true} disposed, {@code false} not disposed and still functionable.
+     * @return {@code true} disposed, {@code false} not disposed and still functional.
      */
     public boolean isDisposed() {
         return disposed;
     }
 
-    public @Nullable ProofScriptEntry getProofScript() {
+    public @Nullable ProofScript getProofScript() {
         return proofScript;
     }