Created package rules.conditions in ncore for common taclet related conditions

unp1 · unp1 · commit 30b238027341 · 2025-01-15T08:07:43.000+01:00
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
@@ -31,6 +31,9 @@
 import org.key_project.logic.sort.Sort;
 import org.key_project.prover.rules.*;
 import org.key_project.prover.rules.Taclet;
+import org.key_project.prover.rules.conditions.NewDependingOn;
+import org.key_project.prover.rules.conditions.NewVarcond;
+import org.key_project.prover.rules.conditions.NotFreeIn;
 import org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate;
 import org.key_project.prover.sequent.Semisequent;
 import org.key_project.prover.sequent.Sequent;
@@ -350,11 +353,11 @@ protected void printRewriteAttributes(RewriteTaclet taclet) {
     }
 
     protected void printVarCond(Taclet taclet) {
-        final ImmutableList<? extends org.key_project.prover.rules.NewVarcond> varsNew =
+        final ImmutableList<? extends NewVarcond> varsNew =
             taclet.varsNew();
-        final ImmutableList<? extends org.key_project.prover.rules.NewDependingOn> varsNewDependingOn =
+        final ImmutableList<? extends NewDependingOn> varsNewDependingOn =
             taclet.varsNewDependingOn();
-        final ImmutableList<? extends org.key_project.prover.rules.NotFreeIn> varsNotFreeIn =
+        final ImmutableList<? extends NotFreeIn> varsNotFreeIn =
             taclet.varsNotFreeIn();
         final ImmutableList<? extends VariableCondition> variableConditions =
             taclet.getVariableConditions();
@@ -364,7 +367,7 @@ protected void printVarCond(Taclet taclet) {
             layouter.nl().beginC().print("\\varcond(").brk(0);
             boolean first = true;
 
-            for (org.key_project.prover.rules.NewDependingOn ndo : varsNewDependingOn) {
+            for (NewDependingOn ndo : varsNewDependingOn) {
                 if (first) {
                     first = false;
                 } else {
@@ -403,7 +406,7 @@ protected void printVarCond(Taclet taclet) {
         }
     }
 
-    private void printNewVarDepOnCond(org.key_project.prover.rules.NewDependingOn on) {
+    private void printNewVarDepOnCond(NewDependingOn on) {
         layouter.beginC(0);
         layouter.print("\\new(");
         printSchemaVariable(on.first());
@@ -414,7 +417,7 @@ private void printNewVarDepOnCond(org.key_project.prover.rules.NewDependingOn on
         layouter.brk(0, -2).print(")").end();
     }
 
-    protected void printNewVarcond(org.key_project.prover.rules.NewVarcond p_sv) {
+    protected void printNewVarcond(NewVarcond p_sv) {
         de.uka.ilkd.key.rule.NewVarcond sv = (de.uka.ilkd.key.rule.NewVarcond) p_sv;
         layouter.beginC();
         layouter.print("\\new(");
@@ -434,7 +437,7 @@ protected void printNewVarcond(org.key_project.prover.rules.NewVarcond p_sv) {
         layouter.brk(0, -2).print(")").end();
     }
 
-    protected void printNotFreeIn(org.key_project.prover.rules.NotFreeIn sv) {
+    protected void printNotFreeIn(NotFreeIn sv) {
         layouter.beginI(0).print("\\notFreeIn(").brk(0);
         printSchemaVariable(sv.first());
         layouter.print(",").brk();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/NewVarcond.java b/key.core/src/main/java/de/uka/ilkd/key/rule/NewVarcond.java
@@ -10,7 +10,7 @@
 /**
  * variable condition used if a new variable is introduced
  */
-public class NewVarcond implements org.key_project.prover.rules.NewVarcond {
+public class NewVarcond implements org.key_project.prover.rules.conditions.NewVarcond {
 
     private final SchemaVariable sv;
     private final SchemaVariable peerSV;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java
@@ -24,6 +24,7 @@
 import org.key_project.logic.SyntaxElement;
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.prover.rules.*;
+import org.key_project.prover.rules.conditions.NotFreeIn;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.rules.instantiation.AssumesMatchResult;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java
@@ -18,6 +18,9 @@
 import org.key_project.logic.Name;
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.prover.rules.*;
+import org.key_project.prover.rules.conditions.NewDependingOn;
+import org.key_project.prover.rules.conditions.NewVarcond;
+import org.key_project.prover.rules.conditions.NotFreeIn;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.DefaultImmutableSet;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletPrefixBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletPrefixBuilder.java
@@ -11,7 +11,7 @@
 import de.uka.ilkd.key.rule.*;
 
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.NotFreeIn;
+import org.key_project.prover.rules.conditions.NotFreeIn;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.*;
diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/Taclet.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/Taclet.java
@@ -8,6 +8,9 @@
 import org.key_project.logic.Name;
 import org.key_project.logic.op.QuantifiableVariable;
 import org.key_project.logic.op.sv.SchemaVariable;
+import org.key_project.prover.rules.conditions.NewDependingOn;
+import org.key_project.prover.rules.conditions.NewVarcond;
+import org.key_project.prover.rules.conditions.NotFreeIn;
 import org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.util.collection.ImmutableList;
diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/TacletApplPart.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/TacletApplPart.java
@@ -3,6 +3,9 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.prover.rules;
 
+import org.key_project.prover.rules.conditions.NewDependingOn;
+import org.key_project.prover.rules.conditions.NewVarcond;
+import org.key_project.prover.rules.conditions.NotFreeIn;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.util.collection.ImmutableList;
 
diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/conditions/NewDependingOn.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/conditions/NewDependingOn.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 org.key_project.prover.rules;
+package org.key_project.prover.rules.conditions;
 
 import org.key_project.logic.op.sv.SchemaVariable;
 
diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/conditions/NewVarcond.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/conditions/NewVarcond.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 org.key_project.prover.rules;
+package org.key_project.prover.rules.conditions;
 
 
 import org.key_project.logic.op.sv.SchemaVariable;
diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/conditions/NotFreeIn.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/conditions/NotFreeIn.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 org.key_project.prover.rules;
+package org.key_project.prover.rules.conditions;
 
 import org.key_project.logic.op.QuantifiableVariable;
 import org.key_project.logic.op.sv.SchemaVariable;
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/TacletDescriber.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/TacletDescriber.java
@@ -14,10 +14,10 @@
 import de.uka.ilkd.key.rule.inst.GenericSortInstantiations;
 
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.NewDependingOn;
-import org.key_project.prover.rules.NewVarcond;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.rules.Taclet;
+import org.key_project.prover.rules.conditions.NewDependingOn;
+import org.key_project.prover.rules.conditions.NewVarcond;
 import org.key_project.util.collection.ImmutableSet;
 
 /**
diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/NewVarcond.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/NewVarcond.java
@@ -6,7 +6,7 @@
 import org.key_project.rusty.ast.abstraction.KeYRustyType;
 import org.key_project.rusty.logic.op.sv.SchemaVariable;
 
-public class NewVarcond implements org.key_project.prover.rules.NewVarcond {
+public class NewVarcond implements org.key_project.prover.rules.conditions.NewVarcond {
     private final SchemaVariable sv;
     private final SchemaVariable peerSV;
     private final KeYRustyType type;
diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/VMTacletMatcher.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/VMTacletMatcher.java
@@ -12,6 +12,7 @@
 import org.key_project.logic.op.QuantifiableVariable;
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.prover.rules.*;
+import org.key_project.prover.rules.conditions.NotFreeIn;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.rules.instantiation.AssumesMatchResult;
diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/tacletbuilder/TacletBuilder.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/tacletbuilder/TacletBuilder.java
@@ -9,6 +9,8 @@
 import org.key_project.logic.Term;
 import org.key_project.logic.op.QuantifiableVariable;
 import org.key_project.prover.rules.*;
+import org.key_project.prover.rules.conditions.NewDependingOn;
+import org.key_project.prover.rules.conditions.NotFreeIn;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.rusty.ast.abstraction.KeYRustyType;
 import org.key_project.rusty.logic.op.sv.ProgramSV;
diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/tacletbuilder/TacletPrefixBuilder.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/tacletbuilder/TacletPrefixBuilder.java
@@ -8,7 +8,7 @@
 
 import org.key_project.logic.Term;
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.NotFreeIn;
+import org.key_project.prover.rules.conditions.NotFreeIn;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.rusty.logic.op.Modality;
 import org.key_project.rusty.logic.op.sv.FormulaSV;
