Refactoring of InstantiationEntry classes

* reduced number of subclasses

key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java

@@ -210,7 +210,7 @@ private void checkNeededInputAvailable(int irow) throws MissingInstantiationExce
 
         final int icol = 1;
 
-        if ((getValueAt(irow, icol) == null || ((String) getValueAt(irow, icol)).length() == 0)
+        if ((getValueAt(irow, icol) == null || ((String) getValueAt(irow, icol)).isEmpty())
                 && !originalApp.complete()) {
             throw new MissingInstantiationException(String.valueOf(getValueAt(irow, 0)),
                 createPosition(irow),
@@ -222,7 +222,7 @@ private void checkNeededInputAvailable(int irow) throws MissingInstantiationExce
      * @return true iff this row is not empty (i.e. a string of data is available)
      */
     private boolean isInputAvailable(int irow) {
-        return getValueAt(irow, 1) != null && ((String) getValueAt(irow, 1)).length() != 0;
+        return getValueAt(irow, 1) != null && !((String) getValueAt(irow, 1)).isEmpty();
     }
 
     /**
@@ -305,7 +305,7 @@ private ProgramElement parseRow(int irow) throws SVInstantiationParserException
         String instantiation = (String) getValueAt(irow, 1);
         ProgramSV sv = (ProgramSV) getValueAt(irow, 0);
 
-        ContextInstantiationEntry contextInstantiation =
+        final ContextStatementBlockInstantiation contextInstantiation =
             originalApp.instantiations().getContextInstantiation();
 
         final PosInProgram prefix;

key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java

@@ -23,7 +23,7 @@
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.io.ProofSaver;
 import de.uka.ilkd.key.rule.TacletApp;
-import de.uka.ilkd.key.rule.inst.ContextInstantiationEntry;
+import de.uka.ilkd.key.rule.inst.ContextStatementBlockInstantiation;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 import de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletGoalTemplate;
 import de.uka.ilkd.key.util.MiscTools;
@@ -324,7 +324,7 @@ private String getBaseNameProposal(Type type) {
         } else {
             String name = type.getName();
             name = MiscTools.filterAlphabetic(name);
-            if (name.length() > 0) {
+            if (!name.isEmpty()) {
                 result = name.substring(0, 1).toLowerCase();
             } else {
                 result = "x"; // use default name otherwise
@@ -432,7 +432,7 @@ public ProgramElementName getTemporaryNameProposal(String basename) {
     public String getProposal(TacletApp app, SchemaVariable var, Services services, Node undoAnchor,
             ImmutableList<String> previousProposals) {
         // determine posOfDeclaration from TacletApp
-        ContextInstantiationEntry cie = app.instantiations().getContextInstantiation();
+        ContextStatementBlockInstantiation cie = app.instantiations().getContextInstantiation();
         PosInProgram posOfDeclaration = (cie == null ? null : cie.prefix());
 
         // determine a suitable base name

key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java

@@ -16,7 +16,6 @@
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.sort.ProgramSVSort;
 import de.uka.ilkd.key.rule.MatchConditions;
-import de.uka.ilkd.key.rule.inst.ProgramList;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 import de.uka.ilkd.key.speclang.HeapContext;
 
@@ -36,8 +35,8 @@ public final class ProgramSV extends OperatorSV
         implements ProgramConstruct, UpdateableOperator {
     public static final Logger LOGGER = LoggerFactory.getLogger(ProgramSV.class);
 
-    private static final ProgramList EMPTY_LIST_INSTANTIATION =
-        new ProgramList(new ImmutableArray<>(new ProgramElement[0]));
+    private static final ImmutableArray<ProgramElement> EMPTY_LIST_INSTANTIATION =
+        new ImmutableArray<>(new ProgramElement[0]);
 
     private final boolean isListSV;
 
@@ -256,14 +255,15 @@ private MatchConditions addProgramInstantiation(ProgramElement pe, MatchConditio
      * @return the updated match conditions including mapping <code>var</code> to <code>list</code>
      *         or null if some variable condition would be hurt by the mapping
      */
-    private MatchConditions addProgramInstantiation(ProgramList list, MatchConditions matchCond,
+    private MatchConditions addProgramInstantiation(ImmutableArray<ProgramElement> list,
+            MatchConditions matchCond,
             Services services) {
         if (matchCond == null) {
             return null;
         }
 
         SVInstantiations insts = matchCond.getInstantiations();
-        final ProgramList pl = (ProgramList) insts.getInstantiation(this);
+        final var pl = (ImmutableArray<ProgramElement>) insts.getInstantiation(this);
         if (pl != null) {
             if (pl.equals(list)) {
                 return matchCond;
@@ -272,7 +272,7 @@ private MatchConditions addProgramInstantiation(ProgramList list, MatchCondition
             }
         }
 
-        insts = insts.add(this, list, services);
+        insts = insts.add(this, list, ProgramElement.class, services);
         return insts == null ? null : matchCond.setInstantiations(insts);
     }
 
@@ -300,9 +300,7 @@ private MatchConditions matchListSV(SourceData source, MatchConditions matchCond
             src = source.getSource();
         }
 
-        return addProgramInstantiation(
-            new ProgramList(new ImmutableArray<>(matchedElements)), matchCond,
-            services);
+        return addProgramInstantiation(new ImmutableArray<>(matchedElements), matchCond, services);
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/proof/ITacletIndex.java

@@ -1,36 +1,41 @@
+/* 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.proof;
 
-import de.uka.ilkd.key.rule.NoPosTacletApp;
-import org.jspecify.annotations.Nullable;
 import de.uka.ilkd.key.proof.rulefilter.RuleFilter;
+import de.uka.ilkd.key.rule.NoPosTacletApp;
+
 import org.key_project.logic.LogicServices;
 import org.key_project.logic.Name;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.util.collection.ImmutableList;
 
+import org.jspecify.annotations.Nullable;
+
 public interface ITacletIndex {
     /**
      * get all Taclets for the antecedent.
      *
-     * @param pos      the PosOfOccurrence describing the formula for which to look for top level taclets
-     * @param filter   Only return taclets the filter selects
+     * @param pos the PosOfOccurrence describing the formula for which to look for top level taclets
+     * @param filter Only return taclets the filter selects
      * @param services the Services object encapsulating information about the java datastructures
-     *                 like (static)types etc.
+     *        like (static)types etc.
      * @return IList<NoPosTacletApp> containing all applicable rules and the corresponding
-     * instantiations to get the rule fit.
+     *         instantiations to get the rule fit.
      */
     ImmutableList<NoPosTacletApp> getAntecedentTaclet(
             PosInOccurrence pos, RuleFilter filter, LogicServices services);
 
     /**
      * get all Taclets for the succedent.
      *
-     * @param pos      the PosOfOccurrence describing the formula for which to look for top level taclets
-     * @param filter   Only return taclets the filter selects
+     * @param pos the PosOfOccurrence describing the formula for which to look for top level taclets
+     * @param filter Only return taclets the filter selects
      * @param services the Services object encapsulating information about the java datastructures
-     *                 like (static)types etc.
+     *        like (static)types etc.
      * @return IList<NoPosTacletApp> containing all applicable rules and the corresponding
-     * instantiations to get the rule fit.
+     *         instantiations to get the rule fit.
      */
     ImmutableList<NoPosTacletApp> getSuccedentTaclet(
             PosInOccurrence pos, RuleFilter filter,
@@ -39,23 +44,23 @@ ImmutableList<NoPosTacletApp> getSuccedentTaclet(
     /**
      * get all Rewrite-Taclets.
      *
-     * @param filter   Only return taclets the filter selects
+     * @param filter Only return taclets the filter selects
      * @param services the Services object encapsulating information about the java datastructures
-     *                 like (static)types etc.
+     *        like (static)types etc.
      * @return IList<NoPosTacletApp> containing all applicable rules and the corresponding
-     * instantiations to get the rule fit.
+     *         instantiations to get the rule fit.
      */
     ImmutableList<NoPosTacletApp> getRewriteTaclet(PosInOccurrence pos, RuleFilter filter,
-                                                   LogicServices services);
+            LogicServices services);
 
     /**
      * get all Taclets having no find expression.
      *
-     * @param filter   Only return taclets the filter selects
+     * @param filter Only return taclets the filter selects
      * @param services the Services object encapsulating information about the java datastructures
-     *                 like (static)types etc.
+     *        like (static)types etc.
      * @return IList<NoPosTacletApp> containing all applicable rules and an empty part for the
-     * instantiations because no instantiations are necessary.
+     *         instantiations because no instantiations are necessary.
      */
     ImmutableList<NoPosTacletApp> getNoFindTaclet(RuleFilter filter, LogicServices services);
 
@@ -67,13 +72,13 @@ ImmutableList<NoPosTacletApp> getRewriteTaclet(PosInOccurrence pos, RuleFilter f
      */
     ImmutableList<NoPosTacletApp> getPartialInstantiatedApps();
 
-        /**
-         * returns a NoPosTacletApp whose Taclet has a name that equals the given name. If more Taclets
-         * have the same name an arbitrary Taclet with that name is returned.
-         *
-         * @param name the name to lookup
-         * @return the found NoPosTacletApp or null if no matching Taclet is there
-         */
+    /**
+     * returns a NoPosTacletApp whose Taclet has a name that equals the given name. If more Taclets
+     * have the same name an arbitrary Taclet with that name is returned.
+     *
+     * @param name the name to lookup
+     * @return the found NoPosTacletApp or null if no matching Taclet is there
+     */
     NoPosTacletApp lookup(Name name);
 
     /**

key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java

@@ -26,7 +26,6 @@
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.rule.Taclet;
 import de.uka.ilkd.key.rule.TacletApp;
-import de.uka.ilkd.key.rule.inst.TermInstantiation;
 
 import org.key_project.logic.Name;
 import org.key_project.proof.LocationVariableTracker;
@@ -241,8 +240,7 @@ public static boolean isSymbolicExecution(Taclet t) {
         RuleSet rs;
         while (!list.isEmpty()) {
             rs = list.head();
-            Name name = rs.name();
-            if (symbolicExecNames.contains(name)) {
+            if (symbolicExecNames.contains(rs.name())) {
                 return true;
             }
             list = list.tail();
@@ -335,10 +333,6 @@ public void setBranchLabel(String s) {
                     if (val instanceof Term) {
                         val = TermLabelManager.removeIrrelevantLabels((Term) val,
                             node.proof().getServices());
-                    } else if (val instanceof TermInstantiation) {
-                        val = TermLabelManager.removeIrrelevantLabels(
-                            ((TermInstantiation) val).getInstantiation(),
-                            node.proof().getServices());
                     } else if (val instanceof LocationVariable locVar) {
                         var originTracker = node.proof().lookup(LocationVariableTracker.class);
                         if (originTracker != null) {

key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java

@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof;
 
-import java.util.Iterator;
 import java.util.Map;
 
 import de.uka.ilkd.key.java.ProgramElement;
@@ -18,7 +17,8 @@
 import de.uka.ilkd.key.rule.inst.*;
 
 import org.key_project.logic.PosInTerm;
-import org.key_project.logic.op.sv.SchemaVariable;
+import org.key_project.prover.rules.inst.InstantiationEntry;
+import org.key_project.prover.rules.inst.ListInstantiation;
 import org.key_project.prover.sequent.*;
 import org.key_project.util.collection.*;
 
@@ -100,29 +100,26 @@ public void replace(TacletIndex tacletIndex) {
     public SVInstantiations replace(SVInstantiations insts) {
         SVInstantiations result = insts;
 
-        Iterator<ImmutableMapEntry<SchemaVariable, InstantiationEntry<?>>> it;
         for (var e : insts.getInstantiationMap()) {
             var sv = e.key();
             InstantiationEntry<?> ie = e.value();
             Object inst = ie.getInstantiation();
 
-            if (ie instanceof ContextInstantiationEntry) {
+            if (inst instanceof ContextStatementBlockInstantiation cie) {
                 ProgramElement pe = (ProgramElement) inst;
                 ProgramElement newPe = replace(pe);
                 if (newPe != pe) {
-                    ContextInstantiationEntry cie = (ContextInstantiationEntry) ie;
                     result = result.replace(cie.prefix(), cie.suffix(),
                         cie.activeStatementContext(), newPe, services);
                 }
-            } else if (ie instanceof OperatorInstantiation) {
+            } else if (ie instanceof org.key_project.logic.op.Operator) {
                 /* nothing to be done (currently) */
-            } else if (ie instanceof ProgramInstantiation) {
-                ProgramElement pe = (ProgramElement) inst;
+            } else if (ie instanceof ProgramElement pe) {
                 ProgramElement newPe = replace(pe);
                 if (newPe != pe) {
                     result = result.replace(sv, newPe, services);
                 }
-            } else if (ie instanceof ProgramListInstantiation) {
+            } else if (ie instanceof ListInstantiation) {
                 @SuppressWarnings("unchecked")
                 ImmutableArray<ProgramElement> a = (ImmutableArray<ProgramElement>) inst;
                 int size = a.size();
@@ -140,9 +137,8 @@ public SVInstantiations replace(SVInstantiations insts) {
                 if (changedSomething) {
                     result = result.replace(sv, new ImmutableArray<>(array), services);
                 }
-            } else if (ie instanceof TermInstantiation) {
-                Term t = (Term) inst;
-                Term newT = replace(t);
+            } else if (inst instanceof Term t) {
+                final Term newT = replace(t);
                 if (newT != t) {
                     result = result.replace(sv, newT, services);
                 }

key.core/src/main/java/de/uka/ilkd/key/proof/VariableNameProposer.java

@@ -199,7 +199,7 @@ private String getNameProposalForLabel(TacletApp app, SchemaVariable var, Servic
             Node undoAnchor, ImmutableList<String> previousProposals) {
 
         ProgramElement contextProgram =
-            app.matchConditions().getInstantiations().getContextInstantiation().contextProgram();
+            app.matchConditions().getInstantiations().getContextInstantiation().program();
 
         if (contextProgram == null) {
             contextProgram = new StatementBlock();

key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java

@@ -32,7 +32,6 @@
 import de.uka.ilkd.key.proof.reference.CopyReferenceResolver;
 import de.uka.ilkd.key.rule.*;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
-import de.uka.ilkd.key.rule.inst.TermInstantiation;
 import de.uka.ilkd.key.rule.merge.CloseAfterMergeRuleBuiltInRuleApp;
 import de.uka.ilkd.key.rule.merge.MergeProcedure;
 import de.uka.ilkd.key.rule.merge.MergeRuleBuiltInRuleApp;
@@ -53,6 +52,7 @@
 import org.key_project.prover.rules.AssumesFormulaInstSeq;
 import org.key_project.prover.rules.AssumesFormulaInstantiation;
 import org.key_project.prover.rules.RuleApp;
+import org.key_project.prover.rules.inst.InstantiationEntry;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentFormula;
@@ -848,8 +848,8 @@ public static String printAnything(Object val, Services services,
             return printSequent((Sequent) val, services);
         } else if (val instanceof Name) {
             return val.toString();
-        } else if (val instanceof TermInstantiation) {
-            return printTerm(((TermInstantiation) val).getInstantiation(), services);
+        } else if (val instanceof InstantiationEntry<?> entry) {
+            return printAnything(entry.getInstantiation(), services);
         } else if (val == null) {
             return null;
         } else {

key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java

@@ -13,7 +13,7 @@
 import de.uka.ilkd.key.logic.*;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.proof.Goal;
-import de.uka.ilkd.key.rule.inst.ContextInstantiationEntry;
+import de.uka.ilkd.key.rule.inst.ContextStatementBlockInstantiation;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 import de.uka.ilkd.key.strategy.quantifierHeuristics.ConstraintAwareSyntacticalReplaceVisitor;
 
@@ -22,13 +22,18 @@
 import org.key_project.util.collection.ImmutableArray;
 
 /**
+ * <p>
  * A lightweight version of {@link SyntacticalReplaceVisitor} which does not replace labels. This
- * saves a lot of dependencies to {@link Goal}, {@link RuleApp}, {@link PosInOccurrence} etc. and is
- * therefore useful for internal computations not having access to all these objects. Since labels
+ * saves a lot of dependencies to {@link Goal}, {@link RuleApp},
+ * {@link org.key_project.prover.sequent.PosInOccurrence}
+ * etc. and is therefore useful for internal computations not having access to all these objects.
+ * Since labels
  * are not refactored, this class is *not* useful for rule applications etc.
- *
+ * </p>
+ * <p>
  * Note that this class is basically a stripped-down copy of {@link SyntacticalReplaceVisitor}, so
  * problems in that class would carry over to this one...
+ * </p>
  *
  * @author Dominic Steinhoefel
  */
@@ -67,14 +72,14 @@ public LightweightSyntacticalReplaceVisitor(Services services) {
     }
 
     private JavaProgramElement addContext(StatementBlock pe) {
-        final ContextInstantiationEntry cie = svInst.getContextInstantiation();
+        final ContextStatementBlockInstantiation cie = svInst.getContextInstantiation();
         if (cie == null) {
             throw new IllegalStateException("Context should also be instantiated");
         }
 
         if (cie.prefix() != null) {
             return ProgramContextAdder.INSTANCE.start(
-                (JavaNonTerminalProgramElement) cie.contextProgram(), pe, cie.getInstantiation());
+                (JavaNonTerminalProgramElement) cie.program(), pe, cie);
         }
 
         return pe;