diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java index bc3170f32af..51097fd1be5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java +++ b/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; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java b/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java index ccc298c17fa..e09b0d96e49 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java +++ b/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 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 diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java index fd547c8403e..22792e4628b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java +++ b/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 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 var to list * or null if some variable condition would be hurt by the mapping */ - private MatchConditions addProgramInstantiation(ProgramList list, MatchConditions matchCond, + private MatchConditions addProgramInstantiation(ImmutableArray 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) 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); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/ITacletIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/ITacletIndex.java index 6be8b8cdb01..f042cf65d05 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/ITacletIndex.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/ITacletIndex.java @@ -1,23 +1,28 @@ +/* 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 containing all applicable rules and the corresponding - * instantiations to get the rule fit. + * instantiations to get the rule fit. */ ImmutableList getAntecedentTaclet( PosInOccurrence pos, RuleFilter filter, LogicServices services); @@ -25,12 +30,12 @@ ImmutableList getAntecedentTaclet( /** * 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 containing all applicable rules and the corresponding - * instantiations to get the rule fit. + * instantiations to get the rule fit. */ ImmutableList getSuccedentTaclet( PosInOccurrence pos, RuleFilter filter, @@ -39,23 +44,23 @@ ImmutableList 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 containing all applicable rules and the corresponding - * instantiations to get the rule fit. + * instantiations to get the rule fit. */ ImmutableList 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 containing all applicable rules and an empty part for the - * instantiations because no instantiations are necessary. + * instantiations because no instantiations are necessary. */ ImmutableList getNoFindTaclet(RuleFilter filter, LogicServices services); @@ -67,13 +72,13 @@ ImmutableList getRewriteTaclet(PosInOccurrence pos, RuleFilter f */ ImmutableList 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); /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java b/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java index 02805bba241..aaaca8b971f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java +++ b/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) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java index 86a0a0d3627..dd54cebcfd3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java +++ b/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>> 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 a = (ImmutableArray) 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); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/VariableNameProposer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/VariableNameProposer.java index 682a9862012..97ef78aa44e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/VariableNameProposer.java +++ b/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 previousProposals) { ProgramElement contextProgram = - app.matchConditions().getInstantiations().getContextInstantiation().contextProgram(); + app.matchConditions().getInstantiations().getContextInstantiation().program(); if (contextProgram == null) { contextProgram = new StatementBlock(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 79eb326fc84..cda65ce87dd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/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 { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java index 9aa2a2eedd5..9023fa1229d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java +++ b/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; /** + *

* 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. - * + *

+ *

* Note that this class is basically a stripped-down copy of {@link SyntacticalReplaceVisitor}, so * problems in that class would carry over to this one... + *

* * @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; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java index 4c94d2204a4..046a27cf5ac 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java @@ -54,7 +54,7 @@ public static NoPosTacletApp createNoPosTacletApp(Taclet taclet) { /** * creates a NoPosTacletApp for the given taclet with some known instantiations and CHECKS * variable conditions as well as it resolves collisions The ifInstantiations parameter is not - * matched against the if sequence, but only stored. For matching use the method + * matched against the assumes-sequence, but only stored. For matching use the method * "setIfFormulaInstantiations". * * @param taclet the Taclet @@ -136,8 +136,7 @@ private NoPosTacletApp(org.key_project.prover.rules.Taclet taclet, */ protected static boolean checkVarCondNotFreeIn(org.key_project.prover.rules.Taclet taclet, SVInstantiations instantiations) { - for (var pair : ((de.uka.ilkd.key.rule.inst.SVInstantiations) instantiations) - .getInstantiationMap()) { + for (var pair : instantiations.getInstantiationMap()) { final var sv = pair.key(); if (sv instanceof ModalOperatorSV || sv instanceof ProgramSV || sv instanceof VariableSV @@ -182,29 +181,11 @@ public TacletApp addInstantiation(SchemaVariable sv, Term term, boolean interest } } - - - @Override - public TacletApp addInstantiation(SchemaVariable sv, Object[] list, boolean interesting, - Services services) { - if (interesting) { - return createNoPosTacletApp(taclet(), - instantiations().addInterestingList(sv, list, services), - assumesFormulaInstantiations(), - services); - } else { - return createNoPosTacletApp(taclet(), instantiations().addList(sv, list, services), - assumesFormulaInstantiations(), services); - } - } - - - /** * adds a new instantiation to this TacletApp * * @param sv the SchemaVariable to be instantiated - * @param pe the ProgramElement the SV is instantiated with + * @param pe the ProgramElement with which the SV is instantiated * @return the new TacletApp */ @Override @@ -272,9 +253,9 @@ protected TacletApp setAllInstantiations(org.key_project.prover.rules.MatchCondi /** - * returns true iff all necessary informations are collected, so that the Taclet can be applied. + * returns true iff all necessary information is collected, so that the Taclet can be applied. * - * @return true iff all necessary informations are collected, so that the Taclet can be applied. + * @return true iff all necessary information is collected, so that the Taclet can be applied. */ @Override public boolean complete() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java index da44e1adfca..40040237659 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java @@ -39,13 +39,13 @@ public class PosTacletApp extends TacletApp { /** * creates a PosTacletApp for the given taclet with some known instantiations and a position * information and CHECKS variable conditions as well as it resolves collisions The - * ifInstantiations parameter is not matched against the if sequence, but only stored. For - * matching use the method "setIfFormulaInstantiations". + * ifInstantiations parameter is not matched against the assumes-sequence, but only stored. For + * matching use the method "setAssumesFormulaInstantiations". * * @param taclet the FindTaclet * @param instantiations the SVInstantiations * @param pos the PosInOccurrence storing the position where to apply the Taclet - * @return new PosTacletApp or null if conditions (assertions) have been hurted + * @return new PosTacletApp or null if conditions (assertions) have been hurt */ public static PosTacletApp createPosTacletApp(FindTaclet taclet, SVInstantiations instantiations, PosInOccurrence pos, Services services) { @@ -73,18 +73,6 @@ public static PosTacletApp createPosTacletApp(FindTaclet taclet, MatchConditions return createPosTacletApp(taclet, matchCond.getInstantiations(), null, pos, services); } - - /** - * creates a PosTacletApp for the given taclet and a position information - * - * @param taclet the FindTaclet - * @param pos the PosInOccurrence storing the position where to apply the Taclet - */ - private PosTacletApp(FindTaclet taclet, PosInOccurrence pos) { - super(taclet); - this.pos = pos; - } - /** * creates a PosTacletApp for the given taclet with some known instantiations and a position * information @@ -199,25 +187,6 @@ public TacletApp addInstantiation(SchemaVariable sv, ProgramElement pe, boolean } } - - - @Override - public TacletApp addInstantiation(SchemaVariable sv, Object[] list, boolean interesting, - Services services) { - if (interesting) { - return createPosTacletApp((FindTaclet) taclet(), - instantiations().addInterestingList(sv, list, services), - assumesFormulaInstantiations(), - posInOccurrence(), services); - } else { - return createPosTacletApp((FindTaclet) taclet(), - instantiations().addList(sv, list, services), assumesFormulaInstantiations(), - posInOccurrence(), services); - } - } - - - /** * creates a new Taclet application containing all the instantiations given by the * SVInstantiations and the ones of this TacletApp @@ -272,9 +241,9 @@ protected TacletApp setAllInstantiations(org.key_project.prover.rules.MatchCondi /** - * returns true iff all necessary informations are collected, so that the Taclet can be applied. + * returns true iff all necessary information is collected, so that the Taclet can be applied. * - * @return true iff all necessary informations are collected, so that the Taclet can be applied. + * @return true iff all necessary information is collected, so that the Taclet can be applied. */ @Override public boolean complete() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java index 6f9b9137fe7..eddd838cc2c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java @@ -22,7 +22,7 @@ import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.rule.Taclet.TacletLabelHint; -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; @@ -170,14 +170,14 @@ public SyntacticalReplaceVisitor(TermLabelState termLabelState, SVInstantiations } 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; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java index a5614168b9f..bc4e1db2899 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java @@ -726,9 +726,6 @@ private void registerSkolemConstants(Namespace<@NonNull Function> fns) { public abstract TacletApp addInstantiation(SchemaVariable sv, Term term, boolean interesting, Services services); - public abstract TacletApp addInstantiation(SchemaVariable sv, Object[] list, - boolean interesting, Services services); - /** * adds a new instantiation to this TacletApp. This method does not check (beside some very * rudimentary tests) if the instantiation is possible. If you cannot guarantee that adding the diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java index ccb04c8efb2..e8801aa8857 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java @@ -54,7 +54,7 @@ public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, } final JavaBlock javaBlock = JavaBlock.createJavaBlock( - (StatementBlock) svInst.getContextInstantiation().contextProgram()); + (StatementBlock) svInst.getContextInstantiation().program()); final MethodFrame mf = // JavaTools.getInnermostMethodFrame(javaBlock, services); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java index 8f66b36e354..76b4532b67b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java @@ -42,7 +42,7 @@ public MatchConditions check(SchemaVariable sv, SyntaxElement instCandidate, final ArrayList labels = new ArrayList<>(); ProgramPrefix prefix = // - (ProgramPrefix) svInst.getContextInstantiation().contextProgram(); + (ProgramPrefix) svInst.getContextInstantiation().program(); do { if (prefix instanceof LabeledStatement && ((LabeledStatement) prefix).getBody().equals(stmt)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java index e03b910dc6b..80665d30144 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java @@ -63,7 +63,7 @@ public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, } final JavaBlock javaBlock = JavaBlock.createJavaBlock( - (StatementBlock) svInst.getContextInstantiation().contextProgram()); + (StatementBlock) svInst.getContextInstantiation().program()); final MethodFrame mf = // JavaTools.getInnermostMethodFrame(javaBlock, services); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java index ee7fb063262..49c0262b051 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java @@ -63,7 +63,7 @@ public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, } final JavaBlock javaBlock = JavaBlock.createJavaBlock( - (StatementBlock) svInst.getContextInstantiation().contextProgram()); + (StatementBlock) svInst.getContextInstantiation().program()); final MethodFrame mf = // JavaTools.getInnermostMethodFrame(javaBlock, services); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java index fd0ef7cd0d9..0a3affe4f30 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java @@ -53,7 +53,7 @@ public MatchConditions check(SchemaVariable var, return null; } final List programs = collect(instantiations); - programs.add(instantiations.getContextInstantiation().contextProgram()); + programs.add(instantiations.getContextInstantiation().program()); if (!isUnique((Label) instCandidate, programs, services)) { return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ContextInstantiationEntry.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ContextInstantiationEntry.java deleted file mode 100644 index e69bfcc8038..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ContextInstantiationEntry.java +++ /dev/null @@ -1,71 +0,0 @@ -/* 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.inst; - -import de.uka.ilkd.key.java.ProgramElement; -import de.uka.ilkd.key.java.reference.ExecutionContext; -import de.uka.ilkd.key.logic.PosInProgram; - -/** - * This class is used to store the information about a matched context of a dl formula. (the pi and - * omega part) TODO: Check if there is a need for ContextStatementBlockInstantiation or if it could - * be unified with this class - */ -public class ContextInstantiationEntry - extends InstantiationEntry { - - /** - * creates a new ContextInstantiationEntry - * - * @param pi the PosInProgram describing the position of the first statement after the prefix - * @param omega the PosInProgram describing the position of the statement just before the suffix - * starts - * @param activeStatementContext the ExecutionContext of the first active statement - * @param pe the ProgramElement the context positions are related to - */ - ContextInstantiationEntry(PosInProgram pi, PosInProgram omega, - ExecutionContext activeStatementContext, ProgramElement pe) { - super(new ContextStatementBlockInstantiation(pi, omega, activeStatementContext, pe)); - } - - /** - * returns the position of the first statement after the prefix - * - * @return the position of the first statement after the prefix - */ - public PosInProgram prefix() { - return getInstantiation().prefix(); - } - - - /** - * returns the position of the statement just before the suffix starts - * - * @return the position of the statement just before the suffix starts - */ - public PosInProgram suffix() { - return getInstantiation().suffix(); - } - - /** - * returns the context program with an ignorable part between prefix and suffix position - */ - public ProgramElement contextProgram() { - return getInstantiation().programElement(); - } - - /** - * returns the execution context of the first active statement or null if match is performed - * outer most - */ - public ExecutionContext activeStatementContext() { - return getInstantiation().activeStatementContext(); - } - - /** toString */ - public String toString() { - return "[\npi:" + prefix() + "\nomega:" + suffix() + "\n]"; - } - -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ContextStatementBlockInstantiation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ContextStatementBlockInstantiation.java index cdade6886b7..72ea61ea0c6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ContextStatementBlockInstantiation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ContextStatementBlockInstantiation.java @@ -71,7 +71,7 @@ public ExecutionContext activeStatementContext() { * * @return returns the program element this context term instantiation refers to */ - public ProgramElement programElement() { + public ProgramElement program() { return programElement; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java index f1cddede647..9573c92d4a4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java @@ -5,12 +5,14 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.op.OperatorSV; -import de.uka.ilkd.key.logic.op.SortDependingFunction; import de.uka.ilkd.key.logic.op.TermSV; import de.uka.ilkd.key.logic.sort.ArraySort; import de.uka.ilkd.key.logic.sort.GenericSort; +import org.key_project.logic.Term; +import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; +import org.key_project.prover.rules.inst.InstantiationEntry; /** @@ -30,39 +32,23 @@ public abstract class GenericSortCondition { * sorts that don't match) */ public static GenericSortCondition createCondition( - org.key_project.logic.op.sv.SchemaVariable sv, + SchemaVariable sv, InstantiationEntry p_entry) { - if (!(p_entry instanceof TermInstantiation ti)) { + if (!(p_entry.getInstantiation() instanceof Term instantiation)) { return null; } - return createCondition(((OperatorSV) sv).sort(), ti.getInstantiation().sort(), + return createCondition(((OperatorSV) sv).sort(), instantiation.sort(), !subSortsAllowed(sv)); } - /** - * Create a condition ensuring that the two given symbols become identical; "p0" may be of - * generic sort, "p1" not - * - * @return the resulting condition; null if the symbols are either incompatible or equal - */ - public static GenericSortCondition createCondition(SortDependingFunction p0, - SortDependingFunction p1) { - - if (!p0.isSimilar(p1)) { - return null; - } - - return createCondition(p0.getSortDependingOn(), p1.getSortDependingOn(), true); - } - /** * @return true iff the variable p_sv is allowed to be instantiated * with expressions that have a real subtype of the type of p_sv. Otherwise * the sorts have to match exactly */ - static boolean subSortsAllowed(org.key_project.logic.op.sv.SchemaVariable p_sv) { + static boolean subSortsAllowed(SchemaVariable p_sv) { return p_sv instanceof TermSV && !p_sv.isStrict(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java index 99f178f45aa..939f9ad9b2b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java @@ -16,6 +16,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.op.sv.OperatorSV; import org.key_project.logic.sort.Sort; +import org.key_project.prover.rules.inst.InstantiationEntry; import org.key_project.util.collection.DefaultImmutableMap; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableMap; @@ -23,7 +24,6 @@ import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; - /** * This class handles the instantiation of generic sorts (used for generic taclets), i.e. the class * tries to find a solution for the conditions on the generic sorts given by the type hierarchy and @@ -31,7 +31,6 @@ * * this class is immutable */ - public final class GenericSortInstantiations { public static final GenericSortInstantiations EMPTY_INSTANTIATIONS = @@ -108,7 +107,7 @@ public static GenericSortInstantiations create(ImmutableList p_sort * choosing the right generic sort instantiations */ public Boolean checkSorts(OperatorSV sv, InstantiationEntry p_entry) { - if (!(p_entry instanceof TermInstantiation) || sv instanceof ProgramSV) { + if (sv instanceof ProgramSV || !(p_entry.getInstantiation() instanceof Term term)) { return Boolean.TRUE; } @@ -117,8 +116,6 @@ public Boolean checkSorts(OperatorSV sv, InstantiationEntry p_entry) { return checkCondition(c); } - final Term term = ((TermInstantiation) p_entry).getInstantiation(); - if (GenericSortCondition.subSortsAllowed(sv)) { return term.sort().extendsTrans(sv.sort()); } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ListInstantiation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ListInstantiation.java deleted file mode 100644 index 31216d0e35f..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ListInstantiation.java +++ /dev/null @@ -1,21 +0,0 @@ -/* 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.inst; - - -import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.util.collection.ImmutableList; - -public class ListInstantiation extends InstantiationEntry> { - - /** - * creates a new ContextInstantiationEntry - * - * @param sv the SchemaVariable that is instantiated - * @param pes the List the SchemaVariable is instantiated with - */ - ListInstantiation(SchemaVariable sv, ImmutableList pes) { - super(pes); - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/NameInstantiationEntry.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/NameInstantiationEntry.java deleted file mode 100644 index abcbea7ce5a..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/NameInstantiationEntry.java +++ /dev/null @@ -1,16 +0,0 @@ -/* 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.inst; - -import org.key_project.logic.Name; - -/** - * This class is used to store the instantiation of a schemavarible if it is a name. - */ -public class NameInstantiationEntry extends InstantiationEntry { - - NameInstantiationEntry(Name name) { - super(name); - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/OperatorInstantiation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/OperatorInstantiation.java deleted file mode 100644 index 84121b7e1b2..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/OperatorInstantiation.java +++ /dev/null @@ -1,22 +0,0 @@ -/* 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.inst; - -import de.uka.ilkd.key.logic.op.Operator; - -/** - * This class is used to store the instantiation of a schemavarible if it is an operator. - */ -public class OperatorInstantiation extends InstantiationEntry { - - /** - * creates a new ContextInstantiationEntry - * - * @param op the Operator the SchemaVariable is instantiated with - */ - OperatorInstantiation(Operator op) { - super(op); - } - -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramInstantiation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramInstantiation.java deleted file mode 100644 index 2c66871a070..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramInstantiation.java +++ /dev/null @@ -1,21 +0,0 @@ -/* 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.inst; - -import de.uka.ilkd.key.java.ProgramElement; - -/** - * This class is used to store the instantiation of a schemavarible if it is a ProgramElement. - */ -public class ProgramInstantiation extends InstantiationEntry { - - /** - * creates a new ContextInstantiationEntry - * - * @param pe the ProgramElement the SchemaVariable is instantiated with - */ - ProgramInstantiation(ProgramElement pe) { - super(pe); - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramList.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramList.java deleted file mode 100644 index e5f38ccbc06..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramList.java +++ /dev/null @@ -1,47 +0,0 @@ -/* 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.inst; - -import de.uka.ilkd.key.java.ProgramElement; - -import org.key_project.logic.SyntaxElement; -import org.key_project.util.collection.ImmutableArray; - -public class ProgramList implements SyntaxElement { - - private final ImmutableArray list; - - - public ProgramList(ImmutableArray list) { - assert list != null - : "Constructor of ProgramList must" + " not be called with null argument"; - this.list = list; - } - - public ImmutableArray getList() { - return list; - } - - public boolean equals(Object o) { - if (!(o instanceof ProgramList)) { - return false; - } - return list.equals(((ProgramList) o).list); - } - - public int hashCode() { - return list.hashCode(); - } - - - @Override - public SyntaxElement getChild(int n) { - return list.get(n); - } - - @Override - public int getChildCount() { - return list.size(); - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramSVEntry.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramSVEntry.java deleted file mode 100644 index 569984d8f83..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramSVEntry.java +++ /dev/null @@ -1,82 +0,0 @@ -/* 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.inst; - -import java.io.Serializable; - -import de.uka.ilkd.key.java.JavaProgramElement; - -import org.key_project.logic.op.sv.SchemaVariable; - -/** - * this class encapsulates a SchemaVariable and its corresponding instantiation if it is a - * JavaProgramElement. The class MapFrom...cannot be used because of the different packages of the - * SchemaVariable and the JavaProgramElement. - */ -public class ProgramSVEntry implements Serializable { - - /** - * - */ - private static final long serialVersionUID = -5837249343101979072L; - /** the SchemaVariable */ - private final SchemaVariable key; - /** the JavaProgramElement */ - private final JavaProgramElement value; - - /** - * creates a new entry encapsulating the SchemaVariable key and its JavaProgramElement - * instantiation value - * - * @param key the SchemaVariable that is instantiated - * @param value the JavaProgramElement - */ - public ProgramSVEntry(SchemaVariable key, JavaProgramElement value) { - this.key = key; - this.value = value; - } - - /** - * returns the SchemaVariable to be instantiated - * - * @return the SchemaVariable to be instantiated - */ - public SchemaVariable key() { - return key; - } - - /** - * returns true iff the keys and the mapped values are equal - * - * @return true iff the keys and the mapped values are equal - */ - public boolean equals(Object o) { - if (!(o instanceof ProgramSVEntry cmp)) { - return false; - } - return key().equals(cmp.key()) && value().equals(cmp.value()); - } - - public int hashCode() { - int result = 17; - result = 37 * result + key().hashCode(); - result = 37 * result + value().hashCode(); - return result; - } - - /** - * returns the instantiation of the SchemaVariable - * - * @return the instantiation of the SchemaVariable - */ - public JavaProgramElement value() { - return value; - } - - /** toString */ - public String toString() { - return "{" + key + "<--" + value + "}"; - } - -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramSVInstantiation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramSVInstantiation.java deleted file mode 100644 index de3ac082238..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramSVInstantiation.java +++ /dev/null @@ -1,173 +0,0 @@ -/* 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.inst; - -import java.util.Iterator; - -import de.uka.ilkd.key.java.JavaProgramElement; - -import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.util.collection.ImmutableList; -import org.key_project.util.collection.ImmutableSLList; - - -/** - * this class wrapps an {@link ImmutableList} and is used to store instantiations - * of schemavariables. The class is immutable, this means changing its content will result in - * creating a new object. - */ -public class ProgramSVInstantiation { - - /** the empty instantiation */ - public static final ProgramSVInstantiation EMPTY_PROGRAMSVINSTANTIATION = - new ProgramSVInstantiation(); - - /** the map with the instantiations */ - private ImmutableList list = ImmutableSLList.nil(); - - /** integer to cache the hashcode */ - private int hashcode = 0; - - - /** creates a new ProgramSVInstantiation object with an empty list */ - private ProgramSVInstantiation() { - } - - /** - * creates a new ProgramSVInstantiation object using the given list - * - * @param list the ListFromSchemaVariableToJavaProgramElement with the instantiations - */ - private ProgramSVInstantiation(ImmutableList list) { - this.list = list; - } - - /** - * adds the given pair to the instantiations. If the given SchemaVariable has been instantiated - * already, the new pair is taken without a warning. - * - * @param sv the SchemaVariable to be instantiated - * @param prgElement the JavaProgramElement The SchemaVariable is instantiated with - * @return ProgramSVInstantiation the new ProgramSVInstantiation containing the given pair - */ - public ProgramSVInstantiation add(SchemaVariable sv, JavaProgramElement prgElement) { - if (!isInstantiated(sv)) { - return new ProgramSVInstantiation(list.prepend(new ProgramSVEntry(sv, prgElement))); - } else { - return replace(sv, prgElement); - } - } - - /** - * replaces the given pair in the instantiations. If the given SchemaVariable has been - * instantiated already, the new pair is taken without a warning. - * - * @param sv the SchemaVariable to be instantiated - * @param prgElement the JavaProgramElement The SchemaVariable is instantiated with - * @return ProgramSVInstantiation the new ProgramSVInstantiation containing the given pair - */ - public ProgramSVInstantiation replace(SchemaVariable sv, JavaProgramElement prgElement) { - ImmutableList result = - ImmutableSLList.nil().prepend(new ProgramSVEntry(sv, prgElement)); - for (final ProgramSVEntry entry : list) { - if (entry.key() != sv) { - result = result.prepend(entry); - } - } - return new ProgramSVInstantiation(result); - } - - /** - * returns true iff the sv has been instantiated already - * - * @return true iff the sv has been instantiated already - */ - public boolean isInstantiated(SchemaVariable sv) { - for (ProgramSVEntry entry : list) { - if (entry.key() == sv) { - return true; - } - } - return false; - } - - /** - * returns the instantiation of the given SchemaVariable - * - * @return the JavaProgramElement the SchemaVariable will be instantiated with, null if no - * instantiation is stored - */ - public JavaProgramElement getInstantiation(SchemaVariable sv) { - for (ProgramSVEntry entry : list) { - if (entry.key() == sv) { - return entry.value(); - } - } - return null; - } - - - /** - * returns iterator of the listped pair (SchemaVariables, JavaProgramElement) - * - * @return the Iterator - */ - public Iterator iterator() { - return list.iterator(); - } - - /** - * returns the number of SchemaVariables of which an instantiation is known - * - * @return int that is the number of SchemaVariables of which an instantiation is known - */ - public int size() { - return list.size(); - } - - /** - * returns true if the given object and this one have the same listpings - * - * @return true if the given object and this one have the same listpings - */ - public boolean equals(Object obj) { - ProgramSVInstantiation cmp; - if (!(obj instanceof ProgramSVInstantiation)) { - return false; - } else { - cmp = (ProgramSVInstantiation) obj; - } - if (size() != cmp.size()) { - return false; - } else { - final Iterator it = iterator(); - while (it.hasNext()) { - final ProgramSVEntry psv = it.next(); - if (!psv.value().equals(cmp.getInstantiation(psv.key()))) { - return false; - } - } - return true; - } - } - - public int hashCode() { - if (hashcode == 0) { - int result = 17; - final Iterator it = iterator(); - while (it.hasNext()) { - final ProgramSVEntry psv = it.next(); - result = 37 * result + psv.key().hashCode() + psv.value().hashCode(); - } - hashcode = result; - } - return hashcode; - } - - /** toString */ - public String toString() { - StringBuilder result = new StringBuilder("ProgramSVInstantiation:\n"); - return (result.append(list.toString())).toString(); - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/RigidnessException.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/RigidnessException.java index dc99f2cebf3..77abbe4607b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/RigidnessException.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/RigidnessException.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.rule.inst; +import java.io.Serial; + /** * this exception is thrown if non-rigid instantiation has been given for a schema variable only * allowing rigid instantiations @@ -12,11 +14,11 @@ public class RigidnessException extends IllegalInstantiationException { /** * */ + @Serial private static final long serialVersionUID = 1109354128591892703L; public RigidnessException(String description) { super(description); } - } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java index 7d5a12bafb7..d268ed73005 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java @@ -20,6 +20,8 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.Name; 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.util.collection.DefaultImmutableMap; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; @@ -125,22 +127,17 @@ public ImmutableList getGenericSortConditions() { * @return SVInstantiations the new SVInstantiations containing the given pair */ public SVInstantiations add(SchemaVariable sv, Term subst, LogicServices services) { - return add(sv, new TermInstantiation(sv, subst), services); + return add(sv, new InstantiationEntry<>(subst), services); } public SVInstantiations addInteresting(SchemaVariable sv, Term subst, LogicServices services) { - return addInteresting(sv, new TermInstantiation(sv, subst), services); + return addInteresting(sv, new InstantiationEntry<>(subst), services); } - - public SVInstantiations add(SchemaVariable sv, ProgramList pes, LogicServices services) { - return add(sv, new ProgramListInstantiation(pes.getList()), services); - } - - public SVInstantiations add(SchemaVariable sv, ImmutableArray labels, + public SVInstantiations add(SchemaVariable sv, ImmutableArray pes, Class type, LogicServices services) { - return add(sv, new TermLabelInstantiationEntry(labels), services); + return add(sv, new ListInstantiation(pes, type), services); } /** @@ -148,17 +145,9 @@ public SVInstantiations add(SchemaVariable sv, ImmutableArray labels, */ public SVInstantiations add(SchemaVariable sv, Modality.JavaModalityKind kind, LogicServices services) throws SortException { - return add(sv, new InstantiationEntry<>(kind) { - }, services); + return add(sv, new InstantiationEntry<>(kind), services); } - public SVInstantiations addList(SchemaVariable sv, Object[] list, LogicServices services) { - return add(sv, new ListInstantiation(sv, ImmutableSLList.nil().prepend(list)), - services); - } - - - /** * adds the given pair to the instantiations. If the given SchemaVariable has been instantiated * already, the new pair is taken without a warning. @@ -168,23 +157,15 @@ public SVInstantiations addList(SchemaVariable sv, Object[] list, LogicServices * @return SVInstantiations the new SVInstantiations containing the given pair */ public SVInstantiations add(SchemaVariable sv, ProgramElement pe, LogicServices services) { - return add(sv, new ProgramInstantiation(pe), services); + return add(sv, new InstantiationEntry<>(pe), services); } public SVInstantiations addInteresting(SchemaVariable sv, ProgramElement pe, LogicServices services) { - return addInteresting(sv, new ProgramInstantiation(pe), services); + return addInteresting(sv, new InstantiationEntry<>(pe), services); } - public SVInstantiations addInterestingList(SchemaVariable sv, Object[] list, - LogicServices services) { - return addInteresting(sv, - new ListInstantiation(sv, ImmutableSLList.nil().prepend(list)), services); - } - - - /** * adds the given pair to the instantiations for the context.If the context has been * instantiated already, the new pair is taken without a warning. @@ -198,7 +179,9 @@ public SVInstantiations addInterestingList(SchemaVariable sv, Object[] list, public SVInstantiations add(PosInProgram prefix, PosInProgram postfix, ExecutionContext activeStatementContext, ProgramElement pe, LogicServices services) { return add(CONTEXTSV, - new ContextInstantiationEntry(prefix, postfix, activeStatementContext, pe), services); + new InstantiationEntry<>(new ContextStatementBlockInstantiation(prefix, postfix, + activeStatementContext, pe)), + services); } @@ -274,7 +257,6 @@ public SVInstantiations addInteresting(SchemaVariable sv, InstantiationEntry .checkSorts(sv, entry, false, services); } - public SVInstantiations addInteresting(SchemaVariable sv, Name name, LogicServices services) { SchemaVariable existingSV = lookupVar(sv.name()); Name oldValue = (Name) getInstantiation(existingSV); @@ -285,11 +267,10 @@ public SVInstantiations addInteresting(SchemaVariable sv, Name name, LogicServic "Trying to add a second name proposal for " + sv + ": " + oldValue + "->" + name); } else { // otherwise (nothing here yet) add it - return addInteresting(sv, new NameInstantiationEntry(name), services); + return addInteresting(sv, new InstantiationEntry<>(name), services); } } - /** * replaces the given pair in the instantiations. If the given SchemaVariable has been * instantiated already, the new pair is taken without a warning. @@ -330,7 +311,7 @@ public SVInstantiations makeInteresting(SchemaVariable sv, LogicServices service * @param term the Term the SchemaVariable is instantiated with */ public SVInstantiations replace(SchemaVariable sv, Term term, Services services) { - return replace(sv, new TermInstantiation(sv, term), services); + return replace(sv, new InstantiationEntry<>(term), services); } /** @@ -341,7 +322,7 @@ public SVInstantiations replace(SchemaVariable sv, Term term, Services services) * @param pe the ProgramElement the SchemaVariable is instantiated with */ public SVInstantiations replace(SchemaVariable sv, ProgramElement pe, Services services) { - return replace(sv, new ProgramInstantiation(pe), services); + return replace(sv, new InstantiationEntry<>(pe), services); } /** @@ -353,7 +334,7 @@ public SVInstantiations replace(SchemaVariable sv, ProgramElement pe, Services s */ public SVInstantiations replace(SchemaVariable sv, ImmutableArray pes, Services services) { - return replace(sv, new ProgramListInstantiation(pes), services); + return replace(sv, new ListInstantiation(pes, ProgramElement.class), services); } /** @@ -370,7 +351,9 @@ public SVInstantiations replace(SchemaVariable sv, ImmutableArray(new ContextStatementBlockInstantiation(prefix, postfix, + activeStatementContext, pe)), + services); } @@ -503,9 +486,9 @@ public SVInstantiations clearUpdateContext() { /** * returns the instantiation entry for the context "schema variable" or null if non such exists */ - public ContextInstantiationEntry getContextInstantiation() { + public ContextStatementBlockInstantiation getContextInstantiation() { final InstantiationEntry entry = getInstantiationEntry(CONTEXTSV); - return (ContextInstantiationEntry) entry; + return entry == null ? null : (ContextStatementBlockInstantiation) entry.getInstantiation(); } /** @@ -660,7 +643,7 @@ public SVInstantiations add(GenericSortCondition p_c, LogicServices services) } public ExecutionContext getExecutionContext() { - final ContextInstantiationEntry cte = getContextInstantiation(); + final ContextStatementBlockInstantiation cte = getContextInstantiation(); if (cte != null) { return cte.activeStatementContext(); } else { @@ -686,6 +669,7 @@ public SchemaVariable lookupVar(Name name) { @Override public Object lookupValue(Name name) { final var e = lookupEntryForSV(name); + // e.value() cannot be null here as null instantiations are not allowed return e == null ? null : e.value().getInstantiation(); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/TacletInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/TacletInstantiations.java deleted file mode 100644 index c9d1bca8368..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/TacletInstantiations.java +++ /dev/null @@ -1,39 +0,0 @@ -/* 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.inst; - - -import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.rule.Taclet; - -import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.util.collection.ImmutableMap; - -/** - * this class contains a Taclet together with its suggested instantiations. - */ -public class TacletInstantiations { - - /** the rule */ - private final Taclet rule; - /** the instantations */ - private final ImmutableMap instantiations; - - public TacletInstantiations(Taclet rule, ImmutableMap instantiations) { - this.rule = rule; - this.instantiations = instantiations; - } - - public Taclet taclet() { - return rule; - } - - public ImmutableMap instantiations() { - return instantiations; - } - - public String toString() { - return "rule: " + taclet() + "; instantiation: " + instantiations(); - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/TermInstantiation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/TermInstantiation.java deleted file mode 100644 index 537f8c9b69c..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/TermInstantiation.java +++ /dev/null @@ -1,34 +0,0 @@ -/* 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.inst; - -import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.op.OperatorSV; - -import org.key_project.logic.op.sv.SchemaVariable; - -/** - * This class is used to store the instantiation of a schemavarible if it is a term. - */ -public class TermInstantiation extends InstantiationEntry { - - private static final RigidnessException RIGIDNESS_EXCEPTION = new RigidnessException( - "Tried to instantiate a rigid schema variable" + " with a non-rigid term/formula"); - - - /** - * creates a new ContextInstantiationEntry - * - * @param sv the SchemaVariable that is instantiated - * @param term the Term the SchemaVariable is instantiated with - */ - TermInstantiation(SchemaVariable sv, Term term) { - super(term); - // TODO: Remove the check below and move it to the matching logic - // Done for VM based matching - if (sv instanceof OperatorSV asv && !term.isRigid() && asv.isRigid()) { - throw RIGIDNESS_EXCEPTION; - } - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/TermLabelInstantiationEntry.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/TermLabelInstantiationEntry.java deleted file mode 100644 index 7b6b59f0601..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/TermLabelInstantiationEntry.java +++ /dev/null @@ -1,29 +0,0 @@ -/* 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.inst; - -import de.uka.ilkd.key.logic.label.TermLabel; - -import org.key_project.util.collection.ImmutableArray; - -/** - * - * - */ -public class TermLabelInstantiationEntry extends InstantiationEntry> { - - TermLabelInstantiationEntry(ImmutableArray labels) { - super(labels); - } - - /** - * {@inheritDoc} - */ - public String toString() { - String sb = String.valueOf(getInstantiation()) + - '\n'; - return sb; - } - -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchTermLabelInstruction.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchTermLabelInstruction.java index 0fe03196bda..0d96c4d78f7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchTermLabelInstruction.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchTermLabelInstruction.java @@ -8,7 +8,6 @@ import de.uka.ilkd.key.logic.op.TermLabelSV; import de.uka.ilkd.key.rule.MatchConditions; import de.uka.ilkd.key.rule.inst.SVInstantiations; -import de.uka.ilkd.key.rule.inst.TermLabelInstantiationEntry; import de.uka.ilkd.key.rule.match.vm.TermNavigator; import org.key_project.logic.LogicServices; @@ -29,14 +28,14 @@ private MatchConditions match(TermLabelSV sv, Term instantiationCandidate, MatchConditions matchCond, LogicServices services) { final SVInstantiations svInsts = matchCond.getInstantiations(); - final TermLabelInstantiationEntry inst = - (TermLabelInstantiationEntry) svInsts.getInstantiation(sv); + final ImmutableArray inst = + (ImmutableArray) svInsts.getInstantiation(sv); if (inst == null) { return matchCond.setInstantiations( - svInsts.add(sv, instantiationCandidate.getLabels(), services)); + svInsts.add(sv, instantiationCandidate.getLabels(), TermLabel.class, services)); } else { - for (TermLabel o : inst.getInstantiation()) { + for (TermLabel o : inst) { if (!instantiationCandidate.containsLabel(o)) { return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReattachLoopInvariant.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReattachLoopInvariant.java index 403dde4f44e..ab67362ce8d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReattachLoopInvariant.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReattachLoopInvariant.java @@ -31,12 +31,12 @@ public ReattachLoopInvariant(LoopStatement ls) { public ProgramElement[] transform(ProgramElement pe, Services services, SVInstantiations svInst) { final ProgramElement context = // - svInst.getContextInstantiation().contextProgram(); + svInst.getContextInstantiation().program(); if (context != null) { final Statement activeStmt = (Statement) JavaTools.getActiveStatement(JavaBlock.createJavaBlock( - (StatementBlock) svInst.getContextInstantiation().contextProgram())); + (StatementBlock) svInst.getContextInstantiation().program())); assert activeStmt instanceof LoopStatement; final LoopStatement loop = (LoopStatement) activeStmt; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractNonDuplicateAppFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractNonDuplicateAppFeature.java index 3f4963a0525..1385bf8b8ab 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractNonDuplicateAppFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractNonDuplicateAppFeature.java @@ -11,12 +11,12 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.rule.PosTacletApp; import de.uka.ilkd.key.rule.TacletApp; -import de.uka.ilkd.key.rule.inst.InstantiationEntry; import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.op.sv.SchemaVariable; 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.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableMap; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InfFlowContractAppFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InfFlowContractAppFeature.java index d9efde3ffa2..f7f2f6c8e1a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InfFlowContractAppFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InfFlowContractAppFeature.java @@ -18,14 +18,15 @@ import de.uka.ilkd.key.proof.init.ProofOblInput; import de.uka.ilkd.key.rule.PosTacletApp; import de.uka.ilkd.key.rule.TacletApp; -import de.uka.ilkd.key.rule.inst.InstantiationEntry; import de.uka.ilkd.key.rule.inst.SVInstantiations; import de.uka.ilkd.key.strategy.NumberRuleAppCost; import de.uka.ilkd.key.strategy.RuleAppCost; import de.uka.ilkd.key.strategy.TopRuleAppCost; +import org.key_project.logic.op.sv.SchemaVariable; 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.Semisequent; import org.key_project.prover.sequent.Sequent; @@ -129,10 +130,10 @@ private boolean equalInterestingInsts(SVInstantiations inst0, SVInstantiations i private boolean subset( - ImmutableMap> insts0, - ImmutableMap> insts1) { + ImmutableMap> insts0, + ImmutableMap> insts1) { - for (final ImmutableMapEntry> entry0 : insts0) { + for (final ImmutableMapEntry> entry0 : insts0) { if (entry0.key() instanceof SkolemTermSV || entry0.key() instanceof VariableSV) { continue; } diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/RuleApplicationUtil.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/RuleApplicationUtil.java index 2308e635dee..8c77c070f93 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/RuleApplicationUtil.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/RuleApplicationUtil.java @@ -1,3 +1,6 @@ +/* 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; public class RuleApplicationUtil { diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/InstantiationEntry.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/InstantiationEntry.java index 08714411fec..1201307028a 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/InstantiationEntry.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/InstantiationEntry.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.inst; +package org.key_project.prover.rules.inst; import org.jspecify.annotations.NonNull; @@ -13,7 +13,7 @@ * map from SchemaVariable to InstantiationEntry is used TODO: Simplify subclasses further or remove * them completely as possible. */ -public abstract class InstantiationEntry { +public class InstantiationEntry { private final @NonNull E instantiation; @@ -22,7 +22,7 @@ public abstract class InstantiationEntry { * * @param instantiation the instantiation to be stored */ - InstantiationEntry(@NonNull E instantiation) { + public InstantiationEntry(@NonNull E instantiation) { assert instantiation != null : "An instantiation for a schemavariable cannot be null."; this.instantiation = instantiation; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramListInstantiation.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/ListInstantiation.java similarity index 54% rename from key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramListInstantiation.java rename to key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/ListInstantiation.java index 9dec3ea8792..877591725a1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramListInstantiation.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/ListInstantiation.java @@ -1,9 +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.inst; - -import de.uka.ilkd.key.java.ProgramElement; +package org.key_project.prover.rules.inst; import org.key_project.util.collection.ImmutableArray; @@ -11,14 +9,25 @@ * This class is used to store the instantiation of a schemavariable if it is a ProgramElement. */ -public class ProgramListInstantiation extends InstantiationEntry> { +public class ListInstantiation extends InstantiationEntry> { + + /** type of the stored elements */ + private final Class type; /** * creates a new ContextInstantiationEntry * * @param pes the ProgramElement array the SchemaVariable is instantiated with */ - ProgramListInstantiation(ImmutableArray pes) { + public ListInstantiation(ImmutableArray pes, Class type) { super(pes); + this.type = type; + } + + /** + * returns the element type of the contained instantiations + */ + public Class getType() { + return type; } } diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/SVInstantiations.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/SVInstantiations.java index a0d3f5b2514..cd301f44c6e 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/SVInstantiations.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/SVInstantiations.java @@ -20,5 +20,5 @@ public interface SVInstantiations { SVInstantiations union(SVInstantiations instantiations, LogicServices services); - ImmutableMap> getInstantiationMap(); + ImmutableMap> getInstantiationMap(); } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ContextInstantiationEntry.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ContextInstantiationEntry.java index 95e86ec6160..9b9a3ca170c 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ContextInstantiationEntry.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ContextInstantiationEntry.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.rusty.rule.inst; +import org.key_project.prover.rules.inst.InstantiationEntry; import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.rusty.logic.PosInProgram; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/GenericSortCondition.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/GenericSortCondition.java index ad2a08cc43f..6f8ece549b4 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/GenericSortCondition.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/GenericSortCondition.java @@ -6,6 +6,7 @@ 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.inst.InstantiationEntry; import org.key_project.rusty.logic.RustyDLTheory; import org.key_project.rusty.logic.op.sv.TermSV; import org.key_project.rusty.logic.sort.GenericSort; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/GenericSortInstantiations.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/GenericSortInstantiations.java index c02f8311868..94098611b69 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/GenericSortInstantiations.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/GenericSortInstantiations.java @@ -14,6 +14,7 @@ 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.inst.InstantiationEntry; import org.key_project.rusty.logic.op.sv.ProgramSV; import org.key_project.rusty.logic.sort.GenericSort; import org.key_project.util.collection.*; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ListInstantiation.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ListInstantiation.java index fcbe4500a5d..f1c24792240 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ListInstantiation.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ListInstantiation.java @@ -4,6 +4,7 @@ package org.key_project.rusty.rule.inst; import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.rules.inst.InstantiationEntry; import org.key_project.util.collection.ImmutableList; public class ListInstantiation extends InstantiationEntry> { diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramInstantiation.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramInstantiation.java index 4ca82b21b48..47dd02030fd 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramInstantiation.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramInstantiation.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.rusty.rule.inst; +import org.key_project.prover.rules.inst.InstantiationEntry; import org.key_project.rusty.ast.RustyProgramElement; /** diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramListInstantiation.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramListInstantiation.java index 04c2adef323..d85e5674d06 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramListInstantiation.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramListInstantiation.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.rusty.rule.inst; +import org.key_project.prover.rules.inst.InstantiationEntry; import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.util.collection.ImmutableArray; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/SVInstantiations.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/SVInstantiations.java index e86412f55d7..6748a416bd0 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/SVInstantiations.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/SVInstantiations.java @@ -10,6 +10,7 @@ import org.key_project.logic.Term; import org.key_project.logic.op.sv.OperatorSV; import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.rules.inst.InstantiationEntry; import org.key_project.rusty.Services; import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.rusty.logic.PosInProgram; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/TermInstantiation.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/TermInstantiation.java index 49ccaa97b43..adc83e6ace3 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/TermInstantiation.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/TermInstantiation.java @@ -5,6 +5,7 @@ import org.key_project.logic.Term; import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.rules.inst.InstantiationEntry; import org.key_project.rusty.logic.op.sv.OperatorSV; public class TermInstantiation extends InstantiationEntry { diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchSchemaVariableInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchSchemaVariableInstruction.java index ecf4828f7d6..f5138e4c6e1 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchSchemaVariableInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchSchemaVariableInstruction.java @@ -6,6 +6,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.Term; import org.key_project.logic.op.sv.OperatorSV; +import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.prover.rules.MatchConditions; import org.key_project.rusty.Services; import org.key_project.rusty.ast.RustyProgramElement;