Move ApplicationRestriction to own file

Drodt · Drodt · commit 714dd501518d · 2025-06-06T14:51:44.000+02:00
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java
@@ -25,7 +25,7 @@
 
 import org.key_project.logic.Name;
 import org.key_project.prover.rules.RuleSet;
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 import org.key_project.prover.rules.TacletApplPart;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentFormula;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.java
@@ -24,7 +24,7 @@
 import org.key_project.logic.Name;
 import org.key_project.logic.op.Function;
 import org.key_project.prover.rules.RuleSet;
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.Pair;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java
@@ -33,7 +33,7 @@
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
 import org.key_project.prover.rules.RuleSet;
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 import org.key_project.prover.rules.TacletAnnotation;
 import org.key_project.prover.rules.Trigger;
 import org.key_project.prover.sequent.Sequent;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java
@@ -38,7 +38,7 @@
 import org.key_project.logic.Name;
 import org.key_project.logic.sort.Sort;
 import org.key_project.prover.rules.RuleSet;
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 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/OneStepSimplifier.java b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java
@@ -37,7 +37,7 @@
 import org.key_project.prover.proof.rulefilter.TacletFilter;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.rules.RuleSet;
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.*;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java b/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java
@@ -27,7 +27,7 @@
 import org.key_project.logic.sort.Sort;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.rules.RuleSet;
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 import org.key_project.prover.sequent.PIOPathIterator;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.sequent.SequentFormula;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/RewriteTacletExecutor.java b/key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/RewriteTacletExecutor.java
@@ -17,7 +17,7 @@
 
 import org.key_project.logic.IntIterator;
 import org.key_project.logic.sort.Sort;
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate;
 import org.key_project.prover.sequent.PosInOccurrence;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecTacletBuilder.java
@@ -7,7 +7,7 @@
 import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit;
 import de.uka.ilkd.key.rule.AntecTaclet;
 
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 import org.key_project.prover.rules.TacletApplPart;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentFormula;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/FindTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/FindTacletBuilder.java
@@ -7,7 +7,7 @@
 import de.uka.ilkd.key.rule.FindTaclet;
 
 import org.key_project.logic.SyntaxElement;
-import org.key_project.prover.rules.Taclet;
+import org.key_project.prover.rules.ApplicationRestriction;
 
 /**
  * Superclass of TacletBuilder objects that have a non-empty find clause. This should be all of them
@@ -20,20 +20,20 @@ public abstract class FindTacletBuilder<T extends FindTaclet> extends TacletBuil
      * encodes restrictions on the state where a rewrite taclet is applicable If the value is equal
      * to
      * <ul>
-     * <li>{@link Taclet.ApplicationRestriction#NONE} no state restrictions are posed</li>
-     * <li>{@link Taclet.ApplicationRestriction#SAME_UPDATE_LEVEL} then <code>\assumes</code> must
+     * <li>{@link ApplicationRestriction#NONE} no state restrictions are posed</li>
+     * <li>{@link ApplicationRestriction#SAME_UPDATE_LEVEL} then <code>\assumes</code> must
      * match on
      * a
      * formula within the same state as <code>\find</code> rsp. <code>\add</code>. For efficiency no
      * modalities are allowed above the <code>\find</code> position</li>
-     * <li>{@link Taclet.ApplicationRestriction#IN_SEQUENT_STATE} the <code>\find</code> part is
+     * <li>{@link ApplicationRestriction#IN_SEQUENT_STATE} the <code>\find</code> part is
      * only
      * allowed to
      * match on formulas which are evaluated in the same state as the sequent</li>
      * </ul>
      */
-    protected Taclet.ApplicationRestriction applicationRestriction =
-        Taclet.ApplicationRestriction.NONE;
+    protected ApplicationRestriction applicationRestriction =
+        ApplicationRestriction.NONE;
 
     /**
      * checks that a SchemaVariable that is used to match pure variables (this means bound
@@ -57,7 +57,7 @@ public SyntaxElement getFind() {
     }
 
     public FindTacletBuilder<T> setApplicationRestriction(
-            Taclet.ApplicationRestriction p_applicationRestriction) {
+            ApplicationRestriction p_applicationRestriction) {
         applicationRestriction = p_applicationRestriction;
         return this;
     }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/NoFindTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/NoFindTacletBuilder.java
@@ -8,7 +8,7 @@
 import de.uka.ilkd.key.rule.NoFindTaclet;
 import de.uka.ilkd.key.rule.Taclet;
 
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 import org.key_project.prover.rules.TacletApplPart;
 
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/SuccTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/SuccTacletBuilder.java
@@ -7,7 +7,7 @@
 import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit;
 import de.uka.ilkd.key.rule.SuccTaclet;
 
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 import org.key_project.prover.rules.TacletApplPart;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentFormula;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java
@@ -26,7 +26,7 @@
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
 import org.key_project.prover.rules.RuleSet;
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 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/speclang/QueryAxiom.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java
@@ -28,7 +28,7 @@
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
 import org.key_project.prover.rules.RuleSet;
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 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/taclettranslation/DefaultTacletTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/DefaultTacletTranslator.java
@@ -18,7 +18,7 @@
 import de.uka.ilkd.key.rule.tacletbuilder.AntecSuccTacletGoalTemplate;
 import de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletGoalTemplate;
 
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 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.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/DefaultLemmaGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/DefaultLemmaGenerator.java
@@ -21,7 +21,7 @@
 import org.key_project.logic.op.Modality;
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
-import org.key_project.prover.rules.Taclet.ApplicationRestriction;
+import org.key_project.prover.rules.ApplicationRestriction;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableSet;
diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/ApplicationRestriction.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/ApplicationRestriction.java
@@ -0,0 +1,86 @@
+package org.key_project.prover.rules;
+
+/// Restricts where a taclet may be applied. Any combination of these restrictions in possible.
+public record ApplicationRestriction(int value) {
+    public ApplicationRestriction {
+        if ((value & ANTECEDENT_POLARITY) == ANTECEDENT_POLARITY
+                && (value & SUCCEDENT_POLARITY) == SUCCEDENT_POLARITY) {
+            throw new IllegalArgumentException(
+                    "Polarity cannot be antecedent and succedent at the same time");
+        }
+    }
+
+    /// does not pose state restrictions on valid matchings
+    public static final ApplicationRestriction NONE = new ApplicationRestriction(0);
+
+    /// all taclet constituents must appear in the same state (and not below a modality (for
+    /// efficiency reasons))
+    public static final int SAME_UPDATE_LEVEL = 1;
+
+    /// all taclet constituents must be in the same state as the sequent
+    public static final int IN_SEQUENT_STATE = 2;
+
+    /// If the surrounding formula has been decomposed completely, the find-term will NOT appear
+    /// on
+    /// the succedent. The formula `wellformed(h)` in `wellformed(h) ==>` or in
+    /// `==> wellformed(h) ->(inv(h) = inv(h2))` or in `==> \if(b) \then(!wellformed(h))
+    /// \else(!wellformed(h2))`
+    /// has
+    /// antecedent polarity. The formula `wellformed(h)` in
+    /// `wellformed(h) <-> wellformed(h2) ==>`
+    /// has NO antecedent polarity.
+    ///
+    /// If this flag is set, the rule matches **only** on positions with antecedent polarity.
+    public static final int ANTECEDENT_POLARITY = 4;
+
+    /// If the surrounding formula has been decomposed completely, the find-term will NOT appear
+    /// on
+    /// the antecedent. The formula `wellformed(h)` in `==> wellformed(h)` or in
+    /// `wellformed(h) ->(inv(h) = inv(h2)) ==>` or in
+    /// `\if(b) \then(!wellformed(h)) \else(!wellformed(h2)) ==>`
+    /// has
+    /// succedent polarity. The formula `wellformed(h)` in
+    /// `wellformed(h) <-> wellformed(h2) ==>` has
+    /// NO succedent polarity.
+    ///
+    /// If this flag is set, the rule matches **only** on positions with succedent polarity.
+    public static final int SUCCEDENT_POLARITY = 8;
+
+    /// @return `true` iff `this` and `o` have at least one common flag.
+    public boolean matches(ApplicationRestriction o) {
+        return (value() & o.value()) != 0;
+    }
+
+    /// @return `true` iff `this` and `value` have at least one common bit set to `1`.
+    public boolean matches(int value) {
+        return (value() & value) != 0;
+    }
+
+    /// @return a new restriction where all flags set by `this` or `restriction` are set.
+    public ApplicationRestriction combine(ApplicationRestriction restriction) {
+        return new ApplicationRestriction(this.value | restriction.value());
+    }
+
+    /// @return a new restriction where all flags set by `this` or `value` are set.
+    public ApplicationRestriction combine(int value) {
+        return new ApplicationRestriction(this.value | value);
+    }
+
+    @Override
+    public String toString() {
+        String res = "";
+        if (matches(SAME_UPDATE_LEVEL)) {
+            res += "\\sameUpdateLevel";
+        }
+        if (matches(IN_SEQUENT_STATE)) {
+            res += "\\inSequentState";
+        }
+        if (matches(ANTECEDENT_POLARITY)) {
+            res += "\\antecedentPolarity";
+        }
+        if (matches(SUCCEDENT_POLARITY)) {
+            res += "\\succedentPolarity";
+        }
+        return res;
+    }
+}
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
@@ -442,88 +442,4 @@ public ImmutableList<RuleSet> getRuleSets() {
         return ruleSets;
     }
 
-    /// Restricts where a taclet may be applied. Any combination of these restrictions in possible.
-    public record ApplicationRestriction(int value) {
-        public ApplicationRestriction {
-            if ((value & ANTECEDENT_POLARITY) == ANTECEDENT_POLARITY
-                    && (value & SUCCEDENT_POLARITY) == SUCCEDENT_POLARITY) {
-                throw new IllegalArgumentException(
-                    "Polarity cannot be antecedent and succedent at the same time");
-            }
-        }
-
-        /// does not pose state restrictions on valid matchings
-        public static final ApplicationRestriction NONE = new ApplicationRestriction(0);
-
-        /// all taclet constituents must appear in the same state (and not below a modality (for
-        /// efficiency reasons))
-        public static final int SAME_UPDATE_LEVEL = 1;
-
-        /// all taclet constituents must be in the same state as the sequent
-        public static final int IN_SEQUENT_STATE = 2;
-
-        /// If the surrounding formula has been decomposed completely, the find-term will NOT appear
-        /// on
-        /// the succedent. The formula `wellformed(h)` in `wellformed(h) ==>` or in
-        /// `==> wellformed(h) ->(inv(h) = inv(h2))` or in `==> \if(b) \then(!wellformed(h))
-        /// \else(!wellformed(h2))`
-        /// has
-        /// antecedent polarity. The formula `wellformed(h)` in
-        /// `wellformed(h) <-> wellformed(h2) ==>`
-        /// has NO antecedent polarity.
-        ///
-        /// If this flag is set, the rule matches **only** on positions with antecedent polarity.
-        public static final int ANTECEDENT_POLARITY = 4;
-
-        /// If the surrounding formula has been decomposed completely, the find-term will NOT appear
-        /// on
-        /// the antecedent. The formula `wellformed(h)` in `==> wellformed(h)` or in
-        /// `wellformed(h) ->(inv(h) = inv(h2)) ==>` or in
-        /// `\if(b) \then(!wellformed(h)) \else(!wellformed(h2)) ==>`
-        /// has
-        /// succedent polarity. The formula `wellformed(h)` in
-        /// `wellformed(h) <-> wellformed(h2) ==>` has
-        /// NO succedent polarity.
-        ///
-        /// If this flag is set, the rule matches **only** on positions with succedent polarity.
-        public static final int SUCCEDENT_POLARITY = 8;
-
-        /// @return `true` iff `this` and `o` have at least one common flag.
-        public boolean matches(ApplicationRestriction o) {
-            return (value() & o.value()) != 0;
-        }
-
-        /// @return `true` iff `this` and `value` have at least one common bit set to `1`.
-        public boolean matches(int value) {
-            return (value() & value) != 0;
-        }
-
-        /// @return a new restriction where all flags set by `this` or `restriction` are set.
-        public ApplicationRestriction combine(ApplicationRestriction restriction) {
-            return new ApplicationRestriction(this.value | restriction.value());
-        }
-
-        /// @return a new restriction where all flags set by `this` or `value` are set.
-        public ApplicationRestriction combine(int value) {
-            return new ApplicationRestriction(this.value | value);
-        }
-
-        @Override
-        public String toString() {
-            String res = "";
-            if (matches(SAME_UPDATE_LEVEL)) {
-                res += "\\sameUpdateLevel";
-            }
-            if (matches(IN_SEQUENT_STATE)) {
-                res += "\\inSequentState";
-            }
-            if (matches(ANTECEDENT_POLARITY)) {
-                res += "\\antecedentPolarity";
-            }
-            if (matches(SUCCEDENT_POLARITY)) {
-                res += "\\succedentPolarity";
-            }
-            return res;
-        }
-    }
 }
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
@@ -13,7 +13,7 @@
 /// application restrictions, a list of new
 /// variables and a list of variable pairs indicating the NotFreeIn relation, a list of
 /// NewDependingOn relations, and a list of general variable conditions.
-public record TacletApplPart(Sequent assumesSequent, Taclet.ApplicationRestriction restriction,
+public record TacletApplPart(Sequent assumesSequent, ApplicationRestriction restriction,
         ImmutableList<? extends NewVarcond> varsNew,
         ImmutableList<? extends NotFreeIn> varsNotFreeIn,
         ImmutableList<? extends NewDependingOn> varsNewDependingOn,
