Removed unnecessary RuleApp interface in Rusty

Drodt · Jan 15, 2025 · 7cc5c77 · 7cc5c77
1 parent 51a792b
commit 7cc5c77
Show file tree

Hide file tree

Showing 13 changed files with 17 additions and 50 deletions.
diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/proof/Goal.java b/keyext.rusty/src/main/java/org/key_project/rusty/proof/Goal.java
@@ -5,11 +5,11 @@
 
 import org.key_project.prover.proof.ProofGoal;
 import org.key_project.prover.rules.RuleAbortException;
+import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.SequentChangeInfo;
 import org.key_project.rusty.Services;
 import org.key_project.rusty.logic.NamespaceSet;
 import org.key_project.rusty.rule.NoPosTacletApp;
-import org.key_project.rusty.rule.RuleApp;
 import org.key_project.rusty.rule.Taclet;
 import org.key_project.rusty.rule.TacletApp;
 import org.key_project.rusty.rule.inst.SVInstantiations;

diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/proof/Node.java b/keyext.rusty/src/main/java/org/key_project/rusty/proof/Node.java
@@ -5,10 +5,10 @@
 
 import java.util.*;
 
+import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.rusty.proof.calculus.RustySequentKit;
 import org.key_project.rusty.rule.NoPosTacletApp;
-import org.key_project.rusty.rule.RuleApp;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableSet;
 

diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/proof/Statistics.java b/keyext.rusty/src/main/java/org/key_project/rusty/proof/Statistics.java
@@ -7,7 +7,7 @@
 import java.util.Iterator;
 import java.util.List;
 
-import org.key_project.rusty.rule.RuleApp;
+import org.key_project.prover.rules.RuleApp;
 import org.key_project.rusty.rule.TacletApp;
 import org.key_project.util.EnhancedStringBuffer;
 import org.key_project.util.collection.Pair;

diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/proof/TermTacletAppIndex.java b/keyext.rusty/src/main/java/org/key_project/rusty/proof/TermTacletAppIndex.java
@@ -4,11 +4,11 @@
 package org.key_project.rusty.proof;
 
 import org.key_project.logic.Term;
+import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.PIOPathIterator;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.rusty.Services;
 import org.key_project.rusty.rule.NoPosTacletApp;
-import org.key_project.rusty.rule.RuleApp;
 import org.key_project.rusty.rule.Taclet;
 import org.key_project.rusty.rule.TacletApp;
 import org.key_project.util.collection.*;

diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/OutputStreamProofSaver.java b/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/OutputStreamProofSaver.java
@@ -12,6 +12,7 @@
 import org.key_project.logic.Name;
 import org.key_project.logic.PosInTerm;
 import org.key_project.logic.Term;
+import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.PosInOccurrence;
@@ -24,7 +25,6 @@
 import org.key_project.rusty.proof.Node;
 import org.key_project.rusty.proof.Proof;
 import org.key_project.rusty.proof.init.Profile;
-import org.key_project.rusty.rule.RuleApp;
 import org.key_project.rusty.rule.TacletApp;
 import org.key_project.rusty.rule.inst.TermInstantiation;
 import org.key_project.rusty.settings.ProofSettings;

diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/BuiltInRule.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/BuiltInRule.java
@@ -3,7 +3,9 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.rusty.rule;
 
+import org.key_project.prover.rules.Rule;
 import org.key_project.prover.rules.RuleAbortException;
+import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.rules.RuleExecutor;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.rusty.proof.Goal;

diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/RuleApp.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/RuleApp.java
diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/SyntacticalReplaceVisitor.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/SyntacticalReplaceVisitor.java
@@ -13,6 +13,7 @@
 import org.key_project.logic.op.QuantifiableVariable;
 import org.key_project.logic.op.UpdateableOperator;
 import org.key_project.prover.rules.Rule;
+import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.rusty.Services;
 import org.key_project.rusty.ast.RustyProgramElement;

diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletApp.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletApp.java
@@ -13,6 +13,8 @@
 import org.key_project.logic.op.sv.OperatorSV;
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
+import org.key_project.prover.rules.Rule;
+import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.rules.instantiation.AssumesMatchResult;
@@ -149,8 +151,7 @@ protected static boolean checkNoFreeVars(Taclet taclet) {
 
     public static boolean checkNoFreeVars(Taclet taclet, SVInstantiations instantiations,
             PosInOccurrence pos) {
-        for (var pair : ((org.key_project.rusty.rule.inst.SVInstantiations) instantiations)
-                .getInstantiationMap()) {
+        for (var pair : instantiations.getInstantiationMap()) {
             final var sv = pair.key();
             if (sv instanceof TermSV || sv instanceof FormulaSV) {
                 // TODO: Is this enough? Do we need, e.g., sort checks?

diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletExecutor.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletExecutor.java
@@ -5,6 +5,7 @@
 
 import org.key_project.logic.LogicServices;
 import org.key_project.logic.Term;
+import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.sequent.SequentChangeInfo;
 import org.key_project.prover.sequent.SequentFormula;
@@ -48,7 +49,7 @@ protected Term and(Term t1, Term t2, @NonNull Goal goal) {
      * @return the (partially) instantiated term
      */
     protected Term syntacticalReplace(Term term, PosInOccurrence applicationPosInOccurrence,
-            MatchConditions mc, Goal goal, RuleApp ruleApp, Services services) {
+            MatchConditions mc, Goal goal, TacletApp ruleApp, Services services) {
         final SyntacticalReplaceVisitor srVisitor =
             new SyntacticalReplaceVisitor(applicationPosInOccurrence,
                 mc.getInstantiations(), goal, taclet, ruleApp, services);

diff --git a/...usty/src/main/java/org/key_project/rusty/rule/executor/rustydl/RewriteTacletExecutor.java b/...usty/src/main/java/org/key_project/rusty/rule/executor/rustydl/RewriteTacletExecutor.java
@@ -15,7 +15,6 @@
 import org.key_project.rusty.proof.Goal;
 import org.key_project.rusty.rule.MatchConditions;
 import org.key_project.rusty.rule.RewriteTaclet;
-import org.key_project.rusty.rule.RuleApp;
 import org.key_project.rusty.rule.TacletApp;
 import org.key_project.rusty.rule.tacletbuilder.RewriteTacletGoalTemplate;
 import org.key_project.rusty.rule.tacletbuilder.TacletGoalTemplate;
@@ -80,7 +79,7 @@ protected void applyReplacewith(TacletGoalTemplate gt, SequentChangeInfo current
 
     private org.key_project.prover.sequent.SequentFormula applyReplacewithHelper(Goal goal,
             RewriteTacletGoalTemplate gt, PosInOccurrence posOfFind, Services services,
-            MatchConditions matchCond, RuleApp ruleApp) {
+            MatchConditions matchCond, TacletApp ruleApp) {
         final Term term = posOfFind.sequentFormula().formula();
         final IntIterator it = posOfFind.posInTerm().iterator();
         final Term rwTemplate = gt.replaceWith();
@@ -98,7 +97,7 @@ private org.key_project.prover.sequent.SequentFormula applyReplacewithHelper(Goa
      * does the work for applyReplacewith (wraps recursion)
      */
     private Term replace(Term term, Term with, PosInOccurrence posOfFind, IntIterator it,
-            MatchConditions mc, Sort maxSort, Goal goal, Services services, RuleApp ruleApp) {
+            MatchConditions mc, Sort maxSort, Goal goal, Services services, TacletApp ruleApp) {
         if (it.hasNext()) {
             final int indexOfNextSubTerm = it.next();
 

diff --git a/keyext.rusty/src/test/java/org/key_project/rusty/BasicTest.java b/keyext.rusty/src/test/java/org/key_project/rusty/BasicTest.java
@@ -8,6 +8,7 @@
 
 import org.key_project.logic.Name;
 import org.key_project.logic.PosInTerm;
+import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.*;
 import org.key_project.rusty.ast.abstraction.KeYRustyType;
 import org.key_project.rusty.logic.op.ProgramVariable;
@@ -19,7 +20,6 @@
 import org.key_project.rusty.proof.init.RustProfile;
 import org.key_project.rusty.proof.io.ProofSaver;
 import org.key_project.rusty.rule.NoPosTacletApp;
-import org.key_project.rusty.rule.RuleApp;
 import org.key_project.rusty.rule.TacletApp;
 import org.key_project.rusty.util.TacletForTests;
 import org.key_project.util.collection.ImmutableList;

diff --git a/keyext.rusty/src/test/java/org/key_project/rusty/rule/TestApplyTaclet.java b/keyext.rusty/src/test/java/org/key_project/rusty/rule/TestApplyTaclet.java
@@ -9,6 +9,7 @@
 import org.key_project.logic.PosInTerm;
 import org.key_project.logic.Term;
 import org.key_project.logic.op.sv.SchemaVariable;
+import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.PosInOccurrence;