more refactoring

KeYProject · Jun 12, 2024 · 704070f · 704070f
1 parent b0220bd
commit 704070f
Show file tree

Hide file tree

Showing 24 changed files with 99 additions and 22 deletions.
diff --git a/...xecution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java b/...xecution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java
@@ -21,7 +21,7 @@
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.rule.DefaultBuiltInRuleApp;
 import de.uka.ilkd.key.rule.IBuiltInRuleApp;
-import de.uka.ilkd.key.rule.RuleAbortException;
+import org.key_project.ncore.rules.RuleAbortException;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;

diff --git a/...c_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java b/...c_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java
@@ -22,7 +22,7 @@
 import de.uka.ilkd.key.rule.DefaultBuiltInRuleApp;
 import de.uka.ilkd.key.rule.IBuiltInRuleApp;
 import de.uka.ilkd.key.rule.QueryExpand;
-import de.uka.ilkd.key.rule.RuleAbortException;
+import org.key_project.ncore.rules.RuleAbortException;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
 import de.uka.ilkd.key.util.Triple;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java
@@ -12,6 +12,7 @@
 import de.uka.ilkd.key.logic.op.LocationVariable;
 import de.uka.ilkd.key.proof.Goal;
 
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java
@@ -24,6 +24,7 @@
 import de.uka.ilkd.key.util.MiscTools;
 
 import org.key_project.logic.Name;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.ImmutableSet;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractExternalRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractExternalRule.java
@@ -27,6 +27,7 @@
 import de.uka.ilkd.key.util.MiscTools;
 
 import org.key_project.logic.Name;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.java.ArrayUtil;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java
@@ -29,6 +29,7 @@
 import de.uka.ilkd.key.util.MiscTools;
 
 import org.key_project.logic.Name;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.java.ArrayUtil;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java
@@ -20,6 +20,7 @@
 import de.uka.ilkd.key.util.MiscTools;
 
 import org.key_project.logic.Name;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableList;
 
 import org.jspecify.annotations.NonNull;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopApplyHeadRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopApplyHeadRule.java
@@ -21,6 +21,7 @@
 import de.uka.ilkd.key.speclang.LoopContractImpl;
 
 import org.key_project.logic.Name;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.ImmutableSet;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractExternalRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractExternalRule.java
@@ -28,6 +28,7 @@
 import de.uka.ilkd.key.util.MiscTools;
 
 import org.key_project.logic.Name;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.java.ArrayUtil;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractInternalRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractInternalRule.java
@@ -22,6 +22,7 @@
 import de.uka.ilkd.key.util.MiscTools;
 
 import org.key_project.logic.Name;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.java.ArrayUtil;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java
@@ -33,6 +33,7 @@
 import de.uka.ilkd.key.speclang.WellDefinednessCheck;
 
 import org.key_project.logic.Name;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.Pair;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/Rule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/Rule.java
@@ -8,14 +8,15 @@
 
 import org.key_project.logic.HasOrigin;
 import org.key_project.logic.Name;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableList;
 
 import org.jspecify.annotations.NonNull;
 
 /**
  * This interface has to be implemented by all classes that want to act as a rule in the calculus.
  */
-public interface Rule extends HasOrigin {
+public interface Rule extends org.key_project.ncore.rules.Rule, HasOrigin {
 
     /**
      * the rule is applied on the given goal using the information of rule application.
@@ -31,6 +32,11 @@ public interface Rule extends HasOrigin {
     ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
             throws RuleAbortException;
 
+    @NonNull
+    default ImmutableList<Goal> apply(Goal goal, RuleApp ruleApp) throws RuleAbortException {
+      return apply(goal, goal.proof().getServices(), ruleApp);
+    };
+
     /**
      * the name of the rule
      */

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/RuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/RuleApp.java
@@ -15,7 +15,7 @@
 /**
  * rule application with specific information how and where the rule has to be applied
  */
-public interface RuleApp extends EqualsModProofIrrelevancy {
+public interface RuleApp extends org.key_project.ncore.rules.RuleApp, EqualsModProofIrrelevancy {
 
     /**
      * returns the rule of this rule application
@@ -39,18 +39,9 @@ public interface RuleApp extends EqualsModProofIrrelevancy {
     @Nullable
     ImmutableList<Goal> execute(Goal goal, Services services);
 
-    /**
-     * returns true if all variables are instantiated
-     *
-     * @return true if all variables are instantiated
-     */
-    boolean complete();
-
-    /**
-     * @return user-friendly name for this rule-application
-     */
-    default String displayName() {
-        return rule().displayName();
+    @Nullable
+    default ImmutableList<Goal> execute(Goal goal) {
+        return execute(goal, goal.proof().getServices());
     }
 
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/SetStatementRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/SetStatementRule.java
@@ -18,6 +18,7 @@
 import de.uka.ilkd.key.util.MiscTools;
 
 import org.key_project.logic.Name;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableList;
 
 import org.jspecify.annotations.NonNull;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java
@@ -55,6 +55,7 @@
 import de.uka.ilkd.key.util.Triple;
 
 import org.key_project.logic.Name;
+import org.key_project.ncore.rules.RuleAbortException;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/CloseAfterMerge.java b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/CloseAfterMerge.java
@@ -28,7 +28,7 @@
 import de.uka.ilkd.key.proof.ProofTreeEvent;
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.rule.IBuiltInRuleApp;
-import de.uka.ilkd.key.rule.RuleAbortException;
+import org.key_project.ncore.rules.RuleAbortException;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.util.mergerule.SymbolicExecutionState;
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java
@@ -24,7 +24,7 @@
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.rule.IBuiltInRuleApp;
 import de.uka.ilkd.key.rule.NoPosTacletApp;
-import de.uka.ilkd.key.rule.RuleAbortException;
+import org.key_project.ncore.rules.RuleAbortException;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.rule.merge.MergeProcedure.ValuesMergeResult;
 import de.uka.ilkd.key.rule.merge.procedures.MergeByIfThenElse;

diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java
@@ -19,7 +19,7 @@
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.rule.Rule;
-import de.uka.ilkd.key.rule.RuleAbortException;
+import org.key_project.ncore.rules.RuleAbortException;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.rule.label.ChildTermLabelPolicy;
 import de.uka.ilkd.key.rule.label.TermLabelPolicy;

diff --git a/key.ncore.calculus/src/main/java/org/key_project/ncore/proof/ProofObject.java b/key.ncore.calculus/src/main/java/org/key_project/ncore/proof/ProofObject.java
@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.ncore.proof;
 
-
 /**
  * <p>
  * A proof object provides an interface to the current proof status.

diff --git a/key.ncore.calculus/src/main/java/org/key_project/ncore/rules/Rule.java b/key.ncore.calculus/src/main/java/org/key_project/ncore/rules/Rule.java
@@ -0,0 +1,32 @@
+package org.key_project.ncore.rules;
+
+import org.jspecify.annotations.NonNull;
+import org.key_project.logic.Name;
+import org.key_project.logic.Named;
+import org.key_project.ncore.proof.ProofGoal;
+import org.key_project.util.collection.ImmutableList;
+
+public interface Rule extends Named {
+    /**
+     * the rule is applied on the given goal using the information of rule application.
+     *
+     * @param goal the Goal on which to apply <tt>ruleApp</tt>
+     * @param ruleApp the rule application to be executed
+     * @return all open goals below \old(goal.node()), i.e. the goals resulting from the rule
+     *         application
+     * @throws RuleAbortException when this rule was aborted
+     */
+    @NonNull
+    <G extends ProofGoal> ImmutableList<G> apply(G goal, RuleApp ruleApp)
+            throws RuleAbortException;
+
+    /**
+     * the name of the rule
+     */
+    Name name();
+
+    /**
+     * returns the display name of the rule
+     */
+    String displayName();
+}
diff --git a/...uka/ilkd/key/rule/RuleAbortException.java → ...oject/ncore/rules/RuleAbortException.java b/...uka/ilkd/key/rule/RuleAbortException.java → ...oject/ncore/rules/RuleAbortException.java
@@ -1,7 +1,7 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.rule;
+package org.key_project.ncore.rules;
 
 /**
  *

diff --git a/key.ncore.calculus/src/main/java/org/key_project/ncore/rules/RuleApp.java b/key.ncore.calculus/src/main/java/org/key_project/ncore/rules/RuleApp.java
@@ -0,0 +1,37 @@
+package org.key_project.ncore.rules;
+
+import org.jspecify.annotations.Nullable;
+import org.key_project.ncore.proof.ProofGoal;
+import org.key_project.util.collection.ImmutableList;
+
+public interface RuleApp {
+    /**
+     * returns the rule of this rule application
+     */
+    Rule rule();
+
+    /**
+     * applies the specified rule at the specified position if all schema variables have been
+     * instantiated
+     *
+     * @param goal the Goal where to apply the rule
+     * @return list of new created goals
+     */
+    @Nullable
+    <G extends ProofGoal> ImmutableList<G> execute(G goal);
+
+    /**
+     * returns true if all variables are instantiated
+     *
+     * @return true if all variables are instantiated
+     */
+    boolean complete();
+
+    /**
+     * @return user-friendly name for this rule-application
+     */
+    default String displayName() {
+        return rule().displayName();
+    }
+
+}
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InvariantConfigurator.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InvariantConfigurator.java
@@ -26,7 +26,7 @@
 import de.uka.ilkd.key.pp.AbbrevMap;
 import de.uka.ilkd.key.pp.PrettyPrinter;
 import de.uka.ilkd.key.proof.io.OutputStreamProofSaver;
-import de.uka.ilkd.key.rule.RuleAbortException;
+import org.key_project.ncore.rules.RuleAbortException;
 import de.uka.ilkd.key.speclang.LoopSpecification;
 import de.uka.ilkd.key.util.InfFlowSpec;
 

diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/LoopInvariantRuleCompletion.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/LoopInvariantRuleCompletion.java
@@ -13,6 +13,7 @@
 import de.uka.ilkd.key.speclang.LoopSpecImpl;
 import de.uka.ilkd.key.speclang.LoopSpecification;
 import de.uka.ilkd.key.util.MiscTools;
+import org.key_project.ncore.rules.RuleAbortException;
 
 /**
  * This class completes the instantiations of the loop invariant rule applications.