diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index e411586a54a..48c0a02ca41 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,5 +1,5 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java index c6084f2b8fb..d997436ad8e 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java @@ -32,6 +32,7 @@ import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -76,7 +77,7 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea * A {@link Map} mapping from relevant variables for the condition to their runtime equivalent * in KeY */ - private Map variableNamingMap; + private Map variableNamingMap; /** * The list of parameter variables of the method that contains the associated breakpoint @@ -162,14 +163,14 @@ private void putValuesFromGlobalVars(ProgramVariable varForCondition, Node node, * * @return the cloned map */ - private Map getOldMap() { - Map oldMap = new HashMap<>(); - for (Entry svSubstituteSVSubstituteEntry : getVariableNamingMap() + private Map getOldMap() { + Map oldMap = new HashMap<>(); + for (Entry svSubstituteSVSubstituteEntry : getVariableNamingMap() .entrySet()) { Entry oldEntry = svSubstituteSVSubstituteEntry; - if (oldEntry.getKey() instanceof SVSubstitute - && oldEntry.getValue() instanceof SVSubstitute) { - oldMap.put((SVSubstitute) oldEntry.getKey(), (SVSubstitute) oldEntry.getValue()); + if (oldEntry.getKey() instanceof SyntaxElement + && oldEntry.getValue() instanceof SyntaxElement) { + oldMap.put((SyntaxElement) oldEntry.getKey(), (SyntaxElement) oldEntry.getValue()); } } return oldMap; @@ -200,7 +201,7 @@ private void freeVariablesAfterReturn(Node node, RuleApp ruleApp, boolean inScop * @param oldMap the oldMap variableNamings */ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, boolean inScope, - Map oldMap, RuleApp ruleApp) { + Map oldMap, RuleApp ruleApp) { // look for renamings KeY did boolean found = false; // get current renaming tables @@ -215,7 +216,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, .getHashMap().entrySet()) { Entry entry = value; if (entry.getKey() instanceof LocationVariable - && entry.getValue() instanceof SVSubstitute) { + && entry.getValue() instanceof SyntaxElement) { if ((VariableNamer.getBasename(((LocationVariable) entry.getKey()).name())) .equals(varForCondition.name()) && ((LocationVariable) entry.getKey()).name().toString() @@ -229,7 +230,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, // add new value toKeep.add((LocationVariable) entry.getValue()); getVariableNamingMap().put(varForCondition, - (SVSubstitute) entry.getValue()); + (SyntaxElement) entry.getValue()); found = true; break; } else if (inScope && ((LocationVariable) entry.getKey()).name() @@ -242,7 +243,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, // add new value toKeep.add((LocationVariable) entry.getValue()); getVariableNamingMap().put(varForCondition, - (SVSubstitute) entry.getValue()); + (SyntaxElement) entry.getValue()); found = true; break; } @@ -263,7 +264,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, protected void refreshVarMaps(RuleApp ruleApp, Node node) { boolean inScope = isInScope(node); // collect old values - Map oldMap = getOldMap(); + Map oldMap = getOldMap(); // put values into map which have to be replaced for (ProgramVariable varForCondition : getVarsForCondition()) { // put global variables only done when a variable is instantiated by @@ -498,14 +499,14 @@ public Set getToKeep() { /** * @return the variableNamingMap */ - public Map getVariableNamingMap() { + public Map getVariableNamingMap() { return variableNamingMap; } /** * @param variableNamingMap the variableNamingMap to set */ - public void setVariableNamingMap(Map variableNamingMap) { + public void setVariableNamingMap(Map variableNamingMap) { this.variableNamingMap = variableNamingMap; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Comment.java b/key.core/src/main/java/de/uka/ilkd/key/java/Comment.java index 0d556acb369..60221fca8fe 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Comment.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Comment.java @@ -5,6 +5,8 @@ import de.uka.ilkd.key.java.visitor.Visitor; +import org.key_project.logic.SyntaxElement; + /** * Comment element of Java source code. */ @@ -71,4 +73,14 @@ public boolean equals(Object o) { } return (getText().equals(cmp.getText())); } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException("Comment has no children"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java index ca20a719d4d..1865f6e964c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java; +import org.key_project.logic.SyntaxElement; + /** * Non terminal program element. taken from COMPOST and changed to achieve an immutable structure */ @@ -25,4 +27,8 @@ public interface NonTerminalProgramElement extends ProgramElement { */ ProgramElement getChildAt(int index); + @Override + default SyntaxElement getChild(int n) { + return getChildAt(n); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java index 046d51538cb..206efd7fb8e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java @@ -4,7 +4,8 @@ package de.uka.ilkd.key.java; import de.uka.ilkd.key.java.visitor.Visitor; -import de.uka.ilkd.key.logic.op.SVSubstitute; + +import org.key_project.logic.SyntaxElement; /** * A source element is a piece of syntax. It does not necessarily have a semantics, at least none @@ -12,7 +13,7 @@ * to achieve an immutable structure */ -public interface SourceElement extends SVSubstitute { +public interface SourceElement extends SyntaxElement { /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java index 902e791ace6..e6fdc309f71 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java @@ -3,9 +3,12 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java; +import org.key_project.logic.TerminalSyntaxElement; + /** * Terminal program element. taken from COMPOST and changed to achieve an immutable structure */ -public interface TerminalProgramElement extends ProgramElement { +public interface TerminalProgramElement extends ProgramElement, TerminalSyntaxElement { + } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java index 04346acf3a7..fc59c65e880 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java @@ -163,7 +163,7 @@ public SourceElement getFirstElement() { @Override public SourceElement getLastElement() { - return getChildAt(getChildCount() - 1).getLastElement(); + return getChildAt(this.getChildCount() - 1).getLastElement(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Modifier.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Modifier.java index 357d417d3ca..b8fd1e2d410 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Modifier.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Modifier.java @@ -4,16 +4,16 @@ package de.uka.ilkd.key.java.declaration; import de.uka.ilkd.key.java.JavaProgramElement; -import de.uka.ilkd.key.java.TerminalProgramElement; import de.uka.ilkd.key.java.visitor.Visitor; +import org.key_project.logic.SyntaxElement; import org.key_project.util.ExtList; /** * Modifier. taken from COMPOST and changed to achieve an immutable structure */ -public abstract class Modifier extends JavaProgramElement implements TerminalProgramElement { +public abstract class Modifier extends JavaProgramElement { /** * Modifier. @@ -56,4 +56,14 @@ public String getText() { public void visit(Visitor v) { v.performActionOnModifier(this); } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException(getClass() + " " + this + " has no children"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/Instanceof.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/Instanceof.java index 284c254db72..d53c134154e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/Instanceof.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/Instanceof.java @@ -31,13 +31,13 @@ public class Instanceof extends TypeOperator { public Instanceof(ExtList children) { super(children); - assert getChildCount() == 2 : "not 2 children but " + getChildCount(); + assert this.getChildCount() == 2 : "not 2 children but " + this.getChildCount(); } public Instanceof(Expression unaryChild, TypeReference typeref) { super(unaryChild, typeref); - assert getChildCount() == 2 : "not 2 children but " + getChildCount(); + assert this.getChildCount() == 2 : "not 2 children but " + this.getChildCount(); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/New.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/New.java index bc7027d5498..6d041245c71 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/New.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/New.java @@ -99,7 +99,7 @@ public SourceElement getFirstElementIncludingBlocks() { @Override public SourceElement getLastElement() { - return getChildAt(getChildCount() - 1).getLastElement(); + return getChildAt(this.getChildCount() - 1).getLastElement(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/IForUpdates.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/IForUpdates.java index a532522aa5e..75d499d1cdf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/IForUpdates.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/IForUpdates.java @@ -7,7 +7,7 @@ import org.key_project.util.collection.ImmutableArray; -public interface IForUpdates extends de.uka.ilkd.key.java.TerminalProgramElement { +public interface IForUpdates extends de.uka.ilkd.key.java.NonTerminalProgramElement { int size(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java index c8528112d4d..ee0bc657b95 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java @@ -4,11 +4,11 @@ package de.uka.ilkd.key.java.statement; import de.uka.ilkd.key.java.LoopInitializer; -import de.uka.ilkd.key.java.TerminalProgramElement; +import de.uka.ilkd.key.java.NonTerminalProgramElement; import org.key_project.util.collection.ImmutableArray; -public interface ILoopInit extends TerminalProgramElement { +public interface ILoopInit extends NonTerminalProgramElement { int size(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java index 90b373e1438..60d71b65f31 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java @@ -107,7 +107,7 @@ public ImmutableArray getPrefixElements() { @Override public PosInProgram getFirstActiveChildPos() { return getStatementCount() == 0 ? PosInProgram.TOP - : PosInProgram.TOP.down(getChildCount() - 1).down(0); + : PosInProgram.TOP.down(this.getChildCount() - 1).down(0); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java index ede5682ff23..105e3ab446a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java @@ -53,7 +53,8 @@ public MethodFrame(IProgramVariable resultVar, IExecutionContext execContext, this.execContext = execContext; firstActiveChildPos = - body.isEmpty() ? PosInProgram.TOP : PosInProgram.TOP.down(getChildCount() - 1).down(0); + body.isEmpty() ? PosInProgram.TOP + : PosInProgram.TOP.down(getChildCount() - 1).down(0); Debug.assertTrue(execContext != null, "methodframe: executioncontext missing"); Debug.assertTrue(body != null, "methodframe: body missing"); @@ -78,7 +79,8 @@ public MethodFrame(IProgramVariable resultVar, IExecutionContext execContext, this.execContext = execContext; firstActiveChildPos = - body.isEmpty() ? PosInProgram.TOP : PosInProgram.TOP.down(getChildCount() - 1).down(0); + body.isEmpty() ? PosInProgram.TOP + : PosInProgram.TOP.down(getChildCount() - 1).down(0); Debug.assertTrue(execContext != null, "methodframe: executioncontext missing"); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java index 9011234e233..02386a7c6e9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java @@ -137,7 +137,7 @@ public SourceElement getFirstElement() { public SourceElement getLastElement() { - return getChildAt(getChildCount() - 1).getLastElement(); + return getChildAt(this.getChildCount() - 1).getLastElement(); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java b/key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java index b7d72e26382..9f18163e5e7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java @@ -8,6 +8,7 @@ import de.uka.ilkd.key.pp.PrettyPrinter; import org.key_project.logic.Program; +import org.key_project.logic.SyntaxElement; import org.key_project.util.EqualsModProofIrrelevancy; import org.slf4j.Logger; @@ -128,4 +129,18 @@ public int hashCodeModProofIrrelevancy() { } return hashCode; } + + @Override + public int getChildCount() { + if (prg == null || this == EMPTY_JAVABLOCK) + return 0; + return 1; + } + + @Override + public SyntaxElement getChild(int n) { + if (n == 0) + return prg; + throw new IndexOutOfBoundsException("JavaBlock " + this + " has only one child"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramConstruct.java b/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramConstruct.java index 70bd980e18b..8b68b44f4dc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramConstruct.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramConstruct.java @@ -18,6 +18,8 @@ import de.uka.ilkd.key.logic.op.IProgramMethod; import de.uka.ilkd.key.logic.op.IProgramVariable; +import org.key_project.logic.SyntaxElement; + /** * A type that implement this interface can be used in all java programs instead of an expression or * statement. For example class SchemaVariable implements this interface to be able to stand for @@ -26,4 +28,9 @@ public interface ProgramConstruct extends Expression, Statement, ILoopInit, IForUpdates, IGuard, Label, TerminalProgramElement, ExpressionStatement, TypeReference, IProgramVariable, IProgramMethod, Branch, IExecutionContext, MethodName { + @Override + SyntaxElement getChild(int n); + + @Override + int getChildCount(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/Term.java b/key.core/src/main/java/de/uka/ilkd/key/logic/Term.java index 60c03e6fdae..73e99f387e2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/Term.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/Term.java @@ -8,7 +8,6 @@ import de.uka.ilkd.key.logic.label.TermLabel; import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.logic.op.QuantifiableVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import org.key_project.logic.Name; import org.key_project.logic.Visitor; @@ -43,7 +42,7 @@ * supported: {@link Term#execPostOrder(Visitor)} and {@link Term#execPreOrder(Visitor)}. */ public interface Term - extends SVSubstitute, Sorted, TermEqualsModProperty, org.key_project.logic.Term { + extends Sorted, TermEqualsModProperty, org.key_project.logic.Term { @Override Operator op(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/BlockContractValidityTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/BlockContractValidityTermLabel.java index c4181e3c988..f4cb02f511f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/BlockContractValidityTermLabel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/BlockContractValidityTermLabel.java @@ -40,7 +40,7 @@ public ProgramVariable exceptionVariable() { * {@inheritDoc} */ @Override - public ProgramVariable getChild(int i) { + public ProgramVariable getTLChild(int i) { if (i == 0) { return exceptionVariable(); } @@ -51,7 +51,7 @@ public ProgramVariable getChild(int i) { * {@inheritDoc} */ @Override - public int getChildCount() { + public int getTLChildCount() { return 1; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java index cde4271a90d..def77a6dd50 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java @@ -134,7 +134,7 @@ public String toString() { * {@inheritDoc} */ @Override - public Object getChild(int i) { + public Object getTLChild(int i) { return switch (i) { case 0 -> getId(); case 1 -> beforeIds; @@ -146,7 +146,7 @@ public Object getChild(int i) { * {@inheritDoc} */ @Override - public int getChildCount() { + public int getTLChildCount() { if (beforeIds != null) { return 2; } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java index 1e3edea26ed..f65285f1849 100755 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java @@ -57,7 +57,7 @@ public class OriginTermLabel implements TermLabel { public final static Name NAME = new Name("origin"); /** - * @see #getChildCount() + * @see #getTLChildCount() */ public final static int CHILD_COUNT = 2; public static final Sort[] EMPTY_SORTS = new Sort[0]; @@ -450,7 +450,7 @@ public Name name() { } @Override - public Object getChild(int i) { + public Object getTLChild(int i) { if (i == 0) { return origin; } else if (i == 1) { @@ -461,7 +461,7 @@ public Object getChild(int i) { } @Override - public int getChildCount() { + public int getTLChildCount() { return CHILD_COUNT; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java index 850c5c1b3d5..596410ce3e8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java @@ -139,7 +139,7 @@ public Name name() { * {@link IndexOutOfBoundsException}. */ @Override - public Object getChild(int i) { + public Object getTLChild(int i) { throw new IndexOutOfBoundsException(); } @@ -150,7 +150,7 @@ public Object getChild(int i) { * Simple term labels have no parameters. This always returns 0. */ @Override - public int getChildCount() { + public int getTLChildCount() { return 0; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/SymbolicExecutionTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/SymbolicExecutionTermLabel.java index 03659186d6a..6596ce2ba89 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/SymbolicExecutionTermLabel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/SymbolicExecutionTermLabel.java @@ -50,7 +50,7 @@ public String toString() { * {@inheritDoc} */ @Override - public Object getChild(int i) { + public Object getTLChild(int i) { if (i == 0) { return id(); } @@ -61,7 +61,7 @@ public Object getChild(int i) { * {@inheritDoc} */ @Override - public int getChildCount() { + public int getTLChildCount() { return 1; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java index b514fbd04d5..a5287c1f2d1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java @@ -20,6 +20,8 @@ import org.key_project.logic.Name; import org.key_project.logic.Named; +import org.key_project.logic.SyntaxElement; +import org.key_project.logic.TerminalSyntaxElement; // spotless:off // this protects the JavaDoc from automatic reformatting /** @@ -34,8 +36,8 @@ * without parameters class {@link ParameterlessTermLabel} can be used. *

*

- * A term label can have parameters accessible via {@link #getChild(int)} and - * {@link #getChildCount()}. Such parameters can be any {@link Object}. But keep in mind that it is + * A term label can have parameters accessible via {@link #getTLChild(int)} and + * {@link #getTLChildCount()}. Such parameters can be any {@link Object}. But keep in mind that it is * required to parse {@link String}s into {@link Term}s, e.g. if it is used in a Taclet definition * or if a cut rule is applied. For convenience parameters are always printed as {@link String}s * and have to be parsed individually into the required {@link Object} instances via a @@ -150,7 +152,7 @@ * @see TermLabelManager */ // spotless:on -public interface TermLabel extends Named { +public interface TermLabel extends Named, SyntaxElement, /* TODO: Remove */ TerminalSyntaxElement { /** * Retrieves the i-th parameter object of this term label. @@ -161,16 +163,16 @@ public interface TermLabel extends Named { * @param i the number of the parameter to retrieve ( {@code 0 <= i < getChildCount()}) * @return the selected parameter * @throws IndexOutOfBoundsException if the given parameter number i is negative or - * greater-or-equal the number of parameters returned by {@link #getChildCount()} + * greater-or-equal the number of parameters returned by {@link #getTLChildCount()} */ - Object getChild(int i); + Object getTLChild(int i); /** * Gets the number of parameters of this term label. * * @return the number of parameters (a non-negative number) */ - int getChildCount(); + int getTLChildCount(); /** * Returns {@code true} iff this label is used in any way during the proof. E.g., diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.java index 0837fda6089..c4ae30a8789 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.java @@ -9,6 +9,7 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; @@ -58,4 +59,16 @@ public static ElementaryUpdate getInstance(UpdateableOperator lhs) { public UpdateableOperator lhs() { return lhs; } + + @Override + public int getChildCount() { + return 1; + } + + @Override + public SyntaxElement getChild(int n) { + if (n == 0) + return lhs; + throw new IndexOutOfBoundsException("Elementary updates only contain 1 child"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java index ecd4c878dfc..09fa71a855e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java @@ -6,6 +6,7 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; @@ -34,4 +35,14 @@ public final class Equality extends AbstractSortedOperator { private Equality(Name name, Sort targetSort) { super(name, new Sort[] { targetSort, targetSort }, JavaDLTheory.FORMULA, true); } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException(name() + " has no children"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/FormulaSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/FormulaSV.java index f93b960860e..270c2a92c89 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/FormulaSV.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/FormulaSV.java @@ -7,12 +7,13 @@ import de.uka.ilkd.key.util.pp.Layouter; import org.key_project.logic.Name; +import org.key_project.logic.TerminalSyntaxElement; /** * A schema variable that is used as placeholder for formulas. */ -public final class FormulaSV extends OperatorSV { +public final class FormulaSV extends OperatorSV implements TerminalSyntaxElement { /** * @param name the name of the SchemaVariable diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfExThenElse.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfExThenElse.java index be40110ea40..c7f05ada203 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfExThenElse.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfExThenElse.java @@ -6,6 +6,7 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.TermCreationException; import org.key_project.logic.op.AbstractOperator; import org.key_project.logic.sort.Sort; @@ -44,4 +45,14 @@ public void validTopLevelException(T term throw new TermCreationException(this, term); } } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException(name() + " has no children"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfThenElse.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfThenElse.java index a7fe9097055..a77b49ec111 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfThenElse.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfThenElse.java @@ -8,6 +8,7 @@ import de.uka.ilkd.key.logic.sort.ProgramSVSort; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.TermCreationException; import org.key_project.logic.op.AbstractOperator; import org.key_project.logic.sort.Sort; @@ -85,4 +86,14 @@ public void validTopLevelException(T term throw new TermCreationException(this, term); } } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException(name() + " has no children"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Junctor.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Junctor.java index e2b1162c6cc..42b78108d67 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Junctor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Junctor.java @@ -6,6 +6,7 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; @@ -62,4 +63,14 @@ private static Sort[] createFormulaSortArray(int arity) { private Junctor(Name name, int arity) { super(name, createFormulaSortArray(arity), JavaDLTheory.FORMULA, true); } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException("The Junctor operator " + name() + " has no children"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java index d4e8aa5def9..fe94c1c3b01 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java @@ -9,6 +9,7 @@ import org.key_project.logic.Name; import org.key_project.logic.ParsableVariable; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; import org.key_project.util.EqualsModProofIrrelevancy; @@ -43,4 +44,14 @@ public boolean equalsModProofIrrelevancy(Object obj) { public int hashCodeModProofIrrelevancy() { return Objects.hash(name(), sort()); } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException("Logic variable " + name() + " does not have children"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java index 0510d66fc73..c9d4557970b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java @@ -125,7 +125,7 @@ public String toString() { return super.toString(); } - public static class JavaModalityKind extends Kind implements SVSubstitute { + public static class JavaModalityKind extends Kind { private static final Map kinds = new HashMap<>(); /** * The diamond operator of dynamic logic. A formula Phi can be read as after diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ObserverFunction.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ObserverFunction.java index 95d0597ab6c..3edd92a4333 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ObserverFunction.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ObserverFunction.java @@ -7,6 +7,7 @@ import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.logic.ProgramElementName; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableArray; @@ -22,7 +23,7 @@ */ public class ObserverFunction extends JFunction implements IObserverFunction { - private final KeYJavaType container; + private final Qualifier container; private final boolean isStatic; private final ImmutableArray paramTypes; private final KeYJavaType type; @@ -42,7 +43,7 @@ public ObserverFunction(String baseName, Sort sort, KeYJavaType type, Sort heapS assert type == null || type.getSort() == sort; assert container != null; this.type = type; - this.container = container; + this.container = Qualifier.create(container); this.isStatic = isStatic; this.paramTypes = paramTypes; this.heapCount = heapCount; @@ -107,7 +108,7 @@ public final KeYJavaType getType() { */ @Override public final KeYJavaType getContainerType() { - return container; + return container.getQualifier(); } @@ -169,4 +170,15 @@ public final ImmutableArray getParamTypes() { return paramTypes; } + @Override + public int getChildCount() { + return 1; + } + + @Override + public SyntaxElement getChild(int n) { + if (n == 0) + return container; + throw new IndexOutOfBoundsException("ObserverFunction " + name() + " has only one child"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Operator.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Operator.java index e12cfc522c6..3647725e850 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Operator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Operator.java @@ -13,7 +13,7 @@ * etc. have to implement this interface. */ public interface Operator - extends org.key_project.logic.op.Operator, SVSubstitute, EqualsModProofIrrelevancy { + extends org.key_project.logic.op.Operator, EqualsModProofIrrelevancy { /** * comparator to compare operators; for modalities only their kind is compared 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 0a4733e4792..0d43f11b6e9 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 @@ -22,6 +22,7 @@ import de.uka.ilkd.key.util.pp.Layouter; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; @@ -32,7 +33,8 @@ * Objects of this class are schema variables matching program constructs within modal operators. * The particular construct being matched is determined by the ProgramSVSort of the schema variable. */ -public final class ProgramSV extends OperatorSV implements ProgramConstruct, UpdateableOperator { +public final class ProgramSV extends OperatorSV + implements ProgramConstruct, UpdateableOperator, SyntaxElement { public static final Logger LOGGER = LoggerFactory.getLogger(ProgramSV.class); private static final ProgramList EMPTY_LIST_INSTANTIATION = @@ -142,13 +144,18 @@ public Expression getExpressionAt(int index) { } @Override - public int getChildCount() { - return 0; + public ProgramElement getChildAt(int index) { + return this; } @Override - public ProgramElement getChildAt(int index) { - return this; + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException("ProgramSV " + this + " has no children"); + } + + @Override + public int getChildCount() { + return 0; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java index 40cb2da7762..67210bebe7f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java @@ -16,6 +16,7 @@ import de.uka.ilkd.key.rule.MatchConditions; import org.key_project.logic.ParsableVariable; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; import org.key_project.util.ExtList; @@ -256,4 +257,15 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { return null; } } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException( + "Program variable " + name() + " does not have children"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java new file mode 100644 index 00000000000..2450b036d2e --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java @@ -0,0 +1,31 @@ +/* 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.logic.op; + +import java.util.WeakHashMap; + +import org.key_project.logic.TerminalSyntaxElement; + +public class Qualifier implements TerminalSyntaxElement { + private final T qualifier; + + private static final WeakHashMap> INSTANCES = new WeakHashMap<>(); + + private Qualifier(T qualifier) { + this.qualifier = qualifier; + } + + synchronized static Qualifier create(T qualifier) { + if (INSTANCES.containsKey(qualifier)) { + return (Qualifier) INSTANCES.get(qualifier); + } + var q = new Qualifier<>(qualifier); + INSTANCES.put(qualifier, q); + return q; + } + + public T getQualifier() { + return qualifier; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Quantifier.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Quantifier.java index bbf777afbfd..e73cb2e17c6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Quantifier.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Quantifier.java @@ -6,6 +6,7 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; /** @@ -36,4 +37,14 @@ private Quantifier(Name name) { super(name, new Sort[] { JavaDLTheory.FORMULA }, JavaDLTheory.FORMULA, new Boolean[] { true }, true); } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException(name() + " has no children"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SVSubstitute.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SVSubstitute.java deleted file mode 100644 index b7f183d6ed5..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SVSubstitute.java +++ /dev/null @@ -1,12 +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.logic.op; - -/** - * JavaCardDL syntactical elements implement this interface if they can occur as instantiations of - * schema variables. - */ -public interface SVSubstitute { - -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SkolemTermSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SkolemTermSV.java index 19bce65bc98..1cd550fa69d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SkolemTermSV.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SkolemTermSV.java @@ -7,6 +7,7 @@ import de.uka.ilkd.key.util.pp.Layouter; import org.key_project.logic.Name; +import org.key_project.logic.TerminalSyntaxElement; import org.key_project.logic.sort.Sort; /** @@ -14,7 +15,7 @@ * variables have to be accompanied by a "NewDependingOn" varcond, although with the removal of the * meta variable mechanism, this would no longer really be necessary. */ -public final class SkolemTermSV extends OperatorSV { +public final class SkolemTermSV extends OperatorSV implements TerminalSyntaxElement { /** * Creates a new schema variable that is used as placeholder for skolem terms. diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java index 4d0e486211a..bd675d35d89 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java @@ -12,6 +12,7 @@ import de.uka.ilkd.key.logic.sort.ProgramSVSort; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableArray; @@ -29,7 +30,7 @@ public final class SortDependingFunction extends JFunction { private static final Logger LOGGER = LoggerFactory.getLogger(SortDependingFunction.class); private final SortDependingFunctionTemplate template; - private final Sort sortDependingOn; + private final Qualifier sortDependingOn; // ------------------------------------------------------------------------- @@ -41,7 +42,7 @@ private SortDependingFunction(SortDependingFunctionTemplate template, Sort sortD instantiateResultSort(template, sortDependingOn), instantiateArgSorts(template, sortDependingOn), null, template.unique, false); this.template = template; - this.sortDependingOn = sortDependingOn; + this.sortDependingOn = Qualifier.create(sortDependingOn); } @@ -168,7 +169,7 @@ && instantiateName(getKind(), sort).toString().contains("seqGet") public Sort getSortDependingOn() { - return sortDependingOn; + return sortDependingOn.getQualifier(); } @@ -188,4 +189,18 @@ public Name getKind() { private record SortDependingFunctionTemplate(GenericSort sortDependingOn, Name kind, Sort sort, ImmutableArray argSorts, boolean unique) { } + + @Override + public int getChildCount() { + return 1; + } + + @Override + public SyntaxElement getChild(int n) { + if (n == 0) { + return sortDependingOn; + } + throw new IndexOutOfBoundsException( + "SortDependingFunction " + name() + " has only one child"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java index f993389d350..193fcc78e60 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java @@ -7,6 +7,7 @@ import de.uka.ilkd.key.logic.TermBuilder; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.TermCreationException; import org.key_project.logic.op.AbstractOperator; import org.key_project.logic.sort.Sort; @@ -72,4 +73,15 @@ public void validTopLevelException(T term // Term res = cfSubst.apply(term.sub(1)); // return res; // } + + + @Override + public int getChildCount() { + return 0; + } + + @Override + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException("SubstOp " + name() + " has no children"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermLabelSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermLabelSV.java index 4662b1f17ad..fc1fb8526e3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermLabelSV.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermLabelSV.java @@ -8,11 +8,12 @@ import de.uka.ilkd.key.util.pp.Layouter; import org.key_project.logic.Name; +import org.key_project.logic.TerminalSyntaxElement; /** * A schema variable which matches term labels */ -public final class TermLabelSV extends OperatorSV implements SchemaVariable, TermLabel { +public final class TermLabelSV extends OperatorSV implements TermLabel, TerminalSyntaxElement { TermLabelSV(Name name) { super(name, JavaDLTheory.TERMLABEL, true, false); @@ -29,12 +30,12 @@ public String toString() { } @Override - public Object getChild(int i) { - throw new IndexOutOfBoundsException(); + public int getTLChildCount() { + return 0; } @Override - public int getChildCount() { - return 0; + public Object getTLChild(int i) { + throw new IndexOutOfBoundsException(); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermSV.java index b057d045105..15353a7aaea 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermSV.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermSV.java @@ -7,13 +7,14 @@ import de.uka.ilkd.key.util.pp.Layouter; import org.key_project.logic.Name; +import org.key_project.logic.TerminalSyntaxElement; import org.key_project.logic.sort.Sort; /** * A schema variable that is used as placeholder for terms. */ -public final class TermSV extends OperatorSV { +public final class TermSV extends OperatorSV implements TerminalSyntaxElement { /** * @param name the name of the schema variable diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermTransformer.java index b722678fd3d..4ca7e30a52f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermTransformer.java @@ -7,11 +7,14 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.TerminalSyntaxElement; + /** * TermTransformer perform complex term transformation which cannot be (efficiently or at all) * described by taclets. */ -public interface TermTransformer extends org.key_project.logic.op.SortedOperator, Operator { +public interface TermTransformer extends org.key_project.logic.op.SortedOperator, Operator, + /* TODO: check */ TerminalSyntaxElement { /** * initiates term transformation of term. Note the top level operator of of parameter diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateApplication.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateApplication.java index fb6ff4791b6..19c503cff67 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateApplication.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateApplication.java @@ -7,6 +7,7 @@ import de.uka.ilkd.key.logic.Term; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.TermCreationException; import org.key_project.logic.op.AbstractOperator; import org.key_project.logic.sort.Sort; @@ -77,4 +78,14 @@ public static Term getTarget(Term t) { assert t.op() == UPDATE_APPLICATION; return t.sub(targetPos()); } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException("UpdateApplication has no children"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateJunctor.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateJunctor.java index 38b43150538..ca3586e9aa8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateJunctor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateJunctor.java @@ -6,6 +6,7 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; @@ -34,4 +35,14 @@ private static Sort[] createUpdateSortArray(int arity) { private UpdateJunctor(Name name, int arity) { super(name, createUpdateSortArray(arity), JavaDLTheory.UPDATE, false); } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException("UpdateJunctor " + name() + " has no children"); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateSV.java index 44b86cbd2c3..089f3b003e4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateSV.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateSV.java @@ -7,12 +7,13 @@ import de.uka.ilkd.key.util.pp.Layouter; import org.key_project.logic.Name; +import org.key_project.logic.TerminalSyntaxElement; /** * A schema variable that is used as placeholder for updates. */ -public final class UpdateSV extends OperatorSV { +public final class UpdateSV extends OperatorSV implements TerminalSyntaxElement { UpdateSV(Name name) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/VariableSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/VariableSV.java index 1024cf7b45d..fcbec1e7937 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/VariableSV.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/VariableSV.java @@ -6,12 +6,14 @@ import de.uka.ilkd.key.util.pp.Layouter; import org.key_project.logic.Name; +import org.key_project.logic.TerminalSyntaxElement; import org.key_project.logic.sort.Sort; /** * Schema variable that is instantiated with logical variables. */ -public final class VariableSV extends OperatorSV implements QuantifiableVariable { +public final class VariableSV extends OperatorSV + implements QuantifiableVariable, TerminalSyntaxElement { /** * Creates a new SchemaVariable that is used as placeholder for bound(quantified) variables. @@ -34,4 +36,6 @@ public void layout(Layouter l) { l.print("\\schemaVar \\variables ").print(sort().name().toString()).print(" ") .print(name().toString()); } + + } diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java index 409c6dd32cd..11deca874c7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java @@ -816,11 +816,11 @@ void printLabels(Term t, String left, String right) { afterFirst = true; } layouter.print(l.name().toString()); - if (l.getChildCount() > 0) { + if (l.getTLChildCount() > 0) { layouter.print("(").beginC(); - for (int i = 0; i < l.getChildCount(); i++) { - layouter.print("\"" + l.getChild(i).toString() + "\""); - if (i < l.getChildCount() - 1) { + for (int i = 0; i < l.getTLChildCount(); i++) { + layouter.print("\"" + l.getTLChild(i).toString() + "\""); + if (i < l.getTLChildCount() - 1) { layouter.print(",").ind(1, 2); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java index 55a54a489f3..a50e7a424b1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java @@ -10,9 +10,9 @@ import de.uka.ilkd.key.logic.TermFactory; import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.logic.op.QuantifiableVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.util.InfFlowSpec; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; @@ -36,7 +36,7 @@ public class OpReplacer { /** * The replacement map. */ - private final ReplacementMap map; + private final ReplacementMap map; /** *

@@ -53,7 +53,7 @@ public class OpReplacer { * with * @param tf a term factory. */ - public OpReplacer(Map map, TermFactory tf) { + public OpReplacer(Map map, TermFactory tf) { this(map, tf, null); } @@ -65,12 +65,12 @@ public OpReplacer(Map map, TermF * @param tf a term factory. * @param proof the currently loaded proof */ - public OpReplacer(Map map, TermFactory tf, + public OpReplacer(Map map, TermFactory tf, Proof proof) { assert map != null; this.map = map instanceof ReplacementMap - ? (ReplacementMap) map + ? (ReplacementMap) map : ReplacementMap.create(tf, proof, map); this.tf = tf; @@ -234,7 +234,7 @@ public Term replace(Term term) { return newTerm; } - for (SVSubstitute svs : map.keySet()) { + for (SyntaxElement svs : map.keySet()) { if (term.equalsModProperty(svs, TERM_LABELS_PROPERTY)) { return (Term) map.get(svs); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/ReplacementMap.java b/key.core/src/main/java/de/uka/ilkd/key/proof/ReplacementMap.java index 88fe0af0499..a6df47649fb 100755 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/ReplacementMap.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/ReplacementMap.java @@ -11,11 +11,12 @@ import de.uka.ilkd.key.logic.TermFactory; import de.uka.ilkd.key.logic.label.OriginTermLabel; import de.uka.ilkd.key.logic.label.TermLabelManager; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.settings.ProofSettings; import de.uka.ilkd.key.settings.TermLabelSettings; import de.uka.ilkd.key.util.LinkedHashMap; +import org.key_project.logic.SyntaxElement; + /** * A map to be used in an {@link OpReplacer}. It maps operators that should be replaced to their * replacements. @@ -25,7 +26,7 @@ * @param the type of the elements to replace. * @param the type of the replacements. */ -public interface ReplacementMap extends Map { +public interface ReplacementMap extends Map { /** * Creates a new replacement map. @@ -36,7 +37,7 @@ public interface ReplacementMap extends Map { * @param proof the currently loaded proof, or {@code null} if no proof is loaded. * @return a new replacement map. */ - static ReplacementMap create(TermFactory tf, + static ReplacementMap create(TermFactory tf, Proof proof) { var noIrrelevantTermLabelsMap = proof == null ? ProofSettings.DEFAULT_SETTINGS.getTermLabelSettings().getUseOriginLabels() @@ -58,7 +59,7 @@ static ReplacementMap create(TermFactory tf, * @param initialMappings a map whose mapping should be added to the new replacement map. * @return a new replacement map. */ - static ReplacementMap create(TermFactory tf, + static ReplacementMap create(TermFactory tf, Proof proof, Map initialMappings) { ReplacementMap result = create(tf, proof); result.putAll(initialMappings); @@ -77,7 +78,7 @@ static ReplacementMap create(TermFactory tf, * @param the type of the operators to replace. * @param the type of the replacements. */ - class DefaultReplacementMap extends LinkedHashMap + class DefaultReplacementMap extends LinkedHashMap implements ReplacementMap { private static final long serialVersionUID = 6223486569442129676L; } @@ -98,7 +99,7 @@ class DefaultReplacementMap extends LinkedHashMap + class NoIrrelevantLabelsReplacementMap implements ReplacementMap { /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java index 567b38b68f1..9ca5be95b01 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java @@ -6,9 +6,10 @@ import de.uka.ilkd.key.java.ProgramElement; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; +import org.key_project.logic.SyntaxElement; + public interface TacletMatcher { /** @@ -69,7 +70,7 @@ MatchConditions checkConditions(MatchConditions p_matchconditions, * instantiationCandidate or null if a match was not possible */ MatchConditions checkVariableConditions(SchemaVariable var, - SVSubstitute instantiationCandidate, MatchConditions matchCond, Services services); + SyntaxElement instantiationCandidate, MatchConditions matchCond, Services services); /** * matches the given term against the taclet's find term if the taclet has no find term or the diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/VariableCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/VariableCondition.java index aa9cc4495e5..1907547ddc7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/VariableCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/VariableCondition.java @@ -4,9 +4,10 @@ package de.uka.ilkd.key.rule; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; +import org.key_project.logic.SyntaxElement; + /** * The instantiations of a schemavariable can be restricted on rule scope by attaching conditions on @@ -30,7 +31,8 @@ public interface VariableCondition { * @return modified match results if the condition can be satisfied, or null * otherwise */ - MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions matchCond, + MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, + MatchConditions matchCond, Services services); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java b/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java index cb29e713636..d2c19ec07fb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java @@ -4,10 +4,11 @@ package de.uka.ilkd.key.rule; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * The variable condition adapter can be used by variable conditions which can either fail or be @@ -24,13 +25,13 @@ public abstract class VariableConditionAdapter implements VariableCondition { * @param services the program information object * @return true iff condition is fulfilled */ - public abstract boolean check(SchemaVariable var, SVSubstitute instCandidate, + public abstract boolean check(SchemaVariable var, SyntaxElement instCandidate, SVInstantiations instMap, Services services); @Override - public final MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, + public final MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, MatchConditions mc, Services services) { return check(var, instCandidate, mc.getInstantiations(), services) ? mc : null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java index 396d872b368..8ff2d7edcb0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java @@ -4,11 +4,11 @@ package de.uka.ilkd.key.rule.conditions; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; @@ -34,7 +34,7 @@ public TypeResolver getTypeResolver() { } @Override - public boolean check(SchemaVariable var, SVSubstitute instCandidate, SVInstantiations instMap, + public boolean check(SchemaVariable var, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { final Sort sort = resolver.resolveSort(var, instCandidate, instMap, services); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java index 5ac5d19f8b3..8b1455e32bb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java @@ -5,11 +5,12 @@ import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * disjoin two variable conditions @@ -30,7 +31,7 @@ public AlternativeVariableCondition(VariableConditionAdapter delegate0, * check whether any of the two delegates apply */ @Override - public boolean check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations svInst, Services services) { return delegate0.check(var, subst, svInst, services) || delegate1.check(var, subst, svInst, services); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java index 78f40a82ba6..511ce913b22 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableSet; @@ -198,7 +199,8 @@ private static boolean nameIsAlreadyUsed(Name name, ImmutableSet toExpArray( @SuppressWarnings("unchecked") @Override - public boolean check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations svInst, Services services) { Map tacletOptions = services.getProof().getSettings().getChoiceSettings().getDefaultChoices(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java index 58f2f5e8ef4..a657c581069 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java @@ -10,6 +10,7 @@ import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.Function; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; @@ -66,7 +67,7 @@ private static boolean clearlyDisjoint(Term t1, Term t2, Services services) { @Override - public boolean check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations svInst, Services services) { final Term s1Inst = (Term) svInst.getInstantiation(var1); final Term s2Inst = (Term) svInst.getInstantiation(var2); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java index 84b479a3a64..cfcc8aa1240 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java @@ -20,11 +20,12 @@ import de.uka.ilkd.key.java.reference.FieldReference; import de.uka.ilkd.key.logic.op.ProgramConstant; import de.uka.ilkd.key.logic.op.ProgramVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * This variable condition checks if the instantiation of a schemavariable (of * type Field) refers to a Java field declared as "model". @@ -47,7 +48,7 @@ public ModelFieldCondition(SchemaVariable field, boolean negated) { } @Override - public boolean check(SchemaVariable var, SVSubstitute subst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations instMap, Services services) { if (var == field) { 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 063b580d813..4823f007a09 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 @@ -12,7 +12,6 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.visitor.LabelCollector; import de.uka.ilkd.key.logic.op.ProgramSV; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.sort.ProgramSVSort; import de.uka.ilkd.key.rule.MatchConditions; @@ -20,6 +19,7 @@ import de.uka.ilkd.key.rule.inst.InstantiationEntry; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableMapEntry; /** @@ -41,11 +41,11 @@ public NewJumpLabelCondition(SchemaVariable sv) { } @Override - public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, + public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, MatchConditions matchCond, Services services) { if (var != labelSV && matchCond.getInstantiations().isInstantiated(labelSV)) { var = labelSV; - instCandidate = (SVSubstitute) matchCond.getInstantiations().getInstantiation(labelSV); + instCandidate = (SyntaxElement) matchCond.getInstantiations().getInstantiation(labelSV); } if (var == labelSV) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java index 88695c74bd0..8c877c2cc6c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java @@ -7,13 +7,14 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.IObserverFunction; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.op.TermSV; import de.uka.ilkd.key.rule.MatchConditions; import de.uka.ilkd.key.rule.VariableCondition; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + public final class ObserverCondition implements VariableCondition { @@ -28,7 +29,8 @@ public ObserverCondition(TermSV obs, TermSV heap) { @Override - public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc, + public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, + MatchConditions mc, Services services) { SVInstantiations svInst = mc.getInstantiations(); final Term obsInst = (Term) svInst.getInstantiation(obs); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SameObserverCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SameObserverCondition.java index 52287cf0a6f..2249534b53e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SameObserverCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SameObserverCondition.java @@ -8,7 +8,6 @@ import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.IObserverFunction; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.MatchConditions; import de.uka.ilkd.key.rule.UseDependencyContractRule; @@ -17,6 +16,7 @@ import de.uka.ilkd.key.speclang.Contract; import org.key_project.logic.ParsableVariable; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableSet; /** @@ -70,7 +70,8 @@ public SameObserverCondition(ParsableVariable schema1, ParsableVariable schema2) // explanation see class javadoc. @Override - public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc, + public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, + MatchConditions mc, Services services) { SVInstantiations svInst = mc.getInstantiations(); final Term term1 = (Term) svInst.getInstantiation(schema1); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java index 980911205ec..7b64f04a5c5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java @@ -17,6 +17,7 @@ import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.Named; +import org.key_project.logic.SyntaxElement; public class SimplifyIfThenElseUpdateCondition implements VariableCondition { @@ -151,7 +152,8 @@ private Term simplify(Term phi, Term u1, Term u2, Term t, TermServices services) @Override - public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc, + public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, + MatchConditions mc, Services services) { SVInstantiations svInst = mc.getInstantiations(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java index 2d942802bf8..f850a1d42be 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java @@ -10,6 +10,8 @@ import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * This variable condition checks if the instantiation of a schemavariable (of type Field) refers to * a Java field declared as "static". @@ -31,7 +33,7 @@ public StaticFieldCondition(SchemaVariable field, boolean negated) { } @Override - public boolean check(SchemaVariable var, SVSubstitute instCandidate, SVInstantiations instMap, + public boolean check(SchemaVariable var, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { final Object o = instMap.getInstantiation(field); if (!(o instanceof Term f)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticMethodCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticMethodCondition.java index 2ce44dab8b6..10524eba651 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticMethodCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticMethodCondition.java @@ -13,12 +13,12 @@ import de.uka.ilkd.key.java.reference.ReferencePrefix; import de.uka.ilkd.key.logic.op.IProgramMethod; import de.uka.ilkd.key.logic.op.LocationVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.sort.NullSort; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableArray; @@ -58,7 +58,7 @@ private static ImmutableArray toExpArray( @SuppressWarnings("unchecked") @Override - public boolean check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations svInst, Services services) { ReferencePrefix rp = (ReferencePrefix) svInst.getInstantiation(caller); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticReferenceCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticReferenceCondition.java index c3ce83b2aa2..332bba35df2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticReferenceCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticReferenceCondition.java @@ -8,11 +8,12 @@ import de.uka.ilkd.key.java.reference.FieldReference; import de.uka.ilkd.key.logic.op.ProgramConstant; import de.uka.ilkd.key.logic.op.ProgramVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * ensures that the given instantiation for the schemavariable denotes a static field @@ -34,7 +35,7 @@ public StaticReferenceCondition(SchemaVariable reference, boolean negation) { @Override - public boolean check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations svInst, Services services) { if (var == reference) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java index 74f87909a8f..a92a20bdb21 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java @@ -9,13 +9,14 @@ import de.uka.ilkd.key.logic.JavaBlock; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.ProgramSV; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.LightweightSyntacticalReplaceVisitor; import de.uka.ilkd.key.rule.MatchConditions; import de.uka.ilkd.key.rule.VariableCondition; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * Stores the given {@link Statement}, after substitution of {@link SchemaVariable}s, into the given * {@link ProgramSV} for later use in other conditions and transformers. The arguments are a @@ -37,7 +38,7 @@ public StoreStmtInCondition(ProgramSV resultVarSV, Term term) { } @Override - public MatchConditions check(SchemaVariable sv, SVSubstitute instCandidate, + public MatchConditions check(SchemaVariable sv, SyntaxElement instCandidate, MatchConditions matchCond, Services services) { final SVInstantiations svInst = matchCond.getInstantiations(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java index a155d62dc1c..6b6e31e5b4e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java @@ -5,13 +5,14 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.LightweightSyntacticalReplaceVisitor; import de.uka.ilkd.key.rule.MatchConditions; import de.uka.ilkd.key.rule.VariableCondition; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * Stores the given {@link Term}, after substitution of {@link SchemaVariable}s, into the given * {@link SchemaVariable} for later use in other conditions and transformers. @@ -28,7 +29,7 @@ public StoreTermInCondition(SchemaVariable resultVarSV, Term term) { } @Override - public MatchConditions check(SchemaVariable sv, SVSubstitute instCandidate, + public MatchConditions check(SchemaVariable sv, SyntaxElement instCandidate, MatchConditions matchCond, Services services) { final SVInstantiations svInst = matchCond.getInstantiations(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java index 7787df797dd..2ac0c4428a2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java @@ -7,11 +7,12 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.FormulaSV; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * This variable condition checks if an instantiation for a formula has sub formulas which are * formulas. It returns false for an arity equal to zero or no sub formulas. This is needed to @@ -32,7 +33,7 @@ public SubFormulaCondition(FormulaSV a, boolean negated) { } @Override - public boolean check(SchemaVariable var, SVSubstitute instCandidate, SVInstantiations instMap, + public boolean check(SchemaVariable var, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { if (!(var instanceof FormulaSV) || var != this.a) { return false; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java index 1f29050176e..6bccef558d5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java @@ -5,13 +5,13 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.op.TermLabelSV; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableArray; /** @@ -33,7 +33,7 @@ public TermLabelCondition(TermLabelSV l, String t, boolean negated) { } @Override - public boolean check(SchemaVariable var, SVSubstitute instCandidate, SVInstantiations instMap, + public boolean check(SchemaVariable var, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { assert instMap.getInstantiation(l) instanceof ImmutableArray; ImmutableArray tInsts = (ImmutableArray) instMap.getInstantiation(l); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java index 6d49717e70d..3c28d087433 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java @@ -12,7 +12,6 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.java.declaration.InterfaceDeclaration; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.sort.ArraySort; import de.uka.ilkd.key.logic.sort.NullSort; @@ -20,6 +19,7 @@ import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; @@ -72,7 +72,7 @@ public Mode getMode() { } @Override - public boolean check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations svInst, Services services) { if (!fst.isComplete(var, subst, svInst, services) diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeCondition.java index febb37096b7..7f041a3731a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeCondition.java @@ -5,13 +5,13 @@ import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.sort.NullSort; import de.uka.ilkd.key.logic.sort.ProxySort; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; @@ -55,7 +55,7 @@ public boolean getNonNull() { @Override - public boolean check(SchemaVariable p_var, SVSubstitute candidate, SVInstantiations svInst, + public boolean check(SchemaVariable p_var, SyntaxElement candidate, SVInstantiations svInst, Services services) { if (!resolver.isComplete(p_var, candidate, svInst, services)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java index f7dd7617ab8..f313becfd78 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java @@ -11,13 +11,13 @@ import de.uka.ilkd.key.logic.op.IObserverFunction; import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.logic.op.ProgramVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.rule.inst.SVInstantiations; import de.uka.ilkd.key.util.Debug; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.Function; import org.key_project.logic.sort.Sort; @@ -50,10 +50,10 @@ public static TypeResolver createNonGenericSortResolver(Sort s) { } - public abstract boolean isComplete(SchemaVariable sv, SVSubstitute instCandidate, + public abstract boolean isComplete(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, TermServices services); - public abstract Sort resolveSort(SchemaVariable sv, SVSubstitute instCandidate, + public abstract Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, Services services); @@ -74,13 +74,13 @@ public GenericSort getGenericSort() { } @Override - public boolean isComplete(SchemaVariable sv, SVSubstitute instCandidate, + public boolean isComplete(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, TermServices services) { return instMap.getGenericSortInstantiations().getInstantiation(gs) != null; } @Override - public Sort resolveSort(SchemaVariable sv, SVSubstitute instCandidate, + public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { return instMap.getGenericSortInstantiations().getInstantiation(gs); } @@ -100,13 +100,13 @@ public NonGenericSortResolver(Sort s) { } @Override - public boolean isComplete(SchemaVariable sv, SVSubstitute instCandidate, + public boolean isComplete(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, TermServices services) { return true; } @Override - public Sort resolveSort(SchemaVariable sv, SVSubstitute instCandidate, + public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { return s; } @@ -130,18 +130,18 @@ public ElementTypeResolverForSV(SchemaVariable sv) { } @Override - public boolean isComplete(SchemaVariable sv, SVSubstitute instCandidate, + public boolean isComplete(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, TermServices services) { return resolveSV == sv || instMap.getInstantiation(resolveSV) != null; } @Override - public Sort resolveSort(SchemaVariable sv, SVSubstitute instCandidate, + public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { final Sort s; - final SVSubstitute inst = (SVSubstitute) (resolveSV == sv ? instCandidate + final SyntaxElement inst = (SyntaxElement) (resolveSV == sv ? instCandidate : instMap.getInstantiation(resolveSV)); if (inst instanceof ProgramVariable) { @@ -178,18 +178,18 @@ public ContainerTypeResolver(SchemaVariable sv) { } @Override - public boolean isComplete(SchemaVariable sv, SVSubstitute instCandidate, + public boolean isComplete(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, TermServices services) { return sv == memberSV || instMap.getInstantiation(memberSV) != null; } @Override - public Sort resolveSort(SchemaVariable sv, SVSubstitute instCandidate, + public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { final Sort result; - final SVSubstitute inst = (SVSubstitute) (memberSV == sv ? instCandidate + final SyntaxElement inst = (SyntaxElement) (memberSV == sv ? instCandidate : instMap.getInstantiation(memberSV)); if (inst instanceof Operator) { 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 index 408e0b82b92..e5f38ccbc06 100644 --- 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 @@ -4,11 +4,11 @@ package de.uka.ilkd.key.rule.inst; import de.uka.ilkd.key.java.ProgramElement; -import de.uka.ilkd.key.logic.op.SVSubstitute; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableArray; -public class ProgramList implements SVSubstitute { +public class ProgramList implements SyntaxElement { private final ImmutableArray list; @@ -34,4 +34,14 @@ 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/label/OriginTermLabelRefactoring.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelRefactoring.java index 3fc16ba6428..9b964549cfb 100755 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelRefactoring.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelRefactoring.java @@ -129,8 +129,8 @@ private Set collectSubtermOrigins(Term term, Set result) { TermLabel label = term.getLabel(OriginTermLabel.NAME); if (label != null) { - result.add((Origin) label.getChild(0)); - result.addAll((Set) label.getChild(1)); + result.add((Origin) label.getTLChild(0)); + result.addAll((Set) label.getTLChild(1)); } ImmutableArray subterms = term.subs(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java index ef2d5270d82..7832eae3b67 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java @@ -13,7 +13,6 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.logic.op.QuantifiableVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.op.UpdateApplication; import de.uka.ilkd.key.rule.FindTaclet; @@ -30,6 +29,7 @@ import de.uka.ilkd.key.rule.match.TacletMatcherKit; import de.uka.ilkd.key.rule.match.vm.instructions.MatchSchemaVariableInstruction; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; @@ -239,8 +239,8 @@ public final MatchConditions checkConditions(MatchConditions cond, Services serv while (result != null && svIterator.hasNext()) { final SchemaVariable sv = svIterator.next(); final Object o = result.getInstantiations().getInstantiation(sv); - if (o instanceof SVSubstitute) { - result = checkVariableConditions(sv, (SVSubstitute) o, result, services); + if (o instanceof SyntaxElement) { + result = checkVariableConditions(sv, (SyntaxElement) o, result, services); } } } @@ -279,7 +279,7 @@ private boolean varIsBound(SchemaVariable v) { */ @Override public final MatchConditions checkVariableConditions(SchemaVariable var, - SVSubstitute instantiationCandidate, MatchConditions matchCond, Services services) { + SyntaxElement instantiationCandidate, MatchConditions matchCond, Services services) { if (matchCond != null) { if (instantiationCandidate instanceof Term term) { if (!(term.op() instanceof QuantifiableVariable)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java index 6d2947127e1..1f72b3d0149 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java @@ -14,7 +14,6 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.IObserverFunction; import de.uka.ilkd.key.logic.op.LocationVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.proof.OpReplacer; import de.uka.ilkd.key.proof.init.ContractPO; @@ -22,6 +21,7 @@ import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.proof.init.ProofOblInput; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableList; import org.key_project.util.java.MapUtil; @@ -145,7 +145,7 @@ public Term getPre(LocationVariable heap, LocationVariable selfVar, assert paramVars != null; assert paramVars.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); if (originalSelfVar != null) { map.put(originalSelfVar, selfVar); } @@ -192,7 +192,7 @@ public Term getPre(LocationVariable heap, Term heapTerm, Term selfTerm, assert paramTerms != null; assert paramTerms.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); map.put(services.getTermBuilder().var(heap), heapTerm); if (originalSelfVar != null) { map.put(services.getTermBuilder().var(originalSelfVar), selfTerm); @@ -259,7 +259,7 @@ public Term getMby(LocationVariable selfVar, ImmutableList par assert paramVars != null; assert paramVars.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); if (originalSelfVar != null) { map.put(originalSelfVar, selfVar); } @@ -281,7 +281,7 @@ public Term getMby(Map heapTerms, Term selfTerm, assert paramTerms != null; assert paramTerms.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); for (LocationVariable heap : heapTerms.keySet()) { map.put(services.getTermBuilder().var(heap), heapTerms.get(heap)); } @@ -370,7 +370,7 @@ public Term getDep(LocationVariable heap, boolean atPre, LocationVariable selfVa assert paramVars != null; assert paramVars.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); if (originalSelfVar != null) { map.put(originalSelfVar, selfVar); } @@ -400,7 +400,7 @@ public Term getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term sel assert paramTerms != null; assert paramTerms.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); map.put(services.getTermBuilder().var(heap), heapTerm); if (originalSelfVar != null) { map.put(services.getTermBuilder().var(originalSelfVar), selfTerm); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java index d3d6b4819d4..675c1393eda 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java @@ -29,6 +29,7 @@ import de.uka.ilkd.key.proof.init.ProofOblInput; import org.key_project.logic.Named; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -744,7 +745,7 @@ public static String getText(FunctionalOperationContract contract, private static String getSignatureText(IProgramMethod pm, Operator originalResultVar, - Operator originalSelfVar, ImmutableList originalParamVars, + Operator originalSelfVar, ImmutableList originalParamVars, LocationVariable originalExcVar, Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols) { final StringBuilder sig = new StringBuilder(); @@ -761,7 +762,7 @@ private static String getSignatureText(IProgramMethod pm, Operator originalResul } sig.append(pm.getName()); sig.append("("); - for (SVSubstitute subst : originalParamVars) { + for (SyntaxElement subst : originalParamVars) { if (subst instanceof Named named) { sig.append(named.name()).append(", "); } else if (subst instanceof Term) { @@ -868,7 +869,7 @@ private static String getPostText(Map originalPosts, } private static String getText(IProgramMethod pm, Operator originalResultVar, - Operator originalSelfVar, ImmutableList originalParamVars, + Operator originalSelfVar, ImmutableList originalParamVars, LocationVariable originalExcVar, boolean hasMby, Term originalMby, Map originalModifiables, Map hasRealModifiable, Term globalDefs, @@ -1300,7 +1301,7 @@ public Term getDep(LocationVariable heap, boolean atPre, LocationVariable selfVa assert paramVars != null; assert paramVars.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); if (originalSelfVar != null) { map.put(originalSelfVar, selfVar); } @@ -1328,7 +1329,7 @@ public Term getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term sel assert paramTerms != null; assert paramTerms.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); map.put(tb.var(heap), heapTerm); if (originalSelfVar != null) { map.put(tb.var(originalSelfVar), selfTerm); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java index cb8f34c0291..86207d1f136 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java @@ -41,13 +41,13 @@ import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.logic.op.Modality; import de.uka.ilkd.key.logic.op.ProgramVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.proof.OpReplacer; import de.uka.ilkd.key.proof.mgt.SpecificationRepository; import de.uka.ilkd.key.rule.metaconstruct.EnhancedForElimination; import de.uka.ilkd.key.speclang.jml.pretranslation.Behavior; import de.uka.ilkd.key.util.InfFlowSpec; +import org.key_project.logic.SyntaxElement; import org.key_project.util.ExtList; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; @@ -331,7 +331,7 @@ public static LoopContract combine(ImmutableSet contracts, Service */ private static OpReplacer createOpReplacer(final ProgramVariable index, final ProgramVariable values, Services services) { - final Map replacementMap = new HashMap<>(); + final Map replacementMap = new HashMap<>(); if (index != null) { replacementMap.put(services.getTermBuilder().index(), services.getTermBuilder().var(index)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/ReplacementMap.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/ReplacementMap.java index 0e1617da870..3bfcaf07435 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/ReplacementMap.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/ReplacementMap.java @@ -13,7 +13,8 @@ import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.logic.op.ProgramVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; + +import org.key_project.logic.SyntaxElement; /** * A map from some type to the same type. @@ -22,7 +23,7 @@ * * @author lanzinger */ -public abstract class ReplacementMap +public abstract class ReplacementMap extends de.uka.ilkd.key.proof.ReplacementMap.NoIrrelevantLabelsReplacementMap { /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java index 76edd2ab297..44fb3a27177 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java @@ -8,11 +8,12 @@ import org.key_project.logic.Name; import org.key_project.logic.ParsableVariable; +import org.key_project.logic.TerminalSyntaxElement; import org.key_project.logic.sort.Sort; @Deprecated public final class Metavariable extends AbstractSortedOperator - implements ParsableVariable, Comparable { + implements ParsableVariable, Comparable, TerminalSyntaxElement { // Used to define an alternative order of all existing // metavariables diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java index c3a3b2599d0..49368cb1602 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java @@ -19,6 +19,7 @@ import org.key_project.logic.Name; import org.key_project.logic.TermCreationException; +import org.key_project.logic.TerminalSyntaxElement; import org.key_project.logic.op.Modifier; import org.key_project.logic.op.SortedOperator; import org.key_project.logic.sort.Sort; @@ -95,7 +96,8 @@ protected Term generateOneTerm(Term superterm, int child) { return services.getTermBuilder().tf().createTerm(binFunc, superterm, index); } - private static class SuperTermGeneratedOp implements SortedOperator, Operator { + private static class SuperTermGeneratedOp + implements SortedOperator, Operator, TerminalSyntaxElement { private final Name NAME; private final IntegerLDT numbers; diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java index 517a5a78a8c..8599f8d81d3 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java @@ -557,18 +557,18 @@ public void testParseLabel() throws TermLabelException { TermLabel label = manager.parseLabel("ONE", null, services); assertTrue(label instanceof LoggingTermLabel); assertEquals("ONE", label.name().toString()); - assertEquals(0, label.getChildCount()); + assertEquals(0, label.getTLChildCount()); // Test empty parameter label = manager.parseLabel("TWO", null, services); assertTrue(label instanceof LoggingTermLabel); assertEquals("TWO", label.name().toString()); - assertEquals(0, label.getChildCount()); + assertEquals(0, label.getTLChildCount()); // Test with parameter label = manager.parseLabel("THREE", Collections.singletonList("Param"), services); assertTrue(label instanceof LoggingTermLabel); assertEquals("THREE", label.name().toString()); - assertEquals(1, label.getChildCount()); - assertEquals("Param", label.getChild(0)); + assertEquals(1, label.getTLChildCount()); + assertEquals("Param", label.getTLChild(0)); // Test unsupported try { manager.parseLabel("UNKNOWN", null, services); @@ -850,12 +850,12 @@ public Name name() { } @Override - public Object getChild(int i) { + public Object getTLChild(int i) { return arguments.get(i); } @Override - public int getChildCount() { + public int getTLChildCount() { return arguments != null ? arguments.size() : 0; } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java index 91ff2692110..fae51cc5a3e 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java @@ -12,6 +12,7 @@ import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; import org.junit.jupiter.api.Test; @@ -229,7 +230,7 @@ private Term applyUpdateOnTerm(Term term) { * @param tOrPhi the {@link SchemaVariable} that is instantiated with the term or formula in * term * @param result the {@link SchemaVariable} that is instantiated with the result of a - * {@link ApplyUpdateOnRigidCondition#check(SchemaVariable, SVSubstitute, MatchConditions, Services)} + * {@link ApplyUpdateOnRigidCondition#check(SchemaVariable, SyntaxElement, MatchConditions, Services)} * call * * @return the original formula or term if the update cannot be applied; else, the updated diff --git a/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java b/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java index 244f53bbe4b..12f2c5be7e5 100644 --- a/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java +++ b/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java @@ -8,4 +8,22 @@ * AST nodes. */ public interface SyntaxElement { + /** + * Get the {@code n}-th child of this syntax element. + * + * @param n index of the child. + * @return the {@code n}-th child of this syntax element. + * @throws IndexOutOfBoundsException if there is no {@code n}-th child. + */ + SyntaxElement getChild(int n); + + /** + * + * @return the number of children of this syntax element. + */ + int getChildCount(); + + default SyntaxElementCursor getCursor() { + return new SyntaxElementCursor(this); + } } diff --git a/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java b/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java new file mode 100644 index 00000000000..52a040d7819 --- /dev/null +++ b/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java @@ -0,0 +1,101 @@ +/* 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.logic; + +import java.util.ArrayDeque; +import java.util.Deque; + +/** + * A cursor (or walker) for navigating {@link SyntaxElement}s in pre-order. * + */ +public class SyntaxElementCursor { + private record ParentAndPosition(SyntaxElement parent, int index) {} + + private final Deque path = new ArrayDeque<>(); + + private SyntaxElement node; + + SyntaxElementCursor(SyntaxElement node) { + this.node = node; + } + + public SyntaxElement getCurrentNode() { + return node; + } + + /** + * Advance the cursor to the current node's first child if possible. + * Otherwise, no changes to the state occur. + * + * @return true iff the current node has at least one child. + */ + public boolean gotoFirstChild() { + if (node.getChildCount() <= 0) + return false; + path.push(new ParentAndPosition(node, 0)); + node = node.getChild(0); + return true; + } + + /** + * Advance the cursor to the current node's next sibling if possible. + * Otherwise, no changes to the state occur. + * + * @return true iff the current node has at least one sibling not yet visited. + */ + public boolean gotoNextSibling() { + if (path.isEmpty()) + return false; + var pnp = path.pop(); + SyntaxElement parent = pnp.parent; + int index = pnp.index + 1; + if (index >= parent.getChildCount()) { + path.push(pnp); + return false; + } + path.push(new ParentAndPosition(parent, index)); + node = parent.getChild(index); + return true; + } + + /** + * Advance the cursor to the current node's parent if possible. + * Otherwise, no changes to the state occur. + * + * @return true iff the current node is not the root. + */ + public boolean gotoParent() { + if (path.isEmpty()) + return false; + node = path.pop().parent; + return true; + } + + /** + * Advance cursor to the next node. + * If the node has children, the cursor advances to the first child. + * Otherwise, if the node has unvisited siblings, the cursor advances to the next unvisited + * sibling. + * Otherwise, no changes to the state. + * + * @return true iff the node has children or an unvisited sibling. + */ + public boolean goToNext() { + var ancestors = new ArrayDeque(); + if (gotoFirstChild()) + return true; + if (gotoNextSibling()) + return true; + while (!path.isEmpty()) { + ancestors.add(path.pop()); + if (gotoNextSibling()) + return true; + } + // Nothing found; re-build stack + for (var ancestor : ancestors) { + path.push(ancestor); + } + return false; + } +} diff --git a/key.ncore/src/main/java/org/key_project/logic/Term.java b/key.ncore/src/main/java/org/key_project/logic/Term.java index c08c5a866fd..5dc16e0ea29 100644 --- a/key.ncore/src/main/java/org/key_project/logic/Term.java +++ b/key.ncore/src/main/java/org/key_project/logic/Term.java @@ -91,4 +91,23 @@ public interface Term extends LogicElement, Sorted { * @param visitor the Visitor */ void execPreOrder(Visitor visitor); + + @Override + default int getChildCount() { + return 1 + boundVars().size() + subs().size(); + } + + @Override + default SyntaxElement getChild(int n) { + if (n == 0) + return op(); + n--; + if (n < boundVars().size()) + return boundVars().get(n); + n -= boundVars().size(); + if (n < subs().size()) + return sub(n); + throw new IndexOutOfBoundsException( + "Term " + this + " has only " + getChildCount() + " children"); + } } diff --git a/key.ncore/src/main/java/org/key_project/logic/TerminalSyntaxElement.java b/key.ncore/src/main/java/org/key_project/logic/TerminalSyntaxElement.java new file mode 100644 index 00000000000..860f1e62a65 --- /dev/null +++ b/key.ncore/src/main/java/org/key_project/logic/TerminalSyntaxElement.java @@ -0,0 +1,16 @@ +/* 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.logic; + +public interface TerminalSyntaxElement extends SyntaxElement { + @Override + default SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException(this.getClass() + " " + this + " has no children"); + } + + @Override + default int getChildCount() { + return 0; + } +} diff --git a/key.ncore/src/main/java/org/key_project/logic/op/Function.java b/key.ncore/src/main/java/org/key_project/logic/op/Function.java index 94b97468c93..ec55b5dcd44 100644 --- a/key.ncore/src/main/java/org/key_project/logic/op/Function.java +++ b/key.ncore/src/main/java/org/key_project/logic/op/Function.java @@ -4,6 +4,7 @@ package org.key_project.logic.op; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableArray; @@ -51,4 +52,14 @@ public final boolean isSkolemConstant() { public final String toString() { return (name() + (whereToBind() == null ? "" : "{" + whereToBind() + "}")); } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException("Function " + name() + " has no children"); + } } diff --git a/key.ncore/src/main/java/org/key_project/logic/op/Modality.java b/key.ncore/src/main/java/org/key_project/logic/op/Modality.java index 10d40f7a239..9c93156a847 100644 --- a/key.ncore/src/main/java/org/key_project/logic/op/Modality.java +++ b/key.ncore/src/main/java/org/key_project/logic/op/Modality.java @@ -5,9 +5,7 @@ import java.util.Objects; -import org.key_project.logic.Name; -import org.key_project.logic.Named; -import org.key_project.logic.Program; +import org.key_project.logic.*; import org.key_project.logic.sort.Sort; import org.jspecify.annotations.Nullable; @@ -41,10 +39,25 @@ public final K kind() { */ public abstract Program program(); + @Override + public int getChildCount() { + return 2; + } + + @Override + public SyntaxElement getChild(int n) { + return switch (n) { + case 0 -> kind; + case 1 -> program(); + default -> throw new IndexOutOfBoundsException( + "Modality " + name() + " has only two children"); + }; + } + /** * Modality kinds like box and diamond. */ - public abstract static class Kind implements Named { + public abstract static class Kind implements Named, TerminalSyntaxElement { private final Name name; public Kind(Name name) { diff --git a/key.ncore/src/main/java/org/key_project/logic/op/Operator.java b/key.ncore/src/main/java/org/key_project/logic/op/Operator.java index 3a4f900dde8..81fd39f426c 100644 --- a/key.ncore/src/main/java/org/key_project/logic/op/Operator.java +++ b/key.ncore/src/main/java/org/key_project/logic/op/Operator.java @@ -4,11 +4,12 @@ package org.key_project.logic.op; import org.key_project.logic.Named; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.Term; import org.key_project.logic.TermCreationException; import org.key_project.logic.sort.Sort; -public interface Operator extends Named { +public interface Operator extends Named, SyntaxElement { /** * the arity of this operator */ diff --git a/key.ncore/src/test/java/org/key_project/logic/SyntaxElementCursorTest.java b/key.ncore/src/test/java/org/key_project/logic/SyntaxElementCursorTest.java new file mode 100644 index 00000000000..86aafe4dba2 --- /dev/null +++ b/key.ncore/src/test/java/org/key_project/logic/SyntaxElementCursorTest.java @@ -0,0 +1,62 @@ +/* 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.logic; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +public class SyntaxElementCursorTest { + class Node implements SyntaxElement { + private final int value; + private final Node[] children; + + public Node(int value, Node... children) { + this.value = value; + this.children = children; + } + + public int getValue() { + return value; + } + + @Override + public int getChildCount() { + return children.length; + } + + @Override + public SyntaxElement getChild(int n) { + return children[n]; + } + } + + private Node example1() { + return new Node(0, + new Node(1, new Node(2), new Node(3)), + new Node(4, new Node(5), new Node(6))); + } + + private List traverse(Node n) { + var lst = new ArrayList(); + var cursor = n.getCursor(); + do { + lst.add(((Node) cursor.getCurrentNode()).getValue()); + } while (cursor.goToNext()); + return lst; + } + + @Test + void testOrder() { + var tree = example1(); + + assertEquals( + Arrays.asList(0, 1, 2, 3, 4, 5, 6), + traverse(tree)); + } +}